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