SSL Kingman.thy

(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
    License: BSD
*)

section ‹Subcocycles, subadditive ergodic theory›

theory Kingman
  imports Ergodicity Fekete
begin

text ‹Subadditive ergodic theory is the branch of ergodic theory devoted
  the study of subadditive cocycles (named subcocycles in what follows), i.e.,
  such that $u(n+m, x) \leq u(n, x) + u(m, T^n x)$ for all $x$ and $m,n$.

  instance, Birkhoff sums are examples of such subadditive cocycles (in fact, they are
 ), but more interesting examples are genuinely subadditive. The main result
  the theory is Kingman's theorem, asserting the almost sure convergence of
 u_n / n$ (this is a generalization of Birkhoff theorem). If the asymptotic average
 \lim \int u_n / n$ (which exists by subadditivity and Fekete lemma) is not $-\infty$,
  the convergence takes also place in $L^1$. We prove all this below.
 ›

context mpt
begin

subsection ‹Definition and basic properties›

definition subcocycle::"(nat ==> 'a ==> real) ==> bool"
  where "subcocycle u = ((∀n. integrable M (u n)) ∧ (∀n m x. u (n+m) x ≤ u n x + u m ((T^^n) x)))"

lemma subcocycle_ineq:
  assumes "subcocycle u"
  shows "u (n+m) x ≤ u n x + u m ((T^^n) x)"
using assms unfolding subcocycle_def by blast

lemma subcocycle_0_nonneg:
  assumes "subcocycle u"
  shows "u 0 x ≥ 0"
proof -
  have "u (0+0) x ≤ u 0 x + u 0 ((T^^0) x)"
    using assms unfolding subcocycle_def by blast
  then show ?thesis by auto
qed

lemma subcocycle_integrable:
  assumes "subcocycle u"
  shows "integrable M (u n)"
        "u n ∈ borel_measurable M"
using assms unfolding subcocycle_def by auto

lemma subcocycle_birkhoff:
  assumes "integrable M f"
  shows "subcocycle (birkhoff_sum f)"
unfolding subcocycle_def by (auto simp add: assms birkhoff_sum_integral(1) birkhoff_sum_cocycle)

text ‹The set of subcocycles is stable under addition, multiplication by positive numbers,
  $\max$.›

lemma subcocycle_add:
  assumes "subcocycle u" "subcocycle v"
  shows "subcocycle (λn x. u n x + v n x)"
unfolding subcocycle_def
proof (auto)
  fix n
  show "integrable M (λx. u n x + v n x)" using assms unfolding subcocycle_def by simp
next
  fix n m x
  have "u (n+m) x ≤ u n x + u m ((T ^^ n) x)" using assms(1) subcocycle_def by simp
  moreover have "v (n+m) x ≤ v n x + v m ((T ^^ n) x)" using assms(2) subcocycle_def by simp
  ultimately show "u (n + m) x + v (n + m) x ≤ u n x + v n x + (u m ((T ^^ n) x) + v m ((T ^^ n) x))"
    by simp
qed

lemma subcocycle_cmult:
  assumes "subcocycle u" "c ≥ 0"
  shows "subcocycle (λn x. c * u n x)"
using assms unfolding subcocycle_def by (auto, metis distrib_left mult_left_mono)

lemma subcocycle_max:
  assumes "subcocycle u" "subcocycle v"
  shows "subcocycle (λn x. max (u n x) (v n x))"
unfolding subcocycle_def proof (auto)
  fix n
  show "integrable M (λx. max (u n x) (v n x))" using assms unfolding subcocycle_def by auto
next
  fix n m x
  have "u (n+m) x ≤ u n x + u m ((T^^n) x)" using assms(1) unfolding subcocycle_def by auto
  then show "u (n + m) x ≤ max (u n x) (v n x) + max (u m ((T ^^ n) x)) (v m ((T ^^ n) x))"
    by simp
next
  fix n m x
  have "v (n+m) x ≤ v n x + v m ((T^^n) x)" using assms(2) unfolding subcocycle_def by auto
  then show "v (n + m) x ≤ max (u n x) (v n x) + max (u m ((T ^^ n) x)) (v m ((T ^^ n) x))"
    by simp
qed

text ‹Applying inductively the subcocycle equation, it follows that a subcocycle is bounded
  the Birkhoff sum of the subcocycle at time $1$.›

lemma subcocycle_bounded_by_birkhoff1:
  assumes "subcocycle u" "n > 0"
  shows "u n x ≤ birkhoff_sum (u 1) n x"
using ‹n > 0› proof (induction rule: ind_from_1)
  case 1
  show ?case by auto
next
  case (Suc p)
  have "u (Suc p) x ≤ u p x + u 1 ((T^^p)x)" using assms(1) subcocycle_def by (metis Suc_eq_plus1)
  then show ?case using Suc birkhoff_sum_cocycle[where ?n = p and ?m = 1] ‹ p>0 › by (simp add: birkhoff_sum_def)
qed

text ‹It is often important to bound a cocycle $u_n(x)$ by the Birkhoff sums of $u_N/N$. Compared
  the trivial upper bound for $u_1$, there are additional boundary errors that make the
  more cumbersome (but these terms only come from a $N$-neighborhood of $0$ and $n$, so
  are negligible if $N$ is fixed and $n$ tends to infinity.›

lemma subcocycle_bounded_by_birkhoffN:
  assumes "subcocycle u" "n > 2*N" "N>0"
  shows "u n x ≤ birkhoff_sum (λx. u N x / real N) (n - 2 * N) x
                + (∑i<N. ∣u 1 ((T ^^ i) x)∣)
                + 2 * (∑i<2*N. ∣u 1 ((T ^^ (n - (2 * N - i))) x)∣)"
proof -
  have Iar: "u (a*N+r) x ≤ u r x + (∑i<a. u N ((T^^(i * N + r))x))" for r a
  proof (induction a)
    case 0
    then show ?case by auto
  next
    case (Suc a)
    have "u ((a+1)*N+r) x = u((a*N+r) + N) x"
      by (simp add: semiring_normalization_rules(2) semiring_normalization_rules(23))
    also have "... ≤ u(a*N+r) x + u N ((T^^(a*N+r))x)"
      using assms(1) unfolding subcocycle_def by auto
    also have "... ≤ u r x + (∑i<a. u N ((T^^(i * N + r))x)) + u N ((T^^(a*N+r))x)"
      using Suc.IH by auto
    also have "... = u r x + (∑i<a+1. u N ((T^^(i * N + r))x))"
      by auto
    finally show ?case by auto
  qed

  have Ia: "u (a*N) x ≤ (∑i<a. u N ((T^^(i * N))x))" if "a>0" for a
  using that proof (induction rule: ind_from_1)
    case 1
    show ?case by auto
  next
    case (Suc a)
    have "u ((a+1)*N) x = u((a*N) + N) x"
      by (simp add: semiring_normalization_rules(2) semiring_normalization_rules(23))
    also have "... ≤ u(a*N) x + u N ((T^^(a*N))x)"
      using assms(1) unfolding subcocycle_def by auto
    also have "... ≤ (∑i<a. u N ((T^^(i * N))x)) + u N ((T^^(a*N))x)"
      using Suc by auto
    also have "... = (∑i<a+1. u N ((T^^(i * N))x))"
      by auto
    finally show ?case by auto
  qed

  define E1 where "E1 = (∑i<N. abs(u 1 ((T^^i)x)))"
  define E2 where "E2 = (∑i<2*N. abs(u 1 ((T^^(n-(2*N-i))) x)))"
  have "E2 ≥ 0" unfolding E2_def by auto

  obtain a0 s0 where 0: "s0 < N" "n = a0 * N + s0"
    using ‹0 < N› mod_div_decomp mod_less_divisor by blast
  then have "a0 ≥ 1" using ‹n > 2 * N› ‹N>0›
    by (metis Nat.add_0_right add.commute add_lessD1 add_mult_distrib comm_monoid_mult_class.mult_1 eq_imp_le
    less_imp_add_positive less_imp_le_nat less_one linorder_neqE_nat mult.left_neutral mult_not_zero not_add_less1 one_add_one)
  define a s where "a = a0-1" and "s = s0+N"
  then have as: "n = a * N + s" unfolding a_def s_def using ‹a0 ≥ 1› 0 by (simp add: mult_eq_if)
  have s: "s ≥ N" "s < 2*N" using 0 unfolding s_def by auto
  have a: "a*N > n - 2*N" "a*N ≤ n - N" using as s ‹n > 2*N› by auto
  then have "(a*N - (n-2*N)) ≤ N" using ‹n > 2*N› by auto
  have "a*N ≥ n - 2*N" using a by simp

  {
    fix r::nat assume "r < N"
    have "a*N+r > n - 2*N" using ‹n>2*N› as s by auto

    define tr where "tr = n-(a*N+r)"
    have "tr > 0" unfolding tr_def using as s ‹r<N\› by auto
    then have *: "n = (a*N+r) + tr" unfolding tr_def by auto

    have "birkhoff_sum (u 1) tr ((T^^(a*N+r))x) = (∑i<tr. u 1 ((T^^(a*N+r+i))x))"
      unfolding birkhoff_sum_def by (simp add: add.commute funpow_add)
    also have "... = (∑i∈{a*N+r..<a*N+r+tr}. u 1 ((T^^i) x))"
      by (rule sum.reindex_bij_betw, rule bij_betw_byWitness[where ?f' = "λi. i - (a * N + r)"], auto)
    also have "... ≤ (∑i∈{a*N+r..<a*N+r+tr}. abs(u 1 ((T^^i) x)))"
      by (simp add: sum_mono)
    also have "... ≤ (∑i∈{n-2*N..<n}. abs(u 1 ((T^^i) x)))"
      apply (rule sum_mono2) using as s ‹r<N\› tr_def by auto
    also have "... = E2" unfolding E2_def
      apply (rule sum.reindex_bij_betw[symmetric], rule bij_betw_byWitness[where ?f' = "λi. i - (n-2*N)"])
      using ‹n > 2*N› by auto
    finally have A: "birkhoff_sum (u 1) tr ((T^^(a*N+r))x) ≤ E2" by simp

    have "u n x ≤ u (a*N+r) x + u tr ((T^^(a*N+r))x)"
      using assms(1) * unfolding subcocycle_def by auto
    also have "... ≤ u (a*N+r) x + birkhoff_sum (u 1) tr ((T^^(a*N+r))x)"
      using subcocycle_bounded_by_birkhoff1[OF assms(1)] ‹tr > 0› by auto
    finally have B: "u n x ≤ u (a*N+r) x + E2"
      using A by auto

    have "u (a*N+r) x ≤ (∑i<N. abs(u 1 ((T^^i)x))) + (∑i<a. u N ((T^^(i*N+r))x))"
    proof (cases "r = 0")
      case True
      then have "a>0" using ‹a*N+r > n - 2*N› not_less by fastforce
      have "u(a*N+r) x ≤ (∑i<a. u N ((T^^(i*N+r))x))" using Ia[OF ‹a>0›] True by auto
      moreover have "0 ≤ (∑i<N. abs(u 1 ((T^^i)x)))" by auto
      ultimately show ?thesis by linarith
    next
      case False
      then have I: "u (a*N+r) x ≤ u r x + (∑i<a. u N ((T^^(i * N + r))x))" using Iar by auto
      have "u r x ≤ (∑i<r. u 1 ((T^^i)x))"
        using subcocycle_bounded_by_birkhoff1[OF assms(1)] False unfolding birkhoff_sum_def by auto
      also have "... ≤ (∑i<r. abs(u 1 ((T^^i)x)))"
        by (simp add: sum_mono)
      also have "... ≤ (∑i<N. abs(u 1 ((T^^i)x)))"
        apply (rule sum_mono2) using ‹r<N\› by auto
      finally show ?thesis using I by auto
    qed
    then have "u n x ≤ E1 + (∑i<a. u N ((T^^(i*N+r))x)) + E2"
      unfolding E1_def using B by auto
  } note * = this

  have I: "u N ((T^^j) x) ≤ E2" if "j∈{n-2*N..<a*N}" for j
  proof -
    have "u N ((T^^j) x) ≤ (∑i<N. u 1 ((T^^i) ((T^^j)x)))"
      using subcocycle_bounded_by_birkhoff1[OF assms(1) ‹N>0›] unfolding birkhoff_sum_def by auto
    also have "... = (∑i<N. u 1 ((T^^(i+j))x))" by (simp add: funpow_add)
    also have "... ≤ (∑i<N. abs(u 1 ((T^^(i+j))x)))" by (rule sum_mono, auto)
    also have "... = (∑k∈{j..<N+j}. abs(u 1 ((T^^k)x)))"
      by (rule sum.reindex_bij_betw, rule bij_betw_byWitness[where ?f' = "λk. k-j"], auto)
    also have "... ≤ (∑i∈{n-2*N..<n}. abs(u 1 ((T^^i) x)))"
      apply (rule sum_mono2) using ‹j∈{n-2*N..<a*N}› ‹a*N ≤ n - N› by auto
    also have "... = E2" unfolding E2_def
      apply (rule sum.reindex_bij_betw[symmetric], rule bij_betw_byWitness[where ?f' = "λi. i - (n-2*N)"])
      using ‹n > 2*N› by auto
    finally show ?thesis by auto
  qed
  have "(∑j<a*N. u N ((T^^j) x)) - (∑j<n-2*N. u N ((T^^j) x)) = (∑j∈{n-2*N..<a*N}. u N ((T^^j) x))"
    using sum.atLeastLessThan_concat[OF _ ‹a*N ≥ n - 2*N›, of 0 "λj. u N ((T^^j) x)", symmetric] atLeast0LessThan by simp
  also have "... ≤ (∑j∈{n-2*N..<a*N}. E2)" by (rule sum_mono[OF I])
  also have "... = (a*N - (n-2*N)) * E2" by simp
  also have "... ≤ N * E2" using ‹(a*N - (n-2*N)) ≤ N› ‹E2 ≥ 0› by (simp add: mult_right_mono)
  finally have J: "(∑j<a*N. u N ((T^^j) x)) ≤ (∑j<n-2*N. u N ((T^^j) x)) + N * E2" by auto

  have "N * u n x = (∑r<N. u n x)" by auto
  also have "... ≤ (∑r<N. E1 + E2 + (∑i<a. u N ((T^^(i*N+r))x)))"
    apply (rule sum_mono) using * by fastforce
  also have "... = (∑r<N. E1 + E2) + (∑r<N. (∑i<a. u N ((T^^(i*N+r))x)))"
    by (rule sum.distrib)
  also have "... = N* (E1 + E2) + (∑j<a*N. u N ((T^^j) x))"
    using sum_arith_progression by auto
  also have "... ≤ N *(E1+E2) + (∑j<n-2*N. u N ((T^^j) x)) + N*E2"
    using J by auto
  also have "... = N * (E1+E2) + N * (∑j<n-2*N. u N ((T^^j) x) / N) + N * E2"
    using ‹N>0› by (simp add: sum_distrib_left)
  also have "... = N*(E1 + E2 + (∑j<n-2*N. u N ((T^^j) x) / N) + E2)"
    by (simp add: distrib_left)
  finally have "u n x ≤ E1 + 2*E2 + birkhoff_sum (λx. u N x / N) (n-2*N) x"
    unfolding birkhoff_sum_def using ‹N>0› by auto
  then show ?thesis unfolding E1_def E2_def by auto
qed

text ‹Many natural cocycles are only defined almost everywhere, and then the
  property only makes sense almost everywhere. We will now show
  such an a.e.-subcocycle coincides almost everywhere with a genuine subcocycle
  the above sense. Then, all the results for subcocycles will apply to such
 .e.-subcocycles. (Usually, in ergodic theory, subcocycles only satisfy the subadditivity
  almost everywhere, but we have requested it everywhere for simplicity in the proofs.)

  subcocycle will be defined in a recursive way. This means that is can not be defined in a
  (since complicated function definitions are not available inside proofs). Since it is
  in terms of $u$, then $u$ has to be available at the top level, which is most
  done using a context.
 ›
context
  fixes u::"nat ==> 'a ==> real"
  assumes H: "∧m n. AE x in M. u (n+m) x ≤ u n x + u m ((T^^n) x)"
          "∧n. integrable M (u n)"
begin

private fun v :: "nat ==> 'a ==> real" where "v n x = (
  if n = 0 then max (u 0 x) 0
  else if n = 1 then u 1 x
  else min (u n x) (Min ((λk. v k x + v (n-k) ((T^^k) x))`{0<..<n})))"

private lemma v0 [simp]:
  ‹v 0 x = max (u 0 x) 0›
  by simp

private lemma v1 [simp]:
  ‹v (Suc 0) x = u 1 x›
  by simp

private lemma v2 [simp]:
  ‹v n x = min (u n x) (Min ((λk. v k x + v (n-k) ((T^^k) x))`{0<..<n}))› if ‹n ≥ 2›
  using that by (subst v.simps) (simp del: v.simps)

declare v.simps [simp del]

private lemma integrable_v:
  "integrable M (v n)" for n
proof (induction n rule: nat_less_induct)
  case (1 n)
  consider "n = 0" | "n = 1" | "n>1" by linarith
  then show ?case
  proof (cases)
    assume "n = 0"
    have "v 0 x = max (u 0 x) 0" for x by simp
    then show ?thesis using integrable_max[OF H(2)[of 0]] ‹n = 0› by auto
  next
    assume "n = 1"
    have "v 1 x = u 1 x" for x by simp
    then show ?thesis using H(2)[of 1] ‹n = 1› by auto
  next
    assume "n > 1"
    hence "v n x = min (u n x) (MIN k ∈ {0<..<n}. v k x + v (n-k) ((T^^k) x))" for x
      by simp
    moreover have "integrable M (λx. min (u n x) (MIN k ∈ {0<..<n}. v k x + v (n-k) ((T^^k) x)))"
      apply (rule integrable_min)
      apply (simp add: H(2))
      apply (rule integrable_MIN, simp)
      using ‹n >1› apply auto[1]
      apply (rule Bochner_Integration.integrable_add)
      using "1.IH" apply auto[1]
      apply (rule Tn_integral_preserving(1))
      using "1.IH" by (metis ‹1 < n› diff_less greaterThanLessThan_iff max_0_1(2) max_less_iff_conj)
    ultimately show ?case by auto
  qed
qed

private lemma u_eq_v_AE:
  "AE x in M. v n x = u n x" for n
proof (induction n rule: nat_less_induct)
  case (1 n)
  consider "n = 0" | "n = 1" | "n>1" by linarith
  then show ?case
  proof (cases)
    assume "n = 0"
    have "AE x in M. u 0 x ≤ u 0 x + u 0 x" using H(1)[of 0 0] by auto
    then have "AE x in M. u 0 x ≥ 0" by auto
    moreover have "v 0 x = max (u 0 x) 0" for x by simp
    ultimately show ?thesis using ‹n = 0› by auto
  next
    assume "n = 1"
    have "v 1 x = u 1 x" for x by simp
    then show ?thesis using ‹n = 1› by simp
  next
    assume "n > 1"
    {
      fix k assume "k<n"
      then have "AE x in M. v k x = u k x" using "1.IH" by simp
      with T_AE_iterates[OF this] have "AE x in M. ∀s. v k ((T^^s) x) = u k ((T^^s) x)" by simp
    } note * = this
    have "AE x in M. ∀k ∈ {..<n}. ∀s. v k ((T^^s) x) = u k ((T^^s) x)"
      apply (rule AE_finite_allI) using * by simp_all
    moreover have "AE x in M. ∀i j. u (i+j) x ≤ u i x + u j ((T^^i) x)"
      apply (subst AE_all_countable, intro allI)+ using H(1) by simp
    moreover
    {
      fix x assume "∀k ∈ {..<n}. ∀s. v k ((T^^s) x) = u k ((T^^s) x)"
                   "∀i j. u (i+j) x ≤ u i x + u j ((T^^i) x)"
      then have Hx: "∧k s. k < n ==> v k ((T^^s) x) = u k ((T^^s) x)"
                    "∧i j. u (i+j) x ≤ u i x + u j ((T^^i) x)"
        by auto
      {
        fix k assume "k ∈ {0<..<n}"
        then have K: "k<n" "n-k<n" by auto
        have "u n x ≤ u k x + u (n-k) ((T^^k) x)" using Hx(2) K by (metis le_add_diff_inverse less_imp_le_nat)
        also have "... = v k x + v (n-k) ((T^^k)x)" using Hx(1)[OF ‹k <n\›, of 0] Hx(1)[OF ‹n-k <n\›, of k] by auto
        finally have "u n x ≤ v k x + v (n-k) ((T^^k)x)" by simp
      }
      then have *: "∧z. z ∈ (λk. v k x + v (n-k) ((T^^k) x))`{0<..<n} ==> u n x ≤ z" by blast
      have "u n x ≤ Min ((λk. v k x + v (n-k) ((T^^k) x))`{0<..<n})"
        apply (rule Min.boundedI) using ‹n>1› * by auto
      moreover have "v n x = min (u n x) (Min ((λk. v k x + v (n-k) ((T^^k) x))`{0<..<n}))"
        using ‹1<n\› by auto
      ultimately have "v n x = u n x" by auto
    }
    ultimately show ?thesis by auto
  qed
qed

private lemma subcocycle_v:
  "v (n+m) x ≤ v n x + v m ((T^^n) x)"
proof -
  consider "n = 0" | "m = 0" | "n>0 ∧ m >0" by auto
  then show ?thesis
  proof (cases)
    case 1
    then have "v n x ≥ 0" by simp
    then show ?thesis using ‹n = 0› by auto
  next
    case 2
    then have "v m x ≥ 0" by simp
    then show ?thesis using ‹m = 0› by auto
  next
    case 3
    then have "n+m > 1" by simp
    then have "v (n+m) x = min (u(n+m) x) (Min ((λk. v k x + v ((n+m)-k) ((T^^k) x))`{0<..<n+m}))" by simp
    also have "... ≤ Min ((λk. v k x + v ((n+m)-k) ((T^^k) x))`{0<..<n+m})" by simp
    also have "... ≤ v n x + v ((n+m)-n) ((T^^n) x)"
      apply (rule Min_le, simp)
      by (metis (lifting) ‹0 < n ∧ 0 < m› add.commute greaterThanLessThan_iff image_iff less_add_same_cancel2)
    finally show ?thesis by simp
  qed
qed

lemma subcocycle_AE_in_context:
  "∃w. subcocycle w ∧ (AE x in M. ∀n. w n x = u n x)"
proof -
  have "subcocycle v" using subcocycle_v integrable_v unfolding subcocycle_def by auto
  moreover have "AE x in M. ∀n. v n x = u n x"
    by (subst AE_all_countable, intro allI, rule u_eq_v_AE)
  ultimately show ?thesis by blast
qed

end

lemma subcocycle_AE:
  fixes u::"nat ==> 'a ==> real"
  assumes "∧m n. AE x in M. u (n+m) x ≤ u n x + u m ((T^^n) x)"
          "∧n. integrable M (u n)"
  shows "∃w. subcocycle w ∧ (AE x in M. ∀n. w n x = u n x)"
using subcocycle_AE_in_context assms by blast


subsection ‹The asymptotic average›

text ‹In this subsection, we define the asymptotic average of a subcocycle $u$, i.e., the
  of $\int u_n(x)/n$ (the convergence follows from subadditivity of $\int u_n$) and study its
  properties, especially in terms of operations on subcocycles. In general, it can be
 -\infty$, so we define it in the extended reals.›

definition subcocycle_avg_ereal::"(nat ==> 'a ==> real) ==> ereal" where
  "subcocycle_avg_ereal u = Inf {ereal((∫x. u n x ∂M) / n) |n. n > 0}"

lemma subcocycle_avg_finite:
  "subcocycle_avg_ereal u < ∞"
unfolding subcocycle_avg_ereal_def using Inf_less_iff less_ereal.simps(4) by blast

lemma subcocycle_avg_subadditive:
  assumes "subcocycle u"
  shows "subadditive (λn. (∫x. u n x ∂M))"
unfolding subadditive_def proof (intro allI)
  have int_u [measurable]: "∧n. integrable M (u n)" using assms unfolding subcocycle_def by auto
  fix m n
  have "(∫x. u (n+m) x ∂M) ≤ (∫x. u n x + u m ((T^^n) x) ∂M)"
    apply (rule integral_mono)
    using int_u apply (auto simp add: Tn_integral_preserving(1))
    using assms unfolding subcocycle_def by auto
  also have "... ≤ (∫x. u n x ∂M) + (∫x. u m ((T^^n) x) ∂M)"
    using int_u by (auto simp add: Tn_integral_preserving(1))
  also have "... = (∫x. u n x ∂M) + (∫x. u m x ∂M)"
    using int_u by (auto simp add: Tn_integral_preserving(2))
  finally show "(∫x. u (n+m) x ∂M) ≤ (∫x. u n x ∂M) + (∫x. u m x ∂M)" by simp
qed

lemma subcocycle_int_tendsto_avg_ereal:
  assumes "subcocycle u"
  shows "(λn. (∫x. u n x / n ∂M)) <---- subcocycle_avg_ereal u"
unfolding subcocycle_avg_ereal_def
using subadditive_converges_ereal[OF subcocycle_avg_subadditive[OF assms]] by auto

text ‹The average behaves well under addition, scalar multiplication and max, trivially.›

lemma subcocycle_avg_ereal_add:
  assumes "subcocycle u" "subcocycle v"
  shows "subcocycle_avg_ereal (λn x. u n x + v n x) = subcocycle_avg_ereal u + subcocycle_avg_ereal v"
proof -
  have int [simp]: "∧n. integrable M (u n)" "∧n. integrable M (v n)" using assms unfolding subcocycle_def by auto
  {
    fix n
    have "(∫x. u n x / n ∂M) + (∫x. v n x / n ∂M) = (∫x. u n x / n + v n x / n ∂M)"
      by (rule Bochner_Integration.integral_add[symmetric], auto)
    also have "... = (∫x. (u n x + v n x) / n ∂M)"
      by (rule Bochner_Integration.integral_cong, auto simp add: add_divide_distrib)
    finally have "ereal (∫x. u n x / n ∂M) + (∫x. v n x / n ∂M) = (∫x. (u n x + v n x) / n ∂M)"
      by auto
  }
  moreover have "(λn. ereal (∫x. u n x / n ∂M) + (∫x. v n x / n ∂M))
                  <---- subcocycle_avg_ereal u + subcocycle_avg_ereal v"
    apply (intro tendsto_intros subcocycle_int_tendsto_avg_ereal[OF assms(1)] subcocycle_int_tendsto_avg_ereal[OF assms(2)])
    using subcocycle_avg_finite by auto
  ultimately have "(λn. (∫x. (u n x + v n x) / n ∂M)) <---- subcocycle_avg_ereal u + subcocycle_avg_ereal v"
    by auto
  moreover have "(λn. (∫x. (u n x + v n x) / n ∂M)) <---- subcocycle_avg_ereal (λn x. u n x + v n x)"
    by (rule subcocycle_int_tendsto_avg_ereal[OF subcocycle_add[OF assms]])
  ultimately show ?thesis using LIMSEQ_unique by blast
qed

lemma subcocycle_avg_ereal_cmult:
  assumes "subcocycle u" "c ≥ (0::real)"
  shows "subcocycle_avg_ereal (λn x. c * u n x) = c * subcocycle_avg_ereal u"
proof (cases "c = 0")
  case True
  have *: "ereal (∫x. (c * u n x) / n ∂M) = 0" if "n>0" for n
    by (subst True, auto)
  have "(λn. ereal (∫x. (c * u n x) / n ∂M)) <---- 0"
    by (subst lim_explicit, metis * less_le_trans zero_less_one)
  moreover have "(λn. ereal (∫x. (c * u n x) / n ∂M)) <---- subcocycle_avg_ereal (λn x. c * u n x)"
    using subcocycle_int_tendsto_avg_ereal[OF subcocycle_cmult[OF assms]] by auto
  ultimately have "subcocycle_avg_ereal (λn x. c * u n x) = 0"
    using LIMSEQ_unique by blast
  then show ?thesis using True by auto
next
  case False
  have int: "∧n. integrable M (u n)" using assms unfolding subcocycle_def by auto
  have "ereal (∫x. c * u n x / n ∂M) = c * ereal (∫x. u n x / n ∂M)" for n by auto
  then have "(λn. c * ereal (∫x. u n x / n ∂M)) <---- subcocycle_avg_ereal (λn x. c * u n x)"
    using subcocycle_int_tendsto_avg_ereal[OF subcocycle_cmult[OF assms]] by auto
  moreover have "(λn. c * ereal (∫x. u n x / n ∂M)) <---- c * subcocycle_avg_ereal u"
    apply (rule tendsto_mult_ereal) using False subcocycle_int_tendsto_avg_ereal[OF assms(1)] by auto
  ultimately show ?thesis using LIMSEQ_unique by blast
qed

lemma subcocycle_avg_ereal_max:
  assumes "subcocycle u" "subcocycle v"
  shows "subcocycle_avg_ereal (λn x. max (u n x) (v n x)) ≥ max (subcocycle_avg_ereal u) (subcocycle_avg_ereal v)"
proof (auto)
  have int: "integrable M (u n)" "integrable M (v n)" for n using assms unfolding subcocycle_def by auto
  have int2: "integrable M (λx. max (u n x) (v n x))" for n using integrable_max int by auto

  have "(∫x. u n x / n ∂M) ≤ (∫x. max (u n x) (v n x) / n ∂M)" for n
    apply (rule integral_mono) using int int2 by (auto simp add: divide_simps)
  then show "subcocycle_avg_ereal u ≤ subcocycle_avg_ereal (λn x. max (u n x) (v n x))"
    using LIMSEQ_le[OF subcocycle_int_tendsto_avg_ereal[OF assms(1)]
          subcocycle_int_tendsto_avg_ereal[OF subcocycle_max[OF assms]]] by auto

  have "(∫x. v n x / n ∂M) ≤ (∫x. max (u n x) (v n x) / n ∂M)" for n
    apply (rule integral_mono) using int int2 by (auto simp add: divide_simps)
  then show "subcocycle_avg_ereal v ≤ subcocycle_avg_ereal (λn x. max (u n x) (v n x))"
    using LIMSEQ_le[OF subcocycle_int_tendsto_avg_ereal[OF assms(2)]
          subcocycle_int_tendsto_avg_ereal[OF subcocycle_max[OF assms]]] by auto
qed

text ‹For a Birkhoff sum, the average at each time is the same, equal to the average of the
 , so the asymptotic average is also equal to this common value.›

lemma subcocycle_avg_ereal_birkhoff:
  assumes "integrable M u"
  shows "subcocycle_avg_ereal (birkhoff_sum u) = (∫x. u x ∂M)"
proof -
  have *: "ereal (∫x. (birkhoff_sum u n x) / n ∂M) = (∫x. u x ∂M)" if "n>0" for n
    using birkhoff_sum_integral(2)[OF assms] that by auto
  have "(λn. ereal (∫x. (birkhoff_sum u n x) / n ∂M)) <---- (∫x. u x ∂M)"
    by (subst lim_explicit, metis * less_le_trans zero_less_one)
  moreover have "(λn. ereal (∫x. (birkhoff_sum u n x) / n ∂M)) <---- subcocycle_avg_ereal (birkhoff_sum u)"
    using subcocycle_int_tendsto_avg_ereal[OF subcocycle_birkhoff[OF assms]] by auto
  ultimately show ?thesis using LIMSEQ_unique by blast
qed

text ‹In nice situations, where one can avoid the use of ereal, the following
  is more convenient. The kind of statements we are after is as follows: if the
  average is finite, then something holds, likely involving the real average.

  particular, we show in this setting what we have proved above under this new assumption:
  (in real numbers) of the average to the asymptotic average, as well as good behavior
  sum, scalar multiplication by positive numbers, max, formula for Birkhoff sums.›

definition subcocycle_avg::"(nat ==> 'a ==> real) ==> real" where
  "subcocycle_avg u = real_of_ereal(subcocycle_avg_ereal u)"

lemma subcocycle_avg_real_ereal:
  assumes "subcocycle_avg_ereal u > - ∞"
  shows "subcocycle_avg_ereal u = ereal(subcocycle_avg u)"
unfolding subcocycle_avg_def using assms subcocycle_avg_finite[of u] ereal_real by auto

lemma subcocycle_int_tendsto_avg:
  assumes "subcocycle u" "subcocycle_avg_ereal u > - ∞"
  shows "(λn. (∫x. u n x / n ∂M)) <---- subcocycle_avg u"
using subcocycle_avg_real_ereal[OF assms(2)] subcocycle_int_tendsto_avg_ereal[OF assms(1)] by auto

lemma subcocycle_avg_add:
  assumes "subcocycle u" "subcocycle v" "subcocycle_avg_ereal u > - ∞" "subcocycle_avg_ereal v > - ∞"
  shows "subcocycle_avg_ereal (λn x. u n x + v n x) > -∞"
        "subcocycle_avg (λn x. u n x + v n x) = subcocycle_avg u + subcocycle_avg v"
using assms subcocycle_avg_finite real_of_ereal_add
unfolding subcocycle_avg_def subcocycle_avg_ereal_add[OF assms(1) assms(2)] by auto

lemma subcocycle_avg_cmult:
  assumes "subcocycle u" "c ≥ (0::real)" "subcocycle_avg_ereal u > - ∞"
  shows "subcocycle_avg_ereal (λn x. c * u n x) > - ∞"
        "subcocycle_avg (λn x. c * u n x) = c * subcocycle_avg u"
using assms subcocycle_avg_finite unfolding subcocycle_avg_def subcocycle_avg_ereal_cmult[OF assms(1) assms(2)] by auto

lemma subcocycle_avg_max:
  assumes "subcocycle u" "subcocycle v" "subcocycle_avg_ereal u > - ∞" "subcocycle_avg_ereal v > - ∞"
  shows "subcocycle_avg_ereal (λn x. max (u n x) (v n x)) > -∞"
        "subcocycle_avg (λn x. max (u n x) (v n x)) ≥ max (subcocycle_avg u) (subcocycle_avg v)"
proof -
  show *: "subcocycle_avg_ereal (λn x. max (u n x) (v n x)) > - ∞"
    using assms(3) subcocycle_avg_ereal_max[OF assms(1) assms(2)] by auto
  have "ereal (subcocycle_avg (λn x. max (u n x) (v n x))) ≥ max (ereal(subcocycle_avg u)) (ereal(subcocycle_avg v))"
    using subcocycle_avg_real_ereal[OF assms(3)] subcocycle_avg_real_ereal[OF assms(4)]
      subcocycle_avg_real_ereal[OF *] subcocycle_avg_ereal_max[OF assms(1) assms(2)] by auto
  then show "subcocycle_avg (λn x. max (u n x) (v n x)) ≥ max (subcocycle_avg u) (subcocycle_avg v)"
    by auto
qed

lemma subcocycle_avg_birkhoff:
  assumes "integrable M u"
  shows "subcocycle_avg_ereal (birkhoff_sum u) > - ∞"
        "subcocycle_avg (birkhoff_sum u) = (∫x. u x ∂M)"
unfolding subcocycle_avg_def subcocycle_avg_ereal_birkhoff[OF assms(1)] by auto

end



subsection ‹Almost sure convergence of subcocycles›

text ‹In this paragraph, we prove Kingman's theorem, i.e., the almost sure convergence of
 . Their limit is almost surely invariant. There is no really easy proof. The one we use
  is arguably the simplest known one, due to Steele (1989). The idea is to show that the limsup
  the subcocycle is bounded by the liminf (which is almost surely constant along trajectories), by
  subadditivity along time intervals where the liminf is almost reached, of length at most $N$.
  some points, the liminf takes a large time $>N$ to be reached. We neglect those times,
  an additional error that gets smaller with $N$, thanks to Birkhoff ergodic theorem
  to the set of bad points. The error is most easily managed if the subcocycle is assumed to
  nonpositive, which one can assume in a first step. The general case is reduced to this one by
  $u_n$ with $u_n - S_n u_1 \leq 0$, and using Birkhoff theorem to control $S_n u_1$.›

context fmpt begin

text ‹First, as explained above, we prove the theorem for nonpositive subcocycles.›

lemma kingman_theorem_AE_aux1:
  assumes "subcocycle u"
          "∧x. u 1 x ≤ 0"
  shows "∃(g::'a==>ereal). (g∈borel_measurable Invariants ∧ (∀x. g x < ∞) ∧ (AE x in M. (λn. u n x / n) <---- g x))"
proof -
  define l where "l = (λx. liminf (λn. u n x / n))"
  have u_meas [measurable]: "∧n. u n ∈ borel_measurable M" using assms(1) unfolding subcocycle_def by auto
  have l_meas [measurable]: "l ∈ borel_measurable M" unfolding l_def by auto

  {
    fix x assume *: "(λn. birkhoff_sum (u 1) n x / n) <---- real_cond_exp M Invariants (u 1) x"
    then have "(λn. birkhoff_sum (u 1) n x / n) <---- ereal(real_cond_exp M Invariants (u 1) x)"
      by auto
    then have a: "liminf (λn. birkhoff_sum (u 1) n x / n) = ereal(real_cond_exp M Invariants (u 1) x)"
      using lim_imp_Liminf by force

    have "ereal(u n x / n) ≤ ereal(birkhoff_sum (u 1) n x / n)" if "n>0" for n
      using subcocycle_bounded_by_birkhoff1[OF assms(1) that, of x] that by (simp add: divide_right_mono)
    with eventually_mono[OF eventually_gt_at_top[of 0] this]
    have "eventually (λn. ereal(u n x / n) ≤ ereal(birkhoff_sum (u 1) n x / n)) sequentially" by auto
    then have "liminf (λn. u n x / n) ≤ liminf (λn. birkhoff_sum (u 1) n x / n)"
      by (simp add: Liminf_mono)
    then have "l x < ∞" unfolding l_def using a by auto
  }
  then have "AE x in M. l x < ∞"
    using birkhoff_theorem_AE_nonergodic[of "u 1"] subcocycle_def assms(1) by auto

  have l_dec: "l x ≤ l (T x)" for x
  proof -
    have "l x = liminf (λn. ereal ((u (n+1) x)/(n+1)))"
      unfolding l_def by (rule liminf_shift[of "λn. ereal (u n x / real n)", symmetric])
    also have "... ≤ liminf (λn. ereal((u 1 x)/(n+1)) + ereal((u n (T x))/(n+1)))"
    proof (rule Liminf_mono[OF eventuallyI])
      fix n
      have "u (1+n) x ≤ u 1 x + u n ((T^^1) x)" using assms(1) unfolding subcocycle_def by blast
      then have "u (n+1) x ≤ u 1 x + u n (T x)" by auto
      then have "(u (n+1) x)/(n+1) ≤ (u 1 x)/(n+1) + (u n (T x))/(n+1)"
        by (metis add_divide_distrib divide_right_mono of_nat_0_le_iff)
      then show "ereal ((u (n+1) x)/(n+1)) ≤ ereal((u 1 x)/(n+1)) + ereal((u n (T x))/(n+1))" by auto
    qed
    also have "... = 0 + liminf(λn. ereal((u n (T x))/(n+1)))"
    proof (rule ereal_liminf_lim_add[of "λn. ereal((u 1 x)/real(n+1))" 0 "λn. ereal((u n (T x))/(n+1))"])
      have "(λn. ereal((u 1 x)*(1/real(n+1)))) <---- ereal((u 1 x) * 0)"
        by (intro tendsto_intros LIMSEQ_ignore_initial_segment)
      then show "(λn. ereal((u 1 x)/real(n+1))) <---- 0" by (simp add: zero_ereal_def)
    qed (simp)
    also have "... = 1 * liminf(λn. ereal((u n (T x))/(n+1)))" by simp
    also have "... = liminf(λn. (n+1)/n * ereal((u n (T x))/(n+1)))"
    proof (rule ereal_liminf_lim_mult[symmetric])
      have "real (n+1) / real n = 1 + 1/real n" if "n>0" for n by (simp add: divide_simps mult.commute that)
      with eventually_mono[OF eventually_gt_at_top[of "0::nat"] this]
      have "eventually (λn. real (n+1) / real n = 1 + 1/real n) sequentially" by simp
      moreover have "(λn. 1 + 1/real n) <---- 1 + 0"
        by (intro tendsto_intros)
      ultimately have "(λn. real (n+1) / real n) <---- 1" using Lim_transform_eventually by (simp add: filterlim_cong)
      then show "(λn. ereal(real (n+1) / real n)) <---- 1" by (simp add: one_ereal_def)
    qed (auto)
    also have "... = l (T x)" unfolding l_def by auto
    finally show "l x ≤ l (T x)" by simp
  qed
  have "AE x in M. l (T x) = l x"
    apply (rule AE_increasing_then_invariant) using l_dec by auto
  then obtain g0 where g0: "g0 ∈ borel_measurable Invariants" "AE x in M. l x = g0 x"
    using Invariants_quasi_Invariants_functions[OF l_meas] by auto
  define g where "g = (λx. if g0 x = ∞ then 0 else g0 x)"
  have g: "g ∈ borel_measurable Invariants" "AE x in M. g x = l x"
    unfolding g_def using g0(1) ‹AE x in M. l x = g0 x› ‹AE x in M. l x < \∞› by auto
  have [measurable]: "g ∈ borel_measurable M" using g(1) Invariants_measurable_func by blast
  have "∧x. g x < ∞" unfolding g_def by auto

  define A where "A = {x ∈ space M. l x < ∞ ∧ (∀n. l ((T^^n) x) = g ((T^^n) x))}"
  have A_meas [measurable]: "A ∈ sets M" unfolding A_def by auto
  have "AE x in M. x ∈ A" unfolding A_def using T_AE_iterates[OF g(2)] ‹AE x in M. l x < \∞› by auto
  then have "space M - A ∈ null_sets M" by (simp add: AE_iff_null set_diff_eq)

  have l_inv: "l((T^^n) x) = l x" if "x ∈ A" for x n
  proof -
    have "l((T^^n) x) = g((T^^n) x)" using ‹ x ∈ A › unfolding A_def by blast
    also have "... = g x" using g(1) A_def Invariants_func_is_invariant_n that by blast
    also have "... = g((T^^0) x)" by auto
    also have "... = l((T^^0) x)" using ‹ x ∈ A › unfolding A_def by (metis (mono_tags, lifting) mem_Collect_eq)
    finally show ?thesis by auto
  qed

  define F where "F = (λ K e x. real_of_ereal(max (l x) (-ereal K)) + e)"
  have F_meas [measurable]: "F K e ∈ borel_measurable M" for K e unfolding F_def by auto
  define B where "B = (λN K e. {x ∈ A. ∃n∈{1..N}. u n x - n * F K e x < 0})"
  have B_meas [measurable]: "B N K e ∈ sets M" for N K e unfolding B_def by (measurable)
  define I where "I = (λN K e x. (indicator (- B N K e) x)::real)"
  have I_meas [measurable]: "I N K e ∈ borel_measurable M" for N K e unfolding I_def by auto
  have I_int: "integrable M (I N K e)" for N K e
    unfolding I_def apply (subst Bochner_Integration.integrable_cong[where ?g = "indicator (space M - B N K e)::_ ==> real"], auto)
    by (auto split: split_indicator simp: less_top[symmetric])

  have main: "AE x in M. limsup (λn. u n x / n) ≤ F K e x + abs(F K e x) * ereal(real_cond_exp M Invariants (I N K e) x)"
    if "N>(1::nat)" "K>(0::real)" "e>(0::real)" for N K e
  proof -
    let ?B = "B N K e" and ?I = "I N K e" and ?F = "F K e"

    define t where "t = (λx. if x ∈ ?B then Min {n∈{1..N}. u n x - n * ?F x < 0} else 1)"
    have [measurable]: "t ∈ measurable M (count_space UNIV)" unfolding t_def by measurable
    have t1: "t x ∈ {1..N}" for x
    proof (cases "x ∈ ?B")
      case False
      then have "t x = 1" by (simp add: t_def)
      then show ?thesis using ‹N>1›by auto
    next
      case True
      let ?A = "{n∈{1..N}. u n x - n * ?F x < 0}"
      have "t x = Min ?A" using True by (simp add: t_def)
      moreover have "Min ?A ∈ ?A" apply (rule Min_in, simp) using True B_def by blast
      ultimately show ?thesis by auto
    qed

    have bound1: "u (t x) x ≤ t x * ?F x + birkhoff_sum ?I (t x) x * abs(?F x)" for x
    proof (cases "x ∈ ?B")
      case True
      let ?A = "{n∈{1..N}. u n x - n * F K e x < 0}"
      have "t x = Min ?A" using True by (simp add: t_def)
      moreover have "Min ?A ∈ ?A" apply (rule Min_in, simp) using True B_def by blast
      ultimately have "u (t x) x ≤ (t x) * ?F x" by auto
      moreover have "0 ≤ birkhoff_sum ?I (t x) x * abs(?F x)" unfolding birkhoff_sum_def I_def by (simp add: sum_nonneg)
      ultimately show ?thesis by auto
    next
      case False
      then have "0 ≤ ?F x + ?I x * abs(?F x)" unfolding I_def by auto
      then have "u 1 x ≤ ?F x + ?I x * abs(?F x)" using assms(2)[of x] by auto
      moreover have "t x = 1" unfolding t_def using False by auto
      ultimately show ?thesis by auto
    qed

    define TB where "TB = (λx. (T^^(t x)) x)"
    have [measurable]: "TB ∈ measurable M M" unfolding TB_def by auto
    define S where "S = (λn x. (∑i<n. t((TB^^i) x)))"
    have [measurable]: "S n ∈ measurable M (count_space UNIV)" for n unfolding S_def by measurable
    have TB_pow: "(TB^^n) x = (T^^(S n x)) x" for n x
      unfolding S_def TB_def
      by (induction n, auto, metis (mono_tags, lifting) add.commute funpow_add o_apply)

    have uS: "u (S n x) x ≤ (S n x) * ?F x + birkhoff_sum ?I (S n x) x * abs(?F x)" if "x ∈ A" "n>0" for x n
    using ‹n > 0› proof (induction rule: ind_from_1)
      case 1
      show ?case unfolding S_def using bound1 by auto
    next
      case (Suc n)
      have *: "?F((TB^^n) x) = ?F x" apply (subst TB_pow) unfolding F_def using l_inv[OF ‹x∈A›] by auto
      have **: "S n x + t ((TB^^n) x) = S (Suc n) x" unfolding S_def by auto
      have "u (S (Suc n) x) x = u (S n x + t((TB^^n) x)) x" unfolding S_def by auto
      also have "... ≤ u (S n x) x + u (t((TB^^n) x)) ((T^^(S n x)) x)"
        using assms(1) unfolding subcocycle_def by auto
      also have "... ≤ u (S n x) x + u (t((TB^^n) x)) ((TB^^n) x)"
        using TB_pow by auto
      also have "... ≤ (S n x) * ?F x + birkhoff_sum ?I (S n x) x * abs(?F x) +
                  t ((TB^^n) x) * ?F ((TB^^n) x) + birkhoff_sum ?I (t ((TB^^n) x)) ((TB^^n) x) * abs(?F ((TB^^n) x))"
        using Suc bound1[of "((TB^^n) x)"] by auto
      also have "... = (S n x) * ?F x + birkhoff_sum ?I (S n x) x * abs(?F x) +
                  t ((TB^^n) x) * ?F x + birkhoff_sum ?I (t ((TB^^n) x)) ((T^^(S n x)) x) * abs(?F x)"
        using * TB_pow by auto
      also have "... = (real(S n x) + t ((TB^^n) x)) * ?F x +
                  (birkhoff_sum ?I (S n x) x + birkhoff_sum ?I (t ((TB^^n) x)) ((T^^(S n x)) x)) * abs(?F x)"
        by (simp add: mult.commute ring_class.ring_distribs(1))
      also have "... = (S n x + t ((TB^^n) x)) * ?F x +
                  (birkhoff_sum ?I (S n x) x + birkhoff_sum ?I (t ((TB^^n) x)) ((T^^(S n x)) x)) * abs(?F x)"
        by simp
      also have "... = (S (Suc n) x) * ?F x + birkhoff_sum ?I (S (Suc n) x) x * abs(?F x)"
        by (subst birkhoff_sum_cocycle[symmetric], subst **, subst **, simp)
      finally show ?case by simp
    qed

    have un: "u n x ≤ n * ?F x + N * abs(?F x) + birkhoff_sum ?I n x * abs(?F x)" if "x ∈ A" "n>N" for x n
    proof -
      let ?A = "{i. S i x > n}"
      let ?iA = "Inf ?A"
      have "n < (∑i<n + 1. 1)" by auto
      also have "... ≤ S (n+1) x" unfolding S_def apply (rule sum_mono) using t1 by auto
      finally have "?A ≠ {}" by blast
      then have "?iA ∈ ?A" by (meson Inf_nat_def1)
      moreover have "0 ∉ ?A" unfolding S_def by auto
      ultimately have "?iA ≠ 0" by fastforce
      define j where "j = ?iA - 1"
      then have "j < ?iA" using ‹?iA ≠ 0› by auto
      then have "j ∉ ?A" by (meson bdd_below_def cInf_lower le0 not_less)
      then have "S j x ≤ n" by auto
      define k where "k = n - S j x"
      have "n = S j x + k" unfolding k_def using ‹S j x ≤ n› by auto
      have "n < S (j+1) x" unfolding j_def using ‹?iA ≠ 0› ‹?iA ∈ ?A› by auto
      also have "... = S j x + t((TB^^j) x)" unfolding S_def by auto
      also have "... ≤ S j x + N" using t1 by auto
      finally have "k ≤ N" unfolding k_def using ‹n > N› by auto
      then have "S j x > 0" unfolding k_def using ‹n > N› by auto
      then have "j > 0" unfolding S_def using not_gr0 by fastforce

      have "birkhoff_sum ?I (S j x) x ≤ birkhoff_sum ?I n x"
        unfolding birkhoff_sum_def I_def using ‹S j x ≤ n›
        by (metis finite_Collect_less_nat indicator_pos_le lessThan_def lessThan_subset_iff sum_mono2)

      have "u n x ≤ u (S j x) x"
      proof (cases "k = 0")
        case True
        show ?thesis using True unfolding k_def using ‹S j x ≤ n› by auto
      next
        case False
        then have "k > 0" by simp
        have "u k ((T^^(S j x)) x) ≤ birkhoff_sum (u 1) k ((T ^^ S j x) x)"
          using subcocycle_bounded_by_birkhoff1[OF assms(1) ‹k>0›, of "(T^^(S j x)) x"] by simp
        also have "... ≤ 0" unfolding birkhoff_sum_def using sum_mono assms(2) by (simp add: sum_nonpos)
        also have "u n x ≤ u (S j x) x + u k ((T^^(S j x)) x)"
          apply (subst ‹n = S j x + k›) using assms(1) subcocycle_def by auto
        ultimately show ?thesis by auto
      qed
      also have "... ≤ (S j x) * ?F x + birkhoff_sum ?I (S j x) x * abs(?F x)"
        using uS[OF ‹x ∈ A› ‹j>0›] by simp
      also have "... ≤ (S j x) * ?F x + birkhoff_sum ?I n x * abs(?F x)"
        using ‹birkhoff_sum ?I (S j x) x ≤ birkhoff_sum ?I n x› by (simp add: mult_right_mono)
      also have "... = n * ?F x - k * ?F x + birkhoff_sum ?I n x * abs(?F x)"
        by (metis ‹n = S j x + k› add_diff_cancel_right' le_add2 left_diff_distrib' of_nat_diff)
      also have "... ≤ n * ?F x + k * abs(?F x) + birkhoff_sum ?I n x * abs(?F x)"
        by (auto, metis abs_ge_minus_self abs_mult abs_of_nat)
      also have "... ≤ n * ?F x + N * abs(?F x) + birkhoff_sum ?I n x * abs(?F x)"
        using ‹k ≤ N› by (simp add: mult_right_mono)
      finally show ?thesis by simp
    qed

    have "limsup (λn. u n x / n) ≤ ?F x + limsup (λn. abs(?F x) * ereal(birkhoff_sum ?I n x / n))" if "x ∈ A" for x
    proof -
      have "(λn. ereal(?F x + N * abs(?F x) * (1 / n))) <---- ereal(?F x + N * abs (?F x) * 0)"
        by (intro tendsto_intros)
      then have *: "limsup (λn. ?F x + N * abs(?F x)/n) = ?F x"
        using sequentially_bot tendsto_iff_Liminf_eq_Limsup by force

      {
        fix n assume "n > N"
        have "u n x / real n ≤ ?F x + N * abs(?F x) / n + abs(?F x) * birkhoff_sum ?I n x / n"
          using un[OF ‹x ∈ A› ‹n > N›] using ‹n>N› by (auto simp add: divide_simps mult.commute)
        then have "ereal(u n x/n) ≤ ereal(?F x + N * abs(?F x) / n) + abs(?F x) * ereal(birkhoff_sum ?I n x / n)"
          by auto
      }
      then have "eventually (λn. ereal(u n x / n) ≤ ereal(?F x + N * abs(?F x) / n) + abs(?F x) * ereal(birkhoff_sum ?I n x / n)) sequentially"
        using eventually_mono[OF eventually_gt_at_top[of N]] by auto
      with Limsup_mono[OF this]
      have "limsup (λn. u n x / n) ≤ limsup (λn. ereal(?F x + N * abs(?F x) / n) + abs(?F x) * ereal(birkhoff_sum ?I n x / n))"
        by auto
      also have "... ≤ limsup (λn. ?F x + N * abs(?F x) / n) + limsup (λn. abs(?F x) * ereal(birkhoff_sum ?I n x / n))"
        by (rule ereal_limsup_add_mono)
      also have "... = ?F x + limsup (λn. abs(?F x) * ereal(birkhoff_sum ?I n x / n))"
        using * by auto
      finally show ?thesis by auto
    qed
    then have *: "AE x in M. limsup (λn. u n x / n) ≤ ?F x + limsup (λn. abs(?F x) * ereal(birkhoff_sum ?I n x / n))"
      using ‹AE x in M. x ∈ A› by auto

    {
      fix x assume H: "(λn. birkhoff_sum ?I n x / n) <---- real_cond_exp M Invariants ?I x"
      have "(λn. abs(?F x) * ereal(birkhoff_sum ?I n x / n)) <---- abs(?F x) * ereal(real_cond_exp M Invariants ?I x)"
        by (rule tendsto_mult_ereal, auto simp add: H)
      then have "limsup (λn. abs(?F x) * ereal(birkhoff_sum ?I n x / n)) = abs(?F x) * ereal(real_cond_exp M Invariants ?I x)"
        using sequentially_bot tendsto_iff_Liminf_eq_Limsup by blast
    }
    moreover have "AE x in M. (λn. birkhoff_sum ?I n x / n) <---- real_cond_exp M Invariants ?I x"
      by (rule birkhoff_theorem_AE_nonergodic[OF I_int])
    ultimately have "AE x in M. limsup (λn. abs(?F x) * ereal(birkhoff_sum ?I n x / n)) = abs(?F x) * ereal(real_cond_exp M Invariants ?I x)"
      by auto
    then show ?thesis using * by auto
  qed

  have bound2: "AE x in M. limsup (λn. u n x / n) ≤ F K e x" if "K > 0" "e > 0" for K e
  proof -
    define C where "C = (λN. A - B N K e)"
    have C_meas [measurable]: "∧N. C N ∈ sets M" unfolding C_def by auto
    {
      fix x assume "x ∈ A"
      have "F K e x > l x" using ‹x ∈ A› ‹e > 0› unfolding F_def A_def
        by (cases "l x", auto, metis add.commute ereal_max less_add_same_cancel2 max_less_iff_conj real_of_ereal.simps(1))
      then have "∃n>0. ereal(u n x / n) < F K e x" unfolding l_def using liminf_upper_bound by fastforce
      then obtain n where "n>0" "ereal(u n x / n) < F K e x" by auto
      then have "u n x - n * F K e x < 0" by (simp add: divide_less_eq mult.commute)
      then have "x ∉ C n" unfolding C_def B_def using ‹x ∈ A› ‹n>0› by auto
      then have "x ∉ (∩n. C n)" by auto
    }
    then have "(∩n. C n) = {}" unfolding C_def by auto
    then have *: "0 = measure M (∩n. C n)" by auto
    have "(λn. measure M (C n)) <---- 0"
      apply (subst *, rule finite_Lim_measure_decseq, auto) unfolding C_def B_def decseq_def by auto
    moreover have "measure M (C n) = (∫x. norm(real_cond_exp M Invariants (I n K e) x) ∂M)" for n
    proof -
      have *: "AE x in M. 0 ≤ real_cond_exp M Invariants (I n K e) x"
        apply (rule real_cond_exp_pos, auto) unfolding I_def by auto

      have "measure M (C n) = (∫x. indicator (C n) x ∂M)"
        by auto
      also have "... = (∫x. I n K e x ∂M)"
        apply (rule integral_cong_AE, auto)
        unfolding C_def I_def indicator_def using ‹AE x in M. x ∈ A› by auto
      also have "... = (∫x. real_cond_exp M Invariants (I n K e) x ∂M)"
        by (rule real_cond_exp_int(2)[symmetric, OF I_int])
      also have "... = (∫x. norm(real_cond_exp M Invariants (I n K e) x) ∂M)"
        apply (rule integral_cong_AE, auto) using * by auto
      finally show ?thesis by auto
    qed
    ultimately have *: "(λn. (∫x. norm(real_cond_exp M Invariants (I n K e) x) ∂M)) <---- 0" by simp

    have "∃r. strict_mono r ∧ (AE x in M. (λn. real_cond_exp M Invariants (I (r n) K e) x) <---- 0)"
      apply (rule tendsto_L1_AE_subseq) using * real_cond_exp_int[OF I_int] by auto
    then obtain r where "strict_mono r" "AE x in M. (λn. real_cond_exp M Invariants (I (r n) K e) x) <---- 0"
      by auto
    moreover have "AE x in M. ∀N ∈ {1<..}. limsup (λn. u n x / n) ≤ F K e x + abs(F K e x) * ereal(real_cond_exp M Invariants (I N K e) x)"
      apply (rule AE_ball_countable') using main[OF _ ‹K>0› ‹e>0›] by auto
    moreover
    {
      fix x assume H: "(λn. real_cond_exp M Invariants (I (r n) K e) x) <---- 0"
                      "∧N. N > 1 ==> limsup (λn. u n x / n) ≤ F K e x + abs(F K e x) * ereal(real_cond_exp M Invariants (I N K e) x)"
      have 1: "eventually (λN. limsup (λn. u n x / n) ≤ F K e x + abs(F K e x) * ereal(real_cond_exp M Invariants (I (r N) K e) x)) sequentially"
        apply (rule eventually_mono[OF eventually_gt_at_top[of 1] H(2)])
        using ‹strict_mono r› less_le_trans seq_suble by blast
      have 2: "(λN. F K e x + (abs(F K e x) * ereal(real_cond_exp M Invariants (I (r N) K e) x))) <---- ereal(F K e x) + (abs(F K e x) * ereal 0)"
        by (intro tendsto_intros) (auto simp add: H(1))
      have "limsup (λn. u n x / n) ≤ F K e x"
        apply (rule LIMSEQ_le_const) using 1 2 by (auto simp add: eventually_at_top_linorder)
    }
    ultimately show "AE x in M. limsup (λn. u n x / n) ≤ F K e x" by auto
  qed
  have "AE x in M. limsup (λn. u n x / n) ≤ real_of_ereal(max (l x) (-ereal K))" if "K>(0::nat)" for K
    apply (rule AE_upper_bound_inf_ereal) using bound2 ‹K>0› unfolding F_def by auto
  then have "AE x in M. ∀K∈{(0::nat)<..}. limsup (λn. u n x / n) ≤ real_of_ereal(max (l x) (-ereal K))"
    by (rule AE_ball_countable', auto)
  moreover have "(λn. u n x / n) <---- l x"
    if H: "∀K∈{(0::nat)<..}. limsup (λn. u n x / n) ≤ real_of_ereal(max (l x) (-ereal K))" for x
  proof -
    have "limsup (λn. u n x / n) ≤ l x"
    proof (cases "l x = ∞")
      case False
      then have "(λK. real_of_ereal(max (l x) (-ereal K))) <---- l x"
        using ereal_truncation_real_bottom by auto
      moreover have "eventually (λK. limsup (λn. u n x / n) ≤ real_of_ereal(max (l x) (-ereal K))) sequentially"
        using H by (metis (no_types, lifting) eventually_at_top_linorder eventually_gt_at_top greaterThan_iff)
      ultimately show "limsup (λn. u n x / n) ≤ l x" using Lim_bounded2 eventually_sequentially by auto
    qed (simp)
    then have "limsup (λn. ereal (u n x / real n)) = l x"
      using Liminf_le_Limsup l_def eq_iff sequentially_bot by blast
    then show "(λn. u n x / n) <---- l x"
      by (simp add: l_def tendsto_iff_Liminf_eq_Limsup)
  qed
  ultimately have "AE x in M. (λn. u n x / n) <---- l x" by auto
  then have "AE x in M. (λn. u n x / n) <---- g x" using g(2) by auto
  then show "∃(g::'a==>ereal). (g∈borel_measurable Invariants ∧ (∀x. g x < ∞) ∧ (AE x in M. (λn. u n x / n) <---- g x))"
    using g(1) ‹∧x. g x < \∞› by auto
qed

text ‹We deduce it for general subcocycles, by reducing to nonpositive subcocycles by subtracting
  Birkhoff sum of $u_1$ (for which the convergence follows from Birkhoff theorem).›

theorem kingman_theorem_AE_aux2:
  assumes "subcocycle u"
  shows "∃(g::'a==>ereal). (g∈borel_measurable Invariants ∧ (∀x. g x < ∞) ∧ (AE x in M. (λn. u n x / n) <---- g x))"
proof -
  define v where "v = (λn x. u n x + birkhoff_sum (λx. - u 1 x) n x)"
  have "subcocycle v" unfolding v_def
    apply (rule subcocycle_add[OF assms], rule subcocycle_birkhoff)
    using assms unfolding subcocycle_def by auto
  have "∃(gv::'a==>ereal). (gv∈borel_measurable Invariants ∧ (∀x. gv x < ∞) ∧ (AE x in M. (λn. v n x / n) <---- gv x))"
    apply (rule kingman_theorem_AE_aux1[OF ‹subcocycle v›]) unfolding v_def by auto
  then obtain gv where gv: "gv ∈ borel_measurable Invariants" "AE x in M. (λn. v n x / n) <---- (gv x::ereal)" "∧x. gv x < ∞"
    by blast
  define g where "g = (λx. gv x + ereal(real_cond_exp M Invariants (u 1) x))"
  have g_meas: "g ∈ borel_measurable Invariants" unfolding g_def using gv(1) by auto
  have g_fin: "∧x. g x < ∞" unfolding g_def using gv(3) by auto

  have "AE x in M. (λn. birkhoff_sum (u 1) n x / n) <---- real_cond_exp M Invariants (u 1) x"
    apply (rule birkhoff_theorem_AE_nonergodic) using assms unfolding subcocycle_def by auto
  moreover
  {
    fix x assume H: "(λn. v n x / n) <---- (gv x)"
                    "(λn. birkhoff_sum (u 1) n x / n) <---- real_cond_exp M Invariants (u 1) x"
    then have "(λn. ereal(birkhoff_sum (u 1) n x / n)) <---- ereal(real_cond_exp M Invariants (u 1) x)"
      by auto
    {
      fix n
      have "u n x = v n x + birkhoff_sum (u 1) n x"
        unfolding v_def birkhoff_sum_def apply auto by (simp add: sum_negf)
      then have "u n x / n = v n x / n + birkhoff_sum (u 1) n x / n" by (simp add: add_divide_distrib)
      then have "ereal(u n x / n) = ereal(v n x / n) + ereal(birkhoff_sum (u 1) n x / n)"
        by auto
    } note * = this
    have "(λn. ereal(u n x / n)) <---- g x" unfolding * g_def
      apply (intro tendsto_intros) using H by auto
  }
  ultimately have "AE x in M. (λn. ereal(u n x / n)) <---- g x" using gv(2) by auto
  then show ?thesis using g_meas g_fin by blast
qed

text ‹For applications, it is convenient to have a limit which is really measurable with respect
  the invariant sigma algebra and does not come from a hard to use abstract existence statement.
  we introduce the following definition for the would-be limit -- Kingman's theorem shows that
  is indeed a limit.

  introduce the definition for any function, not only subcocycles, but it will only be usable for
 . We introduce an if clause in the definition so that the limit is always measurable,
  when $u$ is not a subcocycle and there is no convergence.›

definition subcocycle_lim_ereal::"(nat ==> 'a ==> real) ==> ('a ==> ereal)"
  where "subcocycle_lim_ereal u = (
    if (∃(g::'a==>ereal). (g∈borel_measurable Invariants ∧
      (∀x. g x < ∞) ∧ (AE x in M. (λn. u n x / n) <---- g x)))
    then (SOME (g::'a==>ereal). g∈borel_measurable Invariants ∧
      (∀x. g x < ∞) ∧ (AE x in M. (λn. u n x / n) <---- g x))
    else (λ_. 0))"

definition subcocycle_lim::"(nat ==> 'a ==> real) ==> ('a ==> real)"
  where "subcocycle_lim u = (λx. real_of_ereal(subcocycle_lim_ereal u x))"

lemma subcocycle_lim_meas_Inv [measurable]:
  "subcocycle_lim_ereal u ∈ borel_measurable Invariants"
  "subcocycle_lim u ∈ borel_measurable Invariants"
proof -
  show "subcocycle_lim_ereal u ∈ borel_measurable Invariants"
  proof (cases "∃(g::'a==>ereal). (g∈borel_measurable Invariants ∧ (∀x. g x < ∞) ∧ (AE x in M. (λn. u n x / n) <---- g x))")
    case True
    then have "subcocycle_lim_ereal u = (SOME (g::'a==>ereal). g∈borel_measurable Invariants ∧
          (∀x. g x < ∞) ∧ (AE x in M. (λn. u n x / n) <---- g x))"
      unfolding subcocycle_lim_ereal_def by auto
    then show ?thesis using someI_ex[OF True] by auto
  next
    case False
    then have "subcocycle_lim_ereal u = (λ_. 0)" unfolding subcocycle_lim_ereal_def by auto
    then show ?thesis by auto
  qed
  then show "subcocycle_lim u ∈ borel_measurable Invariants" unfolding subcocycle_lim_def by auto
qed

lemma subcocycle_lim_meas [measurable]:
  "subcocycle_lim_ereal u ∈ borel_measurable M"
  "subcocycle_lim u ∈ borel_measurable M"
using subcocycle_lim_meas_Inv Invariants_measurable_func apply blast
using subcocycle_lim_meas_Inv Invariants_measurable_func by blast

lemma subcocycle_lim_ereal_not_PInf:
  "subcocycle_lim_ereal u x < ∞"
proof (cases "∃(g::'a==>ereal). (g∈borel_measurable Invariants ∧ (∀x. g x < ∞) ∧ (AE x in M. (λn. u n x / n) <---- g x))")
  case True
  then have "subcocycle_lim_ereal u = (SOME (g::'a==>ereal). g∈borel_measurable Invariants ∧
        (∀x. g x < ∞) ∧ (AE x in M. (λn. u n x / n) <---- g x))"
    unfolding subcocycle_lim_ereal_def by auto
  then show ?thesis using someI_ex[OF True] by auto
next
  case False
  then have "subcocycle_lim_ereal u = (λ_. 0)" unfolding subcocycle_lim_ereal_def by auto
  then show ?thesis by auto
qed

text ‹We reformulate the subadditive ergodic theorem of Kingman with this definition.
  this point on, the technical definition of \verb+subcocycle_lim_ereal+ will never be used, only
  following property will be relevant.›

theorem kingman_theorem_AE_nonergodic_ereal:
  assumes "subcocycle u"
  shows "AE x in M. (λn. u n x / n) <---- subcocycle_lim_ereal u x"
proof -
  have *: "∃(g::'a==>ereal). (g∈borel_measurable Invariants ∧ (∀x. g x < ∞) ∧ (AE x in M. (λn. u n x / n) <---- g x))"
    using kingman_theorem_AE_aux2[OF assms] by auto
  then have "subcocycle_lim_ereal u = (SOME (g::'a==>ereal). g∈borel_measurable Invariants ∧
        (∀x. g x < ∞) ∧ (AE x in M. (λn. u n x / n) <---- g x))"
    unfolding subcocycle_lim_ereal_def by auto
  then show ?thesis using someI_ex[OF *] by auto
qed

text ‹The subcocycle limit behaves well under addition, multiplication by a positive scalar,
 , and is simply the conditional expectation with respect to invariants for Birkhoff sums,
  to Birkhoff theorem.›

lemma subcocycle_lim_ereal_add:
  assumes "subcocycle u" "subcocycle v"
  shows "AE x in M. subcocycle_lim_ereal (λn x. u n x + v n x) x = subcocycle_lim_ereal u x + subcocycle_lim_ereal v x"
proof -
  have "AE x in M. (λn. (u n x + v n x)/n) <---- subcocycle_lim_ereal (λn x. u n x + v n x) x"
    by (rule kingman_theorem_AE_nonergodic_ereal[OF subcocycle_add[OF assms]])
  moreover have "AE x in M. (λn. u n x / n) <---- subcocycle_lim_ereal u x"
    by (rule kingman_theorem_AE_nonergodic_ereal[OF assms(1)])
  moreover have "AE x in M. (λn. v n x / n) <---- subcocycle_lim_ereal v x"
    by (rule kingman_theorem_AE_nonergodic_ereal[OF assms(2)])
  moreover
  {
    fix x assume H: "(λn. (u n x + v n x)/n) <---- subcocycle_lim_ereal (λn x. u n x + v n x) x"
                    "(λn. u n x / n) <---- subcocycle_lim_ereal u x"
                    "(λn. v n x / n) <---- subcocycle_lim_ereal v x"
    have *: "(u n x + v n x)/n = ereal (u n x / n) + (v n x / n)" for n
      by (simp add: add_divide_distrib)
    have "(λn. (u n x + v n x)/n) <---- subcocycle_lim_ereal u x + subcocycle_lim_ereal v x"
      unfolding * apply (intro tendsto_intros H(2) H(3)) using subcocycle_lim_ereal_not_PInf by auto
    then have "subcocycle_lim_ereal (λn x. u n x + v n x) x = subcocycle_lim_ereal u x + subcocycle_lim_ereal v x"
      using H(1) by (simp add: LIMSEQ_unique)
  }
  ultimately show ?thesis by auto
qed

lemma subcocycle_lim_ereal_cmult:
  assumes "subcocycle u" "c≥(0::real)"
  shows "AE x in M. subcocycle_lim_ereal (λn x. c * u n x) x = c * subcocycle_lim_ereal u x"
proof -
  have "AE x in M. (λn. (c * u n x)/n) <---- subcocycle_lim_ereal (λn x. c * u n x) x"
    by (rule kingman_theorem_AE_nonergodic_ereal[OF subcocycle_cmult[OF assms]])
  moreover have "AE x in M. (λn. u n x / n) <---- subcocycle_lim_ereal u x"
    by (rule kingman_theorem_AE_nonergodic_ereal[OF assms(1)])
  moreover
  {
    fix x assume H: "(λn. (c * u n x)/n) <---- subcocycle_lim_ereal (λn x. c * u n x) x"
                    "(λn. u n x / n) <---- subcocycle_lim_ereal u x"
    have "(λn. c * ereal (u n x / n)) <---- c * subcocycle_lim_ereal u x"
      by (rule tendsto_cmult_ereal[OF _ H(2)], auto)
    then have "subcocycle_lim_ereal (λn x. c * u n x) x = c * subcocycle_lim_ereal u x"
      using H(1) by (simp add: LIMSEQ_unique)
  }
  ultimately show ?thesis by auto
qed

lemma subcocycle_lim_ereal_max:
  assumes "subcocycle u" "subcocycle v"
  shows "AE x in M. subcocycle_lim_ereal (λn x. max (u n x) (v n x)) x
                    = max (subcocycle_lim_ereal u x) (subcocycle_lim_ereal v x)"
proof -
  have "AE x in M. (λn. max (u n x) (v n x) / n) <---- subcocycle_lim_ereal (λn x. max (u n x) (v n x)) x"
    by (rule kingman_theorem_AE_nonergodic_ereal[OF subcocycle_max[OF assms]])
  moreover have "AE x in M. (λn. u n x / n) <---- subcocycle_lim_ereal u x"
    by (rule kingman_theorem_AE_nonergodic_ereal[OF assms(1)])
  moreover have "AE x in M. (λn. v n x / n) <---- subcocycle_lim_ereal v x"
    by (rule kingman_theorem_AE_nonergodic_ereal[OF assms(2)])
  moreover
  {
    fix x assume H: "(λn. max (u n x) (v n x) / n) <---- subcocycle_lim_ereal (λn x. max (u n x) (v n x)) x"
                    "(λn. u n x / n) <---- subcocycle_lim_ereal u x"
                    "(λn. v n x / n) <---- subcocycle_lim_ereal v x"
    have "(λn. max (ereal(u n x / n)) (ereal(v n x / n)))
            <---- max (subcocycle_lim_ereal u x) (subcocycle_lim_ereal v x)"
      apply (rule tendsto_max) using H by auto
    moreover have "max (ereal(u n x / n)) (ereal(v n x / n)) = max (u n x) (v n x) / n" for n
      by (simp del: ereal_max add:ereal_max[symmetric] max_divide_distrib_right)
    ultimately have "(λn. max (u n x) (v n x) / n)
          <---- max (subcocycle_lim_ereal u x) (subcocycle_lim_ereal v x)"
      by auto
    then have "subcocycle_lim_ereal (λn x. max (u n x) (v n x)) x
                = max (subcocycle_lim_ereal u x) (subcocycle_lim_ereal v x)"
      using H(1) by (simp add: LIMSEQ_unique)
  }
  ultimately show ?thesis by auto
qed

lemma subcocycle_lim_ereal_birkhoff:
  assumes "integrable M u"
  shows "AE x in M. subcocycle_lim_ereal (birkhoff_sum u) x = ereal(real_cond_exp M Invariants u x)"
proof -
  have "AE x in M. (λn. birkhoff_sum u n x / n) <---- real_cond_exp M Invariants u x"
    by (rule birkhoff_theorem_AE_nonergodic[OF assms])
  moreover have "AE x in M. (λn. birkhoff_sum u n x / n) <---- subcocycle_lim_ereal (birkhoff_sum u) x"
    by (rule kingman_theorem_AE_nonergodic_ereal[OF subcocycle_birkhoff[OF assms]])
  moreover
  {
    fix x assume H: "(λn. birkhoff_sum u n x / n) <---- real_cond_exp M Invariants u x"
                    "(λn. birkhoff_sum u n x / n) <---- subcocycle_lim_ereal (birkhoff_sum u) x"
    have "(λn. birkhoff_sum u n x / n) <---- ereal(real_cond_exp M Invariants u x)"
      using H(1) by auto
    then have "subcocycle_lim_ereal (birkhoff_sum u) x = ereal(real_cond_exp M Invariants u x)"
      using H(2) by (simp add: LIMSEQ_unique)
  }
  ultimately show ?thesis by auto
qed


subsection ‹$L^1$ and a.e.\ convergence of subcocycles with finite asymptotic average›

text ‹In this subsection, we show that the almost sure convergence in Kingman theorem
  takes place in $L^1$ if the limit is integrable, i.e., if the asymptotic average
  the subcocycle is $> -\infty$. To deduce it from the almost sure convergence, we only need
  show that there is no loss of mass, i.e., that the integral of the limit is not
  larger than the limit of the integrals (thanks to Scheffe criterion). This follows
  comparison to Birkhoff sums, for which we know that the average of the limit is
  same as the average of the function.›

text ‹First, we show that the subcocycle limit is bounded by the limit of the Birkhoff sums of
 u_N$, i.e., its conditional expectation. This follows from the fact that $u_n$ is bounded by the
  sum of $u_N$ (up to negligible boundary terms).›

lemma subcocycle_lim_ereal_atmost_uN_invariants:
  assumes "subcocycle u" "N>(0::nat)"
  shows "AE x in M. subcocycle_lim_ereal u x ≤ real_cond_exp M Invariants (λx. u N x / N) x"
proof -
  have "AE x in M. (λn. u 1 ((T^^n) x) / n) <---- 0"
    apply (rule limit_foTn_over_n') using assms(1) unfolding subcocycle_def by auto
  moreover have "AE x in M. (λn. birkhoff_sum (λx. u N x/N) n x / n) <---- real_cond_exp M Invariants (λx. u N x / N) x"
    apply (rule birkhoff_theorem_AE_nonergodic) using assms(1) unfolding subcocycle_def by auto
  moreover have "AE x in M. (λn. u n x / n) <---- subcocycle_lim_ereal u x"
    by (rule kingman_theorem_AE_nonergodic_ereal[OF assms(1)])
  moreover
  {
    fix x assume H: "(λn. u 1 ((T^^n) x) / n) <---- 0"
                    "(λn. birkhoff_sum (λx. u N x/N) n x / n) <---- real_cond_exp M Invariants (λx. u N x / N) x"
                    "(λn. u n x / n) <---- subcocycle_lim_ereal u x"

    let ?f = "λn. birkhoff_sum (λx. u N x / real N) (n - 2 * N) x / n
                  + (∑i<N. (1/n) * ∣u 1 ((T ^^ i) x)∣)
                  + 2 * (∑i<2*N. ∣u 1 ((T ^^ (n - (2 * N - i))) x)∣ / n)"
    {
      fix n assume "n≥2*N+1"
      then have "n > 2 * N" by simp
      have "u n x / n ≤ (birkhoff_sum (λx. u N x / real N) (n - 2 * N) x
                  + (∑i<N. ∣u 1 ((T ^^ i) x)∣)
                  + 2 * (∑i<2*N. ∣u 1 ((T ^^ (n - (2 * N - i))) x)∣)) / n"
        using subcocycle_bounded_by_birkhoffN[OF assms(1) ‹n>2*N› ‹N>0›, of x] ‹n>2*N› by (simp add: divide_right_mono)
      also have "... = ?f n"
        apply (subst add_divide_distrib)+ by (auto simp add: sum_divide_distrib[symmetric])
      finally have "u n x / n ≤ ?f n" by simp
      then have "u n x / n ≤ ereal(?f n)" by simp
    }

    have "(λn. ?f n) <---- real_cond_exp M Invariants (λx. u N x / N) x + (∑i<N. 0 * ∣u 1 ((T ^^ i) x)∣) + 2 * (∑i<2*N. 0)"
      apply (intro tendsto_intros) using H(2) tendsto_norm[OF H(1)] by auto
    then have "(λn. ereal(?f n)) <---- real_cond_exp M Invariants (λx. u N x / N) x"
      by auto
    with lim_mono[OF ‹∧n. n ≥ 2*N+1 ==> u n x / n ≤ ereal(?f n)› H(3) this]
    have "subcocycle_lim_ereal u x ≤ real_cond_exp M Invariants (λx. u N x / N) x" by simp
  }
  ultimately show ?thesis by auto
qed

text ‹To apply Scheffe criterion, we need to deal with nonnegative functions, or equivalently
  nonpositive functions after a change of sign. Hence, as in the proof of the almost
  version of Kingman theorem above, we first give the proof assuming that the
  is nonpositive, and deduce the general statement by adding a suitable
  sum.›

lemma kingman_theorem_L1_aux:
  assumes "subcocycle u" "subcocycle_avg_ereal u > -∞" "∧x. u 1 x ≤ 0"
  shows "AE x in M. (λn. u n x / n) <---- subcocycle_lim u x"
        "integrable M (subcocycle_lim u)"
        "(λn. (∫⁺x. abs(u n x / n - subcocycle_lim u x) ∂M)) <---- 0"
proof -
  have int_u [measurable]: "∧n. integrable M (u n)" using assms(1) subcocycle_def by auto
  then have int_F [measurable]: "∧n. integrable M (λx. - u n x/ n)" by auto

  have F_pos: "- u n x / n ≥ 0" for x n
  proof (cases "n > 0")
    case True
    have "u n x ≤ (∑i<n. u 1 ((T ^^ i) x))"
      using subcocycle_bounded_by_birkhoff1[OF assms(1) ‹n>0›] unfolding birkhoff_sum_def by simp
    also have "... ≤ 0" using sum_mono[OF assms(3)] by auto
    finally have "u n x ≤ 0" by simp
    then have "-u n x ≥ 0" by simp
    with divide_nonneg_nonneg[OF this] show "- u n x / n ≥ 0" using ‹n>0› by auto
  qed (auto)

  {
    fix x assume *: "(λn. u n x / n) <---- subcocycle_lim_ereal u x"
    have H: "(λn. - u n x / n) <---- - subcocycle_lim_ereal u x"
      using tendsto_cmult_ereal[OF _ *, of "-1"] by auto
    have "liminf (λn. -u n x / n) = - subcocycle_lim_ereal u x"
         "(λn. - u n x / n) <---- - subcocycle_lim_ereal u x"
         "- subcocycle_lim_ereal u x ≥ 0"
      using H apply (simp add: tendsto_iff_Liminf_eq_Limsup, simp)
      apply (rule LIMSEQ_le_const[OF H]) using F_pos by auto
  }
  then have AE_1: "AE x in M. liminf (λn. -u n x / n) = - subcocycle_lim_ereal u x"
                  "AE x in M. (λn. - u n x / n) <---- - subcocycle_lim_ereal u x"
                  "AE x in M. - subcocycle_lim_ereal u x ≥ 0"
    using kingman_theorem_AE_nonergodic_ereal[OF assms(1)] by auto

  have "(∫⁺ x. -subcocycle_lim_ereal u x ∂M) = (∫⁺ x. liminf (λn. -u n x / n) ∂M)"
    apply (rule nn_integral_cong_AE) using AE_1(1) by auto
  also have "... ≤ liminf (λn. ∫⁺ x. -u n x / n ∂M)"
    apply (subst e2ennreal_Liminf)
    apply (simp_all add: e2ennreal_ereal)
    using F_pos by (intro nn_integral_liminf) (simp add: int_F)
  also have "... = - subcocycle_avg_ereal u"
  proof -
    have "(λn. (∫x. u n x / n ∂M)) <---- subcocycle_avg_ereal u"
      by (rule subcocycle_int_tendsto_avg_ereal[OF assms(1)])
    with tendsto_cmult_ereal[OF _ this, of "-1"]
    have "(λn. (∫x. - u n x / n ∂M)) <---- - subcocycle_avg_ereal u" by simp
    then have "- subcocycle_avg_ereal u = liminf (λn. (∫x. - u n x / n ∂M))"
      by (simp add: tendsto_iff_Liminf_eq_Limsup)
    moreover have "(∫⁺ x. ennreal (-u n x / n) ∂M) = ennreal(∫x. - u n x / n ∂M)" for n
      apply (rule nn_integral_eq_integral[OF int_F]) using F_pos by auto
    ultimately show ?thesis
      by (auto simp: e2ennreal_Liminf e2ennreal_ereal)
  qed
  finally have "(∫⁺ x. -subcocycle_lim_ereal u x ∂M) ≤ - subcocycle_avg_ereal u" by simp
  also have "… < ∞" using assms(2)
    by (cases "subcocycle_avg_ereal u") (auto simp: e2ennreal_ereal e2ennreal_neg)
  finally have *: "(∫⁺ x. -subcocycle_lim_ereal u x ∂M) < ∞" .
  have "AE x in M. e2ennreal (- subcocycle_lim_ereal u x) ≠ ∞"
    apply (rule nn_integral_PInf_AE) using * by auto
  then have **: "AE x in M. - subcocycle_lim_ereal u x ≠ ∞"
    using AE_1(3) by eventually_elim simp

  {
    fix x assume H: "- subcocycle_lim_ereal u x ≠ ∞"
                    "(λn. u n x / n) <---- subcocycle_lim_ereal u x"
                    "- subcocycle_lim_ereal u x ≥ 0"
    then have 1: "abs(subcocycle_lim_ereal u x) ≠ ∞" by auto
    then have 2: "(λn. u n x / n) <---- subcocycle_lim u x" using H(2) unfolding subcocycle_lim_def by auto
    then have 3: "(λn. - (u n x / n)) <---- - subcocycle_lim u x" using tendsto_mult[OF _ 2, of "λ_. -1", of "-1"] by auto
    have 4: "-subcocycle_lim u x ≥ 0" using H(3) unfolding subcocycle_lim_def by auto

    have "abs(subcocycle_lim_ereal u x) ≠ ∞"
         "(λn. u n x / n) <---- subcocycle_lim u x"
         "(λn. - (u n x / n)) <---- - subcocycle_lim u x"
         "-subcocycle_lim u x ≥ 0"
      using 1 2 3 4 by auto
  }
  then have AE_2: "AE x in M. abs(subcocycle_lim_ereal u x) ≠ ∞"
                  "AE x in M. (λn. u n x / n) <---- subcocycle_lim u x"
                  "AE x in M. (λn. - (u n x / n)) <---- - subcocycle_lim u x"
                  "AE x in M. -subcocycle_lim u x ≥ 0"
    using kingman_theorem_AE_nonergodic_ereal[OF assms(1)] ** AE_1(3) by auto
  then show "AE x in M. (λn. u n x / n) <---- subcocycle_lim u x" by simp

  have "(∫⁺x. abs(subcocycle_lim u x) ∂M) = (∫⁺x. -subcocycle_lim_ereal u x ∂M)"
    apply (rule nn_integral_cong_AE)
    using AE_2 unfolding subcocycle_lim_def abs_real_of_ereal
    apply eventually_elim
    by (auto simp: e2ennreal_ereal)
  then have A: "(∫⁺x. abs(subcocycle_lim u x) ∂M) < ∞" using * by auto
  show int_Gr: "integrable M (subcocycle_lim u)"
    apply (rule integrableI_bounded) using A by auto

  have B: "(λn. (∫⁺ x. norm((- u n x /n) - (-subcocycle_lim u x)) ∂M)) <---- 0"
  proof (rule Scheffe_lemma1, auto simp add: int_Gr int_u AE_2(2) AE_2(3))
    {
      fix n assume "n>(0::nat)"
      have *: "AE x in M. subcocycle_lim u x ≤ real_cond_exp M Invariants (λx. u n x / n) x"
        using subcocycle_lim_ereal_atmost_uN_invariants[OF assms(1) ‹n>0›] AE_2(1)
        unfolding subcocycle_lim_def by auto
      have "(∫x. subcocycle_lim u x ∂M) ≤ (∫x. real_cond_exp M Invariants (λx. u n x / n) x ∂M)"
        apply (rule integral_mono_AE[OF int_Gr _ *], rule real_cond_exp_int(1)) using int_u by auto
      also have "... = (∫x. u n x / n ∂M)" apply (rule real_cond_exp_int(2)) using int_u by auto
      finally have A: "(∫x. subcocycle_lim u x ∂M) ≤ (∫x. u n x / n ∂M)" by auto

      have "(∫⁺x. abs(u n x) / n ∂M) = (∫⁺x. - u n x / n ∂M)"
        apply (rule nn_integral_cong) using F_pos abs_of_nonneg by (intro arg_cong[where f = ennreal]) fastforce
      also have "... = (∫x. - u n x / n ∂M)"
        apply (rule nn_integral_eq_integral) using F_pos int_F by auto
      also have "... ≤ (∫x. - subcocycle_lim u x ∂M)" using A by (auto intro!: ennreal_leI)
      also have "... = (∫⁺x. - subcocycle_lim u x ∂M)"
        apply (rule nn_integral_eq_integral[symmetric]) using int_Gr AE_2(4) by auto
      also have "... = (∫⁺x. abs(subcocycle_lim u x) ∂M)"
        apply (rule nn_integral_cong_AE) using AE_2(4) by auto
      finally have "(∫⁺x. abs(u n x) / n ∂M) ≤ (∫⁺x. abs(subcocycle_lim u x) ∂M)" by simp
    }
    with eventually_mono[OF eventually_gt_at_top[of 0] this]
    have "eventually (λn. (∫⁺x. abs(u n x) / n ∂M) ≤ (∫⁺x. abs(subcocycle_lim u x) ∂M)) sequentially"
      by fastforce
    then show "limsup (λn. ∫⁺ x. abs(u n x) / n ∂M) ≤ ∫⁺ x. abs(subcocycle_lim u x) ∂M"
      using Limsup_bounded by fastforce
  qed
  moreover have "norm((- u n x /n) - (-subcocycle_lim u x)) = abs(u n x / n - subcocycle_lim u x)"
    for n x by auto
  ultimately show "(λn. ∫⁺ x. ennreal ∣u n x / real n - subcocycle_lim u x∣ ∂M) <---- 0"
    by auto
qed

text ‹We can then remove the nonpositivity assumption, by subtracting the Birkhoff sums of $u_1$
  a general subcocycle $u$.›

theorem kingman_theorem_nonergodic:
  assumes "subcocycle u" "subcocycle_avg_ereal u > -∞"
  shows "AE x in M. (λn. u n x / n) <---- subcocycle_lim u x"
        "integrable M (subcocycle_lim u)"
        "(λn. (∫⁺x. abs(u n x / n - subcocycle_lim u x) ∂M)) <---- 0"
proof -
  have [measurable]: "u n ∈ borel_measurable M" for n using assms(1) unfolding subcocycle_def by auto
  have int_u [measurable]: "integrable M (u 1)" using assms(1) subcocycle_def by auto
  define v where "v = (λn x. u n x + birkhoff_sum (λx. - u 1 x) n x)"
  have [measurable]: "v n ∈ borel_measurable M" for n unfolding v_def by auto
  define w where "w = birkhoff_sum (u 1)"
  have [measurable]: "w n ∈ borel_measurable M" for n unfolding w_def by auto
  have "subcocycle v" unfolding v_def
    apply (rule subcocycle_add[OF assms(1)], rule subcocycle_birkhoff)
    using assms unfolding subcocycle_def by auto
  have "subcocycle w" unfolding w_def by (rule subcocycle_birkhoff[OF int_u])
  have uvw: "u n x = v n x + w n x" for n x
    unfolding v_def w_def birkhoff_sum_def by (auto simp add: sum_negf)
  then have "subcocycle_avg_ereal (λn x. u n x) = subcocycle_avg_ereal v + subcocycle_avg_ereal w"
    using subcocycle_avg_ereal_add[OF ‹subcocycle v› ‹subcocycle w›] by auto
  then have "subcocycle_avg_ereal u = subcocycle_avg_ereal v + subcocycle_avg_ereal w"
    by auto
  then have "subcocycle_avg_ereal v > -∞"
    unfolding w_def using subcocycle_avg_ereal_birkhoff[OF int_u] assms(2) by auto
  have "subcocycle_avg_ereal w > - ∞"
    unfolding w_def using subcocycle_avg_birkhoff[OF int_u] by auto

  have "∧x. v 1 x ≤ 0" unfolding v_def by auto
  have v: "AE x in M. (λn. v n x / n) <---- subcocycle_lim v x"
            "integrable M (subcocycle_lim v)"
            "(λn. (∫⁺x. abs(v n x / n - subcocycle_lim v x) ∂M)) <---- 0"
    using kingman_theorem_L1_aux[OF ‹subcocycle v› ‹subcocycle_avg_ereal v > -∞› ‹∧x. v 1 x ≤ 0›] by auto
  have w: "AE x in M. (λn. w n x / n) <---- subcocycle_lim w x"
            "integrable M (subcocycle_lim w)"
            "(λn. (∫⁺x. abs(w n x / n - subcocycle_lim w x) ∂M)) <---- 0"
  proof -
    show "AE x in M. (λn. w n x / n) <---- subcocycle_lim w x"
      unfolding w_def subcocycle_lim_def using subcocycle_lim_ereal_birkhoff[OF int_u]
      birkhoff_theorem_AE_nonergodic[OF int_u] by auto
    show "integrable M (subcocycle_lim w)"
      apply (subst integrable_cong_AE[where ?g = "λx. real_cond_exp M Invariants (u 1) x"])
      unfolding w_def subcocycle_lim_def
      using subcocycle_lim_ereal_birkhoff[OF int_u] real_cond_exp_int(1)[OF int_u] by auto
    have "(∫⁺x. abs(w n x / n - subcocycle_lim w x) ∂M)
        = (∫⁺x. abs(birkhoff_sum (u 1) n x / n - real_cond_exp M Invariants (u 1) x) ∂M)" for n
      apply (rule nn_integral_cong_AE)
      unfolding w_def subcocycle_lim_def using subcocycle_lim_ereal_birkhoff[OF int_u] by auto
    then show "(λn. (∫⁺x. abs(w n x / n - subcocycle_lim w x) ∂M)) <---- 0"
      using birkhoff_theorem_L1_nonergodic[OF int_u] by auto
  qed

  {
    fix x assume H: "(λn. v n x / n) <---- subcocycle_lim v x"
                    "(λn. w n x / n) <---- subcocycle_lim w x"
                    "(λn. u n x / n) <---- subcocycle_lim_ereal u x"
    then have "(λn. v n x / n + w n x / n) <---- subcocycle_lim v x + subcocycle_lim w x"
      using tendsto_add[OF H(1) H(2)] by simp
    then have *: "(λn. ereal(u n x / n)) <---- ereal(subcocycle_lim v x + subcocycle_lim w x)"
      unfolding uvw by (simp add: add_divide_distrib)
    then have "subcocycle_lim_ereal u x = ereal(subcocycle_lim v x + subcocycle_lim w x)"
      using H(3) LIMSEQ_unique by blast
    then have **: "subcocycle_lim u x = subcocycle_lim v x + subcocycle_lim w x"
      using subcocycle_lim_def by auto
    have "u n x / n - subcocycle_lim u x = v n x / n - subcocycle_lim v x + w n x / n - subcocycle_lim w x" for n
      apply (subst **, subst uvw) using add_divide_distrib add.commute by auto
    then have "(λn. u n x / n) <---- subcocycle_lim u x
          ∧ subcocycle_lim u x = subcocycle_lim v x + subcocycle_lim w x
          ∧ (∀n. u n x / n - subcocycle_lim u x = v n x / n - subcocycle_lim v x + w n x / n - subcocycle_lim w x)"
      using * ** by auto
  }
  then have AE: "AE x in M. (λn. u n x / n) <---- subcocycle_lim u x"
                "AE x in M. subcocycle_lim u x = subcocycle_lim v x + subcocycle_lim w x"
                "AE x in M. ∀n. u n x / n - subcocycle_lim u x = v n x / n - subcocycle_lim v x + w n x / n - subcocycle_lim w x"
    using v(1) w(1) kingman_theorem_AE_nonergodic_ereal[OF assms(1)] by auto
  then show "AE x in M. (λn. u n x / n) <---- subcocycle_lim u x" by simp
  show "integrable M (subcocycle_lim u)"
    apply (subst integrable_cong_AE[where ?g = "λx. subcocycle_lim v x + subcocycle_lim w x"])
    by (auto simp add: AE(2) v(2) w(2))

  show "(λn. (∫⁺x. abs(u n x / n - subcocycle_lim u x) ∂M)) <---- 0"
  proof (rule tendsto_sandwich[where ?f = "λ_. 0"
    and ?h = "λn. (∫⁺x. abs(v n x / n - subcocycle_lim v x) ∂M) + (∫⁺x. abs(w n x / n - subcocycle_lim w x) ∂M)"], auto)
    {
      fix n
      have "(∫⁺x. abs(u n x / n - subcocycle_lim u x) ∂M)
        = (∫⁺x. abs((v n x / n - subcocycle_lim v x) + (w n x / n - subcocycle_lim w x)) ∂M)"
        apply (rule nn_integral_cong_AE) using AE(3) by auto
      also have "... ≤ (∫⁺x. ennreal(abs(v n x / n - subcocycle_lim v x)) + abs(w n x / n - subcocycle_lim w x) ∂M)"
        by (rule nn_integral_mono, auto simp add: ennreal_plus[symmetric] simp del: ennreal_plus)
      also have "... = (∫⁺x. abs(v n x / n - subcocycle_lim v x) ∂M) + (∫⁺x. abs(w n x / n - subcocycle_lim w x) ∂M)"
        by (rule nn_integral_add, auto, measurable)
      finally have "(∫⁺x. abs(u n x / n - subcocycle_lim u x) ∂M)
        ≤ (∫⁺x. abs(v n x / n - subcocycle_lim v x) ∂M) + (∫⁺x. abs(w n x / n - subcocycle_lim w x) ∂M)"
        using tendsto_sandwich by simp
    }
    then show "eventually (λn. (∫⁺x. abs(u n x / n - subcocycle_lim u x) ∂M)
        ≤ (∫⁺x. abs(v n x / n - subcocycle_lim v x) ∂M) + (∫⁺x. abs(w n x / n - subcocycle_lim w x) ∂M)) sequentially"
      by auto

    have "(λn. (∫⁺x. abs(v n x / n - subcocycle_lim v x) ∂M) + (∫⁺x. abs(w n x / n - subcocycle_lim w x) ∂M))
              <---- 0 + 0"
      by (rule tendsto_add[OF v(3) w(3)])
    then show "(λn. (∫⁺x. abs(v n x / n - subcocycle_lim v x) ∂M) + (∫⁺x. abs(w n x / n - subcocycle_lim w x) ∂M))
              <---- 0"
      by simp
  qed
qed

text ‹From the almost sure convergence, we can prove the basic properties of the (real)
  limit: relationship to the asymptotic average, behavior under sum, multiplication,
 , behavior for Birkhoff sums.›

lemma subcocycle_lim_avg:
  assumes "subcocycle u" "subcocycle_avg_ereal u > -∞"
  shows "(∫x. subcocycle_lim u x ∂M) = subcocycle_avg u"
proof -
  have H: "(λn. (∫⁺x. norm(u n x / n - subcocycle_lim u x) ∂M)) <---- 0"
          "integrable M (subcocycle_lim u)"
    using kingman_theorem_nonergodic[OF assms] by auto
  have "(λn. (∫x. u n x / n ∂M)) <---- (∫x. subcocycle_lim u x ∂M)"
    apply (rule tendsto_L1_int[OF _ H(2) H(1)]) using subcocycle_integrable[OF assms(1)] by auto
  then have "(λn. (∫x. u n x / n ∂M)) <---- ereal (∫x. subcocycle_lim u x ∂M)" by auto
  moreover have "(λn. (∫x. u n x / n ∂M)) <---- ereal (subcocycle_avg u)"
    using subcocycle_int_tendsto_avg[OF assms] by auto
  ultimately show ?thesis using LIMSEQ_unique by blast
qed

lemma subcocycle_lim_real_ereal:
  assumes "subcocycle u" "subcocycle_avg_ereal u > -∞"
  shows "AE x in M. subcocycle_lim_ereal u x = ereal(subcocycle_lim u x)"
proof -
  {
    fix x assume H: "(λn. u n x / n) <---- subcocycle_lim_ereal u x"
                    "(λn. u n x / n) <---- subcocycle_lim u x"
    then have "(λn. u n x / n) <---- ereal(subcocycle_lim u x)" by auto
    then have "subcocycle_lim_ereal u x = ereal(subcocycle_lim u x)"
      using H(1) LIMSEQ_unique by blast
  }
  then show ?thesis
    using kingman_theorem_AE_nonergodic_ereal[OF assms(1)] kingman_theorem_nonergodic(1)[OF assms] by auto
qed

lemma subcocycle_lim_add:
  assumes "subcocycle u" "subcocycle v" "subcocycle_avg_ereal u > -∞" "subcocycle_avg_ereal v > -∞"
  shows "subcocycle_avg_ereal (λn x. u n x + v n x) > - ∞"
        "AE x in M. subcocycle_lim (λn x. u n x + v n x) x = subcocycle_lim u x + subcocycle_lim v x"
proof -
  show *: "subcocycle_avg_ereal (λn x. u n x + v n x) > - ∞"
    using subcocycle_avg_add[OF assms(1) assms(2)] assms(3) assms(4) by auto
  have "AE x in M. (λn. (u n x + v n x)/n) <---- subcocycle_lim (λn x. u n x + v n x) x"
    by (rule kingman_theorem_nonergodic(1)[OF subcocycle_add[OF assms(1) assms(2)] *])
  moreover have "AE x in M. (λn. u n x / n) <---- subcocycle_lim u x"
    by (rule kingman_theorem_nonergodic[OF assms(1) assms(3)])
  moreover have "AE x in M. (λn. v n x / n) <---- subcocycle_lim v x"
    by (rule kingman_theorem_nonergodic[OF assms(2) assms(4)])
  moreover
  {
    fix x assume H: "(λn. (u n x + v n x)/n) <---- subcocycle_lim (λn x. u n x + v n x) x"
                    "(λn. u n x / n) <---- subcocycle_lim u x"
                    "(λn. v n x / n) <---- subcocycle_lim v x"
    have *: "(u n x + v n x)/n = (u n x / n) + (v n x / n)" for n
      by (simp add: add_divide_distrib)
    have "(λn. (u n x + v n x)/n) <---- subcocycle_lim u x + subcocycle_lim v x"
      unfolding * by (intro tendsto_intros H)
    then have "subcocycle_lim (λn x. u n x + v n x) x = subcocycle_lim u x + subcocycle_lim v x"
      using H(1) by (simp add: LIMSEQ_unique)
  }
  ultimately show "AE x in M. subcocycle_lim (λn x. u n x + v n x) x
                    = subcocycle_lim u x + subcocycle_lim v x"
    by auto
qed

lemma subcocycle_lim_cmult:
  assumes "subcocycle u" "subcocycle_avg_ereal u > -∞" "c≥(0::real)"
  shows "subcocycle_avg_ereal (λn x. c * u n x) > - ∞"
        "AE x in M. subcocycle_lim (λn x. c * u n x) x = c * subcocycle_lim u x"
proof -
  show *: "subcocycle_avg_ereal (λn x. c * u n x) > - ∞"
    using subcocycle_avg_cmult[OF assms(1) assms(3)] assms(2) assms(3) by auto

  have "AE x in M. (λn. (c * u n x)/n) <---- subcocycle_lim (λn x. c * u n x) x"
    by (rule kingman_theorem_nonergodic(1)[OF subcocycle_cmult[OF assms(1) assms(3)] *])
  moreover have "AE x in M. (λn. u n x / n) <---- subcocycle_lim u x"
    by (rule kingman_theorem_nonergodic(1)[OF assms(1) assms(2)])
  moreover
  {
    fix x assume H: "(λn. (c * u n x)/n) <---- subcocycle_lim (λn x. c * u n x) x"
                    "(λn. u n x / n) <---- subcocycle_lim u x"
    have "(λn. c * (u n x / n)) <---- c * subcocycle_lim u x"
      by (rule tendsto_mult[OF _ H(2)], auto)
    then have "subcocycle_lim (λn x. c * u n x) x = c * subcocycle_lim u x"
      using H(1) by (simp add: LIMSEQ_unique)
  }
  ultimately show "AE x in M. subcocycle_lim (λn x. c * u n x) x = c * subcocycle_lim u x" by auto
qed

lemma subcocycle_lim_max:
  assumes "subcocycle u" "subcocycle v" "subcocycle_avg_ereal u > -∞" "subcocycle_avg_ereal v > -∞"
  shows "subcocycle_avg_ereal (λn x. max (u n x) (v n x)) > - ∞"
        "AE x in M. subcocycle_lim (λn x. max (u n x) (v n x)) x = max (subcocycle_lim u x) (subcocycle_lim v x)"
proof -
  show *: "subcocycle_avg_ereal (λn x. max (u n x) (v n x)) > - ∞"
    using subcocycle_avg_max(1)[OF assms(1) assms(2)] assms(3) assms(4) by auto
  have "AE x in M. (λn. max (u n x) (v n x) / n) <---- subcocycle_lim (λn x. max (u n x) (v n x)) x"
    by (rule kingman_theorem_nonergodic[OF subcocycle_max[OF assms(1) assms(2)] *])
  moreover have "AE x in M. (λn. u n x / n) <---- subcocycle_lim u x"
    by (rule kingman_theorem_nonergodic[OF assms(1) assms(3)])
  moreover have "AE x in M. (λn. v n x / n) <---- subcocycle_lim v x"
    by (rule kingman_theorem_nonergodic[OF assms(2) assms(4)])
  moreover
  {
    fix x assume H: "(λn. max (u n x) (v n x) / n) <---- subcocycle_lim (λn x. max (u n x) (v n x)) x"
                    "(λn. u n x / n) <---- subcocycle_lim u x"
                    "(λn. v n x / n) <---- subcocycle_lim v x"
    have "(λn. max (u n x / n) (v n x / n)) <---- max (subcocycle_lim u x) (subcocycle_lim v x)"
      apply (rule tendsto_max) using H by auto
    moreover have "max (u n x / n) (v n x / n) = max (u n x) (v n x) / n" for n
      by (simp add: max_divide_distrib_right)
    ultimately have "(λn. max (u n x) (v n x) / n) <---- max (subcocycle_lim u x) (subcocycle_lim v x)"
      by auto
    then have "subcocycle_lim (λn x. max (u n x) (v n x)) x = max (subcocycle_lim u x) (subcocycle_lim v x)"
      using H(1) by (simp add: LIMSEQ_unique)
  }
  ultimately show "AE x in M. subcocycle_lim (λn x. max (u n x) (v n x)) x
                    = max (subcocycle_lim u x) (subcocycle_lim v x)" by auto
qed

lemma subcocycle_lim_birkhoff:
  assumes "integrable M u"
  shows "subcocycle_avg_ereal (birkhoff_sum u) > -∞"
        "AE x in M. subcocycle_lim (birkhoff_sum u) x = real_cond_exp M Invariants u x"
proof -
  show *: "subcocycle_avg_ereal (birkhoff_sum u) > -∞"
    using subcocycle_avg_birkhoff[OF assms] by auto
  have "AE x in M. (λn. birkhoff_sum u n x / n) <---- real_cond_exp M Invariants u x"
    by (rule birkhoff_theorem_AE_nonergodic[OF assms])
  moreover have "AE x in M. (λn. birkhoff_sum u n x / n) <---- subcocycle_lim (birkhoff_sum u) x"
    by (rule kingman_theorem_nonergodic(1)[OF subcocycle_birkhoff[OF assms] *])
  moreover
  {
    fix x assume H: "(λn. birkhoff_sum u n x / n) <---- real_cond_exp M Invariants u x"
                    "(λn. birkhoff_sum u n x / n) <---- subcocycle_lim (birkhoff_sum u) x"
    then have "subcocycle_lim (birkhoff_sum u) x = real_cond_exp M Invariants u x"
      using H(2) by (simp add: LIMSEQ_unique)
  }
  ultimately show "AE x in M. subcocycle_lim (birkhoff_sum u) x = real_cond_exp M Invariants u x" by auto
qed


subsection ‹Conditional expectations of subcocycles›

text ‹In this subsection, we show that the conditional expectations of a subcocycle
 with respect to the invariant subalgebra) also converge, with the same limit as the
 .

  that the conditional expectation of a subcocycle $u$ is still a subcocycle, with the
  average at each step so with the same asymptotic average. Kingman theorem can be applied to
 , and what we have to show is that the limit of this subcocycle is the same as the limit
  the original subcocycle.

  the asymptotic average is $>-\infty$, both limits have the same integral, and moreover
  domination of the subcocycle by the Birkhoff sums of $u_n$ for fixed $n$
 which converge to the conditional expectation of $u_n$) implies that one limit is smaller than
  other. Hence, they coincide almost everywhere.

  case when the asymptotic average is $-\infty$ is deduced from the previous one by truncation.
 ›

text ‹First, we prove the result when the asymptotic average with finite.›

theorem kingman_theorem_nonergodic_invariant:
  assumes "subcocycle u" "subcocycle_avg_ereal u > -∞"
  shows "AE x in M. (λn. real_cond_exp M Invariants (u n) x / n) <---- subcocycle_lim u x"
        "(λn. (∫⁺x. abs(real_cond_exp M Invariants (u n) x / n - subcocycle_lim u x) ∂M)) <---- 0"
proof -
  have int [simp]: "integrable M (u n)" for n using subcocycle_integrable[OF assms(1)] by auto
  then have int2: "integrable M (real_cond_exp M Invariants (u n))" for n using real_cond_exp_int by auto
  {
    fix n m
    have "u (n+m) x ≤ u n x + u m ((T^^n) x)" for x
      using subcocycle_ineq[OF assms(1)] by auto
    have "AE x in M. real_cond_exp M Invariants (u (n+m)) x ≤ real_cond_exp M Invariants (λx. u n x + u m ((T^^n) x)) x"
      apply (rule real_cond_exp_mono)
      using subcocycle_ineq[OF assms(1)] apply auto
      by (rule Bochner_Integration.integrable_add, auto simp add: Tn_integral_preserving)
    moreover have "AE x in M. real_cond_exp M Invariants (λx. u n x + u m ((T^^n) x)) x
              = real_cond_exp M Invariants (u n) x + real_cond_exp M Invariants (λx. u m ((T^^n) x)) x"
      by (rule real_cond_exp_add, auto simp add: Tn_integral_preserving)
    moreover have "AE x in M. real_cond_exp M Invariants (u m ∘ ((T^^n))) x = real_cond_exp M Invariants (u m) x"
      by (rule Invariants_of_foTn, simp)
    moreover have "AE x in M. real_cond_exp M Invariants (u m) x = real_cond_exp M Invariants (u m) ((T^^n) x)"
      using Invariants_func_is_invariant_n[symmetric, of "real_cond_exp M Invariants (u m)"] by auto
    ultimately have "AE x in M. real_cond_exp M Invariants (u (n+m)) x
        ≤ real_cond_exp M Invariants (u n) x + real_cond_exp M Invariants (u m) ((T^^n) x)"
      unfolding o_def by auto
  }
  with subcocycle_AE[OF this int2]
  obtain w where w: "subcocycle w" "AE x in M. ∀n. w n x = real_cond_exp M Invariants (u n) x"
    by blast
  have [measurable]: "integrable M (w n)" for n using subcocycle_integrable[OF w(1)] by simp

  {
    fix n::nat
    have "(∫x. w n x / n ∂M) = (∫x. real_cond_exp M Invariants (u n) x / n ∂M)"
      using w(2) by (intro integral_cong_AE)  (auto simp: eventually_mono)
    also have "... = (∫x. real_cond_exp M Invariants (u n) x ∂M) / n"
      by (rule integral_divide_zero)
    also have "... = (∫x. u n x ∂M) / n"
      by (simp add: divide_simps real_cond_exp_int(2)[OF int[of n]])
    also have "... = (∫x. u n x / n ∂M)"
      by (rule integral_divide_zero[symmetric])
    finally have "ereal (∫x. w n x / n ∂M) = ereal (∫x. u n x / n ∂M)" by simp
  } note * = this
  have "(λn. (∫x. u n x / n ∂M)) <---- subcocycle_avg_ereal w"
    apply (rule Lim_transform_eventually[OF subcocycle_int_tendsto_avg_ereal[OF w(1)]])
    using * by auto
  then have "subcocycle_avg_ereal u = subcocycle_avg_ereal w"
    using subcocycle_int_tendsto_avg_ereal[OF assms(1)] LIMSEQ_unique by auto
  then have "subcocycle_avg_ereal w > -∞" using assms(2) by simp
  have "subcocycle_avg u = subcocycle_avg w"
    using ‹subcocycle_avg_ereal u = subcocycle_avg_ereal w› unfolding subcocycle_avg_def by simp

  have "AE x in M. N > 0 ⟶ subcocycle_lim_ereal u x ≤ real_cond_exp M Invariants (λx. u N x / N) x" for N
    by (cases "N = 0", auto simp add: subcocycle_lim_ereal_atmost_uN_invariants[OF assms(1)])
  then have "AE x in M. ∀N. N > 0 ⟶ subcocycle_lim_ereal u x ≤ real_cond_exp M Invariants (λx. u N x / N) x"
    by (simp add: AE_all_countable)
  moreover have "AE x in M. subcocycle_lim_ereal u x = ereal(subcocycle_lim u x)"
    by (rule subcocycle_lim_real_ereal[OF assms])
  moreover have "AE x in M. (λN. u N x / N) <---- subcocycle_lim u x"
    using kingman_theorem_nonergodic[OF assms] by simp
  moreover have "AE x in M. (λN. w N x / N) <---- subcocycle_lim w x"
    using kingman_theorem_nonergodic[OF w(1) ‹subcocycle_avg_ereal w > -∞› ] by simp
  moreover have "AE x in M. ∀n. w n x = real_cond_exp M Invariants (u n) x"
    using w(2) by simp
  moreover have "AE x in M. ∀n. real_cond_exp M Invariants (u n) x / n = real_cond_exp M Invariants (λx. u n x / n) x"
    apply (subst AE_all_countable, intro allI) using AE_symmetric[OF real_cond_exp_cdiv[OF int]] by auto
  moreover
  {
    fix x assume x: "∀N. N > 0 ⟶ subcocycle_lim_ereal u x ≤ real_cond_exp M Invariants (λx. u N x / N) x"
                    "subcocycle_lim_ereal u x = ereal(subcocycle_lim u x)"
                    "(λN. u N x / N) <---- subcocycle_lim u x"
                    "(λN. w N x / N) <---- subcocycle_lim w x"
                    "∀n. w n x = real_cond_exp M Invariants (u n) x"
                    "∀n. real_cond_exp M Invariants (u n) x / n = real_cond_exp M Invariants (λx. u n x / n) x"
    {
      fix N::nat assume "N≥1"
      have "subcocycle_lim u x ≤ real_cond_exp M Invariants (λx. u N x / N) x"
        using x(1) x(2) ‹N≥1› by auto
      also have "... = real_cond_exp M Invariants (u N) x / N"
        using x(6) by simp
      also have "... = w N x / N"
        using x(5) by simp
      finally have "subcocycle_lim u x ≤ w N x / N"
        by simp
    } note * = this
    have "subcocycle_lim u x ≤ subcocycle_lim w x"
      apply (rule LIMSEQ_le_const[OF x(4)]) using * by auto
  }
  ultimately have *: "AE x in M. subcocycle_lim u x ≤ subcocycle_lim w x"
    by auto
  have **: "(∫x. subcocycle_lim u x ∂M) = (∫x. subcocycle_lim w x ∂M)"
    using subcocycle_lim_avg[OF assms] subcocycle_lim_avg[OF w(1) ‹subcocycle_avg_ereal w > -∞›]
            ‹subcocycle_avg u = subcocycle_avg w› by simp
  have AE_eq: "AE x in M. subcocycle_lim u x = subcocycle_lim w x"
    by (rule integral_ineq_eq_0_then_AE[OF * kingman_theorem_nonergodic(2)[OF assms]
        kingman_theorem_nonergodic(2)[OF w(1) ‹subcocycle_avg_ereal w > -∞›] **])
  moreover have "AE x in M. (λn. w n x / n) <---- subcocycle_lim w x"
    by (rule kingman_theorem_nonergodic(1)[OF w(1) ‹subcocycle_avg_ereal w > -∞›])
  moreover have "AE x in M. ∀n. w n x = real_cond_exp M Invariants (u n) x"
    using w(2) by auto
  moreover
  {
    fix x assume H: "subcocycle_lim u x = subcocycle_lim w x"
                    "(λn. w n x / n) <---- subcocycle_lim w x"
                    "∀n. w n x = real_cond_exp M Invariants (u n) x"
    then have "(λn. real_cond_exp M Invariants (u n) x / n) <---- subcocycle_lim u x"
      by auto
  }
  ultimately show "AE x in M. (λn. real_cond_exp M Invariants (u n) x / n) <---- subcocycle_lim u x"
    by auto

  {
    fix n::nat
    have "AE x in M. subcocycle_lim u x = subcocycle_lim w x"
      using AE_eq by simp
    moreover have "AE x in M. w n x = real_cond_exp M Invariants (u n) x"
      using w(2) by auto
    moreover
    {
      fix x assume H: "subcocycle_lim u x = subcocycle_lim w x"
                    "w n x = real_cond_exp M Invariants (u n) x"
      then have "ennreal ∣real_cond_exp M Invariants (u n) x / real n - subcocycle_lim u x∣
                = ennreal ∣w n x / real n - subcocycle_lim w x∣"
      by auto
    }
    ultimately have "AE x in M. ennreal ∣real_cond_exp M Invariants (u n) x / real n - subcocycle_lim u x∣
        = ennreal ∣w n x / real n - subcocycle_lim w x∣"
      by auto
    then have "(∫⁺ x. ennreal ∣real_cond_exp M Invariants (u n) x / real n - subcocycle_lim u x∣ ∂M)
              = (∫⁺ x. ennreal ∣w n x / real n - subcocycle_lim w x∣ ∂M)"
      by (rule nn_integral_cong_AE)
  }
  moreover have "(λn. (∫⁺ x. ∣w n x / real n - subcocycle_lim w x∣ ∂M)) <---- 0"
    by (rule kingman_theorem_nonergodic(3)[OF w(1) ‹subcocycle_avg_ereal w > -∞›])
  ultimately show "(λn. (∫⁺ x. ∣real_cond_exp M Invariants (u n) x / real n - subcocycle_lim u x∣ ∂M)) <---- 0"
    by auto
qed

text ‹Then, we extend it by truncation to the general case, i.e., to the asymptotic
  in extended reals.›

theorem kingman_theorem_AE_nonergodic_invariant_ereal:
  assumes "subcocycle u"
  shows "AE x in M. (λn. real_cond_exp M Invariants (u n) x / n) <---- subcocycle_lim_ereal u x"
proof -
  have [simp]: "subcocycle u" using assms by simp
  have int [simp]: "integrable M (u n)" for n using subcocycle_integrable[OF assms(1)] by auto

  have limsup_ineq_K: "AE x in M.
    limsup (λn. real_cond_exp M Invariants (u n) x / n) ≤ max (subcocycle_lim_ereal u x) (-real K)" for K::nat
  proof -
    define v where "v = (λ (n::nat) (x::'a). (-n * real K))"
    have [simp]: "subcocycle v"
      unfolding v_def subcocycle_def by (auto simp add: algebra_simps)
    have "ereal (∫x. v n x / n ∂M) = ereal(- real K * measure M (space M))" if "n≥1" for n
      unfolding v_def using that by simp
    then have "(λn. ereal (∫x. v n x / n ∂M)) <---- ereal(- real K * measure M (space M))"
      using lim_explicit by force
    moreover have "(λn. ereal (∫x. v n x / n ∂M)) <---- subcocycle_avg_ereal v"
      using subcocycle_int_tendsto_avg_ereal[OF ‹subcocycle v›] by auto
    ultimately have "subcocycle_avg_ereal v = - real K * measure M (space M)"
      using LIMSEQ_unique by blast
    then have "subcocycle_avg_ereal v > -∞"
      by auto

    {
      fix x assume H: "(λn. v n x / n) <---- subcocycle_lim_ereal v x"
      have "ereal(v n x / n) = -real K" if "n≥1" for n
        unfolding v_def using that by auto
      then have "(λn. ereal(v n x / n)) <---- - real K"
        using lim_explicit by force
      then have "subcocycle_lim_ereal v x = -real K"
        using H LIMSEQ_unique by blast
    }
    then have "AE x in M. subcocycle_lim_ereal v x = -real K"
      using kingman_theorem_AE_nonergodic_ereal[OF ‹subcocycle v›] by auto

    define w where "w = (λn x. max (u n x) (v n x))"
    have [simp]: "subcocycle w"
      unfolding w_def by (rule subcocycle_max, auto)
    have "subcocycle_avg_ereal w ≥ subcocycle_avg_ereal v"
      unfolding w_def using subcocycle_avg_ereal_max by auto
    then have "subcocycle_avg_ereal w > -∞"
      using ‹subcocycle_avg_ereal v > -∞› by auto

    have *: "AE x in M. real_cond_exp M Invariants (u n) x ≤ real_cond_exp M Invariants (w n) x" for n
      apply (rule real_cond_exp_mono)
      using subcocycle_integrable[OF assms, of n] subcocycle_integrable[OF ‹subcocycle w›, of n] apply auto
      unfolding w_def by auto
    have "AE x in M. ∀n. real_cond_exp M Invariants (u n) x ≤ real_cond_exp M Invariants (w n) x"
      apply (subst AE_all_countable) using * by auto
    moreover have "AE x in M. (λn. real_cond_exp M Invariants (w n) x / n) <---- subcocycle_lim w x"
      apply (rule kingman_theorem_nonergodic_invariant(1))
      using ‹subcocycle_avg_ereal w > -∞› by auto
    moreover have "AE x in M. subcocycle_lim_ereal w x = max (subcocycle_lim_ereal u x) (subcocycle_lim_ereal v x)"
      unfolding w_def using subcocycle_lim_ereal_max by auto
    moreover
    {
      fix x assume H: "(λn. real_cond_exp M Invariants (w n) x / n) <---- subcocycle_lim w x"
                      "subcocycle_lim_ereal w x = max (subcocycle_lim_ereal u x) (subcocycle_lim_ereal v x)"
                      "subcocycle_lim_ereal v x = - real K"
                      "∀n. real_cond_exp M Invariants (u n) x ≤ real_cond_exp M Invariants (w n) x"
      have "subcocycle_lim_ereal w x > -∞"
        using H(2) H(3)
        by auto (metis MInfty_neq_ereal(1) ereal_infty_less_eq2(2) max.cobounded2)
      then have "subcocycle_lim_ereal w x = ereal(subcocycle_lim w x)"
        unfolding subcocycle_lim_def using subcocycle_lim_ereal_not_PInf[of w x] ereal_real by force
      moreover have "(λn. real_cond_exp M Invariants (w n) x / n) <---- ereal(subcocycle_lim w x)" using H(1) by auto
      ultimately have "(λn. real_cond_exp M Invariants (w n) x / n) <---- subcocycle_lim_ereal w x" by auto
      then have *: "limsup (λn. real_cond_exp M Invariants (w n) x / n) = subcocycle_lim_ereal w x"
        using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast

      have "ereal(real_cond_exp M Invariants (u n) x / n) ≤ real_cond_exp M Invariants (w n) x / n" for n
        using H(4) by (auto simp add: divide_simps)
      then have "eventually (λn. ereal(real_cond_exp M Invariants (u n) x / n) ≤ real_cond_exp M Invariants (w n) x / n) sequentially"
        by auto
      then have "limsup (λn. real_cond_exp M Invariants (u n) x / n) ≤ limsup (λn. real_cond_exp M Invariants (w n) x / n)"
        using Limsup_mono[of _ _ sequentially] by force
      then have "limsup (λn. real_cond_exp M Invariants (u n) x / n) ≤ max (subcocycle_lim_ereal u x) (-real K)"
        using * H(2) H(3) by auto
    }
    ultimately show ?thesis using ‹AE x in M. subcocycle_lim_ereal v x = -real K› by auto
  qed
  have "AE x in M. ∀K::nat.
        limsup (λn. real_cond_exp M Invariants (u n) x / n) ≤ max (subcocycle_lim_ereal u x) (-real K)"
    apply (subst AE_all_countable) using limsup_ineq_K by auto

  moreover have "AE x in M. liminf (λn. real_cond_exp M Invariants (u n) x / n) ≥ subcocycle_lim_ereal u x"
  proof -
    have "AE x in M. N > 0 ⟶ subcocycle_lim_ereal u x ≤ real_cond_exp M Invariants (λx. u N x / N) x" for N
      by (cases "N = 0", auto simp add: subcocycle_lim_ereal_atmost_uN_invariants[OF assms(1)])
    then have "AE x in M. ∀N. N > 0 ⟶ subcocycle_lim_ereal u x ≤ real_cond_exp M Invariants (λx. u N x / N) x"
      by (simp add: AE_all_countable)
    moreover have "AE x in M. ∀n. real_cond_exp M Invariants (λx. u n x / n) x = real_cond_exp M Invariants (u n) x / n"
      apply (subst AE_all_countable, intro allI) using real_cond_exp_cdiv by auto
    moreover
    {
      fix x assume x: "∀N. N > 0 ⟶ subcocycle_lim_ereal u x ≤ real_cond_exp M Invariants (λx. u N x / N) x"
                      "∀n. real_cond_exp M Invariants (λx. u n x / n) x = real_cond_exp M Invariants (u n) x / n"
      then have *: "subcocycle_lim_ereal u x ≤ real_cond_exp M Invariants (u n) x / n" if "n ≥ 1" for n
        using that by auto
      have "subcocycle_lim_ereal u x ≤ liminf (λn. real_cond_exp M Invariants (u n) x / n)"
        apply (subst liminf_bounded_iff) using * less_le_trans by blast
    }
    ultimately show ?thesis by auto
  qed

  moreover
  {
    fix x assume H: "∀K::nat. limsup (λn. real_cond_exp M Invariants (u n) x / n)
                              ≤ max (subcocycle_lim_ereal u x) (-real K)"
                    "liminf (λn. real_cond_exp M Invariants (u n) x / n) ≥ subcocycle_lim_ereal u x"
    have "(λK::nat. max (subcocycle_lim_ereal u x) (-real K)) <---- subcocycle_lim_ereal u x"
      by (rule ereal_truncation_bottom)
    with LIMSEQ_le_const[OF this]
    have *: "limsup (λn. real_cond_exp M Invariants (u n) x / n) ≤ subcocycle_lim_ereal u x"
      using H(1) by auto
    have "(λn. real_cond_exp M Invariants (u n) x / n) <---- subcocycle_lim_ereal u x"
      apply (subst tendsto_iff_Liminf_eq_Limsup[OF trivial_limit_at_top_linorder])
      using H(2) * Liminf_le_Limsup[OF trivial_limit_at_top_linorder, of "(λn. real_cond_exp M Invariants (u n) x / n)"]
      by auto
  }
  ultimately show ?thesis by auto
qed



end

subsection ‹Subcocycles in the ergodic case›

text ‹In this subsection, we describe how all the previous results simplify in the ergodic case.
 , subcocycle limits are almost surely constant, given by the asymptotic average.›

context ergodic_pmpt begin

lemma subcocycle_ergodic_lim_avg:
  assumes "subcocycle u"
  shows "AE x in M. subcocycle_lim_ereal u x = subcocycle_avg_ereal u"
        "AE x in M. subcocycle_lim u x = subcocycle_avg u"
proof -
  have I: "integrable M (u N)" for N using subcocycle_integrable[OF assms]by auto
  obtain c::ereal where c: "AE x in M. subcocycle_lim_ereal u x = c"
    using Invariant_func_is_AE_constant[OF subcocycle_lim_meas_Inv(1)] by blast
  have "c = subcocycle_avg_ereal u"
  proof (cases "subcocycle_avg_ereal u = - ∞")
    case True
    {
      fix N assume "N > (0::nat)"
      have "AE x in M. real_cond_exp M Invariants (λx. u N x / N) x = (∫ x. u N x / N ∂M)"
        apply (rule Invariants_cond_exp_is_integral) using I by auto
      moreover have "AE x in M. subcocycle_lim_ereal u x ≤ real_cond_exp M Invariants (λx. u N x / N) x"
        using subcocycle_lim_ereal_atmost_uN_invariants[OF assms ‹N>0›] by simp
      ultimately have "AE x in M. c ≤ (∫x. u N x / N ∂M)"
        using c by force
      then have "c ≤ (∫x. u N x / N ∂M)" by auto
    }
    then have "∀N≥1. c ≤ (∫x. u N x / N ∂M)" by auto
    with Lim_bounded2[OF subcocycle_int_tendsto_avg_ereal[OF assms] this]
    have "c ≤ subcocycle_avg_ereal u" by simp
    then show ?thesis using True by auto
  next
    case False
    then have fin: "subcocycle_avg_ereal u > - ∞" by simp
    obtain cr::real where cr: "AE x in M. subcocycle_lim u x = cr"
      using Invariant_func_is_AE_constant[OF subcocycle_lim_meas_Inv(2)] by blast
    have "AE x in M. c = ereal cr" using c cr subcocycle_lim_real_ereal[OF assms fin] by force
    then have "c = ereal cr" by auto
    have "subcocycle_avg u = (∫x. subcocycle_lim u x ∂M)"
      using subcocycle_lim_avg[OF assms fin] by auto
    also have "... = (∫x. cr ∂M)"
      apply (rule integral_cong_AE) using cr by auto
    also have "... = cr"
      by (simp add: prob_space.prob_space prob_space_axioms)
    finally have "ereal(subcocycle_avg u) = ereal cr" by simp
    then show ?thesis using ‹ c = ereal cr › subcocycle_avg_real_ereal[OF fin] by auto
  qed
  then show "AE x in M. subcocycle_lim_ereal u x = subcocycle_avg_ereal u" using c by auto
  then show "AE x in M. subcocycle_lim u x = subcocycle_avg u"
    unfolding subcocycle_lim_def subcocycle_avg_def by auto
qed

theorem kingman_theorem_AE_ereal:
  assumes "subcocycle u"
  shows "AE x in M. (λn. u n x / n) <---- subcocycle_avg_ereal u"
using kingman_theorem_AE_nonergodic_ereal[OF assms] subcocycle_ergodic_lim_avg(1)[OF assms] by auto

theorem kingman_theorem:
  assumes "subcocycle u" "subcocycle_avg_ereal u > -∞"
  shows "AE x in M. (λn. u n x / n) <---- subcocycle_avg u"
        "(λn. (∫⁺x. abs(u n x / n - subcocycle_avg u) ∂M)) <---- 0"
proof -
  have *: "AE x in M. subcocycle_lim u x = subcocycle_avg u"
    using subcocycle_ergodic_lim_avg(2)[OF assms(1)] by auto
  then show "AE x in M. (λn. u n x / n) <---- subcocycle_avg u"
    using kingman_theorem_nonergodic(1)[OF assms] by auto
  have "(∫⁺x. abs(u n x / n - subcocycle_avg u) ∂M) = (∫⁺x. abs(u n x / n - subcocycle_lim u x) ∂M)" for n
    apply (rule nn_integral_cong_AE) using * by auto
  then show "(λn. (∫⁺x. abs(u n x / n - subcocycle_avg u) ∂M)) <---- 0"
    using kingman_theorem_nonergodic(3)[OF assms] by auto
qed

end


subsection ‹Subocycles for invertible maps›

text ‹If $T$ is invertible, then a subcocycle $u_n$ for $T$ gives rise to another subcocycle
  $T^{-1}$. Intuitively, if $u$ is subadditive along the time interval $[0,n)$, then
  should also be subadditive along the time interval $[-n,0)$. This is true, and
  with the following statement.›

proposition (in mpt) subcocycle_u_Tinv:
  assumes "subcocycle u"
          "invertible_qmpt"
  shows "mpt.subcocycle M Tinv (λn x. u n (((Tinv)^^n) x))"
proof -
  have bij: "bij T" using ‹invertible_qmpt› unfolding invertible_qmpt_def by auto
  have int: "integrable M (u n)" for n
    using subcocycle_integrable[OF assms(1)] by simp
  interpret I: mpt M Tinv using Tinv_mpt[OF assms(2)] by simp
  show "I.subcocycle (λn x. u n (((Tinv)^^n) x))" unfolding I.subcocycle_def
  proof(auto)
    show "integrable M (λx. u n ((Tinv ^^ n) x))" for n
      using I.Tn_integral_preserving(1)[OF int[of n]] by simp
    fix n m::nat and x::'a
    define y where "y = (Tinv^^(m+n)) x"
    have "(T^^m) y = (T^^m) ((Tinv^^m) ((Tinv^^n) x))" unfolding y_def by (simp add: funpow_add)
    then have *: "(T^^m) y = (Tinv^^n) x"
      using fn_o_inv_fn_is_id[OF bij, of m] by (metis Tinv_def comp_def)
    have "u (n + m) ((Tinv ^^ (n + m)) x) = u (m+n) y"
      unfolding y_def by (simp add: add.commute[of n m])
    also have "... ≤ u m y + u n ((T^^m) y)"
      using subcocycle_ineq[OF ‹subcocycle u›, of m n y] by simp
    also have "... = u m ((Tinv^^(m+n)) x) + u n ((Tinv^^n) x)"
      using * y_def by auto
    finally show "u (n + m) ((Tinv ^^ (n + m)) x) ≤ u n ((Tinv ^^ n) x) + u m ((Tinv ^^ m) ((Tinv ^^ n) x))"
      by (simp add: funpow_add)
  qed
qed

text ‹The subcocycle averages for $T$ and $T^{-1}$ coincide.›

proposition (in mpt) subcocycle_avg_ereal_Tinv:
  assumes "subcocycle u"
          "invertible_qmpt"
  shows "mpt.subcocycle_avg_ereal M (λn x. u n (((Tinv)^^n) x)) = subcocycle_avg_ereal u"
proof -
  have bij: "bij T" using ‹invertible_qmpt› unfolding invertible_qmpt_def by auto
  have int: "integrable M (u n)" for n
    using subcocycle_integrable[OF assms(1)] by simp
  interpret I: mpt M Tinv using Tinv_mpt[OF assms(2)] by simp
  have "(λn. (∫x. u n (((Tinv)^^n) x) / n ∂M)) <---- I.subcocycle_avg_ereal (λn x. u n (((Tinv)^^n) x))"
    using I.subcocycle_int_tendsto_avg_ereal[OF subcocycle_u_Tinv[OF assms]] by simp
  moreover have "(∫x. u n x / n ∂M) = ereal (∫x. u n (((Tinv)^^n) x) / n ∂M)" for n
    apply (simp)
    apply (rule disjI2)
    apply (rule I.Tn_integral_preserving(2)[symmetric])
    apply (simp add: int)
    done
  ultimately have "(λn. (∫x. u n x / n ∂M)) <---- I.subcocycle_avg_ereal (λn x. u n (((Tinv)^^n) x))"
    by presburger
  moreover have "(λn. (∫x. u n x / n ∂M)) <---- subcocycle_avg_ereal u"
    using subcocycle_int_tendsto_avg_ereal[OF ‹subcocycle u›] by simp
  ultimately show ?thesis
    using LIMSEQ_unique by simp
qed

text ‹The asymptotic limit of the subcocycle is the same for $T$ and $T^{-1}$. This is clear in the
  case, and follows from the ergodic decomposition in the general case (on a standard
  space). We give a direct proof below (on a general probability space) using the fact
  the asymptotic limit is the same for the subcocycle conditioned by the invariant sigma-algebra,
  is clearly the same for $T$ and $T^{-1}$ as it is constant along orbits.›

proposition (in fmpt) subcocycle_lim_ereal_Tinv:
  assumes "subcocycle u"
          "invertible_qmpt"
  shows "AE x in M. fmpt.subcocycle_lim_ereal M Tinv (λn x. u n (((Tinv)^^n) x)) x = subcocycle_lim_ereal u x"
proof -
  have bij: "bij T" using ‹invertible_qmpt› unfolding invertible_qmpt_def by auto
  have int: "integrable M (u n)" for n
    using subcocycle_integrable[OF assms(1)] by simp
  interpret I: fmpt M Tinv using Tinv_fmpt[OF assms(2)] by simp
  have *: "AE x in M. real_cond_exp M I.Invariants (λ x. u n (((Tinv)^^n) x)) x
                  = real_cond_exp M I.Invariants (u n) x" for n
    using I.Invariants_of_foTn int unfolding o_def by simp
  then have "AE x in M. ∀n. real_cond_exp M I.Invariants (λ x. u n (((Tinv)^^n) x)) x
                  = real_cond_exp M I.Invariants (u n) x"
    by (simp add: AE_all_countable)
  moreover have "AE x in M. (λn. real_cond_exp M Invariants (u n) x / n) <---- subcocycle_lim_ereal u x"
    using kingman_theorem_AE_nonergodic_invariant_ereal[OF ‹subcocycle u›] by simp
  moreover have "AE x in M. (λn. real_cond_exp M I.Invariants (λ x. u n (((Tinv)^^n) x)) x / n)
          <---- I.subcocycle_lim_ereal (λ n x. u n (((Tinv)^^n) x)) x"
    using I.kingman_theorem_AE_nonergodic_invariant_ereal[OF subcocycle_u_Tinv[OF assms]] by simp
  moreover
  {
    fix x assume H: "∀n. real_cond_exp M I.Invariants (λ x. u n (((Tinv)^^n) x)) x
                      = real_cond_exp M I.Invariants (u n) x"
                    "(λn. real_cond_exp M Invariants (u n) x / n) <---- subcocycle_lim_ereal u x"
                    "(λn. real_cond_exp M I.Invariants (λ x. u n (((Tinv)^^n) x)) x / n)
                        <---- I.subcocycle_lim_ereal (λ n x. u n (((Tinv)^^n) x)) x"
    have "ereal(real_cond_exp M Invariants (u n) x / n)
          = ereal(real_cond_exp M I.Invariants (λ x. u n (((Tinv)^^n) x)) x / n)" for n
      using H(1) Invariants_Tinv[OF ‹invertible_qmpt›] by auto
    then have "(λn. real_cond_exp M Invariants (u n) x / n)
                <---- I.subcocycle_lim_ereal (λ n x. u n (((Tinv)^^n) x)) x"
      using H(3) by presburger
    then have "I.subcocycle_lim_ereal (λ n x. u n (((Tinv)^^n) x)) x = subcocycle_lim_ereal u x"
      using H(2) LIMSEQ_unique by auto
  }
  ultimately show ?thesis by auto
qed

proposition (in fmpt) subcocycle_lim_Tinv:
  assumes "subcocycle u"
          "invertible_qmpt"
  shows "AE x in M. fmpt.subcocycle_lim M Tinv (λn x. u n (((Tinv)^^n) x)) x = subcocycle_lim u x"
proof -
  interpret I: fmpt M Tinv using Tinv_fmpt[OF assms(2)] by simp
  show ?thesis
    unfolding subcocycle_lim_def I.subcocycle_lim_def
    using subcocycle_lim_ereal_Tinv[OF assms] by auto
qed

end (*of Kingman.thy*)