The Exercise

A measurement with real outcomes is made again and again, each time on a fresh system prepared in the same way. The outcomes are random variables $X_0, X_1, X_2, \dots$ with a common distribution, and no run influences another. After $n$ runs the experimenter takes the average of the results. Theorem 12.3, the law of large numbers, says that for large $n$ this average lies close to the expected outcome of a single run with probability close to one.

Random Variables

A probability space is a set $\Omega$ of outcomes with a measure $p$ on its events of total mass $p(\Omega) = 1$ . A random variable $X$ on $\Omega$ is a measurable real function on $\Omega$ ; its expectation is $\mathbb{E}[X] = \int_\Omega X \, dp$ , and $X$ has a finite second moment when $\mathbb{E}[X^2] < \infty$ .

Two random variables $X$ and $Y$ on $\Omega$ are independent when their joint probabilities factor, $p(X \in A,\ Y \in B) = p(X \in A)\, p(Y \in B) \quad \text{for all Borel sets } A, B \subseteq \mathbb{R},$ (1) and identically distributed when $p(X \in A) = p(Y \in A)$ for every set $A$ in the usual collection of measurable subsets of $\mathbb{R}$ . A sequence of random variables is pairwise independent when any two of its members with different indices are independent.

For a sequence $X_0, X_1, X_2, \dots$ on $\Omega$ , the mean of the first $n$ variables and the expectation of $X_0$ are $S_n = \frac{1}{n} \sum_{i=0}^{n-1} X_i, \qquad \mu = \mathbb{E}[X_0].$ (2)

The Claim

Theorem 1. Let $X_0, X_1, X_2, \dots$ be pairwise independent random variables on a probability space, each identically distributed with $X_0$ , and let $X_0$ have a finite second moment. Then for every $\varepsilon > 0$ the sample means (2) satisfy $\lim_{n \to \infty} p\bigl(|S_n - \mu| > \varepsilon\bigr) = 0.$ (3)^✦

What Is Checked

The claim is stated over a probability space and a sequence of real random variables on it, under the hypotheses in the theorem box. What the library proves about such a sequence is the limit (3).