Theory Measure_Preserving_Transformations

(*  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) = (XA. f --` X)"
using vimage_restr_def by auto

lemma vrestr_UN [simp]:
  "f --` (xA. B x) = (xA. f --` B x)"
using vimage_restr_def by auto

lemma vrestr_Inter [simp]:
  assumes "A  {}"
  shows "f --` (A) = (XA. f --` X)"
using vimage_restr_def assms by auto

lemma vrestr_INT [simp]:
  assumes "A  {}"
  shows "f --` (xA. B x) = (xA. 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)))