# Theory Ergodicity

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

section ‹Ergodicity›

theory Ergodicity
imports Invariants
begin

text ‹A transformation is \emph{ergodic} if any invariant set has zero measure or full measure.
Ergodic transformations are, in a sense, extremal among measure preserving transformations.
Hence, any transformation can be seen as an average of ergodic ones. This can be made precise
by the notion of ergodic decomposition, only valid on standard measure spaces.

Many statements get nicer in the ergodic case, hence we will reformulate many
of the previous results in this setting.›

subsection ‹Ergodicity locales›

locale ergodic_qmpt = qmpt +
assumes ergodic: "⋀A. A ∈ sets Invariants ⟹ (A ∈ null_sets M ∨ space M - A ∈ null_sets M)"

locale ergodic_mpt = mpt + ergodic_qmpt

locale ergodic_fmpt = ergodic_qmpt + fmpt

locale ergodic_pmpt = ergodic_qmpt + pmpt

locale ergodic_conservative = ergodic_qmpt + conservative

locale ergodic_conservative_mpt = ergodic_qmpt + conservative_mpt

sublocale ergodic_fmpt ⊆ ergodic_mpt
by unfold_locales

sublocale ergodic_pmpt ⊆ ergodic_fmpt
by unfold_locales

sublocale ergodic_fmpt ⊆ ergodic_conservative_mpt
by unfold_locales

sublocale ergodic_conservative_mpt ⊆ ergodic_conservative
by unfold_locales

subsection ‹Behavior of sets in ergodic transformations›

text ‹The main property of an ergodic transformation, essentially equivalent to the definition,
is that a set which is almost invariant under the dynamics is null or conull.›

lemma (in ergodic_qmpt) AE_equal_preimage_then_null_or_conull:
assumes [measurable]: "A ∈ sets M" and "A Δ T--A ∈ null_sets M"
shows "A ∈ null_sets M ∨ space M - A ∈ null_sets M"
proof -
obtain B where B: "B ∈ sets Invariants" "A Δ B ∈ null_sets M"
by (metis Un_commute Invariants_quasi_Invariants_sets[OF assms(1)] assms(2))
have [measurable]: "B ∈ sets M" using B(1) using Invariants_in_sets by blast
have *: "B ∈ null_sets M ∨ space M - B ∈ null_sets M" using ergodic B(1) by blast
show ?thesis
proof (cases)
assume "B ∈ null_sets M"
then have "A ∈ null_sets M" by (metis Un_commute B(2) Delta_null_of_null_is_null[OF assms(1), where ?A = B])
then show ?thesis by simp
next
assume "¬(B ∈ null_sets M)"
then have i: "space M - B ∈ null_sets M" using * by simp
have "(space M - B) Δ (space M - A) = A Δ B"
using sets.sets_into_space[OF ‹A ∈ sets M›] sets.sets_into_space[OF ‹B ∈ sets M›] by blast
then have "(space M - B) Δ (space M - A) ∈ null_sets M" using B(2) by auto
then have "space M - A ∈ null_sets M"
using Delta_null_of_null_is_null[where ?A = "space M - B" and ?B = "space M - A"] i by auto
then show ?thesis by simp
qed
qed

text ‹The inverse of an ergodic transformation is also ergodic.›

lemma (in ergodic_qmpt) ergodic_Tinv:
assumes "invertible_qmpt"
shows "ergodic_qmpt M Tinv"
unfolding ergodic_qmpt_def ergodic_qmpt_axioms_def
proof
show "qmpt M Tinv" using Tinv_qmpt[OF assms] by simp
show "∀A. A ∈ sets (qmpt.Invariants M Tinv) ⟶ A ∈ null_sets M ∨ space M - A ∈ null_sets M"
proof (intro allI impI)
fix A assume "A ∈ sets (qmpt.Invariants M Tinv)"
then have "A ∈ sets Invariants" using Invariants_Tinv[OF assms] by simp
then show "A ∈ null_sets M ∨ space M - A ∈ null_sets M" using ergodic by auto
qed
qed

text ‹In the conservative case, instead of the almost invariance of a set, it suffices to
assume that the preimage is contained in the set, or contains the set, to deduce that it is null
or conull.›

lemma (in ergodic_conservative) preimage_included_then_null_or_conull:
assumes "A ∈ sets M" "T--A ⊆ A"
shows "A ∈ null_sets M ∨ space M - A ∈ null_sets M"
proof -
have "A Δ T--A ∈ null_sets M" using preimage_included_then_almost_invariant[OF assms] by auto
then show ?thesis using AE_equal_preimage_then_null_or_conull assms(1) by auto
qed

lemma (in ergodic_conservative) preimage_includes_then_null_or_conull:
assumes "A ∈ sets M" "T--A ⊇ A"
shows "A ∈ null_sets M ∨ space M - A ∈ null_sets M"
proof -
have "A Δ T--A ∈ null_sets M" using preimage_includes_then_almost_invariant[OF assms] by auto
then show ?thesis using AE_equal_preimage_then_null_or_conull assms(1) by auto
qed

lemma (in ergodic_conservative) preimages_conull:
assumes [measurable]: "A ∈ sets M" and "emeasure M A > 0"
shows "space M - (⋃n. (T^^n)--A) ∈ null_sets M"
"space M Δ (⋃n. (T^^n)--A) ∈ null_sets M"
proof -
define B where "B = (⋃n. (T^^n)--A)"
then have [measurable]: "B ∈ sets M" by auto
have "T--B = (⋃n. (T^^(n+1))--A)" unfolding B_def using T_vrestr_composed(2) by auto
then have "T--B ⊆ B" using B_def by blast
then have *: "B ∈ null_sets M ∨ space M - B ∈ null_sets M"
using preimage_included_then_null_or_conull by auto
have "A ⊆ B" unfolding B_def using T_vrestr_0 assms(1) by blast
then have "emeasure M B > 0" using assms(2)
by (metis ‹B ∈ sets M› emeasure_eq_0 zero_less_iff_neq_zero)
then have "B ∉ null_sets M" by auto
then have i: "space M - B ∈ null_sets M" using * by auto
then show "space M - (⋃n. (T^^n)--A) ∈ null_sets M" using B_def by auto

have "B ⊆ space M" using sets.sets_into_space[OF ‹B ∈ sets M›] by auto
then have "space M Δ B ∈ null_sets M" using i by (simp add: Diff_mono sup.absorb1)
then show "space M Δ (⋃n. (T^^n)--A) ∈ null_sets M" using B_def by auto
qed

subsection ‹Behavior of functions in ergodic transformations›

text ‹In the same way that invariant sets are null or conull, invariant functions are almost
everywhere constant in an ergodic transformation. For real functions, one can consider
the set where $\{f x \geq d \}$, it has measure $0$ or $1$ depending on $d$.
Then $f$ is almost surely equal to the maximal $d$ such that this set has measure $1$. For functions
taking values in a general space, the argument is essentially the same, replacing intervals by
a basis of the topology.›

lemma (in ergodic_qmpt) Invariant_func_is_AE_constant:
fixes f::"_⇒ 'b::{second_countable_topology, t1_space}"
assumes "f ∈ borel_measurable Invariants"
shows "∃y. AE x in M. f x = y"
proof (cases)
assume "space M ∈ null_sets M"
obtain y::'b where "True" by auto
have "AE x in M. f x = y" using ‹space M ∈ null_sets M› AE_I' by blast
then show ?thesis by auto
next
assume *: "¬(space M ∈ null_sets M)"
obtain B::"'b set set" where B: "countable B" "topological_basis B" using ex_countable_basis by auto
define C where "C = {b ∈ B. space M - f-b ∈ null_sets M}"
then have "countable C" using ‹countable B› by auto
define Y where "Y = ⋂ C"
have "space M - f-Y = (⋃ b∈ C. space M - f-b)" unfolding Y_def by auto
moreover have "⋀b. b ∈ C ⟹ space M - f-b ∈ null_sets M" unfolding C_def by blast
ultimately have i: "space M - f-Y ∈ null_sets M" using ‹countable C› by (metis null_sets_UN')
then have "f-Y ≠ {}" using * by auto
then have "Y ≠ {}" by auto
then obtain y where "y ∈ Y" by auto
define D where "D = {b ∈ B. y∉b ∧ f-b ∩ space M ∈ null_sets M}"
have "countable D" using ‹countable B› D_def by auto
{
fix z assume "z ≠ y"
obtain U where U: "open U" "z ∈ U" "y ∉ U"
using t1_space[OF ‹z ≠ y›] by blast
obtain V where "V ∈ B" "V ⊆ U" "z ∈ V" by (rule topological_basisE[OF ‹topological_basis B› ‹open U› ‹z ∈ U›])
then have "y ∉ V" using U by blast
then have "V ∉ C" using ‹y ∈ Y› Y_def by auto
then have "space M - f-V ∩ space M ∉ null_sets M" unfolding C_def using ‹V ∈ B›
by (metis (no_types, lifting) Diff_Int2 inf.idem mem_Collect_eq)
moreover have "f-V ∩ space M ∈ sets Invariants"
using measurable_sets[OF assms borel_open[OF topological_basis_open[OF B(2) ‹V ∈ B›]]] subalgebra_def Invariants_is_subalg by metis
ultimately have "f-V ∩ space M ∈ null_sets M" using ergodic by auto
then have "V ∈ D" unfolding D_def using ‹V ∈ B› ‹y ∉ V› by auto
then have "∃b ∈ D. z ∈ b" using ‹z ∈ V› by auto
}
then have *: "⋃D = UNIV - {y}"
apply auto unfolding D_def by auto
have "space M - f-{y} = f-(UNIV -{y}) ∩ space M" by blast
also have "... = (⋃b∈D. f-b ∩ space M)" using * by auto
also have "... ∈ null_sets M" using D_def ‹countable D›
by (metis (no_types, lifting) mem_Collect_eq null_sets_UN')
finally have "space M - f-{y} ∈ null_sets M" by blast
with AE_not_in[OF this] have "AE x in M. x ∈ f-{y}" by auto
then show ?thesis by auto
qed

text ‹The same goes for functions which are only almost invariant, as they coindice almost
everywhere with genuine invariant functions.›

lemma (in ergodic_qmpt) AE_Invariant_func_is_AE_constant:
fixes f::"_ ⇒ 'b::{second_countable_topology, t2_space}"
assumes "f ∈ borel_measurable M" "AE x in M. f(T x) = f x"
shows "∃y. AE x in M. f x = y"
proof -
obtain g where g: "g ∈ borel_measurable Invariants" "AE x in M. f x = g x"
using Invariants_quasi_Invariants_functions[OF assms(1)] assms(2) by auto
then obtain y where y: "AE x in M. g x = y" using Invariant_func_is_AE_constant by auto
have "AE x in M. f x = y" using g(2) y by auto
then show ?thesis by auto
qed

text ‹In conservative systems, it suffices to have an inequality between $f$ and $f \circ T$,
since such a function is almost invariant.›

lemma (in ergodic_conservative) AE_decreasing_func_is_AE_constant:
fixes f::"_ ⇒ 'b::{linorder_topology, second_countable_topology}"
assumes "AE x in M. f(T x) ≤ f x"
and [measurable]: "f ∈ borel_measurable M"
shows "∃y. AE x in M. f x = y"
proof -
have "AE x in M. f(T x) = f x" using AE_decreasing_then_invariant[OF assms] by auto
then show ?thesis using AE_Invariant_func_is_AE_constant[OF assms(2)] by auto
qed

lemma (in ergodic_conservative) AE_increasing_func_is_AE_constant:
fixes f::"_ ⇒ 'b::{linorder_topology, second_countable_topology}"
assumes "AE x in M. f(T x) ≥ f x"
and [measurable]: "f ∈ borel_measurable M"
shows "∃y. AE x in M. f x = y"
proof -
have "AE x in M. f(T x) = f x" using AE_increasing_then_invariant[OF assms] by auto
then show ?thesis using AE_Invariant_func_is_AE_constant[OF assms(2)] by auto
qed

text ‹When the function takes values in a Banach space, the value of the invariant (hence constant)
function can be recovered by integrating the function.›

lemma (in ergodic_fmpt) Invariant_func_integral:
fixes f::"_ ⇒ 'b::{banach, second_countable_topology}"
assumes [measurable]: "f ∈ borel_measurable Invariants"
shows "integrable M f"
"AE x in M. f x = (∫x. f x ∂M)/⇩R (measure M (space M))"
proof -
have [measurable]: "f ∈ borel_measurable M" using assms Invariants_measurable_func by blast
obtain y where y: "AE x in M. f x = y" using Invariant_func_is_AE_constant[OF assms] by auto
moreover have "integrable M (λx. y)" by auto
ultimately show "integrable M f" by (subst integrable_cong_AE[where ?g = "λx. y"], auto)

have "(∫x. f x ∂M) = (∫x. y ∂M)" by (subst integral_cong_AE[where ?g = "λx. y"], auto simp add: y)
also have "... = measure M (space M) *⇩R y" by auto
finally have *: "(∫x. f x ∂M) = measure M (space M) *⇩R y" by simp
show "AE x in M. f x = (∫x. f x ∂M)/⇩R (measure M (space M))"
proof (cases)
assume "emeasure M (space M) = 0"
then have "space M ∈ null_sets M" by auto
then show ?thesis using AE_I' by blast
next
assume "¬(emeasure M (space M) = 0)"
then have "measure M (space M) > 0" using emeasure_eq_measure measure_le_0_iff by fastforce
then have "y = (∫x. f x ∂M)/⇩R (measure M (space M))" using * by auto
then show ?thesis using y by auto
qed
qed

text ‹As the conditional expectation of a function and the original function have the same
integral, it follows that the conditional expectation of a function with respect to the
invariant sigma algebra is given by the average of the function.›

lemma (in ergodic_fmpt) Invariants_cond_exp_is_integral_fmpt:
fixes f::"_ ⇒ real"
assumes "integrable M f"
shows "AE x in M. real_cond_exp M Invariants f x = (∫x. f x ∂M) / measure M (space M)"
proof -
have "AE x in M. real_cond_exp M Invariants f x = (∫x. real_cond_exp M Invariants f x ∂M)/⇩R (measure M (space M))"
by (rule Invariant_func_integral(2), simp add: borel_measurable_cond_exp)
moreover have "(∫x. real_cond_exp M Invariants f x ∂M) = (∫x. f x ∂M)"
ultimately show ?thesis by (simp add: divide_real_def mult.commute)
qed

lemma (in ergodic_pmpt) Invariants_cond_exp_is_integral:
fixes f::"_ ⇒ real"
assumes "integrable M f"
shows "AE x in M. real_cond_exp M Invariants f x = (∫x. f x ∂M)"
by (metis div_by_1 prob_space Invariants_cond_exp_is_integral_fmpt[OF assms])

subsection ‹Kac formula›

text ‹We reformulate the different versions of Kac formula. They simplify as, for any set $A$
with positive measure, the union $\bigcup T^{-n} A$ (which appears in all these statements)
almost coincides with the whole space.›

lemma (in ergodic_conservative_mpt) local_time_unbounded:
assumes [measurable]: "A ∈ sets M" "B ∈ sets M"
and "emeasure M A < ∞" "emeasure M B > 0"
shows "(λn. emeasure M {x ∈ (T^^n)--A. local_time B n x < k}) ⇢ 0"
proof (rule local_time_unbounded3)
have "A - (⋃i. (T ^^ i) -- B) ∈ sets M" by auto
moreover have "A - (⋃i. (T ^^ i) -- B) ⊆ space M - (⋃i. (T ^^ i) -- B)" using sets.sets_into_space[OF assms(1)] by blast
ultimately show "A - (⋃i. (T ^^ i) -- B) ∈ null_sets M" by (metis null_sets_subset preimages_conull(1)[OF assms(2) assms(4)])
show "emeasure M A < ∞" using assms(3) by simp

theorem (in ergodic_conservative_mpt) kac_formula:
assumes [measurable]: "A ∈ sets M" and "emeasure M A > 0"
shows "(∫⇧+y. return_time_function A y ∂M) = emeasure M (space M)"
proof -
have a [measurable]: "(⋃n. (T^^n)--A) ∈ sets M" by auto
then have "space M = (⋃n. (T^^n)--A) ∪ (space M - (⋃n. (T^^n)--A))" using sets.sets_into_space by blast
then have "emeasure M (space M) = emeasure M (⋃n. (T^^n)--A)"
by (metis a preimages_conull(1)[OF assms] emeasure_Un_null_set)
moreover have "(∫⇧+y. return_time_function A y ∂M) = emeasure M (⋃n. (T^^n)--A)"
using kac_formula_nonergodic[OF assms(1)] by simp
ultimately show ?thesis by simp
qed

lemma (in ergodic_conservative_mpt) induced_function_integral:
fixes f::"'a ⇒ real"
assumes [measurable]: "A ∈ sets M" "integrable M f" and "emeasure M A > 0"
shows "integrable M (induced_function A f)"
"(∫y. induced_function A f y ∂M) = (∫ x. f x ∂M)"
proof -
show "integrable M (induced_function A f)"
using induced_function_integral_nonergodic(1)[OF assms(1) assms(2)] by auto
have "(∫y. induced_function A f y ∂M) = (∫ x ∈ (⋃n. (T^^n)--A). f x ∂M)"
using induced_function_integral_nonergodic(2)[OF assms(1) assms(2)] by auto
also have "... = (∫ x ∈ space M. f x ∂M)"
using set_integral_null_delta[OF assms(2), where ?A = "space M" and ?B = "(⋃n. (T^^n)--A)"]
preimages_conull(2)[OF assms(1) assms(3)] by auto
also have "... = (∫ x. f x ∂M)" using set_integral_space[OF assms(2)] by auto
finally show "(∫y. induced_function A f y ∂M) = (∫ x. f x ∂M)" by simp
qed

lemma (in ergodic_conservative_mpt) induced_function_integral_restr:
fixes f::"'a ⇒ real"
assumes [measurable]: "A ∈ sets M" "integrable M f" and "emeasure M A > 0"
shows "integrable (restrict_space M A) (induced_function A f)"
"(∫y. induced_function A f y ∂(restrict_space M A)) = (∫ x. f x ∂M)"
proof -
show "integrable (restrict_space M A) (induced_function A f)"
using induced_function_integral_restr_nonergodic(1)[OF assms(1) assms(2)] by auto
have "(∫y. induced_function A f y ∂(restrict_space M A)) = (∫ x ∈ (⋃n. (T^^n)--A). f x ∂M)"
using induced_function_integral_restr_nonergodic(2)[OF assms(1) assms(2)] by auto
also have "... = (∫ x ∈ space M. f x ∂M)"
using set_integral_null_delta[OF assms(2), where ?A = "space M" and ?B = "(⋃n. (T^^n)--A)"]
preimages_conull(2)[OF assms(1) assms(3)] by auto
also have "... = (∫ x. f x ∂M)" using set_integral_space[OF assms(2)] by auto
finally show "(∫y. induced_function A f y ∂(restrict_space M A)) = (∫ x. f x ∂M)" by simp
qed

subsection ‹Birkhoff theorem›

text ‹The general versions of Birkhoff theorem are formulated in terms of conditional expectations.
In ergodic probability measure preserving transformations (the most common setting), they
reduce to simpler versions that we state now, as the conditional expectations are simply the
averages of the functions.›

theorem (in ergodic_pmpt) birkhoff_theorem_AE:
fixes f::"'a ⇒ real"
assumes "integrable M f"
shows "AE x in M. (λn. birkhoff_sum f n x / n) ⇢ (∫ x. f x ∂M)"
proof -
have "AE x in M. (λn. birkhoff_sum f n x / n) ⇢ real_cond_exp M Invariants f x"
using birkhoff_theorem_AE_nonergodic[OF assms] by simp
moreover have "AE x in M. real_cond_exp M Invariants f x = (∫ x. f x ∂M)"
using Invariants_cond_exp_is_integral[OF assms] by auto
ultimately show ?thesis by auto
qed

theorem (in ergodic_pmpt) birkhoff_theorem_L1:
fixes f::"'a ⇒ real"
assumes [measurable]: "integrable M f"
shows "(λn. ∫⇧+x. norm(birkhoff_sum f n x / n - (∫ x. f x ∂M)) ∂M) ⇢ 0"
proof -
{
fix n::nat
have "AE x in M. real_cond_exp M Invariants f x = (∫ x. f x ∂M)"
using Invariants_cond_exp_is_integral[OF assms] by auto
then have *: "AE x in M. norm(birkhoff_sum f n x / n - real_cond_exp M Invariants f x)
= norm(birkhoff_sum f n x / n - (∫ x. f x ∂M))"
by auto
have "(∫⇧+x. norm(birkhoff_sum f n x / n - real_cond_exp M Invariants f x) ∂M)
= (∫⇧+x. norm(birkhoff_sum f n x / n - (∫ x. f x ∂M)) ∂M)"
apply (rule nn_integral_cong_AE) using * by auto
}
moreover have "(λn. ∫⇧+x. norm(birkhoff_sum f n x / n - real_cond_exp M Invariants f x) ∂M) ⇢ 0"
using birkhoff_theorem_L1_nonergodic[OF assms] by auto
ultimately show ?thesis by simp
qed

theorem (in ergodic_pmpt) birkhoff_sum_small_asymp_pos:
fixes f::"'a ⇒ real"
assumes [measurable]: "integrable M f" and "e>0"
shows "AE x in M. infinite {n. birkhoff_sum f n x ∈ {n * (∫x. f x ∂M) .. n * (∫x. f x ∂M) + e}}"
proof -
have "AE x in M. infinite {n. birkhoff_sum f n x ∈ {n * real_cond_exp M Invariants f x .. n * real_cond_exp M Invariants f x + e}}"
using birkhoff_sum_small_asymp_pos_nonergodic[OF assms] by simp
moreover have "AE x in M. real_cond_exp M Invariants f x = (∫x. f x ∂M)"
using Invariants_cond_exp_is_integral[OF assms(1)] by auto
ultimately show ?thesis by auto
qed

theorem (in ergodic_pmpt) birkhoff_sum_small_asymp_neg:
fixes f::"'a ⇒ real"
assumes [measurable]: "integrable M f" and "e>0"
shows "AE x in M. infinite {n. birkhoff_sum f n x ∈ {n * (∫x. f x ∂M) - e .. n * (∫x. f x ∂M)}}"
proof -
have "AE x in M. infinite {n. birkhoff_sum f n x ∈ {n * real_cond_exp M Invariants f x - e .. n * real_cond_exp M Invariants f x}}"
using birkhoff_sum_small_asymp_neg_nonergodic[OF assms] by simp
moreover have "AE x in M. real_cond_exp M Invariants f x = (∫x. f x ∂M)"
using Invariants_cond_exp_is_integral[OF assms(1)] by auto
ultimately show ?thesis by auto
qed

lemma (in ergodic_pmpt) birkhoff_positive_average:
fixes f::"'a ⇒ real"
assumes [measurable]: "integrable M f" and "AE x in M. (λn. birkhoff_sum f n x) ⇢ ∞"
shows "(∫ x. f x ∂M) > 0"
proof (rule ccontr)
assume "¬((∫ x. f x ∂M) > 0)"
then have *: "(∫ x. f x ∂M) ≤ 0" by simp

have "AE x in M. (λn. birkhoff_sum f n x) ⇢ ∞ ∧ infinite {n. birkhoff_sum f n x ∈ {n * (∫x. f x ∂M) - 1 .. n* (∫x. f x ∂M)}}"
using assms(2) birkhoff_sum_small_asymp_neg[OF assms(1)] by auto
then obtain x where x: "(λn. birkhoff_sum f n x) ⇢ ∞" "infinite {n. birkhoff_sum f n x ∈ {n * (∫x. f x ∂M) - 1 .. n* (∫x. f x ∂M)}}"
using AE_False eventually_elim2 by blast
{
fix n assume "birkhoff_sum f n x ∈ {n * (∫x. f x ∂M) - 1 .. n * (∫x. f x ∂M)}"
then have "birkhoff_sum f n x ≤ n * (∫x. f x ∂M)" by simp
also have "... ≤ 0" using * by (simp add: mult_nonneg_nonpos)
finally have "birkhoff_sum f n x ≤ 0" by simp
}
then have "{n. birkhoff_sum f n x ∈ {n * (∫x. f x ∂M) - 1 .. n* (∫x. f x ∂M)}} ⊆ {n. birkhoff_sum f n x ≤ 0}" by auto
then have inf: "infinite {n. birkhoff_sum f n x ≤ 0}" using x(2) finite_subset by blast

have "0 < (∞::ereal)" by auto
then have "eventually (λn. birkhoff_sum f n x > (0::ereal)) sequentially" using x(1) order_tendsto_iff by metis
then obtain N where "⋀n. n ≥ N ⟹ birkhoff_sum f n x > (0::ereal)" by (meson eventually_at_top_linorder)
then have "⋀n. n ≥ N ⟹ birkhoff_sum f n x > 0" by auto
then have "{n. birkhoff_sum f n x ≤ 0} ⊆ {..<N}" by (metis (mono_tags, lifting) lessThan_iff linorder_not_less mem_Collect_eq subsetI)
then have "finite {n. birkhoff_sum f n x ≤ 0}" using finite_nat_iff_bounded by blast

then show "False" using inf by simp
qed

lemma (in ergodic_pmpt) birkhoff_negative_average:
fixes f::"'a ⇒ real"
assumes [measurable]: "integrable M f" and "AE x in M. (λn. birkhoff_sum f n x) ⇢ -∞"
shows "(∫ x. f x ∂M) < 0"
proof (rule ccontr)
assume "¬((∫ x. f x ∂M) < 0)"
then have *: "(∫ x. f x ∂M) ≥ 0" by simp

have "AE x in M. (λn. birkhoff_sum f n x) ⇢ -∞ ∧ infinite {n. birkhoff_sum f n x ∈ {n * (∫x. f x ∂M) .. n* (∫x. f x ∂M) + 1}}"
using assms(2) birkhoff_sum_small_asymp_pos[OF assms(1)] by auto
then obtain x where x: "(λn. birkhoff_sum f n x) ⇢ -∞" "infinite {n. birkhoff_sum f n x ∈ {n * (∫x. f x ∂M) .. n* (∫x. f x ∂M) + 1}}"
using AE_False eventually_elim2 by blast
{
fix n assume "birkhoff_sum f n x ∈ {n * (∫x. f x ∂M) .. n * (∫x. f x ∂M) + 1}"
then have "birkhoff_sum f n x ≥ n * (∫x. f x ∂M)" by simp
moreover have "n * (∫x. f x ∂M) ≥ 0" using * by simp
ultimately have "birkhoff_sum f n x ≥ 0" by simp
}
then have "{n. birkhoff_sum f n x ∈ {n * (∫x. f x ∂M) .. n* (∫x. f x ∂M) + 1}} ⊆ {n. birkhoff_sum f n x ≥ 0}" by auto
then have inf: "infinite {n. birkhoff_sum f n x ≥ 0}" using x(2) finite_subset by blast

have "0 > (-∞::ereal)" by auto
then have "eventually (λn. birkhoff_sum f n x < (0::ereal)) sequentially" using x(1) order_tendsto_iff by metis
then obtain N where "⋀n. n ≥ N ⟹ birkhoff_sum f n x < (0::ereal)" by (meson eventually_at_top_linorder)
then have "⋀n. n ≥ N ⟹ birkhoff_sum f n x < 0" by auto
then have "{n. birkhoff_sum f n x ≥ 0} ⊆ {..<N}" by (metis (mono_tags, lifting) lessThan_iff linorder_not_less mem_Collect_eq subsetI)
then have "finite {n. birkhoff_sum f n x ≥ 0}" using finite_nat_iff_bounded by blast

then show "False" using inf by simp
qed

lemma (in ergodic_pmpt) birkhoff_nonzero_average:
fixes f::"'a ⇒ real"
assumes [measurable]: "integrable M f" and "AE x in M. (λn. abs(birkhoff_sum f n x)) ⇢ ∞"
shows "(∫ x. f x ∂M) ≠ 0"
proof (rule ccontr)
assume "¬((∫ x. f x ∂M) ≠ 0)"
then have *: "(∫ x. f x ∂M) = 0" by simp

have "AE x in M. (λn. abs(birkhoff_sum f n x)) ⇢ ∞ ∧ infinite {n. birkhoff_sum f n x ∈ {0 .. 1}}"
using assms(2) birkhoff_sum_small_asymp_pos[OF assms(1)] * by auto
then obtain x where x: "(λn. abs(birkhoff_sum f n x)) ⇢ ∞" "infinite {n. birkhoff_sum f n x ∈ {0 .. 1}}"
using AE_False eventually_elim2 by blast

have "1 < (∞::ereal)" by auto
then have "eventually (λn. abs(birkhoff_sum f n x) > (1::ereal)) sequentially" using x(1) order_tendsto_iff by metis
then obtain N where "⋀n. n ≥ N ⟹ abs(birkhoff_sum f n x) > (1::ereal)" by (meson eventually_at_top_linorder)
then have *: "⋀n. n ≥ N ⟹ abs(birkhoff_sum f n x) > 1" by auto
have "{n. birkhoff_sum f n x ∈ {0..1}} ⊆ {..<N}" by (auto, metis (full_types) * abs_of_nonneg not_less)
then have "finite {n. birkhoff_sum f n x ∈ {0..1}}" using finite_nat_iff_bounded by blast

then show "False" using x(2) by simp
qed

end (*of Ergodicity.thy*)