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