(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr License: BSD *) section ‹Conservativity, recurrence› theory Recurrence imports Measure_Preserving_Transformations begin text ‹A dynamical system is conservative if almost every point comes back close to its starting point. This is always the case if the measure is finite, not when it is infinite (think of the translation on $\mathbb{Z}$). In conservative systems, an important construction is the induced map: the first return map to a set of finite measure. It is measure-preserving and conservative if the original system is. This makes it possible to reduce statements about general conservative systems in infinite measure to statements about systems in finite measure, and as such is extremely useful.› subsection ‹Definition of conservativity› locale conservative = qmpt + assumes conservative: "⋀A. A ∈ sets M ⟹ emeasure M A > 0 ⟹ ∃n>0. emeasure M ((T^^n)-`A ∩ A) >0" lemma conservativeI: assumes "qmpt M T" "⋀A. A ∈ sets M ⟹ emeasure M A > 0 ⟹ ∃n>0. emeasure M ((T^^n)-`A ∩ A) >0" shows "conservative M T" unfolding conservative_def conservative_axioms_def using assms by auto text ‹To prove conservativity, it is in fact sufficient to show that the preimages of a set of positive measure intersect it, without any measure control. Indeed, in a non-conservative system, one can construct a set which does not satisfy this property.› lemma conservativeI2: assumes "qmpt M T" "⋀A. A ∈ sets M ⟹ emeasure M A > 0 ⟹ ∃n>0. (T^^n)-`A ∩ A ≠ {}" shows "conservative M T" unfolding conservative_def conservative_axioms_def proof (auto simp add: assms) interpret qmpt M T using assms by auto fix A assume A_meas [measurable]: "A ∈ sets M" and "emeasure M A > 0" show "∃n>0. 0 < emeasure M ((T ^^ n) -` A ∩ A)" proof (rule ccontr) assume "¬ (∃n>0. 0 < emeasure M ((T ^^ n) -` A ∩ A))" then have meas_0: "emeasure M ((T ^^ n) -` A ∩ A) = 0" if "n>0" for n by (metis zero_less_iff_neq_zero that) define C where "C = (⋃n. (T^^(Suc n))-`A ∩ A)" have C_meas [measurable]: "C ∈ sets M" unfolding C_def by measurable have "emeasure M C = 0" unfolding C_def by (intro emeasure_UN_eq_0[of M, of "λn. (T^^(Suc n))-`A ∩ A", OF meas_0], auto) define A2 where "A2 = A-C" then have A2_meas [measurable]: "A2 ∈ sets M" by simp have "¬(∃n>0. (T^^n)-`A2 ∩ A2 ≠ {})" proof (rule ccontr, simp) assume "∃n>0. (T^^n)-`A2 ∩ A2 ≠ {}" then obtain n where n: "n > 0" "(T^^n)-`A2 ∩ A2 ≠ {}" by auto define m where "m = n-1" have "(T^^(m+1))-`A2 ∩ A2 ≠ {}" unfolding m_def using n by auto then show False using C_def A2_def by auto qed then have "emeasure M A2 = 0" using assms(2)[OF A2_meas] by (meson zero_less_iff_neq_zero) then have "emeasure M (C ∪ A2) = 0" using ‹emeasure M C = 0› by (simp add: emeasure_Un_null_set null_setsI) moreover have "A ⊆ C ∪ A2" unfolding A2_def by auto ultimately have "emeasure M A = 0" by (meson A2_meas C_meas emeasure_eq_0 sets.Un) then show False using ‹emeasure M A > 0› by auto qed qed text ‹There is also a dual formulation, saying that conservativity follows from the fact that a set disjoint from all its preimages has to be null.› lemma conservativeI3: assumes "qmpt M T" "⋀A. A ∈ sets M ⟹ (∀n>0. (T^^n)-`A ∩ A = {}) ⟹ A ∈ null_sets M" shows "conservative M T" proof (rule conservativeI2[OF assms(1)]) fix A assume "A ∈ sets M" "0 < emeasure M A" then have "¬(A ∈ null_sets M)" unfolding null_sets_def by auto then show "∃n>0. (T ^^ n) -` A ∩ A ≠ {}" using assms(2)[OF ‹A ∈ sets M›] by auto qed text ‹The inverse of a conservative map is still conservative› lemma (in conservative) conservative_Tinv: assumes "invertible_qmpt" shows "conservative M Tinv" proof (rule conservativeI2) show "qmpt M Tinv" using Tinv_qmpt[OF assms]. have "bij T" using assms unfolding invertible_qmpt_def by auto fix A assume [measurable]: "A ∈ sets M" and "emeasure M A > 0" then obtain n where *: "n>0" "emeasure M ((T^^n)-`A ∩ A) > 0" using conservative[OF ‹A ∈ sets M› ‹emeasure M A > 0›] by blast have "bij (T^^n)" using bij_fn[OF ‹bij T›] by auto then have "bij(inv (T^^n))" using bij_imp_bij_inv by auto then have "bij (Tinv^^n)" unfolding Tinv_def using inv_fn[OF ‹bij T›, of n] by auto have "(T^^n)-`A ∩ A ≠ {}" using * by auto then have "(Tinv^^n)-`((T^^n)-`A ∩ A) ≠ {}" using surj_vimage_empty[OF bij_is_surj[OF ‹bij (Tinv^^n)›]] by meson then have **: "(Tinv^^n)-`((T^^n)-`A) ∩ (Tinv^^n)-` A ≠ {}" by auto have "(Tinv^^n)-`((T^^n)-`A) = ((T^^n) o (Tinv^^n))-`A" by auto moreover have "(T^^n) o (Tinv^^n) = (λx. x)" unfolding Tinv_def using ‹bij T› fn_o_inv_fn_is_id by blast ultimately have "(Tinv^^n)-`((T^^n)-`A) = A" by auto then have "(Tinv^^n)-` A ∩ A ≠ {}" using ** by auto then show "∃n>0. (Tinv ^^ n) -` A ∩ A ≠ {}" using ‹n>0› by auto qed text ‹We introduce the locale of a conservative measure preserving map.› locale conservative_mpt = mpt + conservative lemma conservative_mptI: assumes "mpt M T" "⋀A. A ∈ sets M ⟹ emeasure M A > 0 ⟹ ∃n>0. (T^^n)-`A ∩ A ≠ {}" shows "conservative_mpt M T" unfolding conservative_mpt_def apply (auto simp add: assms(1), rule conservativeI2) using assms(1) by (auto simp add: mpt_def assms(2)) text ‹The fact that finite measure preserving transformations are conservative, albeit easy, is extremely important. This result is known as Poincaré recurrence theorem.› sublocale fmpt ⊆ conservative_mpt proof (rule conservative_mptI) show "mpt M T" by (simp add: mpt_axioms) fix A assume A_meas [measurable]: "A ∈ sets M" and "emeasure M A > 0" show "∃n>0. (T^^n)-`A ∩ A ≠ {}" proof (rule ccontr) assume "¬(∃n>0. (T^^n)-`A ∩ A ≠ {})" then have disj: "(T^^(Suc n))--`A ∩ A = {}" for n unfolding vimage_restr_def using zero_less_one by blast define B where "B = (λ n. (T^^n)--`A)" then have B_meas [measurable]: "B n ∈ sets M" for n by simp have same: "measure M (B n) = measure M A" for n by (simp add: B_def A_meas T_vrestr_same_measure(2)) have "B n ∩ B m = {}" if "n > m" for m n proof - have "B n ∩ B m = (T^^m)--` (B (n-m) ∩ A)" using B_def ‹m < n› A_meas vrestr_intersec T_vrestr_composed(1) by auto moreover have "B (n-m) ∩ A = {}" unfolding B_def by (metis disj ‹m < n› Suc_diff_Suc) ultimately show ?thesis by simp qed then have "disjoint_family B" by (metis disjoint_family_on_def inf_sup_aci(1) less_linear) have "measure M A < e" if "e>0" for e::real proof - obtain N::nat where "N>0" "(measure M (space M))/e<N" using ‹0 < e› by (metis divide_less_0_iff reals_Archimedean2 less_eq_real_def measure_nonneg not_gr0 not_le of_nat_0) then have "(measure M (space M))/N < e" using ‹0 < e› ‹N>0› by (metis bounded_measure div_0 le_less_trans measure_empty mult.commute pos_divide_less_eq) have *: "disjoint_family_on B {..<N}" by (meson UNIV_I ‹disjoint_family B› disjoint_family_on_mono subsetI) then have "(∑i∈{..<N}. measure M (B i)) ≤ measure M (space M)" by (metis bounded_measure ‹⋀n. B n ∈ sets M› image_subset_iff finite_lessThan finite_measure_finite_Union) also have "(∑i∈{..<N}. measure M (B i)) = (∑i∈{..<N}. measure M A)" using same by simp also have "... = N * (measure M A)" by simp finally have "N * (measure M A) ≤ measure M (space M)" by simp then have "measure M A ≤ (measure M (space M))/N" using ‹N>0› by (simp add: mult.commute mult_imp_le_div_pos) then show "measure M A < e" using ‹(measure M (space M))/N<e› by simp qed then have "measure M A ≤ 0" using not_less by blast then have "measure M A = 0" by (simp add: measure_le_0_iff) then have "emeasure M A = 0" using emeasure_eq_measure by simp then show False using ‹emeasure M A > 0› by simp qed qed text ‹The following fact that powers of conservative maps are also conservative is true, but nontrivial. It is proved as follows: consider a set $A$ with positive measure, take a time $n_1$ such that $A_1 = T^{-n_1} A \cap A$ has positive measure, then a time $n_2$ such that $A_2 = T^{-n_2} A_1 \cap A$ has positive measure, and so on. It follows that $T^{-(n_i+n_{i+1}+\dots+n_j)}A \cap A$ has positive measure for all $i<j$. Then, one can find $i<j$ such that $n_i+\dots+n_j$ is a multiple of $N$.› proposition (in conservative) conservative_power: "conservative M (T^^n)" proof (unfold_locales) show "T ^^ n ∈ quasi_measure_preserving M M" by (auto simp add: Tn_quasi_measure_preserving) fix A assume [measurable]: "A ∈ sets M" "0 < emeasure M A" define good_time where "good_time = (λK. Inf{(i::nat). i > 0 ∧ emeasure M ((T^^i)-`K ∩ A) > 0})" define next_good_set where "next_good_set = (λK. (T^^(good_time K))-`K ∩ A)" have good_rec: "((good_time K > 0) ∧ (next_good_set K ⊆ A) ∧ (next_good_set K ∈ sets M) ∧ (emeasure M (next_good_set K) > 0))" if [measurable]: "K ∈ sets M" and "K ⊆ A" "emeasure M K > 0" for K proof - have a: "next_good_set K ∈ sets M" "next_good_set K ⊆ A" using next_good_set_def by simp_all obtain k where "k > 0" and posK: "emeasure M ((T^^k)-`K ∩ K) > 0" using conservative[OF ‹K ∈ sets M›, OF ‹emeasure M K > 0›] by auto have *:"(T^^k)-`K ∩ K ⊆ (T^^k)-`K ∩ A" using ‹K ⊆ A› by auto have posKA: "emeasure M ((T^^k)-`K ∩ A) > 0" using emeasure_mono[OF *, of M] posK by simp let ?S = "{(i::nat). i>0 ∧ emeasure M ((T^^i)-`K ∩ A) > 0}" have "k ∈ ?S" using ‹k>0› posKA by simp then have "?S ≠ {}" by auto then have "Inf ?S ∈ ?S" using Inf_nat_def1[of ?S] by simp then have "good_time K ∈ ?S" using good_time_def by simp then show "(good_time K > 0) ∧ (next_good_set K ⊆ A) ∧ (next_good_set K ∈ sets M) ∧ (emeasure M (next_good_set K) > 0)" using a next_good_set_def by auto qed define B where "B = (λi. (next_good_set^^i) A)" define t where "t = (λi. good_time (B i))" have good_B: "(B i ⊆ A) ∧ (B i ∈ sets M) ∧ (emeasure M (B i) > 0)" for i proof (induction i) case 0 have "B 0 = A" using B_def by simp then show ?case using ‹B 0 = A› ‹A ∈ sets M› ‹emeasure M A > 0› by simp next case (Suc i) moreover have "B (i+1) = next_good_set (B i)" using B_def by simp ultimately show ?case using good_rec[of "B i"] by auto qed have t_pos: "⋀i. t i > 0" using t_def by (simp add: good_B good_rec) define s where "s = (λi k. (∑n ∈ {i..<i+k}. t n))" have "B (i+k) ⊆ (T^^(s i k))-`A ∩ A" for i k proof (induction k) case 0 show ?case using s_def good_B[of i] by simp next case (Suc k) have "B(i+k+1) = (T^^(t (i+k)))-`(B (i+k)) ∩ A" using t_def B_def next_good_set_def by simp moreover have "B(i+k) ⊆ (T^^(s i k))-`A" using Suc.IH by simp ultimately have "B(i+k+1) ⊆ (T^^(t (i+k)))-` (T^^(s i k))-`A ∩ A" by auto then have "B(i+k+1) ⊆ (T^^(t(i+k) + s i k))-`A ∩ A" by (simp add: add.commute funpow_add vimage_comp) moreover have "t(i+k) + s i k = s i (k+1)" using s_def by simp ultimately show ?case by simp qed moreover have "(T^^j)-`A ∩ A ∈ sets M" for j by simp ultimately have *: "emeasure M ((T^^(s i k))-`A ∩ A) > 0" for i k by (metis inf.orderE inf.strict_boundedE good_B emeasure_mono) show "∃k>0. 0 < emeasure M (((T ^^ n) ^^ k) -` A ∩ A)" proof (cases) assume "n = 0" then have "((T ^^ n) ^^ 1) -` A = A" by simp then show ?thesis using ‹emeasure M A > 0› by auto next assume "¬(n = 0)" then have "n > 0" by simp define u where "u = (λi. s 0 i mod n)" have "range u ⊆ {..<n}" by (simp add: ‹0 < n› image_subset_iff u_def) then have "finite (range u)" using finite_nat_iff_bounded by auto then have "∃i j. (i<j) ∧ (u i = u j)" by (metis finite_imageD infinite_UNIV_nat injI less_linear) then obtain i k where "k>0" "u i = u (i+k)" using less_imp_add_positive by blast moreover have "s 0 (i+k) = s 0 i + s i k" unfolding s_def by (simp add: sum.atLeastLessThan_concat) ultimately have "(s i k) mod n = 0" using u_def nat_mod_cong by metis then obtain r where "s i k = n * r" by auto moreover have "s i k > 0" unfolding s_def using ‹k > 0› t_pos sum_strict_mono[of "{i..<i+k}", of "λx. 0", of "λx. t x"] by simp ultimately have "r > 0" by simp moreover have "emeasure M ((T^^(n * r))-`A ∩ A) > 0" using * ‹s i k = n * r› by metis ultimately show ?thesis by (metis funpow_mult) qed qed proposition (in conservative_mpt) conservative_mpt_power: "conservative_mpt M (T^^n)" using conservative_power mpt_power unfolding conservative_mpt_def by auto text ‹The standard way to use conservativity is as follows: if a set is almost disjoint from all its preimages, then it is null:› lemma (in conservative) ae_disjoint_then_null: assumes "A ∈ sets M" "⋀n. n > 0 ⟹ A ∩ (T^^n)-`A ∈ null_sets M" shows "A ∈ null_sets M" by (metis Int_commute assms(1) assms(2) conservative zero_less_iff_neq_zero null_setsD1 null_setsI) lemma (in conservative) disjoint_then_null: assumes "A ∈ sets M" "⋀n. n > 0 ⟹ A ∩ (T^^n)-`A = {}" shows "A ∈ null_sets M" by (rule ae_disjoint_then_null, auto simp add: assms) text ‹Conservativity is preserved by replacing the measure by an equivalent one.› lemma (in conservative) conservative_density: assumes [measurable]: "h ∈ borel_measurable M" and "AE x in M. h x ≠ 0" "AE x in M. h x ≠ ∞" shows "conservative (density M h) T" proof - interpret A: qmpt "density M h" T by (rule qmpt_density[OF assms]) show ?thesis apply (rule conservativeI3) apply (simp add: A.qmpt_axioms) unfolding sets_density null_sets_density[OF assms(1) assms(2)] by (metis conservative emeasure_empty not_gr_zero null_setsI) qed context qmpt begin text ‹We introduce the recurrent subset of $A$, i.e., the set of points of $A$ that return to $A$, and the infinitely recurrent subset, i.e., the set of points of $A$ that return infinitely often to $A$. In conservative systems, both coincide with $A$ almost everywhere.› definition recurrent_subset::"'a set ⇒ 'a set" where "recurrent_subset A = (⋃n ∈ {1..}. A ∩ (T^^n)-`A)" definition recurrent_subset_infty::"'a set ⇒ 'a set" where "recurrent_subset_infty A = A - (⋃n. (T^^n)-` (A - recurrent_subset A))" lemma recurrent_subset_infty_inf_returns: "x ∈ recurrent_subset_infty A ⟷ (x ∈ A ∧ infinite {n. (T^^n) x ∈ A})" proof assume *: "x ∈ recurrent_subset_infty A" have "infinite {n. (T^^n) x ∈ A}" proof (rule ccontr) assume "¬(infinite {n. (T^^n) x ∈ A})" then have F: "finite {n. (T^^n) x ∈ A}" by auto have "0 ∈ {n. (T^^n) x ∈ A}" using * recurrent_subset_infty_def by auto then have NE: "{n. (T^^n) x ∈ A} ≠ {}" by blast define N where "N = Max {n. (T^^n) x ∈ A}" have "N ∈ {n. (T^^n) x ∈ A}" unfolding N_def using F NE using Max_in by auto then have "(T^^N) x ∈ A" by auto moreover have "x ∉ (T^^N)-` (A - recurrent_subset A)" using * unfolding recurrent_subset_infty_def by auto ultimately have "(T^^N) x ∈ recurrent_subset A" by auto then have "(T ^^ N) x ∈ A ∧ (∃n. n ∈ {1..} ∧ (T ^^ n) ((T ^^ N) x) ∈ A)" unfolding recurrent_subset_def by blast then obtain n where "n>0" "(T^^n) ((T^^N) x) ∈ A" by (metis atLeast_iff gr0I not_one_le_zero) then have "n+N ∈ {n. (T^^n) x ∈ A}" by (simp add: funpow_add) then show False unfolding N_def using ‹n>0› F NE by (metis Max_ge Nat.add_0_right add.commute nat_add_left_cancel_less not_le) qed then show "x ∈ A ∧ infinite {n. (T^^n) x ∈ A}" using * recurrent_subset_infty_def by auto next assume *: "(x ∈ A ∧ infinite {n. (T ^^ n) x ∈ A})" { fix n obtain N where "N>n" "(T^^N) x ∈ A" using * using infinite_nat_iff_unbounded by force define k where "k = N-n" then have "k>0" "N = n+k" using ‹N>n› by auto then have "(T^^k) ((T^^n) x) ∈ A" by (metis ‹(T ^^ N) x ∈ A› ‹N = n + k› add.commute comp_def funpow_add) then have "(T^^ n) x ∉ A - recurrent_subset A" unfolding recurrent_subset_def using ‹k>0› by auto } then show "x ∈ recurrent_subset_infty A" unfolding recurrent_subset_infty_def using * by auto qed lemma recurrent_subset_infty_series_infinite: assumes "x ∈ recurrent_subset_infty A" shows "(∑n. indicator A ((T^^n) x)) = (∞::ennreal)" proof (rule ennreal_ge_nat_imp_PInf) have *: "¬ finite {n. (T^^n) x ∈ A}" using recurrent_subset_infty_inf_returns assms by auto fix N::nat obtain F where F: "finite F" "F ⊆ {n. (T^^n) x ∈ A}" "card F = N" using infinite_arbitrarily_large[OF *] by blast have "N = (∑n ∈ F. 1::ennreal)" using F(3) by auto also have "... = (∑n ∈ F. (indicator A ((T^^n) x))::ennreal)" apply (rule sum.cong) using F(2) indicator_def by auto also have "... ≤ (∑n. indicator A ((T^^n) x))" by (rule sum_le_suminf, auto simp add: F) finally show "N ≤ (∑n. (indicator A ((T^^n) x))::ennreal)" by auto qed lemma recurrent_subset_infty_def': "recurrent_subset_infty A = (⋂m. (⋃n∈{m..}. A ∩ (T^^n)-`A))" proof (auto) fix x assume x: "x ∈ recurrent_subset_infty A" then show "x ∈ A" unfolding recurrent_subset_infty_def by auto fix N::nat show "∃n∈{N..}. (T^^n) x ∈ A" using recurrent_subset_infty_inf_returns x using infinite_nat_iff_unbounded_le by auto next fix x assume "x ∈ A" "∀N. ∃n∈{N..}. (T^^n) x ∈ A" then show "x ∈ recurrent_subset_infty A" unfolding recurrent_subset_infty_inf_returns using infinite_nat_iff_unbounded_le by auto qed lemma recurrent_subset_incl: "recurrent_subset A ⊆ A" "recurrent_subset_infty A ⊆ A" "recurrent_subset_infty A ⊆ recurrent_subset A" unfolding recurrent_subset_def recurrent_subset_infty_def' by (simp, simp, fast) lemma recurrent_subset_meas [measurable]: assumes [measurable]: "A ∈ sets M" shows "recurrent_subset A ∈ sets M" "recurrent_subset_infty A ∈ sets M" unfolding recurrent_subset_def recurrent_subset_infty_def' by measurable lemma recurrent_subset_rel_incl: assumes "A ⊆ B" shows "recurrent_subset A ⊆ recurrent_subset B" "recurrent_subset_infty A ⊆ recurrent_subset_infty B" proof - show "recurrent_subset A ⊆ recurrent_subset B" unfolding recurrent_subset_def using assms by auto show "recurrent_subset_infty A ⊆ recurrent_subset_infty B" apply (auto, subst recurrent_subset_infty_inf_returns) using assms recurrent_subset_incl(2) infinite_nat_iff_unbounded_le recurrent_subset_infty_inf_returns by fastforce qed text ‹If a point belongs to the infinitely recurrent subset of $A$, then when they return to $A$ its iterates also belong to the infinitely recurrent subset.› lemma recurrent_subset_infty_returns: assumes "x ∈ recurrent_subset_infty A" "(T^^n) x ∈ A" shows "(T^^n) x ∈ recurrent_subset_infty A" proof (subst recurrent_subset_infty_inf_returns, rule ccontr) assume "¬ ((T ^^ n) x ∈ A ∧ infinite {k. (T ^^ k) ((T ^^ n) x) ∈ A})" then have 1: "finite {k. (T^^k) ((T^^n) x) ∈ A}" using assms(2) by auto have "0 ∈ {k. (T^^k) ((T^^n) x) ∈ A}" using assms(2) by auto then have 2: "{k. (T^^k) ((T^^n) x) ∈ A} ≠ {}" by blast define M where "M = Max {k. (T^^k) ((T^^n) x) ∈ A}" have M_prop: "⋀k. k > M ⟹ (T^^k) ((T^^n) x) ∉ A" unfolding M_def using 1 2 by auto { fix N assume *: "(T^^N) x ∈ A" have "N ≤ n+M" proof (cases) assume "N ≤ n" then show ?thesis by auto next assume "¬(N ≤ n)" then have "N > n" by simp define k where "k = N-n" have "N = n + k" unfolding k_def using ‹N > n› by auto then have "(T^^k) ((T^^n)x) ∈ A" using * by (simp add: add.commute funpow_add) then have "k ≤ M" using M_prop using not_le by blast then show ?thesis unfolding k_def by auto qed } then have "finite {N. (T^^N) x ∈ A}" by (metis (no_types, lifting) infinite_nat_iff_unbounded mem_Collect_eq not_less) moreover have "infinite {N. (T^^N) x ∈ A}" using recurrent_subset_infty_inf_returns assms(1) by auto ultimately show False by auto qed lemma recurrent_subset_of_recurrent_subset: "recurrent_subset_infty(recurrent_subset_infty A) = recurrent_subset_infty A" proof show "recurrent_subset_infty (recurrent_subset_infty A) ⊆ recurrent_subset_infty A" using recurrent_subset_incl(2)[of A] recurrent_subset_rel_incl(2) by auto show "recurrent_subset_infty A ⊆ recurrent_subset_infty (recurrent_subset_infty A)" using recurrent_subset_infty_returns recurrent_subset_infty_inf_returns by (metis (no_types, lifting) Collect_cong subsetI) qed text ‹The Poincare recurrence theorem states that almost every point of $A$ returns (infinitely often) to $A$, i.e., the recurrent and infinitely recurrent subsets of $A$ coincide almost everywhere with $A$. This is essentially trivial in conservative systems, as it is a reformulation of the definition of conservativity. (What is not trivial, and has been proved above, is that it is true in finite measure preserving systems, i.e., finite measure preserving systems are automatically conservative.)› theorem (in conservative) Poincare_recurrence_thm: assumes [measurable]: "A ∈ sets M" shows "A - recurrent_subset A ∈ null_sets M" "A - recurrent_subset_infty A ∈ null_sets M" "A Δ recurrent_subset A ∈ null_sets M" "A Δ recurrent_subset_infty A ∈ null_sets M" "emeasure M (recurrent_subset A) = emeasure M A" "emeasure M (recurrent_subset_infty A) = emeasure M A" "AE x ∈ A in M. x ∈ recurrent_subset_infty A" proof - define B where "B = {x ∈ A. ∀ n∈{1..}. (T^^n) x ∈ (space M - A)}" have rs: "recurrent_subset A = A - B" by (auto simp add: B_def recurrent_subset_def) (meson Tn_meas assms measurable_space sets.sets_into_space subsetCE) then have *: "A - recurrent_subset A = B" using B_def by blast have "B ∈ null_sets M" by (rule disjoint_then_null, auto simp add: B_def) then show "A - recurrent_subset A ∈ null_sets M" using * by simp then have *: "(⋃n. (T^^n)--`(A-recurrent_subset A)) ∈ null_sets M" using T_quasi_preserves_null2(2) by blast have "recurrent_subset_infty A = recurrent_subset_infty A ∩ space M" using sets.sets_into_space by auto also have "... = A ∩ space M - (⋃n. (T^^n)-`(A-recurrent_subset A) ∩ space M)" unfolding recurrent_subset_infty_def by blast also have "... = A - (⋃n. (T^^n)--`(A-recurrent_subset A))" unfolding vimage_restr_def using sets.sets_into_space by auto finally have **: "recurrent_subset_infty A = A - (⋃n. (T ^^ n) --` (A - recurrent_subset A))" . then have "A - recurrent_subset_infty A ⊆ (⋃n. (T^^n)--`(A-recurrent_subset A))" by auto with * ** show "A - recurrent_subset_infty A ∈ null_sets M" by (simp add: Diff_Diff_Int null_set_Int1) have "A Δ recurrent_subset A = A - recurrent_subset A" using recurrent_subset_incl(1)[of A] by blast then show "A Δ recurrent_subset A ∈ null_sets M" using ‹A - recurrent_subset A ∈ null_sets M› by auto then show "emeasure M (recurrent_subset A) = emeasure M A" by (rule Delta_null_same_emeasure[symmetric], auto) have "A Δ recurrent_subset_infty A = A - recurrent_subset_infty A" using recurrent_subset_incl(2)[of A] by blast then show "A Δ recurrent_subset_infty A ∈ null_sets M" using ‹A - recurrent_subset_infty A ∈ null_sets M› by auto then show "emeasure M (recurrent_subset_infty A) = emeasure M A" by (rule Delta_null_same_emeasure[symmetric], auto) show "AE x∈A in M. x ∈ recurrent_subset_infty A" unfolding eventually_ae_filter by (metis (no_types, lifting) DiffI ‹A - recurrent_subset_infty A ∈ null_sets M› mem_Collect_eq subsetI) qed text ‹A convenient way to use conservativity is given in the following theorem: if $T$ is conservative, then the series $\sum_n f(T^n x)$ is infinite for almost every $x$ with $f x > 0$. When $f$ is an indicator function, this is the fact that, starting from $B$, one returns infinitely many times to $B$ almost surely. The general case follows by approximating $f$ from below by constants time indicators.› theorem (in conservative) recurrence_series_infinite: fixes f::"'a ⇒ ennreal" assumes [measurable]: "f ∈ borel_measurable M" shows "AE x in M. f x > 0 ⟶ (∑n. f ((T^^n) x)) = ∞" proof - have *: "AE x in M. f x > epsilon ⟶ (∑n. f ((T^^n) x)) = ⊤" if "epsilon > 0" for epsilon proof - define B where "B = {x ∈ space M. f x > epsilon}" have [measurable]: "B ∈ sets M" unfolding B_def by auto have "(∑n. f ((T^^n) x)) = ∞" if "x ∈ recurrent_subset_infty B" for x proof - have "∞ = epsilon * ∞" using ‹epsilon > 0› ennreal_mult_top by auto also have "... = epsilon * (∑n. indicator B ((T^^n) x))" using recurrent_subset_infty_series_infinite[OF that] by simp also have "... = (∑n. epsilon * indicator B ((T^^n) x))" by auto also have "... ≤ (∑n. f ((T^^n) x))" apply (rule suminf_le) unfolding indicator_def B_def by auto finally show ?thesis by (simp add: dual_order.antisym) qed moreover have "AE x in M. f x > epsilon ⟶ x ∈ recurrent_subset_infty B" using Poincare_recurrence_thm(7)[OF ‹B ∈ sets M›] unfolding B_def by auto ultimately show ?thesis by auto qed have "∃u::(nat ⇒ ennreal). (∀n. u n > 0) ∧ u ⇢ 0" by (meson approx_from_above_dense_linorder ex_gt_or_lt gr_implies_not_zero) then obtain u::"nat ⇒ ennreal" where u: "⋀n. u n > 0" "u ⇢ 0" by auto have "AE x in M. (∀n::nat. (f x > u n ⟶ (∑n. f ((T^^n) x)) = ⊤))" unfolding AE_all_countable using u by (auto intro!: *) moreover have "f x > 0 ⟶ (∑n. f ((T^^n) x)) = ∞" if "(∀n::nat. (f x > u n ⟶ (∑n. f ((T^^n) x)) = ⊤))" for x proof (auto) assume "f x > 0" obtain n where "u n < f x" using order_tendstoD(2)[OF u(2) ‹f x > 0›] eventually_False_sequentially eventually_mono by blast then show "(∑n. f ((T^^n) x)) = ⊤" using that by auto qed ultimately show ?thesis by auto qed subsection ‹The first return time› text ‹The first return time to a set $A$ under the dynamics $T$ is the smallest integer $n$ such that $T^n(x) \in A$. The first return time is only well defined on the recurrent subset of $A$, elsewhere we set it to $0$ for definiteness. We can partition $A$ according to the value of the return time on it, thus defining the return partition of $A$.› definition return_time_function::"'a set ⇒ ('a ⇒ nat)" where "return_time_function A x = ( if (x ∈ recurrent_subset A) then (Inf {n::nat∈{1..}. (T^^n) x ∈ A}) else 0)" definition return_partition::"'a set ⇒ nat ⇒ 'a set" where "return_partition A k = A ∩ (T^^k)--`A - (⋃i∈{0<..<k}. (T^^i)--`A)" text ‹Basic properties of the return partition.› lemma return_partition_basics: assumes A_meas [measurable]: "A ∈ sets M" shows [measurable]: "return_partition A n ∈ sets M" and "disjoint_family (λn. return_partition A (n+1))" "(⋃n. return_partition A (n+1)) = recurrent_subset A" proof - show "return_partition A n ∈ sets M" for n unfolding return_partition_def by auto define B where "B = (λn. A ∩ (T^^(n+1))--`A)" have "return_partition A (n+1) = B n -(⋃i∈{0..<n}. B i)" for n unfolding return_partition_def B_def by (auto) (auto simp add: less_Suc_eq_0_disj) then have *: "⋀n. return_partition A (n+1) = disjointed B n" using disjointed_def[of B] by simp then show "disjoint_family (λn. return_partition A (n+1))" using disjoint_family_disjointed by simp have "A ∩ (T^^n)-`A = A ∩ (T^^n)--`A" for n using sets.sets_into_space[OF A_meas] by auto then have "recurrent_subset A = (⋃n∈ {1..}. A ∩ (T^^n)--`A)" unfolding recurrent_subset_def by simp also have "... = (⋃n. B n)" by (simp add: B_def atLeast_Suc_greaterThan greaterThan_0) also have "... = (⋃n. return_partition A (n+1))" using * UN_disjointed_eq[of B] by simp finally show "(⋃n. return_partition A (n+1)) = recurrent_subset A" by simp qed text ‹Basic properties of the return time, relationship with the return partition.› lemma return_time0: "(return_time_function A)-`{0} = UNIV - recurrent_subset A" proof (auto) fix x assume *: "x ∈ recurrent_subset A" "return_time_function A x = 0" define K where "K = {n::nat∈{1..}. (T^^n) x ∈ A}" have **: "return_time_function A x = Inf K" using K_def return_time_function_def * by simp have "K ≠ {}" using K_def recurrent_subset_def * by auto moreover have "0 ∉ K" using K_def by auto ultimately have "Inf K >0" by (metis (no_types, lifting) K_def One_nat_def atLeast_iff cInf_lessD mem_Collect_eq neq0_conv not_le zero_less_Suc) then have "return_time_function A x > 0" using ** by simp then show "False" using * by simp qed (auto simp add: return_time_function_def) lemma return_time_n: assumes [measurable]: "A ∈ sets M" shows "(return_time_function A)-`{Suc n} = return_partition A (Suc n)" proof (auto) fix x assume *: "return_time_function A x = Suc n" then have rx: "x ∈ recurrent_subset A" using return_time_function_def by (auto, meson Zero_not_Suc) define K where "K = {i∈{1..}. (T^^i) x ∈ A}" have "return_time_function A x = Inf K" using return_time_function_def rx K_def by auto then have "Inf K = Suc n" using * by simp moreover have "K ≠ {}" using rx recurrent_subset_def K_def by auto ultimately have "Suc n ∈ K" using Inf_nat_def1[of K] by simp then have "(T^^(Suc n))x ∈ A" using K_def by auto then have a: "x ∈ A ∩ (T^^(Suc n))--`A" using rx recurrent_subset_incl[of A] sets.sets_into_space[OF assms] by auto have "⋀i. i∈{1..<Suc n} ⟹ i ∉ K" using cInf_lower ‹Inf K = Suc n› by force then have "⋀i. i∈{1..<Suc n} ⟹ x ∉ (T^^i)--`A" using K_def by auto then have "x ∉ (⋃i∈{1..<Suc n}. (T^^i)--`A)" by auto then show "x ∈ return_partition A (Suc n)" using a return_partition_def by simp next fix x assume *: "x ∈ return_partition A (Suc n)" then have a: "x ∈ space M" unfolding return_partition_def using vimage_restr_def by blast define K where "K = {i::nat∈{1..}. (T^^i) x ∈ A}" have "Inf K = Suc n" apply (rule cInf_eq_minimum) using * by (auto simp add: a assms K_def return_partition_def) have "x ∈ recurrent_subset A" using * return_partition_basics(3)[OF assms] by auto then show "return_time_function A x = Suc n" using return_time_function_def K_def ‹Inf K = Suc n› by auto qed text ‹The return time is measurable.› lemma return_time_function_meas [measurable]: assumes [measurable]: "A ∈ sets M" shows "return_time_function A ∈ measurable M (count_space UNIV)" "return_time_function A ∈ borel_measurable M" proof - have "(return_time_function A)-`{n} ∩ space M ∈ sets M" for n proof (cases "n = 0") case True then show ?thesis using return_time0 recurrent_subset_meas[OF assms] by auto next case False show ?thesis using return_time_n return_partition_basics(1)[OF assms] not0_implies_Suc[OF False] by auto qed then show "return_time_function A ∈ measurable M (count_space UNIV)" by (simp add: measurable_count_space_eq2_countable assms) then show "return_time_function A ∈ borel_measurable M" using measurable_cong_sets sets_borel_eq_count_space by blast qed text ‹A close cousin of the return time and the return partition is the first entrance set: we partition the space according to the first positive time where a point enters $A$.› definition first_entrance_set::"'a set ⇒ nat ⇒ 'a set" where "first_entrance_set A n = (T^^n) --` A - (⋃ i<n. (T^^i)--`A)" lemma first_entrance_meas [measurable]: assumes [measurable]: "A ∈ sets M" shows "first_entrance_set A n ∈ sets M" unfolding first_entrance_set_def by measurable lemma first_entrance_disjoint: "disjoint_family (first_entrance_set A)" proof - have "first_entrance_set A = disjointed (λi. (T^^i)--`A)" by (auto simp add: disjointed_def first_entrance_set_def) then show ?thesis by (simp add: disjoint_family_disjointed) qed text ‹There is an important dynamical phenomenon: if a point has first entrance time equal to $n$, then their preimages either have first entrance time equal to $n+1$ (these are the preimages not in $A$) or they belong to $A$ and have first return time equal to $n+1$. When $T$ preserves the measure, this gives an inductive control on the measure of the first entrance set, that will be used again and again in the proof of Kac's Formula. We formulate these (simple but extremely useful) facts now.› lemma first_entrance_rec: assumes [measurable]: "A ∈ sets M" shows "first_entrance_set A (Suc n) = T--`(first_entrance_set A n) - A" proof - have A0: "A = (T^^0)--`A" by auto have "first_entrance_set A n = (T^^n) --` A - (⋃ i<n. (T^^i)--`A)" using first_entrance_set_def by simp then have "T--`(first_entrance_set A n) = (T^^(n+1))--`A - (⋃ i<n. (T^^(i+1))--`A)" using T_vrestr_composed(2) ‹A ∈ sets M› by simp then have *: "T--`(first_entrance_set A n) - A = (T^^(n+1))--`A - (A ∪ (⋃ i<n. (T^^(i+1))--`A))" by blast have "(⋃ i<n. (T^^(i+1))--`A) = (⋃ j∈{1..<n+1}. (T^^j)--`A)" by (rule UN_le_add_shift_strict) then have "A ∪ (⋃ i<n. (T^^(i+1))--`A) = (⋃ j∈{0..<n+1}. (T^^j)--`A)" by (metis A0 Un_commute atLeast0LessThan UN_le_eq_Un0_strict) then show ?thesis using * first_entrance_set_def by auto qed lemma return_time_rec: assumes "A ∈ sets M" shows "(return_time_function A)-`{Suc n} = T--`(first_entrance_set A n) ∩ A" proof - have "return_partition A (Suc n) = T--`(first_entrance_set A n) ∩ A" unfolding return_partition_def first_entrance_set_def by (auto simp add: T_vrestr_composed[OF assms]) (auto simp add: less_Suc_eq_0_disj) then show ?thesis using return_time_n[OF assms] by simp qed subsection ‹Local time controls› text ‹The local time is the time that an orbit spends in a given set. Local time controls are basic to all the forthcoming developments.› definition local_time::"'a set ⇒ nat ⇒ 'a ⇒ nat" where "local_time A n x = card {i∈{..<n}. (T^^i) x ∈ A}" lemma local_time_birkhoff: "local_time A n x = birkhoff_sum (indicator A) n x" proof (induction n) case 0 then show ?case unfolding local_time_def birkhoff_sum_def by simp next case (Suc n) have "local_time A (n+1) x = local_time A n x + indicator A ((T^^n) x)" proof (cases) assume *: "(T^^n) x ∈ A" then have "{i∈{..<Suc n}. (T^^i) x ∈ A} = {i∈{..<n}. (T^^i) x ∈ A} ∪ {n}" by auto then have "card {i∈{..<Suc n}. (T^^i) x ∈ A} = card {i∈{..<n}. (T^^i) x ∈ A} + card {n}" using card_Un_disjoint by auto then have "local_time A (n+1) x = local_time A n x + 1" using local_time_def by simp moreover have "indicator A ((T^^n)x) = (1::nat)" using * indicator_def by auto ultimately show ?thesis by simp next assume *: "¬((T^^n) x ∈ A)" then have "{i∈{..<Suc n}. (T^^i) x ∈ A} = {i∈{..<n}. (T^^i) x ∈ A}" using less_Suc_eq by force then have "card {i∈{..<Suc n}. (T^^i) x ∈ A} = card {i∈{..<n}. (T^^i) x ∈ A}" by auto then have "local_time A (n+1) x = local_time A n x" using local_time_def by simp moreover have "indicator A ((T^^n)x) = (0::nat)" using * indicator_def by auto ultimately show ?thesis by simp qed then have "local_time A (n+1) x = birkhoff_sum (indicator A) n x + indicator A ((T^^n) x)" using Suc.IH by auto moreover have "birkhoff_sum (indicator A) (n+1) x = birkhoff_sum (indicator A) n x + indicator A ((T^^n) x)" by (metis birkhoff_sum_cocycle[where ?n = "n" and ?m = "1"] birkhoff_sum_1(2)) ultimately have "local_time A (n+1) x = birkhoff_sum (indicator A) (n+1) x" by metis then show ?case by (metis Suc_eq_plus1) qed lemma local_time_meas [measurable]: assumes [measurable]: "A ∈ sets M" shows "local_time A n ∈ borel_measurable M" unfolding local_time_birkhoff by auto lemma local_time_cocycle: "local_time A n x + local_time A m ((T^^n)x) = local_time A (n+m) x" by (metis local_time_birkhoff birkhoff_sum_cocycle) lemma local_time_incseq: "incseq (λn. local_time A n x)" using local_time_cocycle incseq_def by (metis le_iff_add) lemma local_time_Suc: "local_time A (n+1) x = local_time A n x + indicator A ((T^^n)x)" by (metis local_time_birkhoff birkhoff_sum_cocycle birkhoff_sum_1(2)) text ‹The local time is bounded by $n$: at most, one returns to $A$ all the time!› lemma local_time_bound: "local_time A n x ≤ n" proof - have "card {i∈{..<n}. (T^^i) x ∈ A} ≤ card {..<n}" by (rule card_mono, auto) then show ?thesis unfolding local_time_def by auto qed text ‹The fact that local times are unbounded will be the main technical tool in the proof of recurrence results or Kac formula below. In this direction, we prove more and more general results in the lemmas below. We show that, in $T^{-n}(A)$, the number of visits to $A$ tends to infinity in measure, when $A$ has finite measure. In other words, the points in $T^{-n}(A)$ with local time $<k$ have a measure tending to $0$ with $k$. The argument, by induction on $k$, goes as follows. Consider the last return to $A$ before time $n$, say at time $n-i$. It lands in the set $S_i$ with retun time $i$. We get $T^{-n} A \subseteq \bigcup_{n<N} T^{-(n-i)}S_i \cup R$, where the union is disjoint and $R$ is a set of measure $\mu(T^{-n}A) - \sum_{n<N} \mu(T^{-(n-i)}S_i) = \mu(A) -\sum_{n<N} \mu(S_i)$, which tends to $0$ with $N$ and that we may therefore discard. A point with local time $<k$ at time $n$ in $T^{-n}A$ is then a point with local time $<k-1$ at time $n-i$ in $T^{-(n-i)}S_i \subseteq T^{-(n-i)}A$. Hence, we may conclude by the induction assumption that this has small measure.› lemma (in conservative_mpt) local_time_unbounded1: assumes A_meas [measurable]: "A ∈ sets M" and fin: "emeasure M A < ∞" shows "(λn. emeasure M {x ∈ (T^^n)--`A. local_time A n x < k}) ⇢ 0" proof (induction k) case 0 have "{x ∈ (T^^n)--`A. local_time A n x < 0} = {}" for n by simp then show ?case by simp next case (Suc k) define K where "K = (λp n. {x ∈ (T^^n)--`A. local_time A n x < p})" have K_meas [measurable]: "K p n ∈ sets M" for n p unfolding K_def by measurable show ?case proof (rule tendsto_zero_ennreal) fix e :: real assume "0 < e" define e2 where "e2 = e/3" have "e2 > 0" using e2_def ‹e>0› by simp have "(∑n. emeasure M (return_partition A (n+1))) = emeasure M ((⋃n. return_partition A (n + 1)))" apply (rule suminf_emeasure) using return_partition_basics[OF A_meas] by auto also have "... = emeasure M (recurrent_subset A)" using return_partition_basics(3)[OF A_meas] by simp also have "... = emeasure M A" by (metis A_meas double_diff emeasure_Diff_null_set order_refl Poincare_recurrence_thm(1)[OF A_meas] recurrent_subset_incl(1)) finally have "(∑n. emeasure M (return_partition A (n+1))) = emeasure M A" by simp moreover have "summable (λn. emeasure M (return_partition A (n+1)))" by simp ultimately have "(λN. (∑n<N. emeasure M (return_partition A (n+1)))) ⇢ emeasure M A" unfolding sums_def[symmetric] sums_iff by simp then have "(λN. (∑n<N. emeasure M (return_partition A (n+1))) + e2) ⇢ emeasure M A + e2" by (intro tendsto_add) auto moreover have "emeasure M A < emeasure M A + e2" using ‹emeasure M A < ∞› ‹0 < e2› by auto ultimately have "eventually (λN. (∑n<N. emeasure M (return_partition A (n+1))) + e2 > emeasure M A) sequentially" by (simp add: order_tendsto_iff) then obtain N where "N>0" and largeM: "(∑n<N. emeasure M (return_partition A (n+1))) + e2 > emeasure M A" by (metis (no_types, lifting) add.commute add_Suc_right eventually_at_top_linorder le_add2 zero_less_Suc) have upper: "emeasure M (K (Suc k) n) ≤ e2 + (∑i<N. emeasure M (K k (n-i-1)))" if "n>N" for n proof - define B where "B = (λi. (T^^(n-i-1))--`(return_partition A (i+1)))" have B_meas [measurable]: "B i ∈ sets M" for i unfolding B_def by measurable have disj_B: "disjoint_family_on B {..<N}" proof - have "B i ∩ B j = {}" if "i∈{..<N}" "j∈{..<N}" "i < j" for i j proof - have "n > i" "n>j" using ‹n>N› that by auto let ?k = "j-i" have "x ∉ B i" if "x ∈ B j" for x proof - have "(T^^(n-j-1)) x ∈ return_partition A (j+1)" using B_def that by auto moreover have "?k>0" using ‹i < j› by simp moreover have "?k < j+1" by simp ultimately have "(T^^(n-j-1)) x ∉ (T^^?k)--`A" using return_partition_def by auto then have "x ∉ (T^^(n-j-1))--` (T^^?k)--`A" by auto then have "x ∉ (T^^(n-j-1 + ?k))--`A" using T_vrestr_composed[OF A_meas] by simp then have "x ∉ (T^^(n-i-1))--`A" using ‹i<j› ‹n>j› by auto then have "x ∉ (T^^(n-i-1))--` (return_partition A (i+1))" using return_partition_def by auto then show "x ∉ B i" using B_def by auto qed then show "B i ∩ B j = {}" by auto qed then have "⋀i j. i∈{..<N} ⟹ j∈{..<N} ⟹ i ≠ j ⟹ B i ∩ B j = {}" by (metis Int_commute linorder_neqE_nat) then show ?thesis unfolding disjoint_family_on_def by auto qed have incl_B: "B i ⊆ (T^^n)--`A" if "i ∈ {..<N}" for i proof - have "n > i" using ‹n>N› that by auto have "B i ⊆ (T^^(n-i-1))--` (T^^(i+1))--` A" using B_def return_partition_def by auto then show "B i ⊆ (T^^n)--`A" using T_vrestr_composed(1)[OF A_meas, of "n-i-1", of "i+1"] ‹n>i› by auto qed define R where "R = (T^^n)--`A - (⋃i ∈ {..<N}. B i)" have [measurable]: "R ∈ sets M" unfolding R_def by measurable have dec_n: "(T^^n)--`A = R ∪ (⋃i ∈ {..<N}. B i)" using R_def incl_B by blast have small_R: "emeasure M R < e2" proof - have "R ∩ (⋃i ∈ {..<N}. B i) = {}" using R_def by blast then have "emeasure M ((T^^n)--`A) = emeasure M R + emeasure M (⋃i ∈ {..<N}. B i)" using plus_emeasure[of R, of M, of "⋃i ∈ {..<N}. B i"] dec_n by auto moreover have "emeasure M (⋃i ∈ {..<N}. B i) = (∑i ∈ {..<N}. emeasure M (B i))" by (intro disj_B sum_emeasure[symmetric], auto) ultimately have "emeasure M ((T^^n)--`A) = emeasure M R + (∑i ∈ {..<N}. emeasure M (B i))" by simp moreover have "emeasure M ((T^^n)--`A) = emeasure M A" using T_vrestr_same_emeasure(2)[OF A_meas] by simp moreover have "⋀i. emeasure M (B i) = emeasure M (return_partition A (i+1))" using T_vrestr_same_emeasure(2) B_def return_partition_basics(1)[OF A_meas] by simp ultimately have a: "emeasure M A = emeasure M R + (∑i ∈ {..<N}. emeasure M (return_partition A (i+1)))" by simp moreover have b: "(∑i ∈ {..<N}. emeasure M (return_partition A (i+1))) ≠ ∞" using fin by (simp add: a less_top) ultimately show ?thesis using largeM fin b by simp qed have "K (Suc k) n ⊆ R ∪ (⋃i<N. K k (n-i-1))" proof fix x assume a: "x ∈ K (Suc k) n" show "x ∈ R ∪ (⋃i<N. K k (n-i-1))" proof (cases) assume "¬(x ∈ R)" have "x ∈ (T^^n)--`A" using a K_def by simp then have "x∈ (⋃i ∈ {..<N}. B i)" using dec_n ‹¬(x ∈ R)› by simp then obtain i where "i∈{..<N}" "x ∈ B i" by auto then have "n>i" using ‹n>N› by auto then have "(T^^(n-i-1)) x ∈ return_partition A (i+1)" using B_def ‹x ∈ B i› by auto then have i: "(T^^(n-i-1)) x ∈ A" using return_partition_def by auto then have "indicator A ((T^^(n-i-1)) x) = (1::nat)" by auto then have "local_time A (n-i) x = local_time A (n-i-1) x + 1" by (metis Suc_diff_Suc Suc_eq_plus1 diff_diff_add local_time_Suc[of A, of "n-i-1"] ‹n>i›) then have "local_time A (n-i) x > local_time A (n-i-1) x" by simp moreover have "local_time A n x ≥ local_time A (n-i) x" using local_time_incseq by (metis ‹i < n› le_add_diff_inverse2 less_or_eq_imp_le local_time_cocycle le_iff_add) ultimately have "local_time A n x > local_time A (n-i-1) x" by simp moreover have "local_time A n x < Suc k" using a K_def by simp ultimately have *: "local_time A (n-i-1) x < k" by simp have "x ∈ space M" using ‹x ∈ (T^^n)--`A› by auto then have "x ∈ (T^^(n-i-1))--`A" using i A_meas vimage_restr_def by (metis IntI sets.Int_space_eq2 vimageI) then have "x ∈ K k (n-i-1)" using * K_def by blast then show ?thesis using ‹i∈{..<N}› by auto qed (simp) qed then have "emeasure M (K (Suc k) n) ≤ emeasure M (R ∪ (⋃i<N. K k (n-i-1)))" by (intro emeasure_mono, auto) also have "... ≤ emeasure M R + emeasure M (⋃i<N. K k (n-i-1))" by (rule emeasure_subadditive, auto) also have "... ≤ emeasure M R + (∑i<N. emeasure M (K k (n-i-1)))" by (metis add_left_mono image_subset_iff emeasure_subadditive_finite[where ?A = "λi. K k (n-i-1)" and ?I = "{..<N}", OF finite_lessThan[of N]] K_meas) also have "... ≤ e2 + (∑i<N. emeasure M (K k (n-i-1)))" using small_R by (auto intro!: add_right_mono) finally show "emeasure M (K (Suc k) n) ≤ e2 + (∑i<N. emeasure M (K k (n-i-1)))" . qed have "(λn. (∑i∈{..<N}. emeasure M (K k (n-i-1)))) ⇢ (∑i∈{..<N}. 0)" apply (intro tendsto_intros seq_offset_neg) using Suc.IH K_def by simp then have "eventually (λn. (∑i∈{..<N}. emeasure M (K k (n-i-1))) < e2) sequentially" using ‹e2 > 0› by (simp add: order_tendsto_iff) then obtain N2 where N2bound: "⋀n. n > N2 ⟹ (∑i∈{..<N}. emeasure M (K k (n-i-1))) < e2" by (meson eventually_at_top_dense) define N3 where "N3 = max N N2" have "emeasure M (K (Suc k) n) < e" if "n > N3" for n proof - have "n>N2" "n > N" using N3_def that by auto then have "emeasure M (K (Suc k) n) ≤ ennreal e2 + (∑i∈{..<N}. emeasure M (K k (n-i-1)))" using upper by simp also have "... ≤ ennreal e2 + ennreal e2" using N2bound[OF ‹n > N2›] less_imp_le by auto also have "... < e" using e2_def ‹e > 0› by (auto simp add: ennreal_plus[symmetric] simp del: ennreal_plus intro!: ennreal_lessI) ultimately show "emeasure M (K (Suc k) n) < e" using le_less_trans by blast qed then show "∀⇩_{F}x in sequentially. emeasure M {xa ∈ (T ^^ x) --` A. local_time A x xa < Suc k} < ennreal e" unfolding K_def by (auto simp: eventually_at_top_dense intro!: exI[of _ N3]) qed qed text ‹We deduce that local times to a set $B$ also tend to infinity on $T^{-n}A$ if $B$ is related to $A$, i.e., if points in $A$ have some iterate in $B$. This is clearly a necessary condition for the lemmas to hold: otherwise, points of $A$ that never visit $B$ have a local time equal to $B$ equal to $0$, and so do all their preimages. The lemmas are readily reduced to the previous one on the local time to $A$, since if one visits $A$ then one visits $B$ in finite time by assumption (uniformly bounded in the first lemma, uniformly bounded on a set of large measure in the second lemma).› lemma (in conservative_mpt) local_time_unbounded2: assumes A_meas [measurable]: "A ∈ sets M" and fin: "emeasure M A < ∞" and incl: "A ⊆ (T^^i)--`B" shows "(λn. emeasure M {x ∈ (T^^n)--`A. local_time B n x < k}) ⇢ 0" proof - have "emeasure M {x ∈ (T^^n)--`A. local_time B n x < k} ≤ emeasure M {x ∈ (T^^n)--`A. local_time A n x < k + i}" if "n > i" for n proof - have "local_time A n x ≤ local_time B n x + i" for x proof - have "local_time B n x ≥ local_time A (n-i) x" proof - define KA where "KA = {t ∈ {0..<n-i}. (T^^t) x ∈ A}" define KB where "KB = {t ∈ {0..<n}. (T^^t) x ∈ B}" then have "KB ⊆ {0..<n}" by auto then have "finite KB" using finite_lessThan[of n] finite_subset by auto let ?g = "λt. t + i" have "⋀t. t ∈ KA ⟹ ?g t ∈ KB" proof - fix t assume "t ∈ KA" then have "(T^^t) x ∈ A" using KA_def by simp then have "(T^^i) ((T^^t) x) ∈ B" using incl by auto then have "(T^^(t+i)) x ∈ B" by (simp add: funpow_add add.commute) moreover have "t+i < n" using ‹t ∈ KA› KA_def ‹n > i› by auto ultimately show "?g t ∈ KB" unfolding KB_def by simp qed then have "?g`KA ⊆ KB" by auto moreover have "inj_on ?g KA" by simp ultimately have "card KB ≥ card KA" using card_inj_on_le[where ?f = "?g" and ?A = KA and ?B = KB] ‹finite KB› by simp then show ?thesis using KA_def KB_def local_time_def by simp qed moreover have "i ≥ local_time A i ((T^^(n-i))x)" using local_time_bound by auto ultimately show "local_time B n x + i ≥ local_time A n x" using local_time_cocycle[where ?n = "n-i" and ?m = i and ?x = x and ?A = A] ‹n>i› by auto qed then have "local_time B n x < k ⟹ local_time A n x < k + i" for x by (meson add_le_cancel_right le_trans not_less) then show ?thesis by (intro emeasure_mono, auto) qed then have "eventually (λn. emeasure M {x ∈ (T^^n)--`A. local_time B n x < k} ≤ emeasure M {x ∈ (T^^n)--`A. local_time A n x < k + i}) sequentially" using eventually_at_top_dense by blast from tendsto_sandwich[OF _ this tendsto_const local_time_unbounded1[OF A_meas fin, of "k+i"]] show ?thesis by auto qed lemma (in conservative_mpt) local_time_unbounded3: assumes A_meas[measurable]: "A ∈ sets M" and B_meas[measurable]: "B ∈ sets M" and fin: "emeasure M A < ∞" and incl: "A - (⋃i. (T^^i)--`B) ∈ null_sets M" shows "(λn. emeasure M {x ∈ (T^^n)--`A. local_time B n x < k}) ⇢ 0" proof - define R where "R = A - (⋃i. (T^^i)--`B)" have R_meas[measurable]: "R ∈ sets M" by (simp add: A_meas B_meas T_vrestr_meas(2)[OF B_meas] R_def countable_Un_Int(1) sets.Diff) have "emeasure M R = 0" using incl R_def by auto define A2 where "A2 = A - R" have A2_meas [measurable]: "A2 ∈ sets M" unfolding A2_def by auto have meq: "emeasure M A2 = emeasure M A" using ‹emeasure M R = 0› unfolding A2_def by (subst emeasure_Diff) (auto simp: R_def) then have A2_fin: "emeasure M A2 < ∞" using fin by auto define K where "K = (λN. A2 ∩ (⋃i<N. (T^^i)--`B))" have K_meas [measurable]: "K N ∈ sets M" for N unfolding K_def by auto have K_incl: "⋀N. K N ⊆ A" using K_def A2_def by blast have "(⋃N. K N) = A2" using A2_def R_def K_def by blast moreover have "incseq K" unfolding K_def incseq_def by fastforce ultimately have "(λN. emeasure M (K N)) ⇢ emeasure M A2" by (auto intro: Lim_emeasure_incseq) then have conv: "(λN. emeasure M (K N)) ⇢ emeasure M A" using meq by simp define Bad where "Bad = (λU n. {x ∈ (T^^n)--`U. local_time B n x < k})" define Bad0 where "Bad0 = (λn. {x ∈ space M. local_time B n x < k})" have Bad0_meas [measurable]: "Bad0 n ∈ sets M" for n unfolding Bad0_def by auto have Bad_inter: "⋀U n. Bad U n = (T^^n)--`U ∩ Bad0 n" unfolding Bad_def Bad0_def by auto have Bad_meas [measurable]: "⋀U n. U ∈ sets M ⟹ Bad U n ∈ sets M" unfolding Bad_def by auto show ?thesis proof (rule tendsto_zero_ennreal) fix e::real assume "e > 0" define e2 where "e2 = e/3" then have "e2 > 0" using ‹e>0› by simp then have "ennreal e2 > 0" by simp have "(λN. emeasure M (K N) + e2) ⇢ emeasure M A + e2" using conv by (intro tendsto_add) auto moreover have "emeasure M A < emeasure M A + e2" using fin ‹e2 > 0› by simp ultimately have "eventually (λN. emeasure M (K N) + e2 > emeasure M A) sequentially" by (simp add: order_tendsto_iff) then obtain N where "N>0" and largeK: "emeasure M (K N) + e2 > emeasure M A" by (metis (no_types, lifting) add.commute add_Suc_right eventually_at_top_linorder le_add2 zero_less_Suc) define S where "S = A - (K N)" have S_meas [measurable]: "S ∈ sets M" using A_meas K_meas S_def by simp have "emeasure M A = emeasure M (K N) + emeasure M S" by (metis Diff_disjoint Diff_partition plus_emeasure[OF K_meas[of N], OF S_meas] S_def K_incl[of N]) then have S_small: "emeasure M S < e2" using largeK fin by simp have A_incl: "A ⊆ S ∪ (⋃i<N. A2 ∩ (T^^i)--`B)" using S_def K_def by auto define L where "L = (λi. A2 ∩ (T^^i)--`B)" have L_meas [measurable]: "L i ∈ sets M" for i unfolding L_def by auto have "⋀i. L i ⊆ A2" using L_def by simp then have L_fin: "emeasure M (L i) < ∞" for i using emeasure_mono[of "L i" A2 M] A2_meas A2_fin by simp have "⋀i. L i ⊆ (T^^i)--`B" using L_def by auto then have a: "⋀i. (λn. emeasure M (Bad (L i) n)) ⇢ 0" unfolding Bad_def using local_time_unbounded2[OF L_meas, OF L_fin] by blast have "(λn. (∑i<N. emeasure M (Bad (L i) n))) ⇢ 0" using tendsto_sum[OF a] by auto then have "eventually (λn. (∑i<N. emeasure M (Bad (L i) n)) < e2) sequentially" using ‹ennreal e2 > 0› order_tendsto_iff by metis then obtain N2 where *: "⋀n. n > N2 ⟹ (∑i<N. emeasure M (Bad (L i) n)) < e2" by (auto simp add: eventually_at_top_dense) have "emeasure M (Bad A n) < e" if "n > N2" for n proof - have "emeasure M (Bad S n) ≤ emeasure M ((T^^n)--`S)" apply (rule emeasure_mono) unfolding Bad_def by auto also have "... = emeasure M S" using T_vrestr_same_emeasure(2) by simp also have "... ≤ e2" using S_small by simp finally have SBad_small: "emeasure M (Bad S n) ≤ e2" by simp have "(T^^n)--`A ⊆ (T^^n)--`S ∪ (⋃i<N. (T^^n)--`(L i))" using A_incl unfolding L_def by fastforce then have I: "Bad A n ⊆ Bad S n ∪ (⋃i<N. Bad (L i) n)" using Bad_inter by force have "emeasure M (Bad A n) ≤ emeasure M (Bad S n ∪ (⋃i<N. Bad (L i) n))" by (rule emeasure_mono[OF I], measurable) also have "... ≤ emeasure M (Bad S n) + emeasure M (⋃i<N. Bad (L i) n)" by (intro emeasure_subadditive countable_Un_Int(1), auto) also have "... ≤ emeasure M (Bad S n) + (∑i<N. emeasure M (Bad (L i) n))" by (simp add: add_left_mono image_subset_iff Bad_meas[OF L_meas] emeasure_subadditive_finite[OF finite_lessThan[of N], where ?A = "λi. Bad (L i) n"]) also have "... ≤ ennreal e2 + ennreal e2" using SBad_small less_imp_le[OF *[OF ‹n > N2›]] by (rule add_mono) also have "... < e" using e2_def ‹e>0› by (simp del: ennreal_plus add: ennreal_plus[symmetric] ennreal_lessI) finally show "emeasure M (Bad A n) < e" by simp qed then show "∀⇩_{F}x in sequentially. emeasure M {xa ∈ (T ^^ x) --` A. local_time B x xa < k} < e" unfolding eventually_at_top_dense Bad_def by auto qed qed subsection ‹The induced map› text ‹The map induced by $T$ on a set $A$ is obtained by iterating $T$ until one lands again in $A$. (Outside of $A$, we take the identity for definiteness.) It has very nice properties: if $T$ is conservative, then the induced map $T_A$ also is. If $T$ is measure preserving, then so is $T_A$. (In particular, even if $T$ preserves an infinite measure, $T_A$ is a probability preserving map if $A$ has measure $1$ -- this makes it possible to prove some statements in infinite measure by using results in finite measure systems). If $T$ is invertible, then so is $T_A$. We prove all these properties in this paragraph.› definition induced_map::"'a set ⇒ ('a ⇒ 'a)" where "induced_map A = (λ x. (T^^(return_time_function A x)) x)" text ‹The set $A$ is stabilized by the induced map.› lemma induced_map_stabilizes_A: "x ∈ A ⟷ induced_map A x ∈ A" proof (rule equiv_neg) fix x assume "x ∈ A" show "induced_map A x ∈ A" proof (cases) assume "x ∉ recurrent_subset A" then have "induced_map A x = x" using induced_map_def return_time_function_def by simp then show ?thesis using ‹x ∈ A› by simp next assume H: "¬(x ∉ recurrent_subset A)" define K where "K = {n∈{1..}. (T^^n) x ∈ A}" have "K ≠ {}" using H recurrent_subset_def K_def by blast moreover have "return_time_function A x = Inf K" using return_time_function_def K_def H by simp ultimately have "return_time_function A x ∈ K" using Inf_nat_def1 by simp then show ?thesis unfolding induced_map_def K_def by blast qed next fix x assume "x ∉ A" then have "x ∉ recurrent_subset A" using recurrent_subset_def by simp then have "induced_map A x = x" using induced_map_def return_time_function_def by simp then show "induced_map A x ∉ A" using ‹x ∉ A› by simp qed lemma induced_map_iterates_stabilize_A: assumes "x ∈ A" shows "((induced_map A)^^n) x ∈ A" proof (induction n) case 0 show ?case using ‹x ∈ A› by auto next case (Suc n) have "((induced_map A)^^(Suc n)) x = (induced_map A) (((induced_map A)^^n) x)" by auto then show ?case using Suc.IH induced_map_stabilizes_A by auto qed lemma induced_map_meas [measurable]: assumes [measurable]: "A ∈ sets M" shows "induced_map A ∈ measurable M M" unfolding induced_map_def by auto text ‹The iterates of the induced map are given by a power of the original map, where the power is the Birkhoff sum (for the induced map) of the first return time. This is obvious, but useful.› lemma induced_map_iterates: "((induced_map A)^^n) x = (T^^(∑i < n. return_time_function A ((induced_map A ^^i) x))) x" proof (induction n) case 0 show ?case by auto next case (Suc n) have "((induced_map A)^^(n+1)) x = induced_map A (((induced_map A)^^n) x)" by (simp add: funpow_add) also have "... = (T^^(return_time_function A (((induced_map A)^^n) x))) (((induced_map A)^^n) x)" using induced_map_def by auto also have "... = (T^^(return_time_function A (((induced_map A)^^n) x))) ((T^^(∑i < n. return_time_function A ((induced_map A ^^i) x))) x)" using Suc.IH by auto also have "... = (T^^(return_time_function A (((induced_map A)^^n) x) + (∑i < n. return_time_function A ((induced_map A ^^i) x)))) x" by (simp add: funpow_add) also have "... = (T^^(∑i < Suc n. return_time_function A ((induced_map A ^^i) x))) x" by (simp add: add.commute) finally show ?case by simp qed lemma induced_map_stabilizes_recurrent_infty: assumes "x ∈ recurrent_subset_infty A" shows "((induced_map A)^^n) x ∈ recurrent_subset_infty A" proof - have "x ∈ A" using assms(1) recurrent_subset_incl(2) by auto define R where "R = (∑i < n. return_time_function A ((induced_map A ^^i) x))" have *: "((induced_map A)^^n) x = (T^^R) x" unfolding R_def by (rule induced_map_iterates) moreover have "((induced_map A)^^n) x ∈ A" by (rule induced_map_iterates_stabilize_A, simp add: ‹x ∈ A›) ultimately have "(T^^R) x ∈ A" by simp then show ?thesis using recurrent_subset_infty_returns[OF assms] * by auto qed text ‹If $x \in A$, then its successive returns to $A$ are exactly given by the iterations of the induced map.› lemma induced_map_returns: assumes "x ∈ A" shows "((T^^n) x ∈ A) ⟷ (∃N≤n. n = (∑i<N. return_time_function A ((induced_map A ^^ i) x)))" proof assume "(T^^n) x ∈ A" have "⋀y. y ∈ A ⟹ (T^^n)y ∈ A ⟹ ∃N≤n. n = (∑i<N. return_time_function A (((induced_map A)^^i) y))" for n proof (induction n rule: nat_less_induct) case (1 n) show "∃N≤n. n = (∑i<N. return_time_function A (((induced_map A)^^i) y))" proof (cases) assume "n = 0" then show ?thesis by auto next assume "¬(n = 0)" then have "n > 0" by simp then have y_rec: "y ∈ recurrent_subset A" using ‹y ∈ A› ‹(T^^n) y ∈ A› recurrent_subset_def by auto then have *: "return_time_function A y > 0" by (metis DiffE insert_iff neq0_conv vimage_eq return_time0) define m where "m = return_time_function A y" have "m > 0" using * m_def by simp define K where "K = {t ∈ {1..}. (T ^^ t) y ∈ A}" have "n ∈ K" unfolding K_def using ‹n > 0› ‹(T^^n)y ∈ A› by simp then have "n ≥ Inf K" by (simp add: cInf_lower) moreover have "m = Inf K" unfolding m_def K_def return_time_function_def using y_rec by simp ultimately have "n ≥ m" by simp define z where "z = induced_map A y" have "z ∈ A" using ‹y ∈ A› induced_map_stabilizes_A z_def by simp have "z = (T^^m) y" using induced_map_def y_rec z_def m_def by auto then have "(T^^(n-m)) z = (T^^n) y" using ‹n ≥ m› funpow_add[of "n-m" m T, symmetric] by (metis comp_apply le_add_diff_inverse2) then have "(T^^(n-m)) z ∈ A" using ‹(T^^n) y ∈ A› by simp moreover have "n-m < n" using ‹m > 0› ‹n > 0› by simp ultimately obtain N0 where "N0 ≤ n-m" "n-m = (∑i<N0. return_time_function A (((induced_map A)^^i) z))" using ‹z ∈ A› "1.IH" by blast then have "n-m = (∑i<N0. return_time_function A (((induced_map A)^^i) (induced_map A y)))" using z_def by auto moreover have "⋀i. ((induced_map A)^^i) (induced_map A y) = ((induced_map A)^^(i+1)) y" by (metis Suc_eq_plus1 comp_apply funpow_Suc_right) ultimately have "n-m = (∑i<N0. return_time_function A (((induced_map A)^^(i+1)) y))" by simp then have "n-m = (∑i ∈ {1..<N0+1}. return_time_function A (((induced_map A)^^i) y))" using sum.shift_bounds_nat_ivl[of "λi. return_time_function A (((induced_map A)^^i) y)", of 0, of 1, of N0, symmetric] atLeast0LessThan by auto moreover have "m = (∑i∈{0..<1}. return_time_function A (((induced_map A)^^i) y))" using m_def by simp ultimately have "n = (∑i∈{0..<1}. return_time_function A (((induced_map A)^^i) y)) + (∑i ∈ {1..<N0+1}. return_time_function A (((induced_map A)^^i) y))" using ‹n ≥ m› by simp then have "n = (∑i∈{0..<N0+1}. return_time_function A (((induced_map A)^^i) y))" using le_add2 sum.atLeastLessThan_concat by blast moreover have "N0 + 1 ≤ n" using ‹N0 ≤ n-m› ‹n - m < n› by linarith ultimately show ?thesis by (metis atLeast0LessThan) qed qed then show "∃N≤n. n = (∑i<N. return_time_function A ((induced_map A ^^ i) x))" using ‹x ∈ A› ‹(T^^n) x ∈ A› by simp next assume "∃N≤n. n = (∑i<N. return_time_function A ((induced_map A ^^ i) x))" then obtain N where "n = (∑i<N. return_time_function A ((induced_map A ^^ i) x))" by blast then have "(T^^n) x = ((induced_map A)^^N) x" using induced_map_iterates[of N, of A, of x] by simp then show "(T^^n) x ∈ A" using ‹x ∈ A› induced_map_iterates_stabilize_A by auto qed text ‹If a map is conservative, then the induced map is still conservative. Note that this statement is not true if one replaces the word "conservative" with "qmpt": inducion only works well in conservative settings. For instance, the right translation on $\mathbb{Z}$ is qmpt, but the induced map on $\mathbb{N}$ (again the right translation) is not, since the measure of $\{0\}$ is nonzero, while its preimage, the empty set, has zero measure. To prove conservativity, given a subset $B$ of $A$, there exists some time $n$ such that $T^{-n} B \cap B$ has positive measure. But this time $n$ corresponds to some returns to $A$ for the induced map, so $T^{-n} B \cap B$ is included in $\bigcup_m T_A^{-m} B \cap B$, hence one of these sets must have positive measure. The fact that the map is qmpt is then deduced from the conservativity. › proposition (in conservative) induced_map_conservative: assumes A_meas: "A ∈ sets M" shows "conservative (restrict_space M A) (induced_map A)" proof have "sigma_finite_measure M" by unfold_locales then have "sigma_finite_measure (restrict_space M A)" using sigma_finite_measure_restrict_space assms by auto then show "∃Aa. countable Aa ∧ Aa ⊆ sets (restrict_space M A) ∧ ⋃Aa = space (restrict_space M A) ∧ (∀a∈Aa. emeasure (restrict_space M A) a ≠ ∞)" using sigma_finite_measure_def by auto have imp: "⋀B. (B ∈ sets M ∧ B ⊆ A ∧ emeasure M B > 0) ⟹ (∃N>0. emeasure M (((induced_map A)^^N)-`B ∩ B) > 0)" proof - fix B assume assm: "B ∈ sets M ∧ B ⊆ A ∧ emeasure M B > 0" then have "B ⊆ A" by simp have inc: "(⋃n∈{1..}. (T^^n)-`B ∩ B) ⊆ (⋃N∈{1..}. ((induced_map A)^^N)-` B ∩ B)" proof fix x assume "x ∈ (⋃n∈{1..}. (T^^n)-`B ∩ B)" then obtain n where "n∈{1..}" and *: "x ∈ (T^^n)-`B ∩ B" by auto then have "n > 0" by auto have "x ∈ A" "(T^^n) x ∈ A" using * ‹B ⊆ A› by auto then obtain N where **: "n = (∑i<N. return_time_function A ((induced_map A ^^ i) x))" using induced_map_returns by auto then have "((induced_map A)^^N) x = (T^^n) x" using induced_map_iterates[of N, of A, of x] by simp then have "((induced_map A)^^N) x ∈ B" using * by simp then have "x ∈ ((induced_map A)^^N)-` B ∩ B" using * by simp moreover have "N > 0" using ** ‹n > 0› by (metis leD lessThan_iff less_nat_zero_code neq0_conv sum.neutral_const sum_mono) ultimately show "x ∈ (⋃N∈{1..}. ((induced_map A)^^N)-` B ∩ B)" by auto qed have B_meas [measurable]: "B ∈ sets M" and B_pos: "emeasure M B > 0" using assm by auto obtain n where "n > 0" and pos: "emeasure M ((T^^n)-`B ∩ B) > 0" using conservative[OF B_meas, OF B_pos] by auto then have "n ∈ {1..}" by auto have itB_meas: "⋀i. ((induced_map A)^^i)-` B ∩ B ∈ sets M" using B_meas measurable_compose_n[OF induced_map_meas[OF A_meas]] by (metis Int_assoc measurable_sets sets.Int sets.Int_space_eq1) then have "(⋃i∈{1..}. ((induced_map A)^^i)-` B ∩ B) ∈ sets M" by measurable moreover have "(T^^n)-`B ∩ B ⊆ (⋃i∈{1..}. ((induced_map A)^^i)-` B ∩ B)" using inc ‹n ∈ {1..}› by force ultimately have "emeasure M (⋃i∈{1..}. ((induced_map A)^^i)-` B ∩ B) > 0" by (metis (no_types, lifting) emeasure_eq_0 zero_less_iff_neq_zero pos) then have "emeasure M (⋃i∈{1..}. ((induced_map A)^^i)-` B ∩ B) ≠ 0" by simp have "∃i∈{1..}. emeasure M (((induced_map A)^^i)-` B ∩ B) ≠ 0" proof (rule ccontr) assume "¬(∃i∈{1..}. emeasure M (((induced_map A)^^i)-` B ∩ B) ≠ 0)" then have a: "⋀i. i ∈ {1..} ⟹ ((induced_map A)^^i)-` B ∩ B ∈ null_sets M" using itB_meas by auto have "(⋃i∈{1..}. ((induced_map A)^^i)-` B ∩ B) ∈ null_sets M" by (rule null_sets_UN', simp_all add: a) then show "False" using ‹emeasure M (⋃i∈{1..}. ((induced_map A)^^i)-` B ∩ B) > 0› by auto qed then show "∃N>0. emeasure M (((induced_map A)^^N)-` B ∩ B) > 0" by (simp add: Bex_def less_eq_Suc_le zero_less_iff_neq_zero) qed define K where "K = {B. B ∈ sets M ∧ B ⊆ A}" have K_stable: "(induced_map A)-`B ∈ K" if "B ∈ K" for B proof - have B_meas: "B ∈ sets M" and "B ⊆ A" using that unfolding K_def by auto then have a: "(induced_map A)-`B ⊆ A" using induced_map_stabilizes_A by auto then have "(induced_map A)-`B = (induced_map A)-`B ∩ space M" using assms sets.sets_into_space by auto then have "(induced_map A)-`B ∈ sets M" using induced_map_meas[OF assms] B_meas by (metis vrestr_meas vrestr_of_set) then show "(induced_map A)-`B ∈ K" unfolding K_def using a by auto qed define K0 where "K0 = K ∩ (null_sets M)" have K0_stable: "(induced_map A)-`B ∈ K0" if "B ∈ K0" for B proof - have "B ∈ K" using that unfolding K0_def by simp then have a: "(induced_map A)-`B ⊆ A" and b: "(induced_map A)-`B ∈ sets M" using K_stable unfolding K_def by auto have B_meas [measurable]: "B ∈ sets M" using ‹B ∈ K› unfolding K_def by simp have B0: "B ∈ null_sets M" using ‹B ∈ K0› unfolding K0_def by simp have "(induced_map A)-`B ⊆ (⋃n. (T^^n)-`B)" unfolding induced_map_def by auto then have "(induced_map A)-`B ⊆ (⋃n. (T^^n)-`B ∩ space M)" using b sets.sets_into_space by simp blast then have inc: "(induced_map A)-`B ⊆ (⋃n. (T^^n)--`B)" unfolding vimage_restr_def using sets.sets_into_space [OF B_meas] by simp have "(T^^n)--`B ∈ null_sets M" for n using B0 T_quasi_preserves_null(2)[OF B_meas] by simp then have "(⋃n. (T^^n)--`B) ∈ null_sets M" using null_sets_UN by auto then have "(induced_map A)-`B ∈ null_sets M" using null_sets_subset[OF _ b inc] by auto then show "(induced_map A)-`B ∈ K0" unfolding K0_def K_def by (simp add: a b) qed have *: "D ∈ null_sets M ⟷ D ∈ null_sets (restrict_space M A)" if "D∈K" for D using that unfolding K_def apply auto apply (metis assms emeasure_restrict_space null_setsD1 null_setsI sets.Int_space_eq2 sets_restrict_space_iff) by (metis assms emeasure_restrict_space null_setsD1 null_setsI sets.Int_space_eq2) show "induced_map A ∈ quasi_measure_preserving (restrict_space M A) (restrict_space M A)" unfolding quasi_measure_preserving_def proof (auto) have "induced_map A ∈ A → A" using induced_map_stabilizes_A by auto then show a: "induced_map A ∈ measurable (restrict_space M A) (restrict_space M A)" using measurable_restrict_space3[where ?A = A and ?B = A and ?M = M and ?N = M] induced_map_meas[OF A_meas] by auto fix B assume H: "B ∈ sets (restrict_space M A)" "induced_map A -`B ∩ space (restrict_space M A) ∈ null_sets (restrict_space M A)" then have "B ∈ K" unfolding K_def by (metis assms mem_Collect_eq sets.Int_space_eq2 sets_restrict_space_iff) then have B_meas [measurable]: "B ∈ sets M" and B_incl: "B ⊆ A" unfolding K_def by auto have "induced_map A -`B ∈ K" using K_stable ‹B ∈ K› by auto then have B2_meas: "induced_map A -`B ∈ sets M" and B2_incl: "induced_map A -`B ⊆ A" unfolding K_def by auto have "induced_map A -` B = induced_map A -`B ∩ space (restrict_space M A)" using B2_incl by (simp add: Int_absorb2 assms space_restrict_space) then have "induced_map A -` B ∈ null_sets (restrict_space M A)" using H(2) by simp then have "induced_map A -` B ∈ K0" unfolding K0_def using ‹induced_map A -`B ∈ K› * by auto { fix n have *: "((induced_map A)^^(n+1))-`B ∈ K0" proof (induction n) case (Suc n) have "((induced_map A)^^(Suc n+1))-`B = (induced_map A)-`(((induced_map A)^^(n+1))-` B)" by (metis Suc_eq_plus1 funpow_Suc_right vimage_comp) then show ?case by (metis Suc.IH K0_stable) qed (auto simp add: ‹induced_map A -` B ∈ K0›) have **: "((induced_map A)^^(n+1))-` B ∈ sets M" using * K0_def K_def by auto have "((induced_map A)^^(n+1))-` B ∩ B ∈ null_sets M" apply (rule null_sets_subset[of "((induced_map A)^^(n+1))-`B"]) using * unfolding K0_def apply simp using ** by auto } then have "((induced_map A)^^n)-` B ∩ B ∈ null_sets M" if "n>0" for n using that by (metis Suc_eq_plus1 neq0_conv not0_implies_Suc) then have "B ∈ null_sets M" using imp B_incl B_meas zero_less_iff_neq_zero inf.strict_order_iff by (metis null_setsD1 null_setsI) then show "B ∈ null_sets (restrict_space M A)" using * ‹B ∈ K› by auto next fix B assume H: "B ∈ sets (restrict_space M A)" "B ∈ null_sets (restrict_space M A)" then have "B ∈ K" unfolding K_def by (metis assms mem_Collect_eq sets.Int_space_eq2 sets_restrict_space_iff) then have B_meas [measurable]: "B ∈ sets M" and B_incl: "B ⊆ A" unfolding K_def by auto have "B ∈ null_sets M" using * H(2) ‹B ∈ K› by simp then have "B ∈ K0" unfolding K0_def using ‹B ∈ K› by simp then have inK: "(induced_map A)-`B ∈ K0" using K0_stable by auto then have inA: "(induced_map A)-`B ⊆ A" unfolding K0_def K_def by auto then have "(induced_map A)-`B = (induced_map A)-`B ∩ space (restrict_space M A)" by (simp add: Int_absorb2 assms space_restrict_space2) then show "induced_map A -` B ∩ space (restrict_space M A) ∈ null_sets (restrict_space M A)" using * inK unfolding K0_def by auto qed fix B assume B_measA: "B ∈ sets (restrict_space M A)" and B_posA: "0 < emeasure (restrict_space M A) B" then have B_meas: "B ∈ sets M" by (metis assms sets.Int_space_eq2 sets_restrict_space_iff) have B_incl: "B ⊆ A" by (metis B_measA assms sets.Int_space_eq2 sets_restrict_space_iff) then have B_pos: "0 < emeasure M B" using B_posA by (simp add: assms emeasure_restrict_space) obtain N where "N>0" "emeasure M (((induced_map A)^^N)-`B ∩ B) > 0" using imp B_meas B_incl B_pos by auto then have "emeasure (restrict_space M A) ((induced_map A ^^ N) -` B ∩ B) > 0" using assms emeasure_restrict_space by (metis B_incl Int_lower2 sets.Int_space_eq2 subset_trans) then show "∃n>0. 0 < emeasure (restrict_space M A) ((induced_map A ^^ n) -` B ∩ B)" using ‹N > 0› by auto qed text ‹Now, we want to prove that, if a map is conservative and measure preserving, then the induced map is also measure preserving. We first prove it for subsets $W$ of $A$ of finite measure, the general case will readily follow. The argument uses the fact that the preimage of the set of points with first entrance time $n$ is the union of the set of points with first entrance time $n+1$, and the points of $A$ with first return $n+1$. Following the preimage of $W$ under this process, we will get the intersection of $T_A^{-1} W$ with the different elements of the return partition, and the points in $T^{-n}W$ whose first $n-1$ iterates do not meet $A$ (and the measures of these sets add up to $\mu(W)$). To conclude, it suffices to show that the measure of points in $T^{-n}W$ whose first $n-1$ iterates do not meet $A$ tends to $0$. This follows from our local times estimates above.› lemma (in conservative_mpt) induced_map_measure_preserving_aux: assumes A_meas [measurable]: "A ∈ sets M" and W_meas [measurable]: "W ∈ sets M" and incl: "W ⊆ A" and fin: "emeasure M W < ∞" shows "emeasure M ((induced_map A)--`W) = emeasure M W" proof - have "W ⊆ space M" using W_meas using sets.sets_into_space by blast define BW where "BW = (λn. (first_entrance_set A n) ∩ (T^^n)--`W)" define DW where "DW = (λn. (return_time_function A)-` {n} ∩ (induced_map A)--`W)" have "⋀n. DW n = (return_time_function A)-` {n} ∩ space M ∩ (induced_map A)--`W" using DW_def by auto then have DW_meas [measurable]: "⋀n. DW n ∈ sets M" by auto have disj_DW: "disjoint_family (λn. DW n)" using DW_def disjoint_family_on_def by blast then have disj_DW2: "disjoint_family (λn. DW (n+1))" by (simp add: disjoint_family_on_def) have "(⋃n. DW n) = DW 0 ∪ (⋃n. DW (n+1))" by (auto) (metis not0_implies_Suc) moreover have "(DW 0) ∩ (⋃n. DW (n+1)) = {}" by (auto) (metis IntI Suc_neq_Zero UNIV_I empty_iff disj_DW disjoint_family_on_def) ultimately have *: "emeasure M (⋃n. DW n) = emeasure M (DW 0) + emeasure M (⋃n. DW (n+1))" by (simp add: countable_Un_Int(1) plus_emeasure) have "DW 0 = (return_time_function A)-` {0} ∩ W" unfolding DW_def induced_map_def return_time_function_def apply (auto simp add: return_time0[of A]) using sets.sets_into_space[OF W_meas] by auto also have "... = W - recurrent_subset A" using return_time0 by blast also have "... ⊆ A - recurrent_subset A" using incl by blast finally have "DW 0 ∈ null_sets M" by (metis A_meas DW_meas null_sets_subset Poincare_recurrence_thm(1)) then have "emeasure M (DW 0) = 0" by auto have "(induced_map A)--`W = (⋃n. DW n)" using DW_def by blast then have "emeasure M ((induced_map A)--`W) = emeasure M (⋃n. DW n)" by simp also have "... = emeasure M (⋃n. DW (n+1))" using * ‹emeasure M (DW 0) = 0› by simp also have "... = (∑n. emeasure M (DW (n+1)))" apply (rule suminf_emeasure[symmetric]) using disj_DW2 by auto finally have m: "emeasure M ((induced_map A)--`W) = (∑n. emeasure M (DW (n+1)))" by simp moreover have "summable (λn. emeasure M (DW (n+1)))" by simp ultimately have lim: "(λN. (∑ n∈{..<N}. emeasure M (DW (n+1)))) ⇢ emeasure M ((induced_map A)--`W)" by (simp add: summable_LIMSEQ) have BW_meas [measurable]: "⋀n. BW n ∈ sets M" unfolding BW_def by simp have *: "⋀n. T--`(BW n) - A = BW (n+1)" proof - fix n have "T--`(BW n) = T--`(first_entrance_set A n) ∩ (T^^(n+1))--`W" unfolding BW_def by (simp add: assms(2) T_vrestr_composed(2)) then have "T--`(BW n) - A = (T--`(first_entrance_set A n) - A) ∩ (T^^(n+1))--`W" by blast then have "T--`(BW n) - A = first_entrance_set A (n+1) ∩ (T^^(n+1))--`W" using first_entrance_rec[OF A_meas] by simp then show "T--`(BW n) - A = BW (n+1)" using BW_def by simp qed have **: "DW (n+1) = T--`(BW n) ∩ A" for n proof - have "T--`(BW n) = T--`(first_entrance_set A n) ∩ (T^^(n+1))--`W" unfolding BW_def by (simp add: assms(2) T_vrestr_composed(2)) then have "T--`(BW n) ∩ A = (T--`(first_entrance_set A n) ∩ A) ∩ (T^^(n+1))--`W" by blast then have *: "T--`(BW n) ∩ A = (return_time_function A)-`{n+1} ∩ (T^^(n+1))--`W" using return_time_rec[OF A_meas] by simp have "DW (n+1) = (return_time_function A)-`{n+1} ∩ (induced_map A)-`W" using DW_def ‹W ⊆ space M› return_time_rec by auto also have "... = (return_time_function A)-`{n+1} ∩ (T^^(n+1))-`W" by (auto simp add: induced_map_def) also have "... = (return_time_function A)-`{n+1} ∩ (T^^(n+1))--`W" using ‹W ⊆ space M› return_time_rec by auto finally show "DW (n+1) = T--`(BW n) ∩ A" using * by simp qed have "emeasure M W = (∑ n∈{..<N}. emeasure M (DW (n+1))) + emeasure M (BW N)" for N proof (induction N) case 0 have "BW 0 = W" unfolding BW_def first_entrance_set_def using incl by auto then show ?case by simp next case (Suc N) have "T--`(BW N) = BW (N+1) ∪ DW (N+1)" using * ** by blast moreover have "BW (N+1) ∩ DW (N+1) = {}" using * ** by blast ultimately have "emeasure M (T--`(BW N)) = emeasure M (BW (N+1)) + emeasure M (DW (N+1))" using DW_meas BW_meas plus_emeasure[of "BW (N+1)"] by simp then have "emeasure M (BW N) = emeasure M (BW (N+1)) + emeasure M (DW (N+1))" using T_vrestr_same_emeasure(1) BW_meas by auto then have "(∑ n∈{..<N}. emeasure M (DW (n+1))) + emeasure M (BW N) = (∑ n∈{..<N+1}. emeasure M (DW (n+1))) + emeasure M (BW (N+1))" by (simp add: add.commute add.left_commute) then show ?case using Suc.IH by simp qed moreover have "(λN. emeasure M (BW N)) ⇢ 0" proof (rule tendsto_sandwich[of "λ_. 0"_ _ "λN. emeasure M {x ∈ (T^^N)--`W. local_time A N x < 1}"]) have "emeasure M (BW N) ≤ emeasure M {x ∈ (T^^N)--`W. local_time A N x < 1}" for N apply (rule emeasure_mono) unfolding BW_def local_time_def first_entrance_set_def by auto then show "∀⇩_{F}n in sequentially. emeasure M (BW n) ≤ emeasure M {x ∈ (T ^^ n) --` W. local_time A n x < 1}" by auto have i: "W ⊆ (T^^0)--`A" using incl by auto show "(λN. emeasure M {x ∈ (T ^^ N) --` W. local_time A N x < 1}) ⇢ 0" apply (rule local_time_unbounded2[OF _ _ i]) using fin by auto qed (auto) then have "(λN. (∑ n∈{..<N}. emeasure M (DW (n+1))) + emeasure M (BW N)) ⇢ emeasure M (induced_map A --` W) + 0" using lim by (intro tendsto_add) auto ultimately show ?thesis by (auto intro: LIMSEQ_unique LIMSEQ_const_iff) qed lemma (in conservative_mpt) induced_map_measure_preserving: assumes A_meas [measurable]: "A ∈ sets M" and W_meas [measurable]: "W ∈ sets M" shows "emeasure M ((induced_map A)--`W) = emeasure M W" proof - define WA where "WA = W ∩ A" have WA_meas [measurable]: "WA ∈ sets M" "WA ⊆ A" using WA_def by auto have WAi_meas [measurable]: "(induced_map A)--`WA ∈ sets M" by simp have a: "emeasure M WA = emeasure M ((induced_map A)--`WA)" proof (cases) assume "emeasure M WA < ∞" then show ?thesis using induced_map_measure_preserving_aux[OF A_meas, OF ‹WA ∈ sets M›, OF ‹WA ⊆ A›] by simp next assume "¬(emeasure M WA < ∞)" then have "emeasure M WA = ∞" by (simp add: less_top[symmetric]) { fix C::real obtain Z where "Z ∈ sets M" "Z ⊆ WA" "emeasure M Z < ∞" "emeasure M Z > C" by (blast intro: ‹emeasure M WA = ∞› WA_meas approx_PInf_emeasure_with_finite) have "Z ⊆ A" using ‹Z ⊆ WA› WA_def by simp have "C < emeasure M Z" using ‹emeasure M Z > C› by simp also have "... = emeasure M ((induced_map A)--`Z)" using induced_map_measure_preserving_aux[OF A_meas, OF ‹Z ∈ sets M›, OF ‹Z ⊆ A›] ‹emeasure M Z < ∞› by simp also have "... ≤ emeasure M ((induced_map A)--`WA)" apply(rule emeasure_mono) using ‹Z ⊆ WA› vrestr_inclusion by auto finally have "emeasure M ((induced_map A)--`WA) > C" by simp } then have "emeasure M ((induced_map A)--`WA) = ∞" by (cases "emeasure M ((induced_map A)--`WA)") auto then show ?thesis using ‹emeasure M WA = ∞› by simp qed define WB where "WB = W - WA" have WB_meas [measurable]: "WB ∈ sets M" unfolding WB_def by simp have WBi_meas [measurable]: "(induced_map A)--`WB ∈ sets M" by simp have "WB ∩ A = {}" unfolding WB_def WA_def by auto moreover have id: "⋀x. x ∉ A ⟹ (induced_map A x) = x" unfolding induced_map_def return_time_function_def apply (auto) using recurrent_subset_incl by auto ultimately have "(induced_map A)--`WB = WB" using induced_map_stabilizes_A sets.sets_into_space[OF WB_meas] apply auto by (metis disjoint_iff_not_equal) fastforce+ then have b: "emeasure M ((induced_map A)--`WB) = emeasure M WB" by simp have "W = WA ∪ WB" "WA ∩ WB = {}" using WA_def WB_def by auto have *: "emeasure M W = emeasure M WA + emeasure M WB" by (subst ‹W = WA ∪ WB›, rule plus_emeasure[symmetric], auto simp add: ‹WA ∩ WB = {}›) have W_AUB: "(induced_map A)--`W = (induced_map A)--`WA ∪ (induced_map A)--`WB" using ‹W = WA ∪ WB› by auto have W_AIB: "(induced_map A)--`WA ∩ (induced_map A)--`WB = {}" by (metis ‹WA ∩ WB = {}› vrestr_empty vrestr_intersec) have "emeasure M ((induced_map A)--`W) = emeasure M ((induced_map A)--`WA) + emeasure M ((induced_map A)--`WB)" unfolding W_AUB by (rule plus_emeasure[symmetric]) (auto simp add: W_AIB) then show ?thesis using a b * by simp qed text ‹We can now express the fact that induced maps preserve the measure.› theorem (in conservative_mpt) induced_map_conservative_mpt: assumes "A ∈ sets M" shows "conservative_mpt (restrict_space M A) (induced_map A)" unfolding conservative_mpt_def proof show *: "conservative (restrict_space M A) (induced_map A)" using induced_map_conservative[OF assms] by auto show "mpt (restrict_space M A) (induced_map A)" unfolding mpt_def mpt_axioms_def proof show "qmpt (restrict_space M A) (induced_map A)" using * conservative_def by auto then have meas: "(induced_map A) ∈ measurable (restrict_space M A) (restrict_space M A)" unfolding qmpt_def qmpt_axioms_def quasi_measure_preserving_def by auto moreover have "⋀B. B ∈ sets (restrict_space M A) ⟹ emeasure (restrict_space M A) ((induced_map A) -`B ∩ space (restrict_space M A)) = emeasure (restrict_space M A) B" proof - have s: "space (restrict_space M A) = A" using assms space_restrict_space2 by auto have i: "⋀D. D ∈ sets M ∧ D ⊆ A ⟹ emeasure (restrict_space M A) D = emeasure M D" using assms by (simp add: emeasure_restrict_space) have j: "⋀D. D ∈ sets (restrict_space M A) ⟷ (D ∈ sets M ∧ D ⊆ A)" using assms by (metis sets.Int_space_eq2 sets_restrict_space_iff) fix B assume a: "B ∈ sets (restrict_space M A)" then have B_meas: "B ∈ sets M" using j by auto then have first: "emeasure (restrict_space M A) B = emeasure M B" using i j a by auto have incl: "(induced_map A) -`B ⊆ A" using j a induced_map_stabilizes_A assms by auto then have eq: "(induced_map A) -`B ∩ space (restrict_space M A) = (induced_map A) --`B" unfolding vimage_restr_def s using assms sets.sets_into_space by (metis a inf.orderE j meas measurable_sets s) then have "emeasure M B = emeasure M ((induced_map A) -`B ∩ space (restrict_space M A))" using induced_map_measure_preserving a j assms by auto also have "... = emeasure (restrict_space M A) ((induced_map A) -`B ∩ space (restrict_space M A))" using incl eq B_meas induced_map_meas[OF assms] assms i j by (metis emeasure_restrict_space inf.orderE s space_restrict_space) finally show "emeasure (restrict_space M A) ((induced_map A) -`B ∩ space (restrict_space M A)) = emeasure (restrict_space M A) B" using first by auto qed ultimately show "induced_map A ∈ measure_preserving (restrict_space M A) (restrict_space M A)" unfolding measure_preserving_def by auto qed qed theorem (in fmpt) induced_map_fmpt: assumes "A ∈ sets M" shows "fmpt (restrict_space M A) (induced_map A)" unfolding fmpt_def proof - have "conservative_mpt (restrict_space M A) (induced_map A)" using induced_map_conservative_mpt[OF assms] by simp then have "mpt (restrict_space M A) (induced_map A)" using conservative_mpt_def by auto moreover have "finite_measure (restrict_space M A)" by (simp add: assms finite_measureI finite_measure_restrict_space) ultimately show "mpt (restrict_space M A) (induced_map A) ∧ finite_measure (restrict_space M A)" by simp qed text ‹It will be useful to reformulate the fact that the recurrent subset has full measure in terms of the induced measure, to simplify the use of the induced map later on.› lemma (in conservative) induced_map_recurrent_typical: assumes A_meas [measurable]: "A ∈ sets M" shows "AE z in (restrict_space M A). z ∈ recurrent_subset A" "AE z in (restrict_space M A). z ∈ recurrent_subset_infty A" proof - have "recurrent_subset A ∈ sets M" using recurrent_subset_meas[OF A_meas] by auto then have rsA: "recurrent_subset A ∈ sets (restrict_space M A)" using recurrent_subset_incl(1)[of A] by (metis (no_types, lifting) A_meas sets_restrict_space_iff space_restrict_space space_restrict_space2) have "emeasure (restrict_space M A) (space (restrict_space M A) - recurrent_subset A) = emeasure (restrict_space M A) (A - recurrent_subset A)" by (metis (no_types, lifting) A_meas space_restrict_space2) also have "... = emeasure M (A - recurrent_subset A)" by (simp add: emeasure_restrict_space) also have "... = 0" using Poincare_recurrence_thm[OF A_meas] by auto finally have "space (restrict_space M A) - recurrent_subset A ∈ null_sets (restrict_space M A)" using rsA by blast then show "AE z in (restrict_space M A). z ∈ recurrent_subset A" by (metis (no_types, lifting) DiffI eventually_ae_filter mem_Collect_eq subsetI) have "recurrent_subset_infty A ∈ sets M" using recurrent_subset_meas[OF A_meas] by auto then have rsiA: "recurrent_subset_infty A ∈ sets (restrict_space M A)" using recurrent_subset_incl(2)[of A] by (metis (no_types, lifting) A_meas sets_restrict_space_iff space_restrict_space space_restrict_space2) have "emeasure (restrict_space M A) (space (restrict_space M A) - recurrent_subset_infty A) = emeasure (restrict_space M A) (A - recurrent_subset_infty A)" by (metis (no_types, lifting) A_meas space_restrict_space2) also have "... = emeasure M (A - recurrent_subset_infty A)" apply (rule emeasure_restrict_space) using A_meas by auto also have "... = 0" using Poincare_recurrence_thm[OF A_meas] by auto finally have "space (restrict_space M A) - recurrent_subset_infty A ∈ null_sets (restrict_space M A)" using rsiA by blast then show "AE z in (restrict_space M A). z ∈ recurrent_subset_infty A" by (metis (no_types, lifting) DiffI eventually_ae_filter mem_Collect_eq subsetI) qed subsection ‹Kac's theorem, and variants› text ‹Kac's theorem states that, for conservative maps, the integral of the return time to a subset $A$ is equal to the measure of the space if the dynamics is ergodic, or of the space seen by $A$ in the general case. This result generalizes to any induced function, not just the return time, that we define now.› definition induced_function::"'a set ⇒ ('a ⇒ 'b::comm_monoid_add) ⇒ ('a ⇒ 'b)" where "induced_function A f = (λx. (∑i∈{..< return_time_function A x}. f((T^^i) x)))" text ‹By definition, the induced function is supported on the recurrent subset of $A$.› lemma induced_function_support: fixes f::"'a ⇒ ennreal" shows "induced_function A f y = induced_function A f y * indicator ((return_time_function A)-`{1..}) y" by (auto simp add: induced_function_def indicator_def not_less_eq_eq) text ‹Basic measurability statements.› lemma induced_function_meas_ennreal [measurable]: fixes f::"'a ⇒ ennreal" assumes [measurable]: "f ∈ borel_measurable M" "A ∈ sets M" shows "induced_function A f ∈ borel_measurable M" unfolding induced_function_def by simp lemma induced_function_meas_real [measurable]: fixes f::"'a ⇒ real" assumes [measurable]: "f ∈ borel_measurable M" "A ∈ sets M" shows "induced_function A f ∈ borel_measurable M" unfolding induced_function_def by simp text ‹The Birkhoff sums of the induced function for the induced map form a subsequence of the original Birkhoff sums for the original map, corresponding to the return times to $A$.› lemma (in conservative) induced_function_birkhoff_sum: fixes f::"'a ⇒ real" assumes "A ∈ sets M" shows "birkhoff_sum f (qmpt.birkhoff_sum (induced_map A) (return_time_function A) n x) x = qmpt.birkhoff_sum (induced_map A) (induced_function A f) n x" proof - interpret A: conservative "restrict_space M A" "induced_map A" by (rule induced_map_conservative[OF assms]) define TA where "TA = induced_map A" define phiA where "phiA = return_time_function A" define R where "R = (λn. A.birkhoff_sum phiA n x)" show ?thesis proof (induction n) case 0 show ?case using birkhoff_sum_1(1) A.birkhoff_sum_1(1) by auto next case (Suc n) have "(T^^(R n)) x = (TA^^n) x" unfolding TA_def R_def A.birkhoff_sum_def phiA_def by (rule induced_map_iterates[symmetric]) have "R(n+1) = R n + phiA ((TA^^n) x)" unfolding R_def using A.birkhoff_sum_cocycle[where ?n = n and ?m = 1 and ?f = phiA] A.birkhoff_sum_1(2) TA_def by auto then have "birkhoff_sum f (R (n+1)) x = birkhoff_sum f (R n) x + birkhoff_sum f (phiA ((TA^^n) x)) ((T^^(R n)) x)" using birkhoff_sum_cocycle[where ?n = "R n" and ?f = f] by auto also have "... = birkhoff_sum f (R n) x + birkhoff_sum f (phiA ((TA^^n) x)) ((TA^^n) x)" using ‹(T^^(R n)) x = (TA^^n) x› by simp also have "... = birkhoff_sum f (R n) x + (induced_function A f) ((TA^^n) x)" unfolding induced_function_def birkhoff_sum_def phiA_def by simp also have "... = A.birkhoff_sum (induced_function A f) n x + (induced_function A f) ((TA^^n) x)" using Suc.IH R_def phiA_def by auto also have "... = A.birkhoff_sum (induced_function A f) (n+1) x" using A.birkhoff_sum_cocycle[where ?n = n and ?m = 1 and ?f = "induced_function A f" and ?x = x, symmetric] A.birkhoff_sum_1(2)[where ?f = "induced_function A f" and ?x = "(TA^^n) x"] unfolding TA_def by auto finally show ?case unfolding R_def phiA_def by simp qed qed text ‹The next lemma is very simple (just a change of variables to reorder the indices in the double sum). However, the proof I give is very tedious: infinite sums on proper subsets are not handled well, hence I use integrals on products of discrete spaces instead, and go back and forth between the two notions -- maybe there are better suited tools in the library, but I could not locate them... This is the main combinatorial tool used in the proof of Kac's Formula.› lemma kac_series_aux: fixes d:: "nat ⇒ nat ⇒ ennreal" shows "(∑n. (∑i≤n. d i n)) = (∑n. d 0 n) + (∑n. (∑i. d (i+1) (n+1+i)))" (is "_ = ?R") proof - define g where "g = (λ(i,n). (i+(1::nat), n+1+i))" define U where "U = {(i,n). (i>(0::nat)) ∧ (n≥i)}" have bij: "bij_betw g UNIV U" by (rule bij_betw_byWitness[where ?f' = "λ(i, n). (i-1, n-i)"], auto simp add: g_def U_def) define e where "e = (λ (i,j). d i j)" have pos: "⋀x. e x ≥ 0" using e_def by auto have "(∑n. (∑i. d (i+1) (n+1+i))) = (∑n. (∑i. e(i+1, n+1+i)))" using e_def by simp also have "... = ∫⇧^{+}n. ∫⇧^{+}i. e (i+1, n+1+i) ∂count_space UNIV ∂count_space UNIV" using pos nn_integral_count_space_nat suminf_0_le by auto also have "... = (∫⇧^{+}x. e (g x) ∂count_space UNIV)" unfolding g_def using nn_integral_snd_count_space[of "λ(i,n). e(i+1, n+1+i)"] by (auto simp add: prod.case_distrib) also have "... = (∫⇧^{+}y ∈ U. e y ∂count_space UNIV)" using nn_integral_count_compose_bij[OF bij] by simp finally have *: "(∑n. (∑i. d (i+1) (n+1+i))) = (∫⇧^{+}y ∈ U. e y ∂count_space UNIV)" by simp define V where "V = {((i::nat),(n::nat)). i = 0}" have i: "e (i, n) * indicator {0} i = e (i, n) * indicator V (i, n)" for i n by (auto simp add: indicator_def V_def) have "d 0 n = (∫⇧^{+}i ∈ {0}. e (i, n) ∂count_space UNIV)" for n proof - have "(∫⇧^{+}i ∈ {0}. e (i, n) ∂count_space UNIV) = (∫⇧^{+}i. e (i, n) ∂count_space {0})" using nn_integral_count_space_indicator[of _ "λi. e(i, n)"] by simp also have "... = e (0, n)" using nn_integral_count_space_finite[where ?f = "λi. e (i, n)"] by simp finally show ?thesis using e_def by simp qed then have "(∑n. d 0 n) = (∑n. (∫⇧^{+}i. e (i, n) * indicator {0} i ∂count_space UNIV))" by simp also have "... = (∫⇧^{+}n. (∫⇧^{+}i. e (i, n) * indicator {0} i ∂count_space UNIV) ∂count_space UNIV)" by (simp add: nn_integral_count_space_nat) also have "... = (∫⇧^{+}(i,n). e (i, n) * indicator {0} i ∂count_space UNIV)" using nn_integral_snd_count_space[of "λ (i,n). e(i,n) * indicator {0} i"] by auto also have "... = (∫⇧^{+}(i,n). e (i, n) * indicator V (i,n) ∂count_space UNIV)" by (metis i) finally have "(∑n. d 0 n) = (∫⇧^{+}y ∈ V. e y ∂count_space UNIV)" by (simp add: split_def) then have "?R = (∫⇧^{+}y ∈ V. e y ∂count_space UNIV) + (∫⇧^{+}y ∈ U. e y ∂count_space UNIV)" using * by simp also have "... = (∫⇧^{+}y ∈ V ∪ U. e y ∂count_space UNIV)" by (rule nn_integral_disjoint_pair_countspace[symmetric], auto simp add: U_def V_def) also have "... = (∫⇧^{+}(i, n). e (i, n) * indicator {..n} i ∂count_space UNIV)" by (rule nn_integral_cong, auto simp add: indicator_def V_def U_def pos, meson) also have "... = (∫⇧^{+}n. (∫⇧^{+}i. e (i, n) * indicator {..n} i ∂count_space UNIV)∂count_space UNIV)" using nn_integral_snd_count_space[of "λ(i,n). e(i,n) * indicator {..n} i"] by auto also have "... = (∑n. (∑i. e (i, n) * indicator {..n} i))" using pos nn_integral_count_space_nat suminf_0_le by auto moreover have "(∑i. e (i, n) * indicator {..n} i) = (∑i≤n. e (i, n))" for n proof - have "finite {..n}" by simp moreover have "⋀i. i ∉ {..n} ⟹ e (i,n) * indicator {..n} i = 0" using indicator_def by simp then have "(∑i. e (i,n) * indicator {..n} i) = (∑i ∈ {..n} . e (i, n) * indicator {..n} i)" by (meson calculation suminf_finite) moreover have "⋀i. i ∈ {..n} ⟹ e (i, n) * indicator {..n} i = e (i, n)" using indicator_def by auto ultimately show "(∑i. e (i, n) * indicator {..n} i) = (∑i≤n. e (i, n))" by simp qed ultimately show ?thesis using e_def by simp qed end context conservative_mpt begin text ‹We prove Kac's Formula (in the general form for induced functions) first for functions taking values in ennreal (to avoid all summabilities issues). The result for real functions will follow by domination. First, we assume additionally that $f$ is bounded and has a support of finite measure, the general case will follow readily by truncation. The proof is again an instance of the fact that the preimage of the set of points with first entrance time $n$ is the union of the set of points with first entrance time $n+1$, and the points of $A$ with first return $n+1$. Keeping track of the integral of $f$ on the different parts that appear in this argument, we will see that the integral of the induced function on the set of points with return time at most $n$ is equal to the integral of the function, up to an error controlled by the measure of points in $T^{-n}(supp(f))$ with local time $0$. Local time controls ensure that this contribution vanishes asymptotically. › lemma induced_function_nn_integral_aux: fixes f::"'a ⇒ ennreal" assumes A_meas [measurable]: "A ∈ sets M" and f_meas [measurable]: "f ∈ borel_measurable M" and f_bound: "⋀x. f x ≤ ennreal C" "0 ≤ C" and f_supp: "emeasure M {x ∈ space M. f x > 0} < ∞" shows "(∫⇧^{+}y. induced_function A f y ∂M) = (∫⇧^{+}x ∈ (⋃n. (T^^n)--`A). f x ∂M)" proof - define B where "B = (λn. first_entrance_set A n)" have B_meas [measurable]: "⋀n. B n ∈ sets M" by (simp add: B_def) then have B2 [measurable]: "(⋃n. B (n+1)) ∈ sets M" by measurable have *: "B = disjointed (λi. (T^^i)--`A)" by (auto simp add: B_def disjointed_def first_entrance_set_def) then have "disjoint_family B" by (simp add: disjoint_family_disjointed) have "(⋃n. (T^^n)--`A) = (⋃n. disjointed (λi. (T^^i)--`A) n)" by (simp add: UN_disjointed_eq) then have "(⋃n. (T^^n)--`A) = (⋃n. B n)" using * by simp then have "(⋃n. (T^^n)--`A) = B 0 ∪ (⋃n. B (n+1))" by (auto) (metis not0_implies_Suc) then have "(∫⇧^{+}x ∈ (⋃n. (T^^n)--`A). f x ∂M) = (∫⇧^{+}x ∈ (B 0 ∪ (⋃n. B (n+1))). f x ∂M)" by simp also have "... = (∫⇧^{+}x ∈ B 0. f x ∂M) + (∫⇧^{+}x ∈ (⋃n. B (n+1)). f x ∂M)" proof (rule nn_integral_disjoint_pair) show "B 0 ∩ (⋃n. B (n+1)) = {}" by (auto) (metis IntI Suc_neq_Zero UNIV_I empty_iff ‹disjoint_family B› disjoint_family_on_def) qed auto finally have "(∫⇧^{+}x ∈ (⋃n. (T^^n)--`A). f x ∂M) = (∫⇧^{+}x ∈ B 0. f x ∂M) + (∫⇧^{+}x ∈ (⋃n. B (n+1)). f x ∂M)" by simp moreover have "(∫⇧^{+}x ∈ (⋃n. B (n+1)). f x ∂M) = (∑n. (∫⇧^{+}x ∈ B (n+1). f x ∂M))" apply (rule nn_integral_disjoint_family) using ‹disjoint_family B› by (auto simp add: disjoint_family_on_def) ultimately have Bdec: "(∫⇧^{+}x ∈ (⋃n. (T^^n)--`A). f x ∂M) = (∫⇧^{+}x ∈ B 0. f x ∂M) + (∑n. ∫⇧^{+}x ∈ B (n+1). f x ∂M)" by simp define D where "D = (λn. (return_time_function A)-` {n+1})" then have "disjoint_family D" by (auto simp add: disjoint_family_on_def) have *: "⋀n. D n = T--`(B n) ∩ A" using D_def B_def return_time_rec[OF assms(1)] by simp then have [measurable]: "⋀n. D n ∈ sets M" by simp have **: "⋀n. B (n+1) = T--`(B n) - A" using first_entrance_rec[OF assms(1)] B_def by simp have pos0: "⋀i x. f((T^^i)x) ≥ 0" using assms(3) by simp have pos:"⋀ i C x. f((T^^i)x) * indicator (C) x ≥ 0" using assms(3) by simp have mes0 [measurable]: "⋀ i. (λx. f((T^^i)x)) ∈ borel_measurable M" by simp then have [measurable]: "⋀ i C. C ∈ sets M ⟹ (λx. f((T^^i)x) * indicator C x) ∈ borel_measurable M" by simp have "⋀y. induced_function A f y = induced_function A f y * indicator ((return_time_function A)-`{1..}) y" by (rule induced_function_support) moreover have "(return_time_function A)-`{(1::nat)..} = (⋃n. D n)" by (auto simp add: D_def Suc_le_D) ultimately have "⋀y. induced_function A f y = induced_function A f y * indicator (⋃n. D n) y" by simp then have "(∫⇧^{+}y. induced_function A f y ∂M) = (∫⇧^{+}y ∈ (⋃n. D n). induced_function A f y ∂M)" by simp also have "... = (∑n. (∫⇧^{+}y ∈ D n. induced_function A f y ∂M))" apply (rule nn_integral_disjoint_family) unfolding induced_function_def by (auto simp add: pos0 sum_nonneg ‹disjoint_family D›) finally have a: "(∫⇧^{+}y. induced_function A f y ∂M) = (∑n. (∫⇧^{+}y ∈ D n. induced_function A f y ∂M))" by simp define d where "d = (λi n. (∫⇧^{+}y ∈ D n. f((T^^i)y) ∂M))" have "(∫⇧^{+}y ∈ D n. induced_function A f y ∂M) = (∑i∈{..n}. d i n)" for n proof - have "induced_function A f y * indicator (D n) y = (∑i∈{..<n+1}. f((T^^i)y) * indicator (D n) y)" for y by (auto simp add: induced_function_def D_def indicator_def) then have "(∫⇧^{+}y ∈ D n. induced_function A f y ∂M) = (∑i∈{..<n+1}. (∫⇧^{+}y ∈ D n. f((T^^i)y) ∂M))" using pos nn_integral_sum[of "{..<n+1}", of "λi y. f((T^^i)y) * indicator (D n) y"] by simp also have "... = (∑i∈{..n}. (∫⇧^{+}y ∈ D n. f((T^^i)y) ∂M))" using lessThan_Suc_atMost by auto finally show ?thesis using d_def by simp qed then have induced_dec: "(∫⇧^{+}y. induced_function A f y ∂M) = (∑n. (∑i∈{..n}. d i n))" using a by simp have "(⋃n∈{1..}. (return_time_function A)-` {n}) = UNIV - (return_time_function A)-` {0}" by auto then have "(⋃n∈{1..}. (return_time_function A)-` {n}) = recurrent_subset A" using return_time0 by auto moreover have "(⋃n. (return_time_function A)-` {n+1}) = (⋃n∈{1..}. (return_time_function A)-` {n})" by (auto simp add: Suc_le_D) ultimately have "(⋃n. D n) = recurrent_subset A" using D_def by simp moreover have "(∫⇧^{+}x ∈ A. f x ∂M) = (∫⇧^{+}x ∈ recurrent_subset A. f x ∂M)" by (rule nn_integral_null_delta, auto simp add: Diff_mono Un_absorb2 recurrent_subset_incl(1)[of A] Poincare_recurrence_thm(1)[OF assms(1)]) moreover have "B 0 = A" using B_def first_entrance_set_def by simp ultimately have "(∫⇧^{+}x ∈ B 0. f x ∂M) = (∫⇧^{+}x ∈ (⋃n. D n). f x ∂M)" by simp also have "... = (∑n. (∫⇧^{+}x ∈ D n. f x ∂M))" by (rule nn_integral_disjoint_family, auto simp add: ‹disjoint_family D›) finally have B0dec: "(∫⇧^{+}x ∈ B 0. f x ∂M) = (∑n. d 0 n)" using d_def by simp have *: "(∫⇧^{+}x ∈ B n. f x ∂M) = (∑i<k. (∫⇧^{+}x ∈ D(n+i). f((T^^(i+1))x) ∂M)) + (∫⇧^{+}x ∈ B(n+k). f((T^^k)x) ∂M)" for n k proof (induction k) case 0 show ?case by simp next case (Suc k) have "T--`(B(n+k)) = B(n+k+1) ∪ D(n+k)" using * ** by blast have "(∫⇧^{+}x ∈ B(n+k). f((T^^k)x) ∂M) = (∫⇧^{+}x. (λx. f((T^^k)x) * indicator (B (n+k)) x)(T x) ∂M)" by (rule measure_preserving_preserves_nn_integral[OF Tm], auto simp add: pos) also have "... = (∫⇧^{+}x. f((T^^(k+1))x) * indicator (T--`(B (n+k))) x ∂M)" proof (rule nn_integral_cong_AE) have "(T^^k)(T x) = (T^^(k+1))x" for x using comp_eq_dest_lhs by (metis Suc_eq_plus1 funpow.simps(2) funpow_swap1) moreover have "AE x in M. f((T^^k)(T x)) * indicator (B (n+k)) (T x) = f((T^^k)(T x)) * indicator (T--`(B (n+k))) x" by (simp add: indicator_def ‹⋀n. B n ∈ sets M›) ultimately show "AE x in M. f((T^^k)(T x)) * indicator (B (n+k)) (T x) = f((T^^(k+1))x) * indicator (T--`(B (n+k))) x" by simp qed also have "... = (∫⇧^{+}x ∈ B(n+k+1) ∪ D(n+k). f((T^^(k+1))x) ∂M)" using ‹T--`(B(n+k)) = B(n+k+1) ∪ D(n+k)› by simp also have "... = (∫⇧^{+}x ∈ B(n+k+1). f((T^^(k+1))x) ∂M) + (∫⇧^{+}x ∈ D(n+k). f((T^^(k+1))x) ∂M)" proof (rule nn_integral_disjoint_pair[OF mes0[of "k+1"]]) show "B(n+k+1) ∩ D(n+k) = {}" using * ** by blast qed (auto) finally have "(∫⇧^{+}x ∈ B(n+k). f((T^^k)x) ∂M) = (∫⇧^{+}x ∈ B(n+k+1). f((T^^(k+1))x) ∂M) + (∫⇧^{+}x ∈ D(n+k). f((T^^(k+1))x) ∂M)" by simp then show ?case by (simp add: Suc.IH add.commute add.left_commute) qed have a: "(λk. (∫⇧^{+}x ∈ B(n+k). f((T^^k)x) ∂M)) ⇢ 0" for n proof - define W where "W = {x ∈ space M. f x > 0} ∩ (T^^n)--`A" have "emeasure M W ≤ emeasure M {x ∈ space M. f x > 0}" by (intro emeasure_mono, auto simp add: W_def) then have W_fin: "emeasure M W < ∞" using f_supp by auto have W_meas [measurable]: "W ∈ sets M" unfolding W_def by simp have W_incl: "W ⊆ (T^^n)--`A" unfolding W_def by simp define V where "V = (λk. {x ∈ (T^^k)--`W. local_time A k x = 0})" have V_meas [measurable]: "V k ∈ sets M" for k unfolding V_def by simp have a: "(∫⇧^{+}x ∈ B(n+k). f((T^^k)x) ∂M) ≤ C * emeasure M (V k)" for k proof - have "f((T^^k)x) * indicator (B(n+k)) x = f((T^^k)x) * indicator (B(n+k) ∩ (T^^k)--`W) x" for x proof (cases) assume "f((T^^k)x) * indicator (B(n+k)) x = 0" then show ?thesis by (simp add: indicator_def) next assume "¬(f((T^^k)x) * indicator (B(n+k)) x = 0)" then have H: "f((T^^k)x) * indicator (B(n+k)) x ≠ 0" by simp then have inB: "x ∈ B(n+k)" using H using indicator_simps(2) by fastforce then have s: "x ∈ space M" using B_meas[of "n+k"] sets.sets_into_space by blast then have a: "(T^^k)x ∈ space M" by (metis measurable_space Tn_meas[of k]) have "f((T^^k)x) > 0" using H by (simp add: le_neq_trans) then have *: "(T^^k)x ∈ {y ∈ space M. f y > 0}" using a by simp have "(T^^(n+k))x ∈ A" using inB B_def first_entrance_set_def by auto then have "(T^^n)((T^^k)x) ∈ A" by (simp add: funpow_add) then have "(T^^k)x ∈ (T^^n)--`A" using a by auto then have "(T^^k)x ∈ W" using * W_def by simp then have "x ∈ (T^^k)--`W" using s a by simp then have "x ∈ (B(n+k) ∩ (T^^k)--`W)" using inB by simp then show ?thesis by auto qed then have *: "(∫⇧^{+}x ∈ B(n+k). f((T^^k)x) ∂M) = (∫⇧^{+}x ∈ B(n+k) ∩ (T^^k)--`W. f((T^^k)x) ∂M)" by simp have "B(n+k) ⊆ {x ∈ space M. local_time A k x = 0}" unfolding local_time_def B_def first_entrance_set_def by auto then have "B(n+k) ∩ (T^^k)--`W ⊆ V k" unfolding V_def by blast then have "f((T^^k)x) * indicator (B(n+k) ∩ (T^^k)--`W) x ≤ ennreal C * indicator (V k) x" for x using f_bound by (auto split: split_indicator) then have "(∫⇧^{+}x ∈ B(n+k) ∩ (T^^k)--`W. f((T^^k)x) ∂M) ≤ (∫⇧^{+}x. ennreal C * indicator (V k) x ∂M)" by (simp add: nn_integral_mono) also have "... = ennreal C * emeasure M (V k)" by (simp add: ‹0 ≤ C› nn_integral_cmult) finally show "(∫⇧^{+}x ∈ B(n+k). f((T^^k)x) ∂M) ≤ C * emeasure M (V k)" using * by simp qed have "(λk. emeasure M (V k)) ⇢ 0" unfolding V_def using local_time_unbounded2[OF W_meas, OF W_fin, OF W_incl, of 1] by auto from ennreal_tendsto_cmult[OF _ this, of C] have t0: "(λk. C * emeasure M (V k)) ⇢ 0" by simp from a show "(λk. (∫⇧^{+}x ∈ B(n+k). f((T^^k)x) ∂M)) ⇢ 0" by (intro tendsto_sandwich[OF _ _ tendsto_const t0]) auto qed have b: "(λk. (∑i<k.(∫⇧^{+}x ∈ D(n+i). f((T^^(i+1))x) ∂M))) ⇢ (∑i. d (i+1) (n+i))" for n proof - define e where "e = (λi. d (i+1) (n+i))" then have "(λk. (∑i<k. e i)) ⇢ (∑i. e i)" by (intro summable_LIMSEQ) simp then show "(λk. (∑i<k.(∫⇧^{+}x ∈ D(n+i). f((T^^(i+1))x) ∂M))) ⇢ (∑i. d (i+1) (n+i))" using e_def d_def by simp qed have "(λk. (∑i<k. (∫⇧^{+}x ∈ D(n+i). f((T^^(i+1))x) ∂M)) + (∫⇧^{+}x ∈ B(n+k). f((T^^k)x) ∂M)) ⇢ (∑i. d (i+1) (n+i))" for n using tendsto_add[OF b a] by simp moreover have "(λk. (∑i<k. (∫⇧^{+}x ∈ D(n+i). f((T^^(i+1))x) ∂M)) + (∫⇧^{+}x ∈ B(n+k). f((T^^k)x) ∂M)) ⇢ (∫⇧^{+}x ∈ B n. f x ∂M)" for n using * by simp ultimately have "(∫⇧^{+}x ∈ B n. f x ∂M) = (∑i. d (i+1) (n+i))" for n using LIMSEQ_unique by blast then have "(∑n. (∫⇧^{+}x ∈ B (n+1). f x ∂M)) = (∑n. (∑i. d (i+1) (n+1+i)))" by simp then have "(∫⇧^{+}x ∈ (⋃n. (T^^n)--`A). f x ∂M) = (∑n. d 0 n) + (∑n. (∑i. d (i+1) (n+1+i)))" using Bdec B0dec by simp then show ?thesis using induced_dec kac_series_aux by simp qed text ‹We remove the boundedness assumption on $f$ and the finiteness assumption on its support by truncation (both in space and on the values of $f$).› theorem induced_function_nn_integral: fixes f::"'a ⇒ ennreal" assumes A_meas [measurable]: "A ∈ sets M" and f_meas [measurable]: "f ∈ borel_measurable M" shows "(∫⇧^{+}y. induced_function A f y ∂M) = (∫⇧^{+}x ∈ (⋃n. (T^^n)--`A). f x ∂M)" proof - obtain Y::"nat ⇒ 'a set" where Y_meas: "⋀ n. Y n ∈ sets M" and Y_fin: "⋀n. emeasure M (Y n) ≠ ∞" and Y_full: "(⋃n. Y n) = space M" and Y_inc: "incseq Y" by (meson range_subsetD sigma_finite_incseq) define F where "F = (λ(n::nat) x. min (f x) n * indicator (Y n) x)" have mes [measurable]: "⋀n. (F n) ∈ borel_measurable M" unfolding F_def using assms(2) Y_meas by measurable then have mes_rel [measurable]: "(λx. F n x * indicator (⋃n. (T^^n)--`A) x) ∈ borel_measurable M" for n by measurable have bound: "⋀n x. F n x ≤ ennreal n" by (simp add: F_def indicator_def ennreal_of_nat_eq_real_of_nat) have "⋀n. {x ∈ space M. F n x > 0} ⊆ Y n" unfolding F_def using not_le by fastforce then have le: "emeasure M {x ∈ space M. F n x > 0} ≤ emeasure M (Y n)" for n by (metis emeasure_mono Y_meas) have fin: "emeasure M {x ∈ space M. F n x > 0} < ∞" for n using Y_fin[of n] le[of n] by (simp add: less_top) have *: "(∫⇧^{+}y. induced_function A (F n) y ∂M) = (∫⇧^{+}x ∈ (⋃n. (T^^n)--`A). (F n) x ∂M)" for n by (rule induced_function_nn_integral_aux[OF A_meas mes bound _ fin]) simp have inc_Fx: "⋀x. incseq (λn. F n x)" unfolding F_def incseq_def proof (auto simp add: incseq_def) fix x::"'a" and m n::"nat" assume "m ≤ n" then have "min (f x) m ≤ min (f x) n" using linear by fastforce moreover have "(indicator (Y m) x::ennreal) ≤ (indicator (Y n) x::ennreal)" using Y_inc apply (auto simp add: incseq_def) using ‹m ≤ n› by blast ultimately show "min (f x) m * (indicator (Y m) x::ennreal) ≤ min (f x) n * (indicator (Y n) x::ennreal)" by (auto split: split_indicator) qed then have "incseq (λn. F n x * indicator (⋃n. (T^^n)--`A) x)" for x by (auto simp add: indicator_def incseq_def) then have inc_rel: "incseq (λn x. F n x * indicator (⋃n. (T^^n)--`A) x)" by (auto simp add: incseq_def le_fun_def) then have a: "(SUP n. (∫⇧^{+}x ∈ (⋃n. (T^^n)--`A). F n x ∂M)) = (∫⇧^{+}x. (SUP n. F n x * indicator (⋃n. (T^^n)--`A) x) ∂M)" using nn_integral_monotone_convergence_SUP[OF inc_rel, OF mes_rel] by simp have SUP_Fx: "(SUP n. F n x) = f x" if "x ∈ space M" for x proof - obtain N where "x ∈ Y N" using Y_full ‹x ∈ space M› by auto have "(SUP n. F n x) = (SUP n. inf (f x) (of_nat n))" proof (rule SUP_eq) show "∃j∈UNIV. F i x ≤ inf (f x) (of_nat j)" for i by (auto simp: F_def intro!: exI[of _ i] split: split_indicator) show "∃i∈UNIV. inf (f x) (of_nat j) ≤ F i x" for j using ‹x ∈ Y N› ‹incseq Y›[THEN monoD, of N "max N j"] by (intro bexI[of _ "max N j"]) (auto simp: F_def subset_eq not_le inf_min intro: min.coboundedI2 less_imp_le split: split_indicator split_max) qed then show ?thesis by (simp add: inf_SUP[symmetric] ennreal_SUP_of_nat_eq_top) qed then have "(SUP n. F n x * indicator (⋃n. (T^^n)--`A) x) = f x * indicator (⋃n. (T^^n)--`A) x" if "x ∈ space M" for x by (auto simp add: indicator_def SUP_Fx that) then have **: "(SUP n. (∫⇧^{+}x ∈ (⋃n. (T^^n)--`A). F n x ∂M)) = (∫⇧^{+}x ∈ (⋃n. (T^^n)--`A). f x ∂M)" by (simp add: a cong: nn_integral_cong) have "incseq (λn. induced_function A (F n) x)" for x unfolding induced_function_def using incseq_sumI2[of "{..<return_time_function A x}", of "λi n. F n ((T^^i)x)"] inc_Fx by simp then have "incseq (λn. induced_function A (F n))" by (auto simp add: incseq_def le_fun_def) then have b: "(SUP n. (∫⇧^{+}x. induced_function A (F n) x ∂M)) = (∫⇧^{+}x. (SUP n. induced_function A (F n) x) ∂M)" by (rule nn_integral_monotone_convergence_SUP[symmetric]) (measurable) have "(SUP n. induced_function A (F n) x) = induced_function A f x" if [simp]: "x ∈ space M" for x proof - have "(SUP n. (∑ i ∈{..<return_time_function A x}. F n ((T^^i)x))) = (∑ i ∈ {..<return_time_function A x}. f ((T^^i)x))" using ennreal_SUP_sum[OF inc_Fx, where ?I = "{..<return_time_function A x}"] SUP_Fx by simp then show "(SUP n. induced_function A (F n) x) = induced_function A f x" by (auto simp add: induced_function_def) qed then have "(SUP n. (∫⇧^{+}x. induced_function A (F n) x ∂M)) = (∫⇧^{+}x. induced_function A f x ∂M)" by (simp add: b cong: nn_integral_cong) then show ?thesis using * ** by simp qed text ‹Taking the constant function equal to $1$ in the previous statement, we obtain the usual Kac Formula.› theorem kac_formula_nonergodic: assumes A_meas [measurable]: "A ∈ sets M" shows "(∫⇧^{+}y. return_time_function A y ∂M) = emeasure M (⋃n. (T^^n)--`A)" proof - define f where "f = (λ(x::'a). 1::ennreal)" have "⋀x. induced_function A f x = return_time_function A x" unfolding induced_function_def f_def by (simp add:) then have "(∫⇧^{+}y. return_time_function A y ∂M) = (∫⇧^{+}y. induced_function A f y ∂M)" by auto also have "... = (∫⇧^{+}x ∈ (⋃n. (T^^n)--`A). f x ∂M)" by (rule induced_function_nn_integral) (auto simp add: f_def) also have "... = emeasure M (⋃n. (T^^n)--`A)" using f_def by auto finally show ?thesis by simp qed lemma (in fmpt) return_time_integrable: assumes A_meas [measurable]: "A ∈ sets M" shows "integrable M (return_time_function A)" by (rule integrableI_nonneg) (auto simp add: kac_formula_nonergodic[OF assms] ennreal_of_nat_eq_real_of_nat[symmetric] less_top[symmetric]) text ‹Now, we want to prove the same result but for real-valued integrable function. We first prove the statement for nonnegative functions by reducing to the nonnegative extended reals, and then for general functions by difference.› lemma induced_function_integral_aux: fixes f::"'a ⇒ real" assumes A_meas [measurable]: "A ∈ sets M" and f_int [measurable]: "integrable M f" and f_pos: "⋀x. f x ≥ 0" shows "integrable M (induced_function A f)" "(∫y. induced_function A f y ∂M) = (∫x ∈ (⋃n. (T^^n)--`A). f x ∂M)" proof - show "integrable M (induced_function A f)" proof (rule integrableI_nonneg) show "AE x in M. induced_function A f x ≥ 0" unfolding induced_function_def by (simp add: f_pos sum_nonneg) have "(∫⇧^{+}x. ennreal (induced_function A f x) ∂M) = (∫⇧^{+}x. induced_function A (λx. ennreal(f x)) x ∂M)" unfolding induced_function_def by (auto simp: f_pos) also have "... = (∫⇧^{+}x ∈ (⋃n. (T^^n)--`A). f x ∂M)" by (rule induced_function_nn_integral, auto simp add: assms) also have "... ≤ (∫⇧^{+}x. f x ∂M)" using nn_set_integral_set_mono[where ?A = "(⋃n. (T^^n)--`A)" and ?B = UNIV and ?f = "λx. ennreal(f x)"] by auto also have "... < ∞" using assms by (auto simp: less_top) finally show "(∫⇧^{+}x. induced_function A f x ∂M) < ∞" by simp qed (simp) have "(∫⇧^{+}x. (f x * indicator (⋃n. (T^^n)--`A) x) ∂M) = (∫⇧^{+}x ∈ (⋃n. (T^^n)--`A). f x ∂M)" by (auto split: split_indicator intro!: nn_integral_cong) also have "... = (∫⇧^{+}x. induced_function A (λx. ennreal(f x)) x ∂M)" by (rule induced_function_nn_integral[symmetric], auto simp add: assms) also have "... = (∫⇧^{+}x. ennreal (induced_function A f x) ∂M)" unfolding induced_function_def by (auto simp: f_pos) finally have *: "(∫⇧^{+}x. (f x * indicator (⋃n. (T^^n)--`A) x) ∂M) = (∫⇧^{+}x. ennreal (induced_function A f x) ∂M)" by simp have "(∫ x ∈ (⋃n. (T^^n)--`A). f x ∂M) = (∫ x. f x * indicator (⋃n. (T^^n)--`A) x ∂M)" by (simp add: mult.commute set_lebesgue_integral_def) also have "... = enn2real (∫⇧^{+}x. (f x * indicator (⋃n. (T^^n)--`A) x) ∂M)" by (rule integral_eq_nn_integral, auto simp add: f_pos) also have "... = enn2real (∫⇧^{+}x. ennreal (induced_function A f x) ∂M)" using * by simp also have "... = (∫ x. induced_function A f x ∂M)" apply (rule integral_eq_nn_integral[symmetric]) unfolding induced_function_def by (auto simp add: f_pos sum_nonneg) finally show "(∫ x. induced_function A f x ∂M) = (∫ x ∈ (⋃n. (T^^n)--`A). f x ∂M)" by simp qed text ‹Here is the general version of Kac's Formula (for a general induced function, starting from a real-valued integrable function).› theorem induced_function_integral_nonergodic: fixes f::"'a ⇒ real" assumes [measurable]: "A ∈ sets M" "integrable M f" shows "integrable M (induced_function A f)" "(∫y. induced_function A f y ∂M) = (∫x ∈ (⋃n. (T^^n)--`A). f x ∂M)" proof - have U_meas [measurable]: "(⋃n. (T^^n)--`A) ∈ sets M" by measurable define g where "g = (λx. max (f x) 0)" have g_int [measurable]: "integrable M g" unfolding g_def using assms by auto then have g_int2: "integrable M (induced_function A g)" using induced_function_integral_aux(1) g_def by auto define h where "h = (λx. max (-f x) 0)" have h_int [measurable]: "integrable M h" unfolding h_def using assms by auto then have h_int2: "integrable M (induced_function A h)" using induced_function_integral_aux(1) h_def by auto have D1: "f = (λx. g x - h x)" unfolding g_def h_def by auto have D2: "induced_function A f = (λx. induced_function A g x - induced_function A h x)" unfolding induced_function_def using D1 by (simp add: sum_subtractf) then show "integrable M (induced_function A f)" using g_int2 h_int2 by auto have "(∫x. induced_function A f x ∂M) = (∫x. induced_function A g x - induced_function A h x ∂M)" using D2 by simp also have "... = (∫x. induced_function A g x ∂M) - (∫x. induced_function A h x ∂M)" using g_int2 h_int2 by auto also have "... = (∫x ∈ (⋃n. (T^^n)--`A). g x ∂M) - (∫x ∈ (⋃n. (T^^n)--`A). h x ∂M)" using induced_function_integral_aux(2) g_def h_def g_int h_int by auto also have "... = (∫x ∈ (⋃n. (T^^n)--`A). (g x - h x) ∂M)" apply (rule set_integral_diff(2)[symmetric]) unfolding set_integrable_def using g_int h_int integrable_mult_indicator[OF U_meas] by blast+ also have "... = (∫x ∈ (⋃n. (T^^n)--`A). f x ∂M)" using D1 by simp finally show "(∫x. induced_function A f x ∂M) = (∫x ∈ (⋃n. (T^^n)--`A). f x ∂M)" by simp qed text ‹We can reformulate the previous statement in terms of induced measure.› lemma induced_function_integral_restr_nonergodic: fixes f::"'a ⇒ real" assumes [measurable]: "A ∈ sets M" "integrable M f" shows "integrable (restrict_space M A) (induced_function A f)" "(∫y. induced_function A f y ∂(restrict_space M A)) = (∫ x ∈ (⋃n. (T^^n)--`A). f x ∂M)" proof - have [measurable]: "integrable M (induced_function A f)" by (rule induced_function_integral_nonergodic(1)[OF assms]) then show "integrable (restrict_space M A) (induced_function A f)" by (metis assms(1) integrable_mult_indicator integrable_restrict_space sets.Int_space_eq2) have "(∫y. induced_function A f y ∂(restrict_space M A)) = (∫y ∈ A. induced_function A f y ∂M)" by (simp add: integral_restrict_space set_lebesgue_integral_def) also have "... = (∫y. induced_function A f y ∂M)" unfolding real_scaleR_def set_lebesgue_integral_def proof (rule Bochner_Integration.integral_cong [OF refl]) have "induced_function A f y = 0" if "y ∉ A" for y unfolding induced_function_def using that return_time0[of A] recurrent_subset_incl(1)[of A] return_time_function_def by auto then show "⋀x. indicator A x * induced_function A f x = induced_function A f x" unfolding indicator_def by auto qed also have "... = (∫ x ∈ (⋃n. (T^^n)--`A). f x ∂M)" by (rule induced_function_integral_nonergodic(2)[OF assms]) finally show "(∫y. induced_function A f y ∂(restrict_space M A)) = (∫ x ∈ (⋃n. (T^^n)--`A). f x ∂M)" by simp qed end end (*of Recurrence.thy*)