# Theory Kingman

theory Kingman
imports Ergodicity Fekete
(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
*)

theory Kingman
imports Ergodicity Fekete
begin

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

For instance, Birkhoff sums are examples of such subadditive cocycles (in fact, they are
of 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$,
then 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,
and $\max$.›

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
by 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
to the trivial upper bound for $u_1$, there are additional boundary errors that make the
estimate more cumbersome (but these terms only come from a $N$-neighborhood of $0$ and $n$, so
they 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"
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"
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›
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))"
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)))"
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)))"
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)"
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
subadditivity property only makes sense almost everywhere. We will now show
that such an a.e.-subcocycle coincides almost everywhere with a genuine subcocycle
in the above sense. Then, all the results for subcocycles will apply to such
a.e.-subcocycles. (Usually, in ergodic theory, subcocycles only satisfy the subadditivity
property almost everywhere, but we have requested it everywhere for simplicity in the proofs.)

The subcocycle will be defined in a recursive way. This means that is can not be defined in a
proof (since complicated function definitions are not available inside proofs). Since it is
defined in terms of $u$, then $u$ has to be available at the top level, which is most
conveniently 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 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 auto
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 (rule integrable_MIN, simp)
using ‹n >1› apply auto
using "1.IH" apply auto
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
limit of $\int u_n(x)/n$ (the convergence follows from subadditivity of $\int u_n$) and study its
basic 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

assumes "subcocycle u"
shows "subadditive (λn. (∫x. u n x ∂M))"
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

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

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)"
also have "... = (∫x. (u n x + v n x) / n ∂M)"
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)"
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
function, 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
definition is more convenient. The kind of statements we are after is as follows: if the
ereal average is finite, then something holds, likely involving the real average.

In particular, we show in this setting what we have proved above under this new assumption:
convergence (in real numbers) of the average to the asymptotic average, as well as good behavior
under 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

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"
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
subcocycles. Their limit is almost surely invariant. There is no really easy proof. The one we use
below is arguably the simplest known one, due to Steele (1989). The idea is to show that the limsup
of the subcocycle is bounded by the liminf (which is almost surely constant along trajectories), by
using subadditivity along time intervals where the liminf is almost reached, of length at most $N$.
For some points, the liminf takes a large time $>N$ to be reached. We neglect those times,
introducing an additional error that gets smaller with $N$, thanks to Birkhoff ergodic theorem
applied to the set of bad points. The error is most easily managed if the subcocycle is assumed to
be nonpositive, which one can assume in a first step. The general case is reduced to this one by
replacing $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)"
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)"
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 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

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)"
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))"
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
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"
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
the 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
to the invariant sigma algebra and does not come from a hard to use abstract existence statement.
Hence we introduce the following definition for the would-be limit -- Kingman's theorem shows that
it is indeed a limit.

We introduce the definition for any function, not only subcocycles, but it will only be usable for
subcocycles. We introduce an if clause in the definition so that the limit is always measurable,
even 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.
From this point on, the technical definition of \verb+subcocycle_lim_ereal+ will never be used, only
the 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,
max, and is simply the conditional expectation with respect to invariants for Birkhoff sums,
thanks to Birkhoff theorem.›

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"
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
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
also takes place in $L^1$ if the limit is integrable, i.e., if the asymptotic average
of the subcocycle is $> -\infty$. To deduce it from the almost sure convergence, we only need
to show that there is no loss of mass, i.e., that the integral of the limit is not
strictly larger than the limit of the integrals (thanks to Scheffe criterion). This follows
from comparison to Birkhoff sums, for which we know that the average of the limit is
the 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
Birkhoff 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"
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
with nonpositive functions after a change of sign. Hence, as in the proof of the almost
sure version of Kingman theorem above, we first give the proof assuming that the
subcocycle is nonpositive, and deduce the general statement by adding a suitable
Birkhoff 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)
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))"
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$
to 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)"
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
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)"
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"
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)
subcocycle limit: relationship to the asymptotic average, behavior under sum, multiplication,
max, 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

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
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
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
cocycle.

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

When the asymptotic average is $>-\infty$, both limits have the same integral, and moreover
the 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
the other. Hence, they coincide almost everywhere.

The 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
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"
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)"
apply (rule integral_cong_AE) using w(2) by auto
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)])
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 (subst AE_all_countable, intro allI, simp add: *)
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
limit 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) MInfty_neq_ereal(1) ereal_MInfty_lessI max.cobounded2 by fastforce
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)])
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 (subst AE_all_countable, intro allI, simp add: *)
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.
Indeed, 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"
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
for $T^{-1}$. Intuitively, if $u$ is subadditive along the time interval $[0,n)$, then
it should also be subadditive along the time interval $[-n,0)$. This is true, and
formalized 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"
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))"
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])
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
ergodic case, and follows from the ergodic decomposition in the general case (on a standard
probability space). We give a direct proof below (on a general probability space) using the fact
that the asymptotic limit is the same for the subcocycle conditioned by the invariant sigma-algebra,
which 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
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"
apply (subst AE_all_countable) using * by simp
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*)