imports SG_Library_Complement

(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr License: BSD *) section ‹Measure preserving or quasi-preserving maps› theory Measure_Preserving_Transformations imports SG_Library_Complement begin text ‹Ergodic theory in general is the study of the properties of measure preserving or quasi-preserving dynamical systems. In this section, we introduce the basic definitions in this respect.› subsection ‹The different classes of transformations› definition quasi_measure_preserving::"'a measure ⇒ 'b measure ⇒ ('a ⇒ 'b) set" where "quasi_measure_preserving M N = {f ∈ measurable M N. ∀ A ∈ sets N. (f -` A ∩ space M ∈ null_sets M) = (A ∈ null_sets N)}" lemma quasi_measure_preservingI [intro]: assumes "f ∈ measurable M N" "⋀A. A ∈ sets N ⟹ (f -` A ∩ space M ∈ null_sets M) = (A ∈ null_sets N)" shows "f ∈ quasi_measure_preserving M N" using assms unfolding quasi_measure_preserving_def by auto lemma quasi_measure_preservingE: assumes "f ∈ quasi_measure_preserving M N" shows "f ∈ measurable M N" "⋀A. A ∈ sets N ⟹ (f -` A ∩ space M ∈ null_sets M) = (A ∈ null_sets N)" using assms unfolding quasi_measure_preserving_def by auto lemma id_quasi_measure_preserving: "(λx. x) ∈ quasi_measure_preserving M M" unfolding quasi_measure_preserving_def by auto lemma quasi_measure_preserving_composition: assumes "f ∈ quasi_measure_preserving M N" "g ∈ quasi_measure_preserving N P" shows "(λx. g(f x)) ∈ quasi_measure_preserving M P" proof (rule quasi_measure_preservingI) have f_meas [measurable]: "f ∈ measurable M N" by (rule quasi_measure_preservingE(1)[OF assms(1)]) have g_meas [measurable]: "g ∈ measurable N P" by (rule quasi_measure_preservingE(1)[OF assms(2)]) then show [measurable]: "(λx. g (f x)) ∈ measurable M P" by auto fix C assume [measurable]: "C ∈ sets P" define B where "B = g-`C ∩ space N" have [measurable]: "B ∈ sets N" unfolding B_def by simp have *: "B ∈ null_sets N ⟷ C ∈ null_sets P" unfolding B_def using quasi_measure_preservingE(2)[OF assms(2)] by simp define A where "A = f-`B ∩ space M" have [measurable]: "A ∈ sets M" unfolding A_def by simp have "A ∈ null_sets M ⟷ B ∈ null_sets N" unfolding A_def using quasi_measure_preservingE(2)[OF assms(1)] by simp then have "A ∈ null_sets M ⟷ C ∈ null_sets P" using * by simp moreover have "A = (λx. g (f x)) -` C ∩ space M" by (auto simp add: A_def B_def) (meson f_meas measurable_space) ultimately show "((λx. g (f x)) -` C ∩ space M ∈ null_sets M) ⟷ C ∈ null_sets P" by simp qed lemma quasi_measure_preserving_comp: assumes "f ∈ quasi_measure_preserving M N" "g ∈ quasi_measure_preserving N P" shows "g o f ∈ quasi_measure_preserving M P" unfolding comp_def using assms quasi_measure_preserving_composition by blast lemma quasi_measure_preserving_AE: assumes "f ∈ quasi_measure_preserving M N" "AE x in N. P x" shows "AE x in M. P (f x)" proof - obtain A where "⋀x. x ∈ space N - A ⟹ P x" "A ∈ null_sets N" using AE_E3[OF assms(2)] by blast define B where "B = f-`A ∩ space M" have "B ∈ null_sets M" unfolding B_def using quasi_measure_preservingE(2)[OF assms(1)] ‹A ∈ null_sets N› by auto moreover have "x ∈ space M - B ⟹ P (f x)" for x using ‹⋀x. x ∈ space N - A ⟹ P x› quasi_measure_preservingE(1)[OF assms(1)] unfolding B_def by (metis (no_types, lifting) Diff_iff IntI measurable_space vimage_eq) ultimately show ?thesis using AE_not_in AE_space by force qed lemma quasi_measure_preserving_AE': assumes "f ∈ quasi_measure_preserving M N" "AE x in M. P (f x)" "{x ∈ space N. P x} ∈ sets N" shows "AE x in N. P x" proof - have [measurable]: "f ∈ measurable M N" using quasi_measure_preservingE(1)[OF assms(1)] by simp define U where "U = {x ∈ space N. ¬(P x)}" have [measurable]: "U ∈ sets N" unfolding U_def using assms(3) by auto have "f-`U ∩ space M = {x ∈ space M. ¬(P (f x))}" unfolding U_def using ‹f ∈ measurable M N› by (auto, meson measurable_space) also have "... ∈ null_sets M" apply (subst AE_iff_null[symmetric]) using assms by auto finally have "U ∈ null_sets N" using quasi_measure_preservingE(2)[OF assms(1) ‹U ∈ sets N›] by auto then show ?thesis unfolding U_def using AE_iff_null by blast qed text ‹The push-forward under a quasi-measure preserving map $f$ of a measure absolutely continuous with respect to $M$ is absolutely continuous with respect to $N$.› lemma quasi_measure_preserving_absolutely_continuous: assumes "f ∈ quasi_measure_preserving M N" "u ∈ borel_measurable M" shows "absolutely_continuous N (distr (density M u) N f)" proof - have [measurable]: "f ∈ measurable M N" using quasi_measure_preservingE[OF assms(1)] by auto have "S ∈ null_sets (distr (density M u) N f)" if [measurable]: "S ∈ null_sets N" for S proof - have [measurable]: "S ∈ sets N" using null_setsD2[OF that] by auto have *: "AE x in N. x ∉ S" by (metis AE_not_in that) have "AE x in M. f x ∉ S" by (rule quasi_measure_preserving_AE[OF _ *], simp add: assms) then have *: "AE x in M. indicator S (f x) * u x = 0" by force have "emeasure (distr (density M u) N f) S = (∫⇧^{+}x. indicator S x ∂(distr (density M u) N f))" by auto also have "... = (∫⇧^{+}x. indicator S (f x) ∂(density M u))" by (rule nn_integral_distr, auto) also have "... = (∫⇧^{+}x. indicator S (f x) * u x ∂M)" by (rule nn_integral_densityR[symmetric], auto simp add: assms) also have "... = (∫⇧^{+}x. 0 ∂M)" using * by (rule nn_integral_cong_AE) finally have "emeasure (distr (density M u) N f) S = 0" by auto then show ?thesis by auto qed then show ?thesis unfolding absolutely_continuous_def by auto qed definition measure_preserving::"'a measure ⇒ 'b measure ⇒ ('a ⇒ 'b) set" where "measure_preserving M N = {f ∈ measurable M N. (∀ A ∈ sets N. emeasure M (f-`A ∩ space M) = emeasure N A)}" lemma measure_preservingE: assumes "f ∈ measure_preserving M N" shows "f ∈ measurable M N" "⋀A. A ∈ sets N ⟹ emeasure M (f-`A ∩ space M) = emeasure N A" using assms unfolding measure_preserving_def by auto lemma measure_preservingI [intro]: assumes "f ∈ measurable M N" "⋀A. A ∈ sets N ⟹ emeasure M (f-`A ∩ space M) = emeasure N A" shows "f ∈ measure_preserving M N" using assms unfolding measure_preserving_def by auto lemma measure_preserving_distr: assumes "f ∈ measure_preserving M N" shows "distr M N f = N" proof - let ?N2 = "distr M N f" have "sets ?N2 = sets N" by simp moreover have "emeasure ?N2 A = emeasure N A" if "A ∈ sets N" for A proof - have "emeasure ?N2 A = emeasure M (f-`A ∩ space M)" using ‹A ∈ sets N› assms emeasure_distr measure_preservingE(1)[OF assms] by blast then show "emeasure ?N2 A = emeasure N A" using ‹A ∈ sets N› measure_preservingE(2)[OF assms] by auto qed ultimately show ?thesis by (metis measure_eqI) qed lemma measure_preserving_distr': assumes "f ∈ measurable M N" shows "f ∈ measure_preserving M (distr M N f)" proof (rule measure_preservingI) show "f ∈ measurable M (distr M N f)" using assms(1) by auto show "emeasure M (f-`A ∩ space M) = emeasure (distr M N f) A" if "A ∈ sets (distr M N f)" for A using that emeasure_distr[OF assms] by auto qed lemma measure_preserving_preserves_nn_integral: assumes "T ∈ measure_preserving M N" "f ∈ borel_measurable N" shows "(∫⇧^{+}x. f x ∂N) = (∫⇧^{+}x. f (T x) ∂M)" proof - have "(∫⇧^{+}x. f (T x) ∂M) = (∫⇧^{+}y. f y ∂distr M N T)" using assms nn_integral_distr[of T M N f, OF measure_preservingE(1)[OF assms(1)]] by simp also have "... = (∫⇧^{+}y. f y ∂N)" using measure_preserving_distr[OF assms(1)] by simp finally show ?thesis by simp qed lemma measure_preserving_preserves_integral: fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}" assumes "T ∈ measure_preserving M N" and [measurable]: "integrable N f" shows "integrable M (λx. f(T x))" "(∫x. f x ∂N) = (∫x. f (T x) ∂M)" proof - have a [measurable]: "T ∈ measurable M N" by (rule measure_preservingE(1)[OF assms(1)]) have b [measurable]: "f ∈ borel_measurable N" by simp have "distr M N T = N" using measure_preserving_distr[OF assms(1)] by simp then have "integrable (distr M N T) f" using assms(2) by simp then show "integrable M (λx. f(T x))" using integrable_distr_eq[OF a b] by simp have "(∫x. f (T x) ∂M) = (∫y. f y ∂distr M N T)" using integral_distr[OF a b] by simp then show "(∫x. f x ∂N) = (∫x. f (T x) ∂M)" using ‹distr M N T = N› by simp qed lemma measure_preserving_preserves_integral': fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}" assumes "T ∈ measure_preserving M N" and [measurable]: "integrable M (λx. f (T x))" "f ∈ borel_measurable N" shows "integrable N f" "(∫x. f x ∂N) = (∫x. f (T x) ∂M)" proof - have a [measurable]: "T ∈ measurable M N" by (rule measure_preservingE(1)[OF assms(1)]) have "integrable M (λx. f(T x))" using assms(2) unfolding comp_def by auto then have "integrable (distr M N T) f" using integrable_distr_eq[OF a assms(3)] by simp then show *: "integrable N f" using measure_preserving_distr[OF assms(1)] by simp then show "(∫x. f x ∂N) = (∫x. f (T x) ∂M)" using measure_preserving_preserves_integral[OF assms(1) *] by simp qed lemma id_measure_preserving: "(λx. x) ∈ measure_preserving M M" unfolding measure_preserving_def by auto lemma measure_preserving_is_quasi_measure_preserving: assumes "f ∈ measure_preserving M N" shows "f ∈ quasi_measure_preserving M N" using assms unfolding measure_preserving_def quasi_measure_preserving_def apply auto by (metis null_setsD1 null_setsI, metis measurable_sets null_setsD1 null_setsI) lemma measure_preserving_composition: assumes "f ∈ measure_preserving M N" "g ∈ measure_preserving N P" shows "(λx. g(f x)) ∈ measure_preserving M P" proof (rule measure_preservingI) have f [measurable]: "f ∈ measurable M N" by (rule measure_preservingE(1)[OF assms(1)]) have g [measurable]: "g ∈ measurable N P" by (rule measure_preservingE(1)[OF assms(2)]) show [measurable]: "(λx. g (f x)) ∈ measurable M P" by auto fix C assume [measurable]: "C ∈ sets P" define B where "B = g-`C ∩ space N" have [measurable]: "B ∈ sets N" unfolding B_def by simp have *: "emeasure N B = emeasure P C" unfolding B_def using measure_preservingE(2)[OF assms(2)] by simp define A where "A = f-`B ∩ space M" have [measurable]: "A ∈ sets M" unfolding A_def by simp have "emeasure M A = emeasure N B" unfolding A_def using measure_preservingE(2)[OF assms(1)] by simp then have "emeasure M A = emeasure P C" using * by simp moreover have "A = (λx. g(f x))-`C ∩ space M" by (auto simp add: A_def B_def) (meson f measurable_space) ultimately show "emeasure M ((λx. g(f x))-`C ∩ space M) = emeasure P C" by simp qed lemma measure_preserving_comp: assumes "f ∈ measure_preserving M N" "g ∈ measure_preserving N P" shows "g o f ∈ measure_preserving M P" unfolding o_def using measure_preserving_composition assms by blast lemma measure_preserving_total_measure: assumes "f ∈ measure_preserving M N" shows "emeasure M (space M) = emeasure N (space N)" proof - have "f ∈ measurable M N" by (rule measure_preservingE(1)[OF assms(1)]) then have "f-`(space N) ∩ space M = space M" by (meson Int_absorb1 measurable_space subsetI vimageI) then show "emeasure M (space M) = emeasure N (space N)" by (metis (mono_tags, lifting) measure_preservingE(2)[OF assms(1)] sets.top) qed lemma measure_preserving_finite_measure: assumes "f ∈ measure_preserving M N" shows "finite_measure M ⟷ finite_measure N" using measure_preserving_total_measure[OF assms] by (metis finite_measure.emeasure_finite finite_measureI infinity_ennreal_def) lemma measure_preserving_prob_space: assumes "f ∈ measure_preserving M N" shows "prob_space M ⟷ prob_space N" using measure_preserving_total_measure[OF assms] by (metis prob_space.emeasure_space_1 prob_spaceI) locale qmpt = sigma_finite_measure + fixes T assumes Tqm: "T ∈ quasi_measure_preserving M M" locale mpt = qmpt + assumes Tm: "T ∈ measure_preserving M M" locale fmpt = mpt + finite_measure locale pmpt = fmpt + prob_space lemma qmpt_I: assumes "sigma_finite_measure M" "T ∈ measurable M M" "⋀A. A ∈ sets M ⟹ ((T-`A ∩ space M) ∈ null_sets M) ⟷ (A ∈ null_sets M)" shows "qmpt M T" unfolding qmpt_def qmpt_axioms_def quasi_measure_preserving_def by (auto simp add: assms) lemma mpt_I: assumes "sigma_finite_measure M" "T ∈ measurable M M" "⋀A. A ∈ sets M ⟹ emeasure M (T-`A ∩ space M) = emeasure M A" shows "mpt M T" proof - have *: "T ∈ measure_preserving M M" by (rule measure_preservingI[OF assms(2) assms(3)]) then have **: "T ∈ quasi_measure_preserving M M" using measure_preserving_is_quasi_measure_preserving by auto show "mpt M T" unfolding mpt_def qmpt_def qmpt_axioms_def mpt_axioms_def using * ** assms(1) by auto qed lemma fmpt_I: assumes "finite_measure M" "T ∈ measurable M M" "⋀A. A ∈ sets M ⟹ emeasure M (T-`A ∩ space M) = emeasure M A" shows "fmpt M T" proof - have *: "T ∈ measure_preserving M M" by (rule measure_preservingI[OF assms(2) assms(3)]) then have **: "T ∈ quasi_measure_preserving M M" using measure_preserving_is_quasi_measure_preserving by auto show "fmpt M T" unfolding fmpt_def mpt_def qmpt_def mpt_axioms_def qmpt_axioms_def using * ** assms(1) finite_measure_def by auto qed lemma pmpt_I: assumes "prob_space M" "T ∈ measurable M M" "⋀A. A ∈ sets M ⟹ emeasure M (T-`A ∩ space M) = emeasure M A" shows "pmpt M T" proof - have *: "T ∈ measure_preserving M M" by (rule measure_preservingI[OF assms(2) assms(3)]) then have **: "T ∈ quasi_measure_preserving M M" using measure_preserving_is_quasi_measure_preserving by auto show "pmpt M T" unfolding pmpt_def fmpt_def mpt_def qmpt_def mpt_axioms_def qmpt_axioms_def using * ** assms(1) prob_space_imp_sigma_finite prob_space.finite_measure by auto qed subsection ‹Examples› lemma fmpt_null_space: assumes "emeasure M (space M) = 0" "T ∈ measurable M M" shows "fmpt M T" apply (rule fmpt_I) apply (auto simp add: assms finite_measureI) apply (metis assms emeasure_eq_0 measurable_sets sets.sets_into_space sets.top) done lemma fmpt_empty_space: assumes "space M = {}" shows "fmpt M T" by (rule fmpt_null_space, auto simp add: assms measurable_empty_iff) text ‹Translations are measure-preserving› lemma mpt_translation: fixes c :: "'a::euclidean_space" shows "mpt lborel (λx. x + c)" proof (rule mpt_I, auto simp add: lborel.sigma_finite_measure_axioms) fix A::"'a set" assume [measurable]: "A ∈ sets borel" have "emeasure lborel ((λx. x + c) -` A) = emeasure lborel ((((+))c)-`A)" by (meson add.commute) also have "... = emeasure lborel ((((+))c)-`A ∩ space lborel)" by simp also have "... = emeasure (distr lborel borel ((+) c)) A" by (rule emeasure_distr[symmetric], auto) also have "... = emeasure lborel A" using lborel_distr_plus[of c] by simp finally show "emeasure lborel ((λx. x + c) -` A) = emeasure lborel A" by simp qed text ‹Skew products are fibered maps of the form $(x,y)\mapsto (Tx, U(x,y))$. If the base map and the fiber maps all are measure preserving, so is the skew product.› lemma pair_measure_null_product: assumes "emeasure M (space M) = 0" shows "emeasure (M ⨂⇩_{M}N) (space (M ⨂⇩_{M}N)) = 0" proof - have "(∫⇧^{+}x. (∫⇧^{+}y. indicator X (x,y) ∂N) ∂M) = 0" for X proof - have "(∫⇧^{+}x. (∫⇧^{+}y. indicator X (x,y) ∂N) ∂M) = (∫⇧^{+}x. 0 ∂M)" by (intro nn_integral_cong_AE emeasure_0_AE[OF assms]) then show ?thesis by auto qed then have "M ⨂⇩_{M}N = measure_of (space M × space N) {a × b | a b. a ∈ sets M ∧ b ∈ sets N} (λX. 0)" unfolding pair_measure_def by auto then show ?thesis by (simp add: emeasure_sigma) qed lemma mpt_skew_product: assumes "mpt M T" "AE x in M. mpt N (U x)" and [measurable]: "(λ(x,y). U x y) ∈ measurable (M ⨂⇩_{M}N) N" shows "mpt (M ⨂⇩_{M}N) (λ(x,y). (T x, U x y))" proof (cases) assume H: "emeasure M (space M) = 0" then have *: "emeasure (M ⨂⇩_{M}N) (space (M ⨂⇩_{M}N)) = 0" using pair_measure_null_product by auto have [measurable]: "T ∈ measurable M M" using assms(1) unfolding mpt_def qmpt_def qmpt_axioms_def quasi_measure_preserving_def by auto then have [measurable]: "(λ(x, y). (T x, U x y)) ∈ measurable (M ⨂⇩_{M}N) (M ⨂⇩_{M}N)" by auto with fmpt_null_space[OF *] show ?thesis by (simp add: fmpt.axioms(1)) next assume "¬(emeasure M (space M) = 0)" show ?thesis proof (rule mpt_I) have "sigma_finite_measure M" using assms(1) unfolding mpt_def qmpt_def by auto then interpret M: sigma_finite_measure M . have "∃p. ¬ almost_everywhere M p" by (metis (lifting) AE_E ‹emeasure M (space M) ≠ 0› emeasure_eq_AE emeasure_notin_sets) then have "∃x. mpt N (U x)" using assms(2) ‹¬(emeasure M (space M) = 0)› by (metis (full_types) ‹AE x in M. mpt N (U x)› eventually_mono) then have "sigma_finite_measure N" unfolding mpt_def qmpt_def by auto then interpret N: sigma_finite_measure N . show "sigma_finite_measure (M ⨂⇩_{M}N)" by (rule sigma_finite_pair_measure) standard+ have [measurable]: "T ∈ measurable M M" using assms(1) unfolding mpt_def qmpt_def qmpt_axioms_def quasi_measure_preserving_def by auto show [measurable]: "(λ(x, y). (T x, U x y)) ∈ measurable (M ⨂⇩_{M}N) (M ⨂⇩_{M}N)" by auto have "T ∈ measure_preserving M M" using assms(1) by (simp add: mpt.Tm) fix A assume [measurable]: "A ∈ sets (M ⨂⇩_{M}N)" then have [measurable]: "(λ (x,y). (indicator A (x,y))::ennreal) ∈ borel_measurable (M ⨂⇩_{M}N)" by auto then have [measurable]: "(λx. ∫⇧^{+}y. indicator A (x, y) ∂N) ∈ borel_measurable M" by simp define B where "B = (λ(x, y). (T x, U x y)) -` A ∩ space (M ⨂⇩_{M}N)" then have [measurable]: "B ∈ sets (M ⨂⇩_{M}N)" by auto have "(∫⇧^{+}y. indicator B (x,y) ∂N) = (∫⇧^{+}y. indicator A (T x, y) ∂N)" if "x ∈ space M" "mpt N (U x)" for x proof - have "T x ∈ space M" by (meson ‹T ∈ measurable M M› ‹x ∈ space M› measurable_space) then have 1: "(λy. (indicator A (T x, y))::ennreal) ∈ borel_measurable N" using ‹A ∈ sets (M ⨂⇩_{M}N)› by auto have 2: "⋀y. ((indicator B (x, y))::ennreal) = indicator A (T x, U x y) * indicator (space M) x * indicator (space N) y" unfolding B_def by (simp add: indicator_def space_pair_measure) have 3: "U x ∈ measure_preserving N N" using assms(2) that(2) by (simp add: mpt.Tm) have "(∫⇧^{+}y. indicator B (x,y) ∂N) = (∫⇧^{+}y. indicator A (T x, U x y) ∂N)" using 2 by (intro nn_integral_cong_simp) (auto simp add: indicator_def ‹x ∈ space M›) also have "... = (∫⇧^{+}y. indicator A (T x, y) ∂N)" by (rule measure_preserving_preserves_nn_integral[OF 3, symmetric], metis 1) finally show ?thesis by simp qed then have *: "AE x in M. (∫⇧^{+}y. indicator B (x,y) ∂N) = (∫⇧^{+}y. indicator A (T x, y) ∂N)" using assms(2) by auto have "emeasure (M ⨂⇩_{M}N) B = (∫⇧^{+}x. (∫⇧^{+}y. indicator B (x,y) ∂N) ∂M)" using ‹B ∈ sets (M ⨂⇩_{M}N)› ‹sigma_finite_measure N› sigma_finite_measure.emeasure_pair_measure by fastforce also have "... = (∫⇧^{+}x. (∫⇧^{+}y. indicator A (T x, y) ∂N) ∂M)" by (intro nn_integral_cong_AE *) also have "... = (∫⇧^{+}x. (∫⇧^{+}y. indicator A (x, y) ∂N) ∂M)" by (rule measure_preserving_preserves_nn_integral[OF ‹T ∈ measure_preserving M M›, symmetric]) auto also have "... = emeasure (M ⨂⇩_{M}N) A" by (simp add: ‹sigma_finite_measure N› sigma_finite_measure.emeasure_pair_measure) finally show "emeasure (M ⨂⇩_{M}N) ((λ(x, y). (T x, U x y)) -` A ∩ space (M ⨂⇩_{M}N)) = emeasure (M ⨂⇩_{M}N) A" unfolding B_def by simp qed qed lemma mpt_skew_product_real: fixes f::"'a ⇒ 'b::euclidean_space" assumes "mpt M T" and [measurable]: "f ∈ borel_measurable M" shows "mpt (M ⨂⇩_{M}lborel) (λ(x,y). (T x, y + f x))" by (rule mpt_skew_product, auto simp add: mpt_translation assms(1)) subsection ‹Preimages restricted to $space M$› context qmpt begin text ‹One is all the time lead to take the preimages of sets, and restrict them to \verb+space M+ where the dynamics is living. We introduce a shortcut for this notion.› definition vimage_restr :: "('a ⇒ 'a) ⇒ 'a set ⇒ 'a set" (infixr "--`" 90) where "f --` A ≡ f-` (A ∩ space M) ∩ space M" lemma vrestr_eq [simp]: "a ∈ f--` A ⟷ a ∈ space M ∧ f a ∈ A ∩ space M" unfolding vimage_restr_def by auto lemma vrestr_intersec [simp]: "f--` (A ∩ B) = (f--`A) ∩ (f--` B)" using vimage_restr_def by auto lemma vrestr_union [simp]: "f--` (A ∪ B) = f--`A ∪ f--`B" using vimage_restr_def by auto lemma vrestr_difference [simp]: "f--`(A-B) = f--`A - f--`B" using vimage_restr_def by auto lemma vrestr_inclusion: "A ⊆ B ⟹ f--`A ⊆ f--`B" using vimage_restr_def by auto lemma vrestr_Union [simp]: "f --` (⋃A) = (⋃X∈A. f --` X)" using vimage_restr_def by auto lemma vrestr_UN [simp]: "f --` (⋃x∈A. B x) = (⋃x∈A. f --` B x)" using vimage_restr_def by auto lemma vrestr_Inter [simp]: assumes "A ≠ {}" shows "f --` (⋂A) = (⋂X∈A. f --` X)" using vimage_restr_def assms by auto lemma vrestr_INT [simp]: assumes "A ≠ {}" shows "f --` (⋂x∈A. B x) = (⋂x∈A. f --` B x)" using vimage_restr_def assms by auto lemma vrestr_empty [simp]: "f--`{} = {}" using vimage_restr_def by auto lemma vrestr_sym_diff [simp]: "f--`(A Δ B) = (f--`A) Δ (f--`B)" by auto lemma vrestr_image: assumes "x ∈ f--`A" shows "x ∈ space M" "f x ∈ space M" "f x ∈ A" using assms unfolding vimage_restr_def by auto lemma vrestr_intersec_in_space: assumes "A ∈ sets M" "B ∈ sets M" shows "A ∩ f--`B = A ∩ f-`B" unfolding vimage_restr_def using assms sets.sets_into_space by auto lemma vrestr_compose: assumes "g ∈ measurable M M" shows "(λ x. f(g x))--` A = g--` (f--` A)" proof - define B where "B = A ∩ space M" have "(λ x. f(g x))--` A = (λ x. f(g x)) -` B ∩ space M" using B_def vimage_restr_def by blast moreover have "(λ x. f(g x)) -` B ∩ space M = g-` (f-` B ∩ space M) ∩ space M" using measurable_space[OF ‹g ∈ measurable M M›] by auto moreover have "g-` (f-` B ∩ space M) ∩ space M = g--` (f--` A)" using B_def vimage_restr_def by simp ultimately show ?thesis by auto qed lemma vrestr_comp: assumes "g ∈ measurable M M" shows "(f o g)--` A = g--` (f--` A)" proof - have "f o g = (λ x. f(g x))" by auto then have "(f o g)--` A = (λ x. f(g x))--` A" by auto moreover have "(λ x. f(g x))--` A = g--` (f--` A)" using vrestr_compose assms by auto ultimately show ?thesis by simp qed lemma vrestr_of_set: assumes "g ∈ measurable M M" shows "A ∈ sets M ⟹ g--`A = g-`A ∩ space M" by (simp add: vimage_restr_def) lemma vrestr_meas [measurable (raw)]: assumes "g ∈ measurable M M" "A ∈ sets M" shows "g--`A ∈ sets M" using assms vimage_restr_def by auto lemma vrestr_same_emeasure_f: assumes "f ∈ measure_preserving M M" "A ∈ sets M" shows "emeasure M (f--`A) = emeasure M A" by (metis (mono_tags, lifting) assms measure_preserving_def mem_Collect_eq sets.Int_space_eq2 vimage_restr_def) lemma vrestr_same_measure_f: assumes "f ∈ measure_preserving M M" "A ∈ sets M" shows "measure M (f--`A) = measure M A" proof - have "measure M (f--`A) = enn2real (emeasure M (f--`A))" by (simp add: Sigma_Algebra.measure_def) also have "... = enn2real (emeasure M A)" using vrestr_same_emeasure_f[OF assms] by simp also have "... = measure M A" by (simp add: Sigma_Algebra.measure_def) finally show "measure M (f--` A) = measure M A" by simp qed subsection ‹Basic properties of qmpt› lemma T_meas [measurable (raw)]: "T ∈ measurable M M" by (rule quasi_measure_preservingE(1)[OF Tqm]) lemma Tn_quasi_measure_preserving: "T^^n ∈ quasi_measure_preserving M M" proof (induction n) case 0 show ?case using id_quasi_measure_preserving by simp next case (Suc n) then show ?case using Tqm quasi_measure_preserving_comp by (metis funpow_Suc_right) qed lemma Tn_meas [measurable (raw)]: "T^^n ∈ measurable M M" by (rule quasi_measure_preservingE(1)[OF Tn_quasi_measure_preserving]) lemma T_vrestr_meas [measurable]: assumes "A ∈ sets M" shows "T--` A ∈ sets M" "(T^^n)--` A ∈ sets M" by (auto simp add: vrestr_meas assms) text ‹We state the next lemma both with $T^0$ and with $id$ as sometimes the simplifier simplifies $T^0$ to $id$ before applying the first instance of the lemma.› lemma T_vrestr_0 [simp]: assumes "A ∈ sets M" shows "(T^^0)--`A = A" "id--`A = A" using sets.sets_into_space[OF assms] by auto lemma T_vrestr_composed: assumes "A ∈ sets M" shows "(T^^n)--` (T^^m)--` A = (T^^(n+m))--` A" "T--` (T^^m)--` A = (T^^(m+1))--` A" "(T^^m)--` T--` A = (T^^(m+1))--` A" proof - show "(T^^n)--` (T^^m)--` A = (T^^(n+m))--` A" by (simp add: Tn_meas funpow_add add.commute vrestr_comp) show "T--` (T^^m)--` A = (T^^(m+1))--` A" by (metis Suc_eq_plus1 T_meas funpow_Suc_right vrestr_comp) show "(T^^m)--` T--` A = (T^^(m+1))--` A" by (simp add: Tn_meas vrestr_comp) qed text ‹In the next two lemmas, we give measurability statements that show up all the time for the usual preimage.› lemma T_intersec_meas [measurable]: assumes [measurable]: "A ∈ sets M" "B ∈ sets M" shows "A ∩ T-`B ∈ sets M" "A ∩ (T^^n)-`B ∈ sets M" "T-`A ∩ B ∈ sets M" "(T^^n)-`A ∩ B ∈ sets M" "A ∩ (T ∘ T ^^ n) -` B ∈ sets M" "(T ∘ T ^^ n) -` A ∩ B ∈ sets M" by (metis T_meas Tn_meas assms(1) assms(2) measurable_comp sets.Int inf_commute vrestr_intersec_in_space vrestr_meas)+ lemma T_diff_meas [measurable]: assumes [measurable]: "A ∈ sets M" "B ∈ sets M" shows "A - T-`B ∈ sets M" "A - (T^^n)-`B ∈ sets M" proof - have "A - T-`B = A ∩ space M - (T-`B ∩ space M)" using sets.sets_into_space[OF assms(1)] by auto then show "A - T-`B ∈ sets M" by auto have "A - (T^^n)-`B = A ∩ space M - ((T^^n)-`B ∩ space M)" using sets.sets_into_space[OF assms(1)] by auto then show "A - (T^^n)-`B ∈ sets M" by auto qed lemma T_spaceM_stable [simp]: assumes "x ∈ space M" shows "T x ∈ space M" "(T^^n) x ∈ space M" proof - show "T x ∈ space M" by (meson measurable_space T_meas measurable_def assms) show "(T^^n) x ∈ space M" by (meson measurable_space Tn_meas measurable_def assms) qed lemma T_quasi_preserves_null: assumes "A ∈ sets M" shows "A ∈ null_sets M ⟷ T--` A ∈ null_sets M" "A ∈ null_sets M ⟷ (T^^n)--` A ∈ null_sets M" using Tqm Tn_quasi_measure_preserving unfolding quasi_measure_preserving_def by (auto simp add: assms vimage_restr_def) lemma T_quasi_preserves: assumes "A ∈ sets M" shows "emeasure M A = 0 ⟷ emeasure M (T--` A) = 0" "emeasure M A = 0 ⟷ emeasure M ((T^^n)--` A) = 0" using T_quasi_preserves_null[OF assms] T_vrestr_meas assms by blast+ lemma T_quasi_preserves_null2: assumes "A ∈ null_sets M" shows "T--` A ∈ null_sets M" "(T^^n)--` A ∈ null_sets M" using T_quasi_preserves_null[OF null_setsD2[OF assms]] assms by auto lemma T_composition_borel [measurable]: assumes "f ∈ borel_measurable M" shows "(λx. f(T x)) ∈ borel_measurable M" "(λx. f((T^^k) x)) ∈ borel_measurable M" using T_meas Tn_meas assms measurable_compose by auto lemma T_AE_iterates: assumes "AE x in M. P x" shows "AE x in M. ∀n. P ((T^^n) x)" proof - have "AE x in M. P ((T^^n) x)" for n by (rule quasi_measure_preserving_AE[OF Tn_quasi_measure_preserving[of n] assms]) then show ?thesis unfolding AE_all_countable by simp qed lemma qmpt_power: "qmpt M (T^^n)" by (standard, simp add: Tn_quasi_measure_preserving) lemma T_Tn_T_compose: "T ((T^^n) x) = (T^^(Suc n)) x" "(T^^n) (T x) = (T^^(Suc n)) x" by (auto simp add: funpow_swap1) lemma (in qmpt) qmpt_density: assumes [measurable]: "h ∈ borel_measurable M" and "AE x in M. h x ≠ 0" "AE x in M. h x ≠ ∞" shows "qmpt (density M h) T" proof - interpret A: sigma_finite_measure "density M h" apply (subst sigma_finite_iff_density_finite) using assms by auto show ?thesis apply (standard) apply (rule quasi_measure_preservingI) unfolding null_sets_density[OF ‹h ∈ borel_measurable M› ‹AE x in M. h x ≠ 0›] sets_density space_density using quasi_measure_preservingE(2)[OF Tqm] by auto qed end subsection ‹Basic properties of mpt› context mpt begin lemma Tn_measure_preserving: "T^^n ∈ measure_preserving M M" proof (induction n) case (Suc n) then show ?case using Tm measure_preserving_comp by (metis funpow_Suc_right) qed (simp add: id_measure_preserving) lemma T_integral_preserving: fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}" assumes "integrable M f" shows "integrable M (λx. f(T x))" "(∫x. f(T x) ∂M) = (∫x. f x ∂M)" using measure_preserving_preserves_integral[OF Tm assms] by auto lemma Tn_integral_preserving: fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}" assumes "integrable M f" shows "integrable M (λx. f((T^^n) x))" "(∫x. f((T^^n) x) ∂M) = (∫x. f x ∂M)" using measure_preserving_preserves_integral[OF Tn_measure_preserving assms] by auto lemma T_nn_integral_preserving: fixes f :: "'a ⇒ ennreal" assumes "f ∈ borel_measurable M" shows "(∫⇧^{+}x. f(T x) ∂M) = (∫⇧^{+}x. f x ∂M)" using measure_preserving_preserves_nn_integral[OF Tm assms] by auto lemma Tn_nn_integral_preserving: fixes f :: "'a ⇒ ennreal" assumes "f ∈ borel_measurable M" shows "(∫⇧^{+}x. f((T^^n) x) ∂M) = (∫⇧^{+}x. f x ∂M)" using measure_preserving_preserves_nn_integral[OF Tn_measure_preserving assms(1)] by auto lemma mpt_power: "mpt M (T^^n)" by (standard, simp_all add: Tn_quasi_measure_preserving Tn_measure_preserving) lemma T_vrestr_same_emeasure: assumes "A ∈ sets M" shows "emeasure M (T--` A) = emeasure M A" "emeasure M ((T ^^ n)--`A) = emeasure M A" by (auto simp add: vrestr_same_emeasure_f Tm Tn_measure_preserving assms) lemma T_vrestr_same_measure: assumes "A ∈ sets M" shows "measure M (T--` A) = measure M A" "measure M ((T ^^ n)--`A) = measure M A" by (auto simp add: vrestr_same_measure_f Tm Tn_measure_preserving assms) lemma (in fmpt) fmpt_power: "fmpt M (T^^n)" by (standard, simp_all add: Tn_quasi_measure_preserving Tn_measure_preserving) end subsection ‹Birkhoff sums› text ‹Birkhoff sums, obtained by summing a function along the orbit of a map, are basic objects to be understood in ergodic theory.› context qmpt begin definition birkhoff_sum::"('a ⇒ 'b::comm_monoid_add) ⇒ nat ⇒ 'a ⇒ 'b" where "birkhoff_sum f n x = (∑i∈{..<n}. f((T^^i)x))" lemma birkhoff_sum_meas [measurable]: fixes f::"'a ⇒ 'b::{second_countable_topology, topological_comm_monoid_add}" assumes "f ∈ borel_measurable M" shows "birkhoff_sum f n ∈ borel_measurable M" proof - define F where "F = (λi x. f((T^^i)x))" have "⋀i. F i ∈ borel_measurable M" using assms F_def by auto then have "(λx. (∑i<n. F i x)) ∈ borel_measurable M" by measurable then have "(λx. birkhoff_sum f n x) ∈ borel_measurable M" unfolding birkhoff_sum_def F_def by auto then show ?thesis by simp qed lemma birkhoff_sum_1 [simp]: "birkhoff_sum f 0 x = 0" "birkhoff_sum f 1 x = f x" "birkhoff_sum f (Suc 0) x = f x" unfolding birkhoff_sum_def by auto lemma birkhoff_sum_cocycle: "birkhoff_sum f (n+m) x = birkhoff_sum f n x + birkhoff_sum f m ((T^^n)x)" proof - have "(∑i<m. f ((T ^^ i) ((T ^^ n) x))) = (∑i<m. f ((T ^^ (i+n)) x))" by (simp add: funpow_add) also have "... = (∑j∈{n..< m+n}. f ((T ^^j) x))" using atLeast0LessThan sum.shift_bounds_nat_ivl[where ?g = "λj. f((T^^j)x)" and ?k = n and ?m = 0 and ?n = m, symmetric] add.commute add.left_neutral by auto finally have *: "birkhoff_sum f m ((T^^n)x) = (∑j∈{n..< m+n}. f ((T ^^j) x))" unfolding birkhoff_sum_def by auto have "birkhoff_sum f (n+m) x = (∑i<n. f((T^^i)x)) + (∑i∈{n..<m+n}. f((T^^i)x))" unfolding birkhoff_sum_def by (metis add.commute add.right_neutral atLeast0LessThan le_add2 sum.atLeastLessThan_concat) also have "... = birkhoff_sum f n x + (∑i∈{n..<m+n}. f((T^^i)x))" unfolding birkhoff_sum_def by simp finally show ?thesis using * by simp qed lemma birkhoff_sum_mono: fixes f g::"_ ⇒ real" assumes "⋀x. f x ≤ g x" shows "birkhoff_sum f n x ≤ birkhoff_sum g n x" unfolding birkhoff_sum_def by (simp add: assms sum_mono) lemma birkhoff_sum_abs: fixes f::"_ ⇒ 'b::real_normed_vector" shows "norm(birkhoff_sum f n x) ≤ birkhoff_sum (λx. norm(f x)) n x" unfolding birkhoff_sum_def using norm_sum by auto lemma birkhoff_sum_add: "birkhoff_sum (λx. f x + g x) n x = birkhoff_sum f n x + birkhoff_sum g n x" unfolding birkhoff_sum_def by (simp add: sum.distrib) lemma birkhoff_sum_diff: fixes f g::"_ ⇒ real" shows "birkhoff_sum (λx. f x - g x) n x = birkhoff_sum f n x - birkhoff_sum g n x" unfolding birkhoff_sum_def by (simp add: sum_subtractf) lemma birkhoff_sum_cmult: fixes f::"_ ⇒ real" shows "birkhoff_sum (λx. c * f x) n x = c * birkhoff_sum f n x" unfolding birkhoff_sum_def by (simp add: sum_distrib_left) lemma skew_product_real_iterates: fixes f::"'a ⇒ real" shows "((λ(x,y). (T x, y + f x))^^n) (x,y) = ((T^^n) x, y + birkhoff_sum f n x)" apply (induction n) apply (auto) apply (metis (no_types, lifting) Suc_eq_plus1 birkhoff_sum_cocycle qmpt.birkhoff_sum_1(2) qmpt_axioms) done end lemma (in mpt) birkhoff_sum_integral: fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}" assumes [measurable]: "integrable M f" shows "integrable M (birkhoff_sum f n)" "(∫x. birkhoff_sum f n x ∂M) = n *⇩_{R}(∫x. f x ∂M)" proof - have a: "⋀k. integrable M (λx. f((T^^k) x))" using Tn_integral_preserving(1) assms by blast then have "integrable M (λx. ∑k∈{..<n}. f((T^^k) x))" by simp then have "integrable M (λx. birkhoff_sum f n x)" unfolding birkhoff_sum_def by auto then show "integrable M (birkhoff_sum f n)" by simp have b: "⋀k. (∫x. f((T^^k)x) ∂M) = (∫x. f x ∂M)" using Tn_integral_preserving(2) assms by blast have "(∫x. birkhoff_sum f n x ∂M) = (∫x. (∑k∈{..<n}. f((T^^k) x)) ∂M)" unfolding birkhoff_sum_def by blast also have "... = (∑k∈{..<n}. (∫x. f((T^^k) x) ∂M))" by (rule Bochner_Integration.integral_sum, simp add: a) also have "... = (∑k∈{..<n}. (∫x. f x ∂M))" using b by simp also have "... = n *⇩_{R}(∫x. f x ∂M)" by (simp add: sum_constant_scaleR) finally show "(∫x. birkhoff_sum f n x ∂M) = n *⇩_{R}(∫x. f x ∂M)" by simp qed lemma (in mpt) birkhoff_sum_nn_integral: fixes f :: "'a ⇒ ennreal" assumes [measurable]: "f ∈ borel_measurable M" and pos: "⋀x. f x ≥ 0" shows "(∫⇧^{+}x. birkhoff_sum f n x ∂M) = n * (∫⇧^{+}x. f x ∂M)" proof - have [measurable]: "⋀k. (λx. f((T^^k)x)) ∈ borel_measurable M" by simp have posk: "⋀k x. f((T^^k)x) ≥ 0" using pos by simp have b: "⋀k. (∫⇧^{+}x. f((T^^k)x) ∂M) = (∫⇧^{+}x. f x ∂M)" using Tn_nn_integral_preserving assms by blast have "(∫⇧^{+}x. birkhoff_sum f n x ∂M) = (∫⇧^{+}x. (∑k∈{..<n}. f((T^^k) x)) ∂M)" unfolding birkhoff_sum_def by blast also have "... = (∑k∈{..<n}. (∫⇧^{+}x. f((T^^k) x) ∂M))" by (rule nn_integral_sum, auto simp add: posk) also have "... = (∑k∈{..<n}. (∫⇧^{+}x. f x ∂M))" using b by simp also have "... = n * (∫⇧^{+}x. f x ∂M)" by simp finally show "(∫⇧^{+}x. birkhoff_sum f n x ∂M) = n * (∫⇧^{+}x. f x ∂M)" by simp qed subsection ‹Inverse map› context qmpt begin definition "invertible_qmpt ≡ (bij T ∧ inv T ∈ measurable M M)" definition "Tinv ≡ inv T" lemma T_Tinv_of_set: assumes "invertible_qmpt" "A ∈ sets M" shows "T-`(Tinv-`A ∩ space M) ∩ space M = A" using assms sets.sets_into_space unfolding Tinv_def invertible_qmpt_def apply (auto simp add: bij_betw_def) using T_spaceM_stable(1) by blast lemma Tinv_quasi_measure_preserving: assumes "invertible_qmpt" shows "Tinv ∈ quasi_measure_preserving M M" proof (rule quasi_measure_preservingI, auto) fix A assume [measurable]: "A ∈ sets M" "Tinv -` A ∩ space M ∈ null_sets M" then have "T-`(Tinv -` A ∩ space M) ∩ space M ∈ null_sets M" by (metis T_quasi_preserves_null2(1) null_sets.Int_space_eq2 vimage_restr_def) then show "A ∈ null_sets M" using T_Tinv_of_set[OF assms ‹A ∈ sets M›] by auto next show [measurable]: "Tinv ∈ measurable M M" using assms unfolding Tinv_def invertible_qmpt_def by blast fix A assume [measurable]: "A ∈ sets M" "A ∈ null_sets M" then have "T-`(Tinv -` A ∩ space M) ∩ space M ∈ null_sets M" using T_Tinv_of_set[OF assms ‹A ∈ sets M›] by auto moreover have [measurable]: "Tinv-`A ∩ space M ∈ sets M" by auto ultimately show "Tinv -` A ∩ space M ∈ null_sets M" using T_meas T_quasi_preserves_null(1) vrestr_of_set by presburger qed lemma Tinv_qmpt: assumes "invertible_qmpt" shows "qmpt M Tinv" unfolding qmpt_def qmpt_axioms_def using Tinv_quasi_measure_preserving[OF assms] by (simp add: sigma_finite_measure_axioms) end lemma (in mpt) Tinv_measure_preserving: assumes "invertible_qmpt" shows "Tinv ∈ measure_preserving M M" proof (rule measure_preservingI) show [measurable]: "Tinv ∈ measurable M M" using assms unfolding Tinv_def invertible_qmpt_def by blast fix A assume [measurable]: "A ∈ sets M" have "A = T-`(Tinv -` A ∩ space M) ∩ space M" using T_Tinv_of_set[OF assms ‹A ∈ sets M›] by auto then show "emeasure M (Tinv -` A ∩ space M) = emeasure M A" by (metis T_vrestr_same_emeasure(1) ‹A ∈ sets M› ‹Tinv ∈ M →⇩_{M}M› measurable_sets sets.Int_space_eq2 vimage_restr_def) qed lemma (in mpt) Tinv_mpt: assumes "invertible_qmpt" shows "mpt M Tinv" unfolding mpt_def mpt_axioms_def using Tinv_qmpt[OF assms] Tinv_measure_preserving[OF assms] by auto lemma (in fmpt) Tinv_fmpt: assumes "invertible_qmpt" shows "fmpt M Tinv" unfolding fmpt_def using Tinv_mpt[OF assms] by (simp add: finite_measure_axioms) lemma (in pmpt) Tinv_fmpt: assumes "invertible_qmpt" shows "pmpt M Tinv" unfolding pmpt_def using Tinv_fmpt[OF assms] by (simp add: prob_space_axioms) subsection ‹Factors› text ‹Factors of a system are quotients of this system, i.e., systems that can be obtained by a projection, forgetting some part of the dynamics. It is sometimes possible to transfer a result from a factor to the original system, making it possible to prove theorems by reduction to a simpler situation. The dual notion, extension, is equally important and useful. We only mention factors below, as the results for extension readily follow by considering the original system as a factor of its extension. In this paragraph, we define factors both in the qmpt and mpt categories, and prove their basic properties. › definition (in qmpt) qmpt_factor::"('a ⇒ 'b) ⇒ ('b measure) ⇒ ('b ⇒ 'b) ⇒ bool" where "qmpt_factor proj M2 T2 = ((proj ∈ quasi_measure_preserving M M2) ∧ (AE x in M. proj (T x) = T2 (proj x)) ∧ qmpt M2 T2)" lemma (in qmpt) qmpt_factorE: assumes "qmpt_factor proj M2 T2" shows "proj ∈ quasi_measure_preserving M M2" "AE x in M. proj (T x) = T2 (proj x)" "qmpt M2 T2" using assms unfolding qmpt_factor_def by auto lemma (in qmpt) qmpt_factor_iterates: assumes "qmpt_factor proj M2 T2" shows "AE x in M. ∀n. proj ((T^^n) x) = (T2^^n) (proj x)" proof - have "AE x in M. ∀n. proj (T ((T^^n) x)) = T2 (proj ((T^^n) x))" by (rule T_AE_iterates[OF qmpt_factorE(2)[OF assms]]) moreover { fix x assume "∀n. proj (T ((T^^n) x)) = T2 (proj ((T^^n) x))" then have H: "proj (T ((T^^n) x)) = T2 (proj ((T^^n) x))" for n by auto have "proj ((T^^n) x) = (T2^^n) (proj x)" for n apply (induction n) using H by auto then have "∀n. proj ((T^^n) x) = (T2^^n) (proj x)" by auto } ultimately show ?thesis by fast qed lemma (in qmpt) qmpt_factorI: assumes "proj ∈ quasi_measure_preserving M M2" "AE x in M. proj (T x) = T2 (proj x)" "qmpt M2 T2" shows "qmpt_factor proj M2 T2" using assms unfolding qmpt_factor_def by auto text ‹When there is a quasi-measure-preserving projection, then the quotient map automatically is quasi-measure-preserving. The same goes for measure-preservation below.› lemma (in qmpt) qmpt_factorI': assumes "proj ∈ quasi_measure_preserving M M2" "AE x in M. proj (T x) = T2 (proj x)" "sigma_finite_measure M2" "T2 ∈ measurable M2 M2" shows "qmpt_factor proj M2 T2" proof - have [measurable]: "T ∈ measurable M M" "T2 ∈ measurable M2 M2" "proj ∈ measurable M M2" using assms(4) quasi_measure_preservingE(1)[OF assms(1)] by auto have *: "(T2 -` A ∩ space M2 ∈ null_sets M2) = (A ∈ null_sets M2)" if "A ∈ sets M2" for A proof - obtain U where U: "⋀x. x ∈ space M - U ⟹ proj (T x) = T2 (proj x)" "U ∈ null_sets M" using AE_E3[OF assms(2)] by blast then have [measurable]: "U ∈ sets M" by auto have [measurable]: "A ∈ sets M2" using that by simp have e1: "(T-`(proj-`A ∩ space M)) ∩ space M = T-`(proj-`A) ∩ space M" using subset_eq by auto have e2: "T-`(proj-`A) ∩ space M - U = proj-`(T2-`A) ∩ space M - U" using U(1) by auto have e3: "proj-`(T2-`A) ∩ space M = proj-`(T2-`A ∩ space M2) ∩ space M" by (auto, meson ‹proj ∈ M →⇩_{M}M2› measurable_space) have "A ∈ null_sets M2 ⟷ proj-`A ∩ space M ∈ null_sets M" using quasi_measure_preservingE(2)[OF assms(1)] by simp also have "... ⟷ (T-`(proj-`A ∩ space M)) ∩ space M ∈ null_sets M" by (rule quasi_measure_preservingE(2)[OF Tqm, symmetric], auto) also have "... ⟷ T-`(proj-`A) ∩ space M ∈ null_sets M" using e1 by simp also have "... ⟷ T-`(proj-`A) ∩ space M - U ∈ null_sets M" using emeasure_Diff_null_set[OF ‹U ∈ null_sets M›] unfolding null_sets_def by auto also have "... ⟷ proj-`(T2-`A) ∩ space M - U ∈ null_sets M" using e2 by simp also have "... ⟷ proj-`(T2-`A) ∩ space M ∈ null_sets M" using emeasure_Diff_null_set[OF ‹U ∈ null_sets M›] unfolding null_sets_def by auto also have "... ⟷ proj-`(T2-`A ∩ space M2) ∩ space M ∈ null_sets M" using e3 by simp also have "... ⟷ T2-`A ∩ space M2 ∈ null_sets M2" using quasi_measure_preservingE(2)[OF assms(1), of "T2-`A ∩ space M2"] by simp finally show "T2-`A ∩ space M2 ∈ null_sets M2 ⟷ A ∈ null_sets M2" by simp qed show ?thesis by (intro qmpt_factorI qmpt_I) (auto simp add: assms *) qed lemma qmpt_factor_compose: assumes "qmpt M1 T1" "qmpt.qmpt_factor M1 T1 proj1 M2 T2" "qmpt.qmpt_factor M2 T2 proj2 M3 T3" shows "qmpt.qmpt_factor M1 T1 (proj2 o proj1) M3 T3" proof - have *: "proj1 ∈ quasi_measure_preserving M1 M2 ⟹ AE x in M2. proj2 (T2 x) = T3 (proj2 x) ⟹ (AE x in M1. proj1 (T1 x) = T2 (proj1 x) ⟶ proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x)))" proof - assume "AE y in M2. proj2 (T2 y) = T3 (proj2 y)" "proj1 ∈ quasi_measure_preserving M1 M2" then have "AE x in M1. proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))" using quasi_measure_preserving_AE by auto moreover { fix x assume "proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))" then have "proj1 (T1 x) = T2 (proj1 x) ⟶ proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))" by auto } ultimately show "AE x in M1. proj1 (T1 x) = T2 (proj1 x) ⟶ proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))" by auto qed interpret I: qmpt M1 T1 using assms(1) by simp interpret J: qmpt M2 T2 using I.qmpt_factorE(3)[OF assms(2)] by simp show "I.qmpt_factor (proj2 o proj1) M3 T3" apply (rule I.qmpt_factorI) using I.qmpt_factorE[OF assms(2)] J.qmpt_factorE[OF assms(3)] by (auto simp add: quasi_measure_preserving_comp *) qed text ‹The left shift on natural integers is a very natural dynamical system, that can be used to model many systems as we see below. For invertible systems, one uses rather all the integers.› definition nat_left_shift::"(nat ⇒ 'a) ⇒ (nat ⇒ 'a)" where "nat_left_shift x = (λi. x (i+1))" lemma nat_left_shift_continuous [intro, continuous_intros]: "continuous_on UNIV nat_left_shift" by (rule continuous_on_coordinatewise_then_product, auto simp add: nat_left_shift_def) lemma nat_left_shift_measurable [intro, measurable]: "nat_left_shift ∈ measurable borel borel" by (rule borel_measurable_continuous_onI, auto) definition int_left_shift::"(int ⇒ 'a) ⇒ (int ⇒ 'a)" where "int_left_shift x = (λi. x (i+1))" definition int_right_shift::"(int ⇒ 'a) ⇒ (int ⇒ 'a)" where "int_right_shift x = (λi. x (i-1))" lemma int_shift_continuous [intro, continuous_intros]: "continuous_on UNIV int_left_shift" "continuous_on UNIV int_right_shift" apply (rule continuous_on_coordinatewise_then_product, auto simp add: int_left_shift_def) apply (rule continuous_on_coordinatewise_then_product, auto simp add: int_right_shift_def) done lemma int_shift_measurable [intro, measurable]: "int_left_shift ∈ measurable borel borel" "int_right_shift ∈ measurable borel borel" by (rule borel_measurable_continuous_onI, auto)+ lemma int_shift_bij: "bij int_left_shift" "inv int_left_shift = int_right_shift" "bij int_right_shift" "inv int_right_shift = int_left_shift" proof - show "bij int_left_shift" apply (rule bij_betw_byWitness[where ?f' = "λx. (λi. x (i-1))"]) unfolding int_left_shift_def by auto show "inv int_left_shift = int_right_shift" apply (rule inv_equality) unfolding int_left_shift_def int_right_shift_def by auto show "bij int_right_shift" apply (rule bij_betw_byWitness[where ?f' = "λx. (λi. x (i+1))"]) unfolding int_right_shift_def by auto show "inv int_right_shift = int_left_shift" apply (rule inv_equality) unfolding int_left_shift_def int_right_shift_def by auto qed lemma (in qmpt) qmpt_factor_projection: fixes f::"'a ⇒ ('b::second_countable_topology)" assumes [measurable]: "f ∈ borel_measurable M" and "sigma_finite_measure (distr M borel (λx n. f ((T ^^ n) x)))" shows "qmpt_factor (λx. (λn. f ((T^^n)x))) (distr M borel (λx. (λn. f ((T^^n)x)))) nat_left_shift" proof (rule qmpt_factorI') have * [measurable]: "(λx. (λn. f ((T^^n)x))) ∈ borel_measurable M" using measurable_coordinatewise_then_product by measurable show "(λx n. f ((T ^^ n) x)) ∈ quasi_measure_preserving M (distr M borel (λx n. f ((T ^^ n) x)))" by (rule measure_preserving_is_quasi_measure_preserving[OF measure_preserving_distr'[OF *]]) have "(λn. f ((T ^^ n) (T x))) = nat_left_shift (λn. f ((T ^^ n) x))" for x unfolding nat_left_shift_def by (auto simp add: funpow_swap1) then show "AE x in M. (λn. f ((T ^^ n) (T x))) = nat_left_shift (λn. f ((T ^^ n) x))" by simp qed (auto simp add: assms(2)) text ‹Let us now define factors of measure-preserving transformations, in the same way as above.› definition (in mpt) mpt_factor::"('a ⇒ 'b) ⇒ ('b measure) ⇒ ('b ⇒ 'b) ⇒ bool" where "mpt_factor proj M2 T2 = ((proj ∈ measure_preserving M M2) ∧ (AE x in M. proj (T x) = T2 (proj x)) ∧ mpt M2 T2)" lemma (in mpt) mpt_factor_is_qmpt_factor: assumes "mpt_factor proj M2 T2" shows "qmpt_factor proj M2 T2" using assms unfolding mpt_factor_def qmpt_factor_def by (simp add: measure_preserving_is_quasi_measure_preserving mpt_def) lemma (in mpt) mpt_factorE: assumes "mpt_factor proj M2 T2" shows "proj ∈ measure_preserving M M2" "AE x in M. proj (T x) = T2 (proj x)" "mpt M2 T2" using assms unfolding mpt_factor_def by auto lemma (in mpt) mpt_factorI: assumes "proj ∈ measure_preserving M M2" "AE x in M. proj (T x) = T2 (proj x)" "mpt M2 T2" shows "mpt_factor proj M2 T2" using assms unfolding mpt_factor_def by auto text ‹When there is a measure-preserving projection commuting with the dynamics, and the dynamics above preserves the measure, then so does the dynamics below.› lemma (in mpt) mpt_factorI': assumes "proj ∈ measure_preserving M M2" "AE x in M. proj (T x) = T2 (proj x)" "sigma_finite_measure M2" "T2 ∈ measurable M2 M2" shows "mpt_factor proj M2 T2" proof - have [measurable]: "T ∈ measurable M M" "T2 ∈ measurable M2 M2" "proj ∈ measurable M M2" using assms(4) measure_preservingE(1)[OF assms(1)] by auto have *: "emeasure M2 (T2 -` A ∩ space M2) = emeasure M2 A" if "A ∈ sets M2" for A proof - obtain U where U: "⋀x. x ∈ space M - U ⟹ proj (T x) = T2 (proj x)" "U ∈ null_sets M" using AE_E3[OF assms(2)] by blast then have [measurable]: "U ∈ sets M" by auto have [measurable]: "A ∈ sets M2" using that by simp have e1: "(T-`(proj-`A ∩ space M)) ∩ space M = T-`(proj-`A) ∩ space M" using subset_eq by auto have e2: "T-`(proj-`A) ∩ space M - U = proj-`(T2-`A) ∩ space M - U" using U(1) by auto have e3: "proj-`(T2-`A) ∩ space M = proj-`(T2-`A ∩ space M2) ∩ space M" by (auto, meson ‹proj ∈ M →⇩_{M}M2› measurable_space) have "emeasure M2 A = emeasure M (proj-`A ∩ space M)" using measure_preservingE(2)[OF assms(1)] by simp also have "... = emeasure M (T-`(proj-`A ∩ space M) ∩ space M)" by (rule measure_preservingE(2)[OF Tm, symmetric], auto) also have "... = emeasure M (T-`(proj-`A) ∩ space M)" using e1 by simp also have "... = emeasure M (T-`(proj-`A) ∩ space M - U)" using emeasure_Diff_null_set[OF ‹U ∈ null_sets M›] by auto also have "... = emeasure M (proj-`(T2-`A) ∩ space M - U)" using e2 by simp also have "... = emeasure M (proj-`(T2-`A) ∩ space M)" using emeasure_Diff_null_set[OF ‹U ∈ null_sets M›] by auto also have "... = emeasure M (proj-`(T2-`A ∩ space M2) ∩ space M)" using e3 by simp also have "... = emeasure M2 (T2-`A ∩ space M2)" using measure_preservingE(2)[OF assms(1), of "T2-`A ∩ space M2"] by simp finally show "emeasure M2 (T2-`A ∩ space M2) = emeasure M2 A" by simp qed show ?thesis by (intro mpt_factorI mpt_I) (auto simp add: assms *) qed lemma (in fmpt) mpt_factorI'': assumes "proj ∈ measure_preserving M M2" "AE x in M. proj (T x) = T2 (proj x)" "T2 ∈ measurable M2 M2" shows "mpt_factor proj M2 T2" apply (rule mpt_factorI', auto simp add: assms) using measure_preserving_finite_measure[OF assms(1)] finite_measure_axioms finite_measure_def by blast lemma (in fmpt) fmpt_factor: assumes "mpt_factor proj M2 T2" shows "fmpt M2 T2" unfolding fmpt_def using mpt_factorE(3)[OF assms] measure_preserving_finite_measure[OF mpt_factorE(1)[OF assms]] finite_measure_axioms by auto lemma (in pmpt) pmpt_factor: assumes "mpt_factor proj M2 T2" shows "pmpt M2 T2" unfolding pmpt_def using fmpt_factor[OF assms] measure_preserving_prob_space[OF mpt_factorE(1)[OF assms]] prob_space_axioms by auto lemma mpt_factor_compose: assumes "mpt M1 T1" "mpt.mpt_factor M1 T1 proj1 M2 T2" "mpt.mpt_factor M2 T2 proj2 M3 T3" shows "mpt.mpt_factor M1 T1 (proj2 o proj1) M3 T3" proof - have *: "proj1 ∈ measure_preserving M1 M2 ⟹ AE x in M2. proj2 (T2 x) = T3 (proj2 x) ⟹ (AE x in M1. proj1 (T1 x) = T2 (proj1 x) ⟶ proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x)))" proof - assume "AE y in M2. proj2 (T2 y) = T3 (proj2 y)" "proj1 ∈ measure_preserving M1 M2" then have "AE x in M1. proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))" using quasi_measure_preserving_AE measure_preserving_is_quasi_measure_preserving by blast moreover { fix x assume "proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))" then have "proj1 (T1 x) = T2 (proj1 x) ⟶ proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))" by auto } ultimately show "AE x in M1. proj1 (T1 x) = T2 (proj1 x) ⟶ proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))" by auto qed interpret I: mpt M1 T1 using assms(1) by simp interpret J: mpt M2 T2 using I.mpt_factorE(3)[OF assms(2)] by simp show "I.mpt_factor (proj2 o proj1) M3 T3" apply (rule I.mpt_factorI) using I.mpt_factorE[OF assms(2)] J.mpt_factorE[OF assms(3)] by (auto simp add: measure_preserving_comp *) qed text ‹Left shifts are naturally factors of finite measure preserving transformations.› lemma (in mpt) mpt_factor_projection: fixes f::"'a ⇒ ('b::second_countable_topology)" assumes [measurable]: "f ∈ borel_measurable M" and "sigma_finite_measure (distr M borel (λx n. f ((T ^^ n) x)))" shows "mpt_factor (λx. (λn. f ((T^^n)x))) (distr M borel (λx. (λn. f ((T^^n)x)))) nat_left_shift" proof (rule mpt_factorI') have * [measurable]: "(λx. (λn. f ((T^^n)x))) ∈ borel_measurable M" using measurable_coordinatewise_then_product by measurable show "(λx n. f ((T ^^ n) x)) ∈ measure_preserving M (distr M borel (λx n. f ((T ^^ n) x)))" by (rule measure_preserving_distr'[OF *]) have "(λn. f ((T ^^ n) (T x))) = nat_left_shift (λn. f ((T ^^ n) x))" for x unfolding nat_left_shift_def by (auto simp add: funpow_swap1) then show "AE x in M. (λn. f ((T ^^ n) (T x))) = nat_left_shift (λn. f ((T ^^ n) x))" by simp qed (auto simp add: assms(2)) lemma (in fmpt) fmpt_factor_projection: fixes f::"'a ⇒ ('b::second_countable_topology)" assumes [measurable]: "f ∈ borel_measurable M" shows "mpt_factor (λx. (λn. f ((T^^n)x))) (distr M borel (λx. (λn. f ((T^^n)x)))) nat_left_shift" proof (rule mpt_factor_projection, simp add: assms) have * [measurable]: "(λx. (λn. f ((T^^n)x))) ∈ borel_measurable M" using measurable_coordinatewise_then_product by measurable have **: "(λx n. f ((T ^^ n) x)) ∈ measure_preserving M (distr M borel (λx n. f ((T ^^ n) x)))" by (rule measure_preserving_distr'[OF *]) have a: "finite_measure (distr M borel (λx n. f ((T ^^ n) x)))" using measure_preserving_finite_measure[OF **] finite_measure_axioms by blast then show "sigma_finite_measure (distr M borel (λx n. f ((T ^^ n) x)))" by (simp add: finite_measure_def) qed subsection ‹Natural extension› text ‹Many probability preserving dynamical systems are not invertible, while invertibility is often useful in proofs. The notion of natural extension is a solution to this problem: it shows that (essentially) any system has an extension which is invertible. This extension is constructed by considering the space of orbits indexed by integer numbers, with the left shift acting on it. If one considers the orbits starting from time $-N$ (for some fixed $N$), then there is a natural measure on this space: such an orbit is parameterized by its starting point at time $-N$, hence one may use the original measure on this point. The invariance of the measure ensures that these measures are compatible with each other. Their projective limit (when $N$ tends to infinity) is thus an invariant measure on the bilateral shift. The shift with this measure is the desired extension of the original system. There is a difficulty in the above argument: one needs to make sure that the projective limit of a system of compatible measures is well defined. This requires some topological conditions on the measures (they should be inner regular, i.e., the measure of any set should be approximated from below by compact subsets -- this is automatic on polish spaces). The existence of projective limits is proved in \verb+Projective_Limits.thy+ under the (sufficient) polish condition. We use this theory, so we need the underlying space to be a polish space and the measure to be a Borel measure. This is almost completely satisfactory. What is not completely satisfactory is that the completion of a Borel measure on a polish space (i.e., we add all subsets of sets of measure $0$ into the sigma algebra) does not fit into this setting, while this is an important framework in dynamical systems. It would readily follow once \verb+Projective_Limits.thy+ is extended to the more general inner regularity setting (the completion of a Borel measure on a polish space is always inner regular). › locale polish_pmpt = pmpt "M::('a::polish_space measure)" T for M T + assumes M_eq_borel: "sets M = sets borel" begin definition natural_extension_map where "natural_extension_map = (int_left_shift::((int ⇒ 'a) ⇒ (int ⇒ 'a)))" definition natural_extension_measure::"(int ⇒ 'a) measure" where "natural_extension_measure = projective_family.lim UNIV (λI. distr M (Π⇩_{M}i∈I. borel) (λx. (λi∈I. (T^^(nat(i- Min I))) x))) (λi. borel)" definition natural_extension_proj::"(int ⇒ 'a) ⇒ 'a" where "natural_extension_proj = (λx. x 0)" theorem natural_extension: "pmpt natural_extension_measure natural_extension_map" "qmpt.invertible_qmpt natural_extension_measure natural_extension_map" "mpt.mpt_factor natural_extension_measure natural_extension_map natural_extension_proj M T" proof - define P::"int set ⇒ (int ⇒ 'a) measure" where "P = (λI. distr M (Π⇩_{M}i∈I. borel) (λx. (λi∈I. (T^^(nat(i- Min I))) x)))" have [measurable]: "(T^^n) ∈ measurable M borel" for n using M_eq_borel by auto interpret polish_projective UNIV P unfolding polish_projective_def projective_family_def proof (auto) show "prob_space (P I)" if "finite I" for I unfolding P_def by (rule prob_space_distr, auto) fix J H::"int set" assume "J ⊆ H" "finite H" then have "H ∩ J = J" by blast have "((λf. restrict f J) o (λx. (λi∈H. (T^^(nat(i- Min H))) x))) x = ((λx. (λi∈J. (T^^(nat(i- Min J))) x)) o (T^^(nat(Min J - Min H)))) x" for x proof - have "nat(i- Min H) = nat(i- Min J) + nat(Min J - Min H)" if "i ∈ J" for i proof - have "finite J" using ‹J ⊆ H› ‹finite H› finite_subset by auto then have "Min J ∈ J" using Min_in ‹i ∈ J› by auto then have "Min J ∈ H" using ‹J ⊆ H› by blast then have "Min H ≤ Min J" using Min.coboundedI[OF ‹finite H›] by auto moreover have "Min J ≤ i" using Min.coboundedI[OF ‹finite J› ‹i ∈ J›] by auto ultimately show ?thesis by auto qed then show ?thesis unfolding comp_def by (auto simp add: ‹H ∩ J = J› funpow_add) qed then have *: "(λf. restrict f J) o (λx. (λi∈H. (T^^(nat(i- Min H))) x)) = (λx. (λi∈J. (T^^(nat(i- Min J))) x)) o (T^^(nat(Min J - Min H)))" by auto have "distr (P H) (Pi⇩_{M}J (λ_. borel)) (λf. restrict f J) = distr M (Π⇩_{M}i∈J. borel) ((λf. restrict f J) o (λx. (λi∈H. (T^^(nat(i- Min H))) x)))" unfolding P_def by (rule distr_distr, auto simp add: ‹J ⊆ H› measurable_restrict_subset) also have "... = distr M (Π⇩_{M}i∈J. borel) ((λx. (λi∈J. (T^^(nat(i- Min J))) x)) o (T^^(nat(Min J - Min H))))" using * by auto also have "... = distr (distr M M (T^^(nat(Min J - Min H)))) (Π⇩_{M}i∈J. borel) (λx. (λi∈J. (T^^(nat(i- Min J))) x))" by (rule distr_distr[symmetric], auto) also have "... = distr M (Π⇩_{M}i∈J. borel) (λx. (λi∈J. (T^^(nat(i- Min J))) x))" using measure_preserving_distr[OF Tn_measure_preserving] by auto also have "... = P J" unfolding P_def by auto finally show "P J = distr (P H) (Pi⇩_{M}J (λ_. borel)) (λf. restrict f J)" by simp qed have S: "sets (Pi⇩_{M}UNIV (λ_. borel)) = sets (borel::(int ⇒ 'a) measure)" by (rule sets_PiM_equal_borel) have "natural_extension_measure = lim" unfolding natural_extension_measure_def P_def by simp have "measurable lim lim = measurable borel borel" by (rule measurable_cong_sets, auto simp add: S) then have [measurable]: "int_left_shift ∈ measurable lim lim" "int_right_shift ∈ measurable lim lim" using int_shift_measurable by fast+ have [simp]: "space lim = UNIV" unfolding space_lim space_PiM space_borel by auto show "pmpt natural_extension_measure natural_extension_map" proof (rule pmpt_I) show "prob_space natural_extension_measure" unfolding ‹natural_extension_measure = lim› by (simp add: P.prob_space_axioms) show "natural_extension_map ∈ measurable natural_extension_measure natural_extension_measure" unfolding natural_extension_map_def ‹natural_extension_measure = lim› by simp define E where "E = {(Π⇩_{E}i∈UNIV. X i) |X::(int ⇒ 'a set). (∀i. X i ∈ sets borel) ∧ finite {i. X i ≠ UNIV}}" have "lim = distr lim lim int_left_shift" proof (rule measure_eqI_generator_eq[of E UNIV, where ?A = "λ_. UNIV"]) show "sets lim = sigma_sets UNIV E" unfolding E_def using sets_PiM_finite[of "UNIV::int set" "λ_. (borel::'a measure)"] by (simp add: PiE_def) moreover have "sets (distr lim lim int_left_shift) = sets lim" by auto ultimately show "sets (distr lim lim int_left_shift) = sigma_sets UNIV E" by simp show "emeasure lim UNIV ≠ ∞" by (simp add: P.prob_space_axioms) have "UNIV = (Π⇩_{E}i∈(UNIV::int set). (UNIV::'a set))" by (simp add: PiE_def) moreover have "... ∈ E" unfolding E_def by auto ultimately show "range (λ(i::nat). (UNIV::(int ⇒ 'a) set)) ⊆ E" by auto show "Int_stable E" proof (rule Int_stableI) fix U V assume "U ∈ E" "V ∈ E" then obtain X Y where H: "U = (Π⇩_{E}i∈UNIV. X i)" "⋀i. X i ∈ sets borel" "finite {i. X i ≠ UNIV}" "V = (Π⇩_{E}i∈UNIV. Y i)" "⋀i. Y i ∈ sets borel" "finite {i. Y i ≠ UNIV}" unfolding E_def by blast define Z where "Z = (λi. X i ∩ Y i)" have "{i. Z i ≠ UNIV} ⊆ {i. X i ≠ UNIV} ∪ {i. Y i ≠ UNIV}" unfolding Z_def by auto then have "finite {i. Z i ≠ UNIV}" using H(3) H(6) finite_subset by auto moreover have "U ∩ V = (Π⇩_{E}i∈UNIV. Z i)" unfolding Z_def using H(1) H(4) by auto moreover have "⋀i. Z i ∈ sets borel" unfolding Z_def using H(2) H(5) by auto ultimately show "U ∩ V ∈ E" unfolding E_def by auto qed fix U assume "U ∈ E" then obtain X where H [measurable]: "U = (Π⇩_{E}i∈UNIV. X i)" "⋀i. X i ∈ sets borel" "finite {i. X i ≠ UNIV}" unfolding E_def by blast define I where "I = {i. X i ≠ UNIV}" have [simp]: "finite I" unfolding I_def using H(3) by auto have [measurable]: "(Π⇩_{E}i∈I. X i) ∈ sets (Pi⇩_{M}I (λi. borel))" using H(2) by simp have *: "U = emb UNIV I (Π⇩_{E}i∈I. X i)" unfolding H(1) I_def prod_emb_def space_borel apply (auto simp add: PiE_def) by (metis (mono_tags, lifting) PiE UNIV_I mem_Collect_eq restrict_Pi_cancel) have "emeasure lim U = emeasure lim (int_left_shift-`U)" proof (cases "I = {}") case True then have "U = UNIV" unfolding H(1) I_def by auto then show ?thesis by auto next case False have "emeasure lim U = emeasure (P I) (Π⇩_{E}i∈I. X i)" unfolding * by (rule emeasure_lim_emb, auto) also have "... = emeasure M (((λx. (λi∈I. (T^^(nat(i- Min I))) x)))-`(Π⇩_{E}i∈I. X i) ∩ space M)" unfolding P_def by (rule emeasure_distr, auto) finally have A: "emeasure lim U = emeasure M (((λx. (λi∈I. (T^^(nat(i- Min I))) x)))-`(Π⇩_{E}i∈I. X i) ∩ space M)" by simp have i: "int_left_shift-`U = (Π⇩_{E}i∈UNIV. X (i-1))" unfolding H(1) apply (auto simp add: int_left_shift_def PiE_def) by (metis PiE UNIV_I diff_add_cancel, metis Pi_mem add.commute add_diff_cancel_left' iso_tuple_UNIV_I) define Im where "Im = {i. X (i-1) ≠ UNIV}" have "Im = (λi. i+1)`I" unfolding I_def Im_def using image_iff by (auto, fastforce) then have [simp]: "finite Im" by auto have *: "int_left_shift-`U = emb UNIV Im (Π⇩_{E}i∈Im. X (i-1))" unfolding i Im_def prod_emb_def space_borel apply (auto simp add: PiE_def) by (metis (mono_tags, lifting) PiE UNIV_I mem_Collect_eq restrict_Pi_cancel) have "emeasure lim (int_left_shift-`U) = emeasure (P Im) (Π⇩_{E}i∈Im. X (i-1))" unfolding * by (rule emeasure_lim_emb, auto) also have "... = emeasure M (((λx. (λi∈Im. (T^^(nat(i- Min Im))) x)))-`(Π⇩_{E}i∈Im. X (i-1)) ∩ space M)" unfolding P_def by (rule emeasure_distr, auto) finally have B: "emeasure lim (int_left_shift-`U) = emeasure M (((λx. (λi∈Im. (T^^(nat(i- Min Im))) x)))-`(Π⇩_{E}i∈Im. X (i-1)) ∩ space M)" by simp have "Min Im = Min I + 1" unfolding ‹Im = (λi. i+1)`I› by (rule mono_Min_commute[symmetric], auto simp add: False monoI) have "((λx. (λi∈Im. (T^^(nat(i- Min Im))) x)))-`(Π⇩_{E}i∈Im. X (i-1)) = ((λx. (λi∈I. (T^^(nat(i- Min I))) x)))-`(Π⇩_{E}i∈I. X i)" unfolding ‹Min Im = Min I + 1› unfolding ‹Im = (λi. i+1)`I› by (auto simp add: Pi_iff) then show "emeasure lim U = emeasure lim (int_left_shift -` U)" using A B by auto qed also have "... = emeasure lim (int_left_shift-`U ∩ space lim)" unfolding ‹space lim = UNIV› by auto also have "... = emeasure (distr lim lim int_left_shift) U" apply (rule emeasure_distr[symmetric], auto) using * by auto finally show "emeasure lim U = emeasure (distr lim lim int_left_shift) U" by simp qed (auto) fix U assume "U ∈ sets natural_extension_measure" then have [measurable]: "U ∈ sets lim" using ‹natural_extension_measure = lim› by simp have "emeasure natural_extension_measure (natural_extension_map -` U ∩ space natural_extension_measure) = emeasure lim (int_left_shift-`U ∩ space lim)" unfolding ‹natural_extension_measure = lim› natural_extension_map_def by simp also have "... = emeasure (distr lim lim int_left_shift) U" apply (rule emeasure_distr[symmetric], auto) using ‹U ∈ P.events› by auto also have "... = emeasure lim U" using ‹lim = distr lim lim int_left_shift› by simp also have "... = emeasure natural_extension_measure U" using ‹natural_extension_measure = lim› by simp finally show "emeasure natural_extension_measure (natural_extension_map -` U ∩ space natural_extension_measure) = emeasure natural_extension_measure U" by simp qed then interpret I: pmpt natural_extension_measure natural_extension_map by simp show "I.invertible_qmpt" unfolding I.invertible_qmpt_def unfolding natural_extension_map_def ‹natural_extension_measure = lim› by (auto simp add: int_shift_bij) show "I.mpt_factor natural_extension_proj M T" unfolding I.mpt_factor_def proof (auto) show "mpt M T" by (simp add: mpt_axioms) show "natural_extension_proj ∈ measure_preserving natural_extension_measure M" unfolding ‹natural_extension_measure = lim› proof have *: "measurable lim M = measurable borel borel" apply (rule measurable_cong_sets) using sets_PiM_equal_borel M_eq_borel by auto show "natural_extension_proj ∈ measurable lim M" unfolding * natural_extension_proj_def by auto fix U assume [measurable]: "U ∈ sets M" have *: "(((λx. λi∈{0}. (T ^^ nat (i - Min {0})) x))-` ({0} →⇩_{E}U) ∩ space M) = U" using sets.sets_into_space[OF ‹U ∈ sets M›] by auto have "natural_extension_proj-`U ∩ space lim = emb UNIV {0} (Π⇩_{E}i∈{0}. U)" unfolding ‹space lim = UNIV› natural_extension_proj_def prod_emb_def by (auto simp add: PiE_iff) then have "emeasure lim (natural_extension_proj-`U ∩ space lim) = emeasure lim (emb UNIV {0} (Π⇩_{E}i∈{0}. U))" by simp also have "... = emeasure (P {0}) (Π⇩_{E}i∈{0}. U)" apply (rule emeasure_lim_emb, auto) using ‹U ∈ sets M› M_eq_borel by auto also have "... = emeasure M (((λx. λi∈{0}. (T ^^ nat (i - Min {0})) x))-` ({0} →⇩_{E}U) ∩ space M)" unfolding P_def apply (rule emeasure_distr) using ‹U ∈ sets M› M_eq_borel by auto also have "... = emeasure M U" using * by simp finally show "emeasure lim (natural_extension_proj-`U ∩ space lim) = emeasure M U" by simp qed define U::"(int ⇒ 'a) set" where "U = {x ∈ space (Pi⇩_{M}{0, 1} (λi. borel)). x 1 = T (x 0)}" have *: "((λx. λi∈{0, 1}. (T ^^ nat (i - Min {0, 1})) x))-` U ∩ space M = space M" unfolding U_def space_PiM space_borel by auto have [measurable]: "T ∈ measurable borel borel" using M_eq_borel by auto have [measurable]: "U ∈ sets (Pi⇩_{M}{0, 1} (λi. borel))" unfolding U_def by (rule measurable_equality_set, auto) have "emeasure natural_extension_measure (emb UNIV {0, 1} U) = emeasure (P {0, 1}) U" unfolding ‹natural_extension_measure = lim› by (rule emeasure_lim_emb, auto) also have "... = emeasure M (((λx. λi∈{0, 1}. (T ^^ nat (i - Min {0, 1})) x))-` U ∩ space M)" unfolding P_def by (rule emeasure_distr, auto) also have "... = emeasure M (space M)" using * by simp also have "... = 1" by (simp add: emeasure_space_1) finally have *: "emeasure natural_extension_measure (emb UNIV {0, 1} U) = 1" by simp have "AE x in natural_extension_measure. x ∈ emb UNIV {0, 1} U" apply (rule I.AE_prob_1) using * by (simp add: I.emeasure_eq_measure) moreover { fix x assume "x ∈ emb UNIV {0, 1} U" then have "x 1 = T (x 0)" unfolding prod_emb_def U_def by auto then have "natural_extension_proj (natural_extension_map x) = T (natural_extension_proj x)" unfolding natural_extension_proj_def natural_extension_map_def int_left_shift_def by auto } ultimately show "AE x in natural_extension_measure. natural_extension_proj (natural_extension_map x) = T (natural_extension_proj x)" by auto qed qed end end (*of Measure_Preserving_Transformations.thy*)