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