# mathlib3documentation

probability.strong_law

# The strong law of large numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We prove the strong law of large numbers, in probability_theory.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 probability_theory.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, 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 by 1 + 𝔼[X] (see sum_prob_mem_Ioc_le and tsum_prob_mem_Ioi_lt_top).
• Let c > 1. Along the sequence n = c ^ k, then (∑_{i=0}^{n-1} Yᵢ - 𝔼[Yᵢ])/n converges almost surely to 0. 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 Cesaro that, along the sequence n = 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, if c is close enough to 1, the gap between c^k and c^(k+1) is small.

### Prerequisites on truncations #

noncomputable def probability_theory.truncation {α : Type u_1} (f : α ) (A : ) :
α

Truncating a real-valued function to the interval (-A, A].

Equations
theorem probability_theory.abs_truncation_le_bound {α : Type u_1} (f : α ) (A : ) (x : α) :
@[simp]
theorem probability_theory.truncation_zero {α : Type u_1} (f : α ) :
theorem probability_theory.abs_truncation_le_abs_self {α : Type u_1} (f : α ) (A : ) (x : α) :
|f x|
theorem probability_theory.truncation_eq_self {α : Type u_1} {f : α } {A : } {x : α} (h : |f x| < A) :
= f x
theorem probability_theory.truncation_eq_of_nonneg {α : Type u_1} {f : α } {A : } (h : (x : α), 0 f x) :
theorem probability_theory.truncation_nonneg {α : Type u_1} {f : α } (A : ) {x : α} (h : 0 f x) :
theorem probability_theory.moment_truncation_eq_interval_integral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α } {A : } (hA : 0 A) {n : } (hn : n 0) :
(x : α), μ = (y : ) in -A..A, y ^ n
theorem probability_theory.moment_truncation_eq_interval_integral_of_nonneg {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α } {A : } {n : } (hn : n 0) (h'f : 0 f) :
(x : α), μ = (y : ) in 0..A, y ^ n
theorem probability_theory.integral_truncation_eq_interval_integral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α } {A : } (hA : 0 A) :
(x : α), μ = (y : ) in -A..A, y
theorem probability_theory.integral_truncation_eq_interval_integral_of_nonneg {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α } {A : } (h'f : 0 f) :
(x : α), μ = (y : ) in 0..A, y
theorem probability_theory.integral_truncation_le_integral_of_nonneg {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α } (hf : μ) (h'f : 0 f) {A : } :
(x : α), μ (x : α), f x μ
theorem probability_theory.tendsto_integral_truncation {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α } (hf : μ) :
filter.tendsto (λ (A : ), (x : α), μ) filter.at_top (nhds ( (x : α), f x μ))

If a function is integrable, then the integral of its truncated versions converges to the integral of the whole function.

theorem probability_theory.ident_distrib.truncation {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} {ν : measure_theory.measure β} {f : α } {g : β } (h : ν) {A : } :
theorem probability_theory.sum_prob_mem_Ioc_le {Ω : Type u_1} {X : Ω } (hnonneg : 0 X) {K N : } (hKN : K N) :
(finset.range K).sum (λ (j : ), measure_theory.measure_space.volume {ω : Ω | X ω N}) ennreal.of_real (( (a : Ω), X a) + 1)
theorem probability_theory.tsum_prob_mem_Ioi_lt_top {Ω : Type u_1} {X : Ω } (hnonneg : 0 X) :
theorem probability_theory.sum_variance_truncation_le {Ω : Type u_1} {X : Ω } (hnonneg : 0 X) (K : ) :
(finset.range K).sum (λ (j : ), (j ^ 2)⁻¹ * (a : Ω), a) 2 * (a : Ω), X a
theorem probability_theory.strong_law_aux1 {Ω : Type u_1} (X : Ω ) (hindep : pairwise (λ (i j : ), ) (hident : (i : ), ) (hnonneg : (i : ) (ω : Ω), 0 X i ω) {c : } (c_one : 1 < c) {ε : } (εpos : 0 < ε) :
∀ᵐ (ω : Ω), ∀ᶠ (n : ) in filter.at_top, |(finset.range c ^ n⌋₊).sum (λ (i : ), ω) - (a : Ω), (finset.range c ^ n⌋₊).sum (λ (i : ), i) a| < ε * c ^ n⌋₊
theorem probability_theory.strong_law_aux2 {Ω : Type u_1} (X : Ω ) (hindep : pairwise (λ (i j : ), ) (hident : (i : ), ) (hnonneg : (i : ) (ω : Ω), 0 X i ω) {c : } (c_one : 1 < c) :
∀ᵐ (ω : Ω), (λ (n : ), (finset.range c ^ n⌋₊).sum (λ (i : ), ω) - (a : Ω), (finset.range c ^ n⌋₊).sum (λ (i : ), i) a) =o[filter.at_top] λ (n : ), c ^ n⌋₊
theorem probability_theory.strong_law_aux3 {Ω : Type u_1} (X : Ω ) (hident : (i : ), ) :
(λ (n : ), ( (a : Ω), (finset.range n).sum (λ (i : ), i) a) - n * (a : Ω), X 0 a) =o[filter.at_top] coe

The expectation of the truncated version of Xᵢ behaves asymptotically like the whole expectation. This follows from convergence and Cesaro averaging.

theorem probability_theory.strong_law_aux4 {Ω : Type u_1} (X : Ω ) (hindep : pairwise (λ (i j : ), ) (hident : (i : ), ) (hnonneg : (i : ) (ω : Ω), 0 X i ω) {c : } (c_one : 1 < c) :
∀ᵐ (ω : Ω), (λ (n : ), (finset.range c ^ n⌋₊).sum (λ (i : ), ω) - c ^ n⌋₊ * (a : Ω), X 0 a) =o[filter.at_top] λ (n : ), c ^ n⌋₊
theorem probability_theory.strong_law_aux5 {Ω : Type u_1} (X : Ω ) (hident : (i : ), ) (hnonneg : (i : ) (ω : Ω), 0 X i ω) :
∀ᵐ (ω : Ω), (λ (n : ), (finset.range n).sum (λ (i : ), ω) - (finset.range n).sum (λ (i : ), X i ω)) =o[filter.at_top] λ (n : ), n

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.

theorem probability_theory.strong_law_aux6 {Ω : Type u_1} (X : Ω ) (hindep : pairwise (λ (i j : ), ) (hident : (i : ), ) (hnonneg : (i : ) (ω : Ω), 0 X i ω) {c : } (c_one : 1 < c) :
∀ᵐ (ω : Ω), filter.tendsto (λ (n : ), (finset.range c ^ n⌋₊).sum (λ (i : ), X i ω) / c ^ n⌋₊) filter.at_top (nhds ( (a : Ω), X 0 a))
theorem probability_theory.strong_law_aux7 {Ω : Type u_1} (X : Ω ) (hindep : pairwise (λ (i j : ), ) (hident : (i : ), ) (hnonneg : (i : ) (ω : Ω), 0 X i ω) :
∀ᵐ (ω : Ω), filter.tendsto (λ (n : ), (finset.range n).sum (λ (i : ), X i ω) / n) filter.at_top (nhds ( (a : Ω), X 0 a))

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).

theorem probability_theory.strong_law_ae {Ω : Type u_1} (X : Ω ) (hindep : pairwise (λ (i j : ), ) (hident : (i : ), ) :
∀ᵐ (ω : Ω), filter.tendsto (λ (n : ), (finset.range n).sum (λ (i : ), X i ω) / n) filter.at_top (nhds ( (a : Ω), X 0 a))

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.

theorem probability_theory.strong_law_Lp {Ω : Type u_1} {p : ennreal} (hp : 1 p) (hp' : p ) (X : Ω ) (hℒp : p measure_theory.measure_space.volume) (hindep : pairwise (λ (i j : ), ) (hident : (i : ), ) :
filter.tendsto (λ (n : ), measure_theory.snorm (λ (ω : Ω), (finset.range n).sum (λ (i : ), X i ω) / n - (a : Ω), X 0 a) p measure_theory.measure_space.volume) filter.at_top (nhds 0)

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].