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 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.
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 #
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_le
andtsum_prob_mem_Ioi_lt_top
). - Let
c > 1
. Along the sequencen = c ^ k
, then(ā_{i=0}^{n-1} Yįµ¢ - š¼[Yįµ¢])/n
converges 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, ifc
is close enough to1
, the gap betweenc^k
andc^(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.
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.
Strong law of large numbers, Lįµ version: if X n
is a sequence of independent
identically distributed real-valued random variables in Lįµ, then ā i in range n, X i / n
converges in Lįµ to š¼[X 0]
.