# Theory Measure_Preserving_Transformations

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

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

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"

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

lemma T_Tn_T_compose:
"T ((T^^n) x) = (T^^(Suc n)) x"
"(T^^n) (T x) = (T^^(Suc n)) x"

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)

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]:
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]
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))"
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

"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
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]

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

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

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