Commit 11edcdb1 by Gerwin Klein

 ... ... @@ -4,12 +4,12 @@ *) section \The Laws of Large Numbers\ theory Laws_of_Large_Numbers imports Ergodic_Theory.Ergodicity Shift_Operator imports Ergodic_Theory.Shift_Operator begin text \ We prove the strong law of large numbers in the following form: Let $(X_i)_{i\in\mathbb{N}}$ be a sequence of i.i.d. random variables over a probability space \M\. Further assume that be a sequence of i.i.d. random variables over a probability space \M\. Further assume that the expected value $E[X_0]$ of $X_0$ exists. Then the sequence of random variables $\overline{X}_n = \frac{1}{n} \sum_{i=0}^n X_i$ of running averages almost surely converges to $E[X_0]$. ... ...
 (* File: ME_Library_Complement.thy Author: Manuel Eberl, TU München *) section \Auxiliary Material\ theory ME_Library_Complement imports "HOL-Analysis.Analysis" begin (* TODO: this file is redundent for AFP 2021 since it is then already in Ergodic_Theory *) subsection \The trivial measurable space\ text \ The trivial measurable space is the smallest possible \\\-algebra, i.e. only the empty set and everything. \ definition trivial_measure :: "'a set \ 'a measure" where "trivial_measure X = sigma X {{}, X}" lemma space_trivial_measure [simp]: "space (trivial_measure X) = X" by (simp add: trivial_measure_def) lemma sets_trivial_measure: "sets (trivial_measure X) = {{}, X}" by (simp add: trivial_measure_def sigma_algebra_trivial sigma_algebra.sigma_sets_eq) lemma measurable_trivial_measure: assumes "f \ space M \ X" and "f - X \ space M \ sets M" shows "f \ M \\<^sub>M trivial_measure X" using assms unfolding measurable_def by (auto simp: sets_trivial_measure) lemma measurable_trivial_measure_iff: "f \ M \\<^sub>M trivial_measure X \ f \ space M \ X \ f - X \ space M \ sets M" unfolding measurable_def by (auto simp: sets_trivial_measure) subsection \Pullback algebras\ text \ The pullback algebra $f^{-1}(\Sigma)$ of a \\\-algebra $(\Omega, \Sigma)$ is the smallest \\\-algebra such that $f$ is $f^{-1}(\Sigma)$--$\Sigma$-measurable. \ definition (in sigma_algebra) pullback_algebra :: "('b \ 'a) \ 'b set \ 'b set set" where "pullback_algebra f \' = sigma_sets \' {f - A \ \' |A. A \ M}" lemma pullback_algebra_minimal: assumes "f \ M \\<^sub>M N" shows "sets.pullback_algebra N f (space M) \ sets M" proof fix X assume "X \ sets.pullback_algebra N f (space M)" thus "X \ sets M" unfolding sets.pullback_algebra_def by induction (use assms in \auto simp: measurable_def\) qed lemma (in sigma_algebra) sigma_algebra_pullback: "sigma_algebra \' (pullback_algebra f \')" unfolding pullback_algebra_def by (rule sigma_algebra_sigma_sets) auto lemma (in sigma_algebra) in_pullback_algebra: "A \ M \ f - A \ \' \ pullback_algebra f \'" unfolding pullback_algebra_def by (rule sigma_sets.Basic) auto end \ No newline at end of file
 (* File: Shift_Operator.thy Author: Manuel Eberl, TU München *) section \The shift operator on an infinite product measure\ theory Shift_Operator imports Ergodic_Theory.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 \\<^sub>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) \\<^sub>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) \\<^sub>M tail_algebra m" proof (induction n) case (Suc n) have "(T ^^ n) \ T \ tail_algebra (m + Suc n) \\<^sub>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 \\<^sub>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\)+ text \ Related to the tail algebra, we define the algebra induced by the \i\-th variable (i.e. the algebra that contains only information about the \i\-th variable): \ sublocale X: sigma_algebra "space P" "sets.pullback_algebra M (\f. f i) (space P)" by (rule sets.sigma_algebra_pullback) lemma indep_sets_pullback_algebra: "P.indep_sets (\i. sets.pullback_algebra M (\f. f i) (space P)) UNIV" using indep_vars unfolding P.indep_vars_def sets.pullback_algebra_def 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\<^sub>i\ with \i \ n\: \ lemma tail_algebra_subset: "sets (tail_algebra n) \ sigma_sets (space P) (\i\{n..}. sets.pullback_algebra M (\f. f i) (space P))" 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.pullback_algebra M (\f. f i) (space P))" 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\<^sub>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.pullback_algebra M (\f. f i) (space P))" 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.pullback_algebra M (\f. f i) (space P))" (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.pullback_algebra M (\f. f i) (space P)" using C'_2[OF i] by (intro sets.in_pullback_algebra) auto thus ?thesis using i by blast qed next have "C \ space P" if "C \ sets.pullback_algebra M (\f. f i) (space P)" for i C proof - show ?thesis by (rule sigma_sets_into_sp) (use that X.space_closed[of i] in auto) qed thus "(\i\{n..}. sets.pullback_algebra M (\f. f i) (space P))\ 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.pullback_algebra M (\f. f i) (space P))" 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.pullback_algebra M (\f. f i) (space P))" 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.pullback_algebra M (\f. f i) (space P))" by (rule tail_algebra_subset) finally show "A \ sigma_sets (space P) (\i\{n..}. sets.pullback_algebra M (\f. f i) (space P))" . 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 "P.prob A = 0 \ P.prob A = 1" using X.sigma_algebra_axioms indep_sets_pullback_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 \ No newline at end of file