 # The Laws of Large Numbers

 Title: The Laws of Large Numbers Author: Manuel Eberl Submission date: 2021-02-10 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. BibTeX: @article{Laws_of_Large_Numbers-AFP, author = {Manuel Eberl}, title = {The Laws of Large Numbers}, journal = {Archive of Formal Proofs}, month = feb, year = 2021, note = {\url{https://isa-afp.org/entries/Laws_of_Large_Numbers.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Ergodic_Theory Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.