Commit ab95621b by Gerwin Klein

### merge from afp-2021

 ... ... @@ -10240,3 +10240,29 @@ abstract = modeling the behavior of perfect logicians and formalize a solution of the puzzle. [Laws_of_Large_Numbers] title = The Laws of Large Numbers author = Manuel Eberl topic = Mathematics/Probability theory date = 2021-02-10 notify = eberlm@in.tum.de abstract =

The Law of Large Numbers states that, informally, if one performs a random experiment $X$ many times and takes the average of the results, that average will be very close to the expected value $E[X]$.

More formally, let $(X_i)_{i\in\mathbb{N}}$ be a sequence of independently identically distributed random variables whose expected value $E[X_1]$ exists. Denote the running average of $X_1, \ldots, X_n$ as $\overline{X}_n$. Then:

• The Weak Law of Large Numbers states that $\overline{X}_{n} \longrightarrow E[X_1]$ in probability for $n\to\infty$, i.e. $\mathcal{P}(|\overline{X}_{n} - E[X_1]| > \varepsilon) \longrightarrow 0$ as $n\to\infty$ for any $\varepsilon > 0$.
• The Strong Law of Large Numbers states that $\overline{X}_{n} \longrightarrow E[X_1]$ almost surely for $n\to\infty$, i.e. $\mathcal{P}(\overline{X}_{n} \longrightarrow E[X_1]) = 1$.

In this entry, I formally prove the strong law and from it the weak law. The approach used for the proof of the strong law is a particularly quick and slick one based on ergodic theory, which was formalised by Gouëzel in another AFP entry.

 (* File: Laws_of_Large_Numbers.thy Author: Manuel Eberl, TU München *) section \The Laws of Large Numbers\ theory Laws_of_Large_Numbers 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 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]$. This means that $\mathcal{P}[\overline{X}_n \longrightarrow E[X_0]] = 1\ .$ We start with the strong law. \ subsection \The strong law\ text \ The proof uses Birkhoff's Theorem from Gouëzel's formalisation of ergodic theory~\cite{gouezel} and the fact that the shift operator $T(x_1, x_2, x_3, \ldots) = (x_2, x_3, \ldots)$ is ergodic. This proof can be found in various textbooks on probability theory/ergodic theory, e.g. the ones by Krengel~\cite[p.~24]{krengel} and Simmonet~\cite[Chapter 15, pp.~311--325]{Simonnet1996}. \ theorem (in prob_space) strong_law_of_large_numbers_iid: fixes X :: "nat \ 'a \ real" assumes indep: "indep_vars (\_. borel) X UNIV" assumes distr: "\i. distr M borel (X i) = distr M borel (X 0)" assumes L1: "integrable M (X 0)" shows "AE x in M. (\n. (\i expectation (X 0)" proof - text \ We adopt a more explicit view of \<^term>\M\ as a countably infinite product of i.i.d. random variables, indexed by the natural numbers: \ define M' :: "(nat \ real) measure" where "M' = Pi\<^sub>M UNIV (\i. distr M borel (X i))" have [measurable]: "random_variable borel (X i)" for i using indep by (auto simp: indep_vars_def) have M'_eq: "M' = distr M (Pi\<^sub>M UNIV (\i. borel)) (\x. \i\UNIV. X i x)" using indep unfolding M'_def by (subst (asm) indep_vars_iff_distr_eq_PiM) auto have space_M': "space M' = UNIV" by (simp add: M'_def space_PiM) have sets_M' [measurable_cong]: "sets M' = sets (Pi\<^sub>M UNIV (\i. borel))" by (simp add: M'_eq) interpret M': prob_space M' unfolding M'_eq by (intro prob_space_distr) auto text \We introduce a shift operator that forgets the first variable in the sequence.\ define T :: "(nat \ real) \ (nat \ real)" where "T = (\f. f \ Suc)" have funpow_T: "(T ^^ i) = (\f. f \ (\n. n + i))" for i by (induction i) (auto simp: T_def) interpret T: shift_operator_ergodic "distr M borel (X 0)" T M' proof - interpret X0: prob_space "distr M borel (X 0)" by (rule prob_space_distr) auto show "shift_operator_ergodic (distr M borel (X 0))" by unfold_locales show "M' \ Pi\<^sub>M UNIV (\_. distr M borel (X 0)) " unfolding M'_def by (subst distr) qed (simp_all add: T_def) have [intro]: "integrable M' (\f. f 0)" unfolding M'_eq by (subst integrable_distr_eq) (use L1 in auto) have "AE f in M'. (\n. T.birkhoff_sum (\f. f 0) n f / real n) \ real_cond_exp M' T.Invariants (\f. f 0) f" by (rule T.birkhoff_theorem_AE_nonergodic) auto moreover have "AE x in M'. real_cond_exp M' T.Invariants (\f. f 0) x = M'.expectation (\f. f 0) / M'.prob (space M')" by (intro T.Invariants_cond_exp_is_integral_fmpt) auto ultimately have "AE f in M'. (\n. T.birkhoff_sum (\f. f 0) n f / real n) \ M'.expectation (\f. f 0)" by eventually_elim (simp_all add: M'.prob_space) also have "M'.expectation (\f. f 0) = expectation (X 0)" unfolding M'_eq by (subst integral_distr) simp_all also have "T.birkhoff_sum (\f. f 0) = (\n f. sum f {..The weak law\ text \ To go from the strong law to the weak one, we need the fact that almost sure convergence implies convergence in probability. We prove this for sequences of random variables here. \ lemma (in prob_space) AE_convergence_imp_convergence_in_prob: assumes [measurable]: "\i. random_variable borel (X i)" "random_variable borel Y" assumes AE: "AE x in M. (\i. X i x) \ Y x" assumes "\ > (0 :: real)" shows "(\i. prob {x\space M. \X i x - Y x\ > \}) \ 0" proof - define A where "A = (\i. {x\space M. \X i x - Y x\ > \})" define B where "B = (\n. (\i\{n..}. A i))" have [measurable]: "A i \ sets M" "B i \ sets M" for i unfolding A_def B_def by measurable have "AE x in M. x \ (\i. B i)" using AE unfolding B_def A_def by eventually_elim (use \\ > 0\ in \fastforce simp: tendsto_iff dist_norm eventually_at_top_linorder\) hence "(\i. B i) \ null_sets M" by (subst AE_iff_null_sets) auto show "(\i. prob (A i)) \ 0" proof (rule Lim_null_comparison) have "(\i. prob (B i)) \ prob (\i. B i)" proof (rule finite_Lim_measure_decseq) show "decseq B" by (rule decseq_SucI) (force simp: B_def) qed auto also have "prob (\i. B i) = 0" using $$\i. B i) \ null_sets M\ by (simp add: measure_eq_0_null_sets) finally show "(\i. prob (B i)) \ 0" . next have "prob (A n) \ prob (B n)" for n unfolding B_def by (intro finite_measure_mono) auto thus "\\<^sub>F n in at_top. norm (prob (A n)) \ prob (B n)" by (intro always_eventually) auto qed qed text \ The weak law is now a simple corollary: we again have the same setting as before. The weak law now states that \overline{X}_n converges to E[X_0] in probability. This means that for any \\ > 0\, the probability that |\overline{X}_n - X_0| > \varepsilon vanishes as \n \ \\. \ corollary (in prob_space) weak_law_of_large_numbers_iid: fixes X :: "nat \ 'a \ real" and \ :: real assumes indep: "indep_vars (\_. borel) X UNIV" assumes distr: "\i. distr M borel (X i) = distr M borel (X 0)" assumes L1: "integrable M (X 0)" assumes "\ > 0" shows "(\n. prob {x\space M. \(\i > \}) \ 0" proof (rule AE_convergence_imp_convergence_in_prob) show "AE x in M. (\n. (\i expectation (X 0)" by (rule strong_law_of_large_numbers_iid) fact+ next have [measurable]: "random_variable borel (X i)" for i using indep by (auto simp: indep_vars_def) show "random_variable borel (\x. (\i\ > 0\ in simp_all) end \ No newline at end of file  (* File: Laws_of_Large_Numbers.thy Author: Manuel Eberl, TU München *) subsection \Example\ theory Laws_of_Large_Numbers_Example imports Laws_of_Large_Numbers begin text \ As an example, we apply the strong law to the proportion of successes in an independent sequence of coin flips with success probability \p\. We will show that proportion of successful coin flips among the first \n\ attempts almost surely converges to \p\ as \n \ \\. \ (* TODO: Move *) lemma (in prob_space) indep_vars_iff_distr_eq_PiM': fixes I :: "'i set" and X :: "'i \ 'a \ 'b" assumes "I \ {}" assumes rv: "\i. i \ I \ random_variable (M' i) (X i)" shows "indep_vars M' X I \ distr M (\\<^sub>M i\I. M' i) (\x. \i\I. X i x) = (\\<^sub>M i\I. distr M (M' i) (X i))" proof - from assms obtain j where j: "j \ I" by auto define N' where "N' = (\i. if i \ I then M' i else M' j)" define Y where "Y = (\i. if i \ I then X i else X j)" have rv: "random_variable (N' i) (Y i)" for i using j by (auto simp: N'_def Y_def intro: assms) have "indep_vars M' X I = indep_vars N' Y I" by (intro indep_vars_cong) (auto simp: N'_def Y_def) also have "\ \ distr M (\\<^sub>M i\I. N' i) (\x. \i\I. Y i x) = (\\<^sub>M i\I. distr M (N' i) (Y i))" by (intro indep_vars_iff_distr_eq_PiM rv assms) also have "(\\<^sub>M i\I. N' i) = (\\<^sub>M i\I. M' i)" by (intro PiM_cong) (simp_all add: N'_def) also have "(\x. \i\I. Y i x) = (\x. \i\I. X i x)" by (simp_all add: Y_def fun_eq_iff) also have "(\\<^sub>M i\I. distr M (N' i) (Y i)) = (\\<^sub>M i\I. distr M (M' i) (X i))" by (intro PiM_cong distr_cong) (simp_all add: N'_def Y_def) finally show ?thesis . qed (* TODO: Move *) lemma indep_vars_PiM_components: assumes "\i. i \ A \ prob_space (M i)" shows "prob_space.indep_vars (PiM A M) M (\i f. f i) A" proof (cases "A = {}") case False have "distr (Pi\<^sub>M A M) (Pi\<^sub>M A M) (\x. restrict x A) = distr (Pi\<^sub>M A M) (Pi\<^sub>M A M) (\x. x)" by (intro distr_cong) (auto simp: restrict_def space_PiM PiE_def extensional_def Pi_def) also have "\ = Pi\<^sub>M A M" by simp also have "\ = Pi\<^sub>M A (\i. distr (Pi\<^sub>M A M) (M i) (\f. f i))" by (intro PiM_cong refl, subst distr_PiM_component) (auto simp: assms) finally show ?thesis by (subst prob_space.indep_vars_iff_distr_eq_PiM') (simp_all add: prob_space_PiM assms False) next case True interpret prob_space "PiM A M" by (intro prob_space_PiM assms) show ?thesis unfolding indep_vars_def indep_sets_def by (auto simp: True) qed (* TODO: Move *) lemma indep_vars_PiM_components': assumes "\i. i \ A \ prob_space (M i)" assumes "\i. i \ A \ g i \ M i \\<^sub>M N i" shows "prob_space.indep_vars (PiM A M) N (\i f. g i (f i)) A" by (rule prob_space.indep_vars_compose2[OF prob_space_PiM indep_vars_PiM_components]) (use assms in simp_all) (* TODO: Move *) lemma integrable_bernoulli_pmf [intro]: fixes f :: "bool \ 'a :: {banach, second_countable_topology}" shows "integrable (bernoulli_pmf p) f" by (rule integrable_measure_pmf_finite) auto (* TODO: Move *) lemma expectation_bernoulli_pmf: fixes f :: "bool \ 'a :: {banach, second_countable_topology}" assumes p: "p \ {0..1}" shows "measure_pmf.expectation (bernoulli_pmf p) f = p *\<^sub>R f True + (1 - p) *\<^sub>R f False" using p by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool) experiment fixes p :: real assumes p: "p \ {0..1}" begin definition M :: "(nat \ bool) measure" where "M = (\\<^sub>M i\(UNIV :: nat set). measure_pmf (bernoulli_pmf p))" definition X :: "nat \ (nat \ bool) \ real" where "X = (\i f. if f i then 1 else 0)" interpretation prob_space M unfolding M_def by (intro prob_space_PiM measure_pmf.prob_space_axioms) lemma random_variable_component: "random_variable (count_space UNIV) (\f. f i)" unfolding X_def M_def by measurable lemma random_variable_X [measurable]: "random_variable borel (X i)" unfolding X_def M_def by measurable lemma distr_M_component: "distr M (count_space UNIV) (\f. f i) = measure_pmf (bernoulli_pmf p)" proof - have "distr M (count_space UNIV) (\f. f i) = distr M (measure_pmf (bernoulli_pmf p)) (\f. f i)" by (rule distr_cong) auto also have "\ = measure_pmf (bernoulli_pmf p)" unfolding M_def by (subst distr_PiM_component) (simp_all add: measure_pmf.prob_space_axioms) finally show ?thesis . qed lemma distr_M_X: "distr M borel (X i) = distr (measure_pmf (bernoulli_pmf p)) borel (\b. if b then 1 else 0)" proof - have "distr M borel (X i) = distr (distr M (count_space UNIV) (\f. f i)) borel (\b. if b then 1 else 0 :: real)" by (subst distr_distr) (auto simp: M_def X_def o_def) also note distr_M_component[of i] finally show ?thesis by simp qed lemma X_has_expectation: "integrable M (X 0)" proof - have "integrable (bernoulli_pmf p) (\b. if b then 1 else 0 :: real)" by auto also have "measure_pmf (bernoulli_pmf p) = distr M (count_space UNIV) (\f. f 0)" by (simp add: distr_M_component) also have "integrable \ (\b. if b then 1 else 0 :: real) = integrable M (X 0)" unfolding X_def using random_variable_component by (subst integrable_distr_eq) auto finally show ?thesis . qed lemma indep: "indep_vars (\_. borel) X UNIV" unfolding M_def X_def by (rule indep_vars_PiM_components') (simp_all add: measure_pmf.prob_space_axioms) lemma expectation_X: "expectation (X i) = p" proof - have "expectation (X i) = lebesgue_integral (distr M (count_space UNIV) (\f. f i)) (\b. if b then 1 else 0 :: real)" by (subst integral_distr) (simp_all add: random_variable_component X_def) also have "distr M (count_space UNIV) (\x. x i) = measure_pmf (bernoulli_pmf p)" by (rule distr_M_component) also have "measure_pmf.expectation (bernoulli_pmf p) (\b. if b then 1 else 0 :: real) = p" using p by (subst integral_bernoulli_pmf) auto finally show ?thesis . qed theorem "AE f in M. (\n. card {i. i < n \ f i} / n) \ p" proof - have "AE f in M. (\n. (\i expectation (X 0)" by (rule strong_law_of_large_numbers_iid) (use indep X_has_expectation in \simp_all add: distr_M_X$$ also have "expectation (X 0) = p" by (simp add: expectation_X) also have "(\x n. \ix n. \i\{i\{.. = (\x n. real (card {i. i < n \ x i}))" by simp finally show ?thesis . qed end end \ No newline at end of file
 chapter AFP session "Laws_of_Large_Numbers" (AFP) = "Ergodic_Theory" + options [timeout = 600] theories Laws_of_Large_Numbers Laws_of_Large_Numbers_Example document_files "root.tex" "root.bib"
 @book{Simonnet1996, author="Simonnet, Michel", title="Measures and Probabilities", year="1996", publisher="Springer New York", address="New York, NY", isbn="978-1-4612-4012-9", doi="10.1007/978-1-4612-4012-9_15", } @article{gouezel, author = {Sébastien Gouëzel}, title = {Ergodic Theory}, journal = {Archive of Formal Proofs}, month = dec, year = 2015, note = {\url{https://isa-afp.org/entries/Ergodic_Theory.html}, Formal proof development}, ISSN = {2150-914x}, } @book{krengel, doi = {10.1515/9783110844641}, year = {1985}, month = jan, publisher = {De Gruyter}, author = {Ulrich Krengel}, title = {Ergodic Theorems}, pages= {24} }
 \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} \usepackage{mathtools} \usepackage{amssymb} \usepackage{stmaryrd} \usepackage[numbers]{natbib} % this should be the last package used \usepackage{pdfsetup} \usepackage{doi} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \DeclarePairedDelimiter{\norm}{\lVert}{\rVert} \begin{document} \nocite{Simonnet1996} \nocite{krengel} \title{The Laws of Large Numbers} \author{Manuel Eberl} \date{} \maketitle \begin{abstract} The Law of Large Numbers states that, informally, if one performs a random experiment $X$ many times and takes the average of the results, that average will be very close to the expected value $E[X]$. More formally, let $(X_i)_{i\in\mathbb{N}}$ be a sequence of independently identically distributed random variables whose expected value $E[X_1]$ exists. Denote the running average of $X_1, \ldots, X_n$ for $\overline{X}_n$. Then: \begin{itemize} \item The Weak Law of Large Numbers states that $\overline{X}_{\!n} \longrightarrow E[X_1]$ in probability for $n\to\infty$, i.e. $\mathcal{P}(|\overline{X}_{\!n} - E[X_1]| > \varepsilon) \longrightarrow 0$ for $n\to\infty$ for any $\varepsilon > 0$. \item The Strong Law of Large Numbers states that $\overline{X}_{\!n} \longrightarrow E[X_1]$ almost surely for $n\to\infty$, i.e. $\mathcal{P}(\overline{X}_{\!n} \longrightarrow E[X_1]) = 1$. \end{itemize} In this entry, I formally prove the strong law and from it the weak law. The approach used for the proof of the strong law is a particularly quick and slick one based on ergodic theory, which was formalised by Gou\"ezel in another AFP entry. \end{abstract} \tableofcontents % sane default for proof documents \parindent 0pt\parskip 0.5ex % generated text of all theories \input{session} \vspace{2em} \textbf{Acknowledgements.} I thank Sébastien Gouëzel for providing advice and context about the law of large numbers and ergodic theory. I do not actually know any ergodic theory and without him, I would probably have shied away from formalising this. % optional bibliography {\raggedright \bibliographystyle{plainnat} \bibliography{root} } \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End:
 ... ... @@ -297,6 +297,7 @@ Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer ... ...
 ... ... @@ -97,6 +97,14 @@ MathJax = {
Contributor: Manuel Eberl
Used by: Gromov_Hyperbolicity, Lp
Gromov_Hyperbolicity, Laws_of_Large_Numbers, Lp
... ... @@ -132,7 +140,7 @@ MathJax = { ... ...
 The Laws of Large Numbers - Archive of Formal Proofs

The Laws of Large Numbers

Title: The Laws of Large Numbers
Author: Manuel Eberl
Submission date: 2021-02-10
Abstract: