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