Theory Ergodicity

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

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)"
    by (simp add: assms real_cond_exp_int(2))
  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
qed (simp_all add: assms)

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*)