mathlib3 documentation

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

  _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.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.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 μ

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

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