mathlib documentation

probability.strong_law

The strong law of large numbers #

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.

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

  _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`)

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 : α) :
theorem probability_theory.truncation_eq_self {α : Type u_1} {f : α → } {A : } {x : α} (h : |f x| < A) :
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 : α → } (hf : measure_theory.ae_strongly_measurable f μ) {A : } (hA : 0 A) {n : } (hn : n 0) :
theorem probability_theory.moment_truncation_eq_interval_integral_of_nonneg {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : measure_theory.ae_strongly_measurable f μ) {A : } {n : } (hn : n 0) (h'f : 0 f) :
theorem probability_theory.integral_truncation_le_integral_of_nonneg {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : measure_theory.integrable f μ) (h'f : 0 f) {A : } :
(x : α), probability_theory.truncation f A x μ (x : α), f x μ
theorem probability_theory.tendsto_integral_truncation {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : measure_theory.integrable f μ) :
filter.tendsto (λ (A : ), (x : α), probability_theory.truncation f 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.strong_law_aux1 {Ω : Type u_1} [measure_theory.measure_space Ω] [measure_theory.is_probability_measure measure_theory.measure_space.volume] (X : Ω → ) (hint : measure_theory.integrable (X 0) measure_theory.measure_space.volume) (hindep : pairwise (λ (i j : ), probability_theory.indep_fun (X i) (X j) measure_theory.measure_space.volume)) (hident : ∀ (i : ), probability_theory.ident_distrib (X i) (X 0) measure_theory.measure_space.volume measure_theory.measure_space.volume) (hnonneg : ∀ (i : ) (ω : Ω), 0 X i ω) {c : } (c_one : 1 < c) {ε : } (εpos : 0 < ε) :
∀ᵐ (ω : Ω), ∀ᶠ (n : ) in filter.at_top, |(finset.range c ^ n⌋₊).sum (λ (i : ), probability_theory.truncation (X i) i ω) - ∫ (a : Ω), (finset.range c ^ n⌋₊).sum (λ (i : ), probability_theory.truncation (X i) i) a| < ε * c ^ n⌋₊

The expectation of the truncated version of Xᵢ behaves asymptotically like the whole expectation. This follows from convergence and Cesaro 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.

theorem probability_theory.strong_law_aux6 {Ω : Type u_1} [measure_theory.measure_space Ω] [measure_theory.is_probability_measure measure_theory.measure_space.volume] (X : Ω → ) (hint : measure_theory.integrable (X 0) measure_theory.measure_space.volume) (hindep : pairwise (λ (i j : ), probability_theory.indep_fun (X i) (X j) measure_theory.measure_space.volume)) (hident : ∀ (i : ), probability_theory.ident_distrib (X i) (X 0) measure_theory.measure_space.volume measure_theory.measure_space.volume) (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))

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.