# Documentation

Mathlib.Probability.StrongLaw

# 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 #

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 Cesàro 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 #

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

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

Instances For
theorem MeasureTheory.AEStronglyMeasurable.truncation {α : Type u_1} {m : } {μ : } {f : α} (hf : ) {A : } :
theorem ProbabilityTheory.abs_truncation_le_bound {α : Type u_1} (f : α) (A : ) (x : α) :
|| |A|
@[simp]
theorem ProbabilityTheory.truncation_zero {α : Type u_1} (f : α) :
theorem ProbabilityTheory.abs_truncation_le_abs_self {α : Type u_1} (f : α) (A : ) (x : α) :
|| |f x|
theorem ProbabilityTheory.truncation_eq_self {α : Type u_1} {f : α} {A : } {x : α} (h : |f x| < A) :
= f x
theorem ProbabilityTheory.truncation_eq_of_nonneg {α : Type u_1} {f : α} {A : } (h : ∀ (x : α), 0 f x) :
theorem ProbabilityTheory.truncation_nonneg {α : Type u_1} {f : α} (A : ) {x : α} (h : 0 f x) :
theorem MeasureTheory.AEStronglyMeasurable.memℒp_truncation {α : Type u_1} {m : } {μ : } {f : α} (hf : ) {A : } {p : ENNReal} :
theorem MeasureTheory.AEStronglyMeasurable.integrable_truncation {α : Type u_1} {m : } {μ : } {f : α} (hf : ) {A : } :
theorem ProbabilityTheory.moment_truncation_eq_intervalIntegral {α : Type u_1} {m : } {μ : } {f : α} (hf : ) {A : } (hA : 0 A) {n : } (hn : n 0) :
∫ (x : α), μ = ∫ (y : ) in -A..A, y ^ n
theorem ProbabilityTheory.moment_truncation_eq_intervalIntegral_of_nonneg {α : Type u_1} {m : } {μ : } {f : α} (hf : ) {A : } {n : } (hn : n 0) (h'f : 0 f) :
∫ (x : α), μ = ∫ (y : ) in 0 ..A, y ^ n
theorem ProbabilityTheory.integral_truncation_eq_intervalIntegral {α : Type u_1} {m : } {μ : } {f : α} (hf : ) {A : } (hA : 0 A) :
∫ (x : α), μ = ∫ (y : ) in -A..A, y
theorem ProbabilityTheory.integral_truncation_eq_intervalIntegral_of_nonneg {α : Type u_1} {m : } {μ : } {f : α} (hf : ) {A : } (h'f : 0 f) :
∫ (x : α), μ = ∫ (y : ) in 0 ..A, y
theorem ProbabilityTheory.integral_truncation_le_integral_of_nonneg {α : Type u_1} {m : } {μ : } {f : α} (hf : ) (h'f : 0 f) {A : } :
∫ (x : α), μ ∫ (x : α), f xμ
theorem ProbabilityTheory.tendsto_integral_truncation {α : Type u_1} {m : } {μ : } {f : α} (hf : ) :
Filter.Tendsto (fun A => ∫ (x : α), μ) Filter.atTop (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 ProbabilityTheory.IdentDistrib.truncation {α : Type u_1} {m : } {μ : } {β : Type u_2} [] {ν : } {f : α} {g : β} (h : ) {A : } :
theorem ProbabilityTheory.sum_prob_mem_Ioc_le {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Ω} (hint : ) (hnonneg : 0 X) {K : } {N : } (hKN : K N) :
(Finset.sum () fun j => MeasureTheory.volume {ω | X ω Set.Ioc j N}) ENNReal.ofReal ((∫ (a : Ω), X a) + 1)
theorem ProbabilityTheory.tsum_prob_mem_Ioi_lt_top {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Ω} (hint : ) (hnonneg : 0 X) :
∑' (j : ), MeasureTheory.volume {ω | X ω Set.Ioi j} <
theorem ProbabilityTheory.sum_variance_truncation_le {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Ω} (hint : ) (hnonneg : 0 X) (K : ) :
(Finset.sum () fun j => (j ^ 2)⁻¹ * ∫ (a : Ω), ^ 2) a) 2 * ∫ (a : Ω), X a
theorem ProbabilityTheory.strong_law_aux1 {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : Ω) (hint : ) (hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j)) (hident : ∀ (i : ), ProbabilityTheory.IdentDistrib (X i) (X 0)) (hnonneg : ∀ (i : ) (ω : Ω), 0 X i ω) {c : } (c_one : 1 < c) {ε : } (εpos : 0 < ε) :
∀ᵐ (ω : Ω), ∀ᶠ (n : ) in Filter.atTop, |(Finset.sum (Finset.range c ^ n⌋₊) fun i => ProbabilityTheory.truncation (X i) (i) ω) - ∫ (a : Ω), Finset.sum (Finset.range c ^ n⌋₊) (fun i => ProbabilityTheory.truncation (X i) i) a| < ε * c ^ n⌋₊
theorem ProbabilityTheory.strong_law_aux2 {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : Ω) (hint : ) (hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j)) (hident : ∀ (i : ), ProbabilityTheory.IdentDistrib (X i) (X 0)) (hnonneg : ∀ (i : ) (ω : Ω), 0 X i ω) {c : } (c_one : 1 < c) :
∀ᵐ (ω : Ω), (fun n => (Finset.sum (Finset.range c ^ n⌋₊) fun i => ProbabilityTheory.truncation (X i) (i) ω) - ∫ (a : Ω), Finset.sum (Finset.range c ^ n⌋₊) (fun i => ProbabilityTheory.truncation (X i) i) a) =o[Filter.atTop] fun n => c ^ n⌋₊
theorem ProbabilityTheory.strong_law_aux3 {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : Ω) (hint : ) (hident : ∀ (i : ), ProbabilityTheory.IdentDistrib (X i) (X 0)) :
(fun n => (∫ (a : Ω), Finset.sum () (fun i => ProbabilityTheory.truncation (X i) i) a) - n * ∫ (a : Ω), X 0 a) =o[Filter.atTop] Nat.cast

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

theorem ProbabilityTheory.strong_law_aux4 {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : Ω) (hint : ) (hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j)) (hident : ∀ (i : ), ProbabilityTheory.IdentDistrib (X i) (X 0)) (hnonneg : ∀ (i : ) (ω : Ω), 0 X i ω) {c : } (c_one : 1 < c) :
∀ᵐ (ω : Ω), (fun n => (Finset.sum (Finset.range c ^ n⌋₊) fun i => ProbabilityTheory.truncation (X i) (i) ω) - c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[Filter.atTop] fun n => c ^ n⌋₊
theorem ProbabilityTheory.strong_law_aux5 {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : Ω) (hint : ) (hident : ∀ (i : ), ProbabilityTheory.IdentDistrib (X i) (X 0)) (hnonneg : ∀ (i : ) (ω : Ω), 0 X i ω) :
∀ᵐ (ω : Ω), (fun n => (Finset.sum () fun i => ProbabilityTheory.truncation (X i) (i) ω) - Finset.sum () fun i => X i ω) =o[Filter.atTop] fun 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 ProbabilityTheory.strong_law_aux6 {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : Ω) (hint : ) (hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j)) (hident : ∀ (i : ), ProbabilityTheory.IdentDistrib (X i) (X 0)) (hnonneg : ∀ (i : ) (ω : Ω), 0 X i ω) {c : } (c_one : 1 < c) :
∀ᵐ (ω : Ω), Filter.Tendsto (fun n => (Finset.sum (Finset.range c ^ n⌋₊) fun i => X i ω) / c ^ n⌋₊) Filter.atTop (nhds (∫ (a : Ω), X 0 a))
theorem ProbabilityTheory.strong_law_aux7 {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : Ω) (hint : ) (hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j)) (hident : ∀ (i : ), ProbabilityTheory.IdentDistrib (X i) (X 0)) (hnonneg : ∀ (i : ) (ω : Ω), 0 X i ω) :
∀ᵐ (ω : Ω), Filter.Tendsto (fun n => (Finset.sum () fun i => X i ω) / n) Filter.atTop (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 ProbabilityTheory.strong_law_ae {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : Ω) (hint : ) (hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j)) (hident : ∀ (i : ), ProbabilityTheory.IdentDistrib (X i) (X 0)) :
∀ᵐ (ω : Ω), Filter.Tendsto (fun n => (Finset.sum () fun i => X i ω) / n) Filter.atTop (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 ProbabilityTheory.strong_law_Lp {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {p : ENNReal} (hp : 1 p) (hp' : p ) (X : Ω) (hℒp : MeasureTheory.Memℒp (X 0) p) (hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j)) (hident : ∀ (i : ), ProbabilityTheory.IdentDistrib (X i) (X 0)) :
Filter.Tendsto (fun n => MeasureTheory.snorm (fun ω => (Finset.sum () fun i => X i ω) / n - ∫ (a : Ω), X 0 a) p MeasureTheory.volume) Filter.atTop (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].