The strong law of large numbers #
We prove the strong law of large numbers, in ProbabilityTheory.strong_law_ae:
If X n is a sequence of independent identically distributed integrable random
variables, then ∑ i in range n, X i / n converges almost surely to 𝔼[X 0].
We give here the strong version, due to Etemadi, that only requires pairwise independence.
This file also contains the Lᵖ version of the strong law of large numbers provided by
ProbabilityTheory.strong_law_Lp which shows ∑ i in range n, X i / n converges in Lᵖ to
𝔼[X 0] provided X n is independent identically distributed and is Lᵖ.
Implementation #
The main point is to prove the result for real-valued random variables, as the general case
of Banach-space valued random variables follows from this case and approximation by simple
functions. The real version is given in ProbabilityTheory.strong_law_ae_real.
We follow the proof by Etemadi [Etemadi, An elementary proof of the strong law of large numbers][etemadi_strong_law], which goes as follows.
It suffices to prove the result for nonnegative X, as one can prove the general result by
splitting a general X into its positive part and negative part.
Consider Xₙ a sequence of nonnegative integrable identically distributed pairwise independent
random variables. Let Yₙ be the truncation of Xₙ up to n. We claim that
- Almost surely,
Xₙ = Yₙfor all but finitely many indices. Indeed,∑ ℙ (Xₙ ≠ Yₙ)is bounded by1 + 𝔼[X](seesum_prob_mem_Ioc_leandtsum_prob_mem_Ioi_lt_top). - Let
c > 1. Along the sequencen = c ^ k, then(∑_{i=0}^{n-1} Yᵢ - 𝔼[Yᵢ])/nconverges almost surely to0. This follows from a variance control, as
∑_k ℙ (|∑_{i=0}^{c^k - 1} Yᵢ - 𝔼[Yᵢ]| > c^k ε)
≤ ∑_k (c^k ε)^{-2} ∑_{i=0}^{c^k - 1} Var[Yᵢ] (by Markov inequality)
≤ ∑_i (C/i^2) Var[Yᵢ] (as ∑_{c^k > i} 1/(c^k)^2 ≤ C/i^2)
≤ ∑_i (C/i^2) 𝔼[Yᵢ^2]
≤ 2C 𝔼[X^2] (see `sum_variance_truncation_le`)
- As
𝔼[Yᵢ]converges to𝔼[X], it follows from the two previous items and Cesàro that, along the sequencen = c^k, one has(∑_{i=0}^{n-1} Xᵢ) / n → 𝔼[X]almost surely. - To generalize it to all indices, we use the fact that
∑_{i=0}^{n-1} Xᵢis nondecreasing and that, ifcis close enough to1, the gap betweenc^kandc^(k+1)is small.
Prerequisites on truncations #
Truncating a real-valued function to the interval (-A, A].
Equations
- ProbabilityTheory.truncation f A = Set.indicator (Set.Ioc (-A) A) id ∘ f
Instances For
If a function is integrable, then the integral of its truncated versions converges to the integral of the whole function.
The expectation of the truncated version of Xᵢ behaves asymptotically like the whole
expectation. This follows from convergence and Cesàro averaging.
The truncated and non-truncated versions of Xᵢ have the same asymptotic behavior, as they
almost surely coincide at all but finitely many steps. This follows from a probability computation
and Borel-Cantelli.
Xᵢ satisfies the strong law of large numbers along all integers. This follows from the
corresponding fact along the sequences c^n, and the fact that any integer can be sandwiched
between c^n and c^(n+1) with comparably small error if c is close enough to 1
(which is formalized in tendsto_div_of_monotone_of_tendsto_div_floor_pow).
Strong law of large numbers, almost sure version: if X n is a sequence of independent
identically distributed integrable real-valued random variables, then ∑ i in range n, X i / n
converges almost surely to 𝔼[X 0]. We give here the strong version, due to Etemadi, that only
requires pairwise independence. Superseded by strong_law_ae, which works for random variables
taking values in any Banach space.
Preliminary lemma for the strong law of large numbers for vector-valued random variables: the composition of the random variables with a simple function satisfies the strong law of large numbers.
Preliminary lemma for the strong law of large numbers for vector-valued random variables,
assuming measurability in addition to integrability. This is weakened to ae measurability in
the full version ProbabilityTheory.strong_law_ae.
Strong law of large numbers, almost sure version: if X n is a sequence of independent
identically distributed integrable random variables taking values in a Banach space,
then n⁻¹ • ∑ i in range n, X i converges almost surely to 𝔼[X 0]. We give here the strong
version, due to Etemadi, that only requires pairwise independence.
Strong law of large numbers, Lᵖ version: if X n is a sequence of independent
identically distributed random variables in Lᵖ, then n⁻¹ • ∑ i in range n, X i
converges in Lᵖ to 𝔼[X 0].