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 β 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 β 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 #
If a function is integrable, then the integral of its truncated versions converges to the integral of the whole function.
Proof of the strong law of large numbers (almost sure version, assuming only pairwise independence) for nonnegative random variables, following Etemadi's proof.
The truncation of Xα΅’ up to i satisfies the strong law of large numbers (with respect to
the truncated expectation) along the sequence c^n, for any c > 1, up to a given Ξ΅ > 0.
This follows from a variance control.
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 β 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 β 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 β range n, X i
converges in Lα΅ to πΌ[X 0].