(* File: Shift_Operator.thy Author: Manuel Eberl, TU München *) section ‹The shift operator on an infinite product measure› theory Shift_Operator imports Ergodicity ME_Library_Complement begin text ‹ Let ‹P› be an an infinite product of i.i.d. instances of the distribution ‹M›. Then the shift operator is the map \[T(x_0, x_1, x_2, \ldots) = T(x_1, x_2, \ldots)\ .\] In this section, we define this operator and show that it is ergodic using Kolmogorov's 0--1 law. › locale shift_operator_ergodic = prob_space + fixes T :: "(nat ⇒ 'a) ⇒ (nat ⇒ 'a)" and P :: "(nat ⇒ 'a) measure" defines "T ≡ (λf. f ∘ Suc)" defines "P ≡ PiM (UNIV :: nat set) (λ_. M)" begin sublocale P: product_prob_space "λ_. M" UNIV by unfold_locales sublocale P: prob_space P by (simp add: prob_space_PiM prob_space_axioms P_def) lemma measurable_T [measurable]: "T ∈ P →⇩_{M}P" unfolding P_def T_def o_def by (rule measurable_abs_UNIV[OF measurable_compose[OF measurable_component_singleton]]) auto text ‹ The ‹n›-th tail algebra $\mathcal{T}_n$ is, in some sense, the algebra in which we forget all information about all $x_i$ with ‹i < n›. We simply change the product algebra of ‹P› by replacing the algebra for each ‹i < n› with the trivial algebra that contains only the empty set and the entire space. › definition tail_algebra :: "nat ⇒ (nat ⇒ 'a) measure" where "tail_algebra n = PiM UNIV (λi. if i < n then trivial_measure (space M) else M)" lemma tail_algebra_0 [simp]: "tail_algebra 0 = P" by (simp add: tail_algebra_def P_def) lemma space_tail_algebra [simp]: "space (tail_algebra n) = PiE UNIV (λ_. space M)" by (simp add: tail_algebra_def space_PiM PiE_def Pi_def) lemma measurable_P_component [measurable]: "P.random_variable M (λf. f i)" unfolding P_def by measurable lemma P_component [simp]: "distr P M (λf. f i) = M" unfolding P_def by (subst P.PiM_component) auto lemma indep_vars: "P.indep_vars (λ_. M) (λi f. f i) UNIV" by (subst P.indep_vars_iff_distr_eq_PiM) (simp_all add: restrict_def distr_id2 P.PiM_component P_def) text ‹ The shift operator takes us from $\mathcal{T}_n$ to $\mathcal{T}_{n+1}$ (it forgets the information about one more variable): › lemma measurable_T_tail: "T ∈ tail_algebra (Suc n) →⇩_{M}tail_algebra n" unfolding T_def tail_algebra_def o_def by (rule measurable_abs_UNIV[OF measurable_compose[OF measurable_component_singleton]]) simp_all lemma measurable_funpow_T: "T ^^ n ∈ tail_algebra (m + n) →⇩_{M}tail_algebra m" proof (induction n) case (Suc n) have "(T ^^ n) ∘ T ∈ tail_algebra (m + Suc n) →⇩_{M}tail_algebra m" by (rule measurable_comp[OF _ Suc]) (simp_all add: measurable_T_tail) thus ?case by (simp add: o_def funpow_swap1) qed auto lemma measurable_funpow_T': "T ^^ n ∈ tail_algebra n →⇩_{M}P" using measurable_funpow_T[of n 0] by simp text ‹ The shift operator is clearly measure-preserving: › lemma measure_preserving: "T ∈ measure_preserving P P" proof fix A :: "(nat ⇒ 'a) set" assume "A ∈ P.events" hence "emeasure P (T -` A ∩ space P) = emeasure (distr P P T) A" by (subst emeasure_distr) simp_all also have "distr P P T = P" unfolding P_def T_def o_def using distr_PiM_reindex[of UNIV "λ_. M" Suc UNIV] by (simp add: prob_space_axioms restrict_def) finally show "emeasure P (T -` A ∩ space P) = emeasure P A" . qed auto sublocale fmpt P T by unfold_locales (use measure_preserving in ‹blast intro: measure_preserving_is_quasi_measure_preserving›)+ lemma indep_sets_vimage_algebra: "P.indep_sets (λi. sets (vimage_algebra (space P) (λf. f i) M)) UNIV" using indep_vars unfolding P.indep_vars_def sets_vimage_algebra by blast text ‹ We can now show that the tail algebra $\mathcal{T}_n$ is a subalgebra of the algebra generated by the algebras induced by all the variables ‹x⇩_{i}› with ‹i ≥ n›: › lemma tail_algebra_subset: "sets (tail_algebra n) ⊆ sigma_sets (space P) (⋃i∈{n..}. sets (vimage_algebra (space P) (λf. f i) M))" proof - have "sets (tail_algebra n) = sigma_sets (space P) (prod_algebra UNIV (λi. if i < n then trivial_measure (space M) else M))" by (simp add: tail_algebra_def sets_PiM PiE_def Pi_def P_def space_PiM) also have "… ⊆ sigma_sets (space P) (⋃i∈{n..}. sets (vimage_algebra (space P) (λf. f i) M))" proof (intro sigma_sets_mono subsetI) fix C assume "C ∈ prod_algebra UNIV (λi. if i < n then trivial_measure (space M) else M)" then obtain C' where C': "C = Pi⇩_{E}UNIV C'" "C' ∈ (Π i∈UNIV. sets (if i < n then trivial_measure (space M) else M))" by (elim prod_algebraE_all) have C'_1: "C' i ∈ {{}, space M}" if "i < n" for i using C'(2) that by (auto simp: Pi_def sets_trivial_measure split: if_splits) have C'_2: "C' i ∈ sets M" if "i ≥ n" for i proof - from that have "¬(i < n)" by auto with C'(2) show ?thesis by (force simp: Pi_def sets_trivial_measure split: if_splits) qed have "C' i ∈ events" for i using C'_1[of i] C'_2[of i] by (cases "i ≥ n") auto hence "C ∈ sets P" unfolding P_def C'(1) by (intro sets_PiM_I_countable) auto hence "C ⊆ space P" using sets.sets_into_space by blast show "C ∈ sigma_sets (space P) (⋃i∈{n..}. sets (vimage_algebra (space P) (λf. f i) M))" proof (cases "C = {}") case False have "C = (⋂i∈{n..}. (λf. f i) -` C' i) ∩ space P" proof (intro equalityI subsetI, goal_cases) case (1 f) hence "f ∈ space P" using 1 ‹C ⊆ space P› by blast thus ?case using C' 1 by (auto simp: Pi_def sets_trivial_measure split: if_splits) next case (2 f) hence f: "f i ∈ C' i" if "i ≥ n" for i using that by auto have "f i ∈ C' i" for i proof (cases "i ≥ n") case True thus ?thesis using C'_2[of i] f[of i] by auto next case False thus ?thesis using C'_1[of i] C'(1) ‹C ≠ {}› 2 by (auto simp: P_def space_PiM) qed thus "f ∈ C" using C' by auto qed also have "(⋂i∈{n..}. (λf. f i) -` C' i) ∩ space P = (⋂i∈{n..}. (λf. f i) -` C' i ∩ space P)" by blast also have "… ∈ sigma_sets (space P) (⋃i∈{n..}. sets (vimage_algebra (space P) (λf. f i) M))" (is "_ ∈ ?rhs") proof (intro sigma_sets_INTER, goal_cases) fix i show "(λf. f i) -` C' i ∩ space P ∈ ?rhs" proof (cases "i ≥ n") case False hence "C' i = {} ∨ C' i = space M" using C'_1[of i] by auto thus ?thesis proof assume [simp]: "C' i = space M" have "space P ⊆ (λf. f i) -` C' i" by (auto simp: P_def space_PiM) hence "(λf. f i) -` C' i ∩ space P = space P" by blast thus ?thesis using sigma_sets_top by metis qed (auto intro: sigma_sets.Empty) next case i: True have "(λf. f i) -` C' i ∩ space P ∈ sets (vimage_algebra (space P) (λf. f i) M)" using C'_2[OF i] by (blast intro: in_vimage_algebra) thus ?thesis using i by blast qed next have "C ⊆ space P" if "C ∈ sets (vimage_algebra (space P) (λf. f i) M)" for i C using sets.sets_into_space[OF that] by simp thus "(⋃i∈{n..}. sets (vimage_algebra (space P) (λf. f i) M)) ⊆ Pow (space P)" by auto qed auto finally show ?thesis . qed (auto simp: sigma_sets.Empty) qed finally show ?thesis . qed text ‹ It now follows that the ‹T›-invariant events are a subset of the tail algebra induced by the variables: › lemma Invariants_subset_tail_algebra: "sets Invariants ⊆ P.tail_events (λi. sets (vimage_algebra (space P) (λf. f i) M))" proof fix A assume A: "A ∈ sets Invariants" have A': "A ∈ P.events" using A unfolding Invariants_sets by simp_all show "A ∈ P.tail_events (λi. sets (vimage_algebra (space P) (λf. f i) M))" unfolding P.tail_events_def proof safe fix n :: nat have "vimage_restr T A = A" using A by (simp add: Invariants_vrestr) hence "A = vimage_restr (T ^^ n) A" using A' by (induction n) (simp_all add: vrestr_comp) also have "vimage_restr (T ^^ n) A = (T ^^ n) -` (A ∩ space P) ∩ space P" unfolding vimage_restr_def .. also have "A ∩ space P = A" using A' by simp also have "space P = space (tail_algebra n)" by (simp add: P_def space_PiM) also have "(T ^^ n) -` A ∩ space (tail_algebra n) ∈ sets (tail_algebra n)" by (rule measurable_sets[OF measurable_funpow_T' A']) also have "sets (tail_algebra n) ⊆ sigma_sets (space P) (⋃i∈{n..}. sets (vimage_algebra (space P) (λf. f i) M))" by (rule tail_algebra_subset) finally show "A ∈ sigma_sets (space P) (⋃i∈{n..}. sets (vimage_algebra (space P) (λf. f i) M))" . qed qed text ‹ A simple invocation of Kolmogorov's 0--1 law now proves that ‹T› is indeed ergodic: › sublocale ergodic_fmpt P T proof fix A assume A: "A ∈ sets Invariants" have A': "A ∈ P.events" using A unfolding Invariants_sets by simp_all have "sigma_algebra (space P) (sets (vimage_algebra (space P) (λf. f i) M))" for i by (metis sets.sigma_algebra_axioms space_vimage_algebra) hence "P.prob A = 0 ∨ P.prob A = 1" using indep_sets_vimage_algebra by (rule P.kolmogorov_0_1_law) (use A Invariants_subset_tail_algebra in blast) thus "A ∈ null_sets P ∨ space P - A ∈ null_sets P" by (rule disj_forward) (use A'(1) P.prob_compl[of A] in ‹auto simp: P.emeasure_eq_measure›) qed end end