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 random variables, then ∑ i ∈ 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 ∈ range n, X i / n converges in Lᵖ to 𝔼[X 0] provided X n is independent identically distributed and is Lᵖ.

Implementation

The main point is to prove the result for real-valued random variables, as the general case of Banach-space valued random variables follows from this case and approximation by simple functions. The real version is given in ProbabilityTheory.strong_law_ae_real.

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

Equations

• ProbabilityTheory.truncation f A = (Set.Ioc (-A) A).indicator id ∘ f

theorem MeasureTheory.AEStronglyMeasurable.truncation {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) {A : ℝ} : MeasureTheory.AEStronglyMeasurable (ProbabilityTheory.truncation f A) μ

theorem ProbabilityTheory.abs_truncation_le_bound {α : Type u_1} (f : α → ℝ) (A : ℝ) (x : α) : |ProbabilityTheory.truncation f A x| ≤ |A|

@[simp]

theorem ProbabilityTheory.truncation_zero {α : Type u_1} (f : α → ℝ) : ProbabilityTheory.truncation f 0 = 0

theorem ProbabilityTheory.abs_truncation_le_abs_self {α : Type u_1} (f : α → ℝ) (A : ℝ) (x : α) : |ProbabilityTheory.truncation f A x| ≤ |f x|

theorem ProbabilityTheory.truncation_eq_self {α : Type u_1} {f : α → ℝ} {A : ℝ} {x : α} (h : |f x| < A) : ProbabilityTheory.truncation f A x = f x

theorem ProbabilityTheory.truncation_eq_of_nonneg {α : Type u_1} {f : α → ℝ} {A : ℝ} (h : ∀ (x : α), 0 ≤ f x) : ProbabilityTheory.truncation f A = (Set.Ioc 0 A).indicator id ∘ f

theorem ProbabilityTheory.truncation_nonneg {α : Type u_1} {f : α → ℝ} (A : ℝ) {x : α} (h : 0 ≤ f x) : 0 ≤ ProbabilityTheory.truncation f A x

theorem MeasureTheory.AEStronglyMeasurable.memℒp_truncation {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.AEStronglyMeasurable f μ) {A : ℝ} {p : ENNReal} : MeasureTheory.Memℒp (ProbabilityTheory.truncation f A) p μ

theorem MeasureTheory.AEStronglyMeasurable.integrable_truncation {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.AEStronglyMeasurable f μ) {A : ℝ} : MeasureTheory.Integrable (ProbabilityTheory.truncation f A) μ

theorem ProbabilityTheory.moment_truncation_eq_intervalIntegral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) {A : ℝ} (hA : 0 ≤ A) {n : ℕ} (hn : n ≠ 0) : ∫ (x : α), ProbabilityTheory.truncation f A x ^ n ∂μ = ∫ (y : ℝ) in -A..A, y ^ n ∂MeasureTheory.Measure.map f μ

theorem ProbabilityTheory.moment_truncation_eq_intervalIntegral_of_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) {A : ℝ} {n : ℕ} (hn : n ≠ 0) (h'f : 0 ≤ f) : ∫ (x : α), ProbabilityTheory.truncation f A x ^ n ∂μ = ∫ (y : ℝ) in 0 ..A, y ^ n ∂MeasureTheory.Measure.map f μ

theorem ProbabilityTheory.integral_truncation_eq_intervalIntegral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) {A : ℝ} (hA : 0 ≤ A) : ∫ (x : α), ProbabilityTheory.truncation f A x ∂μ = ∫ (y : ℝ) in -A..A, y ∂MeasureTheory.Measure.map f μ

theorem ProbabilityTheory.integral_truncation_eq_intervalIntegral_of_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) {A : ℝ} (h'f : 0 ≤ f) : ∫ (x : α), ProbabilityTheory.truncation f A x ∂μ = ∫ (y : ℝ) in 0 ..A, y ∂MeasureTheory.Measure.map f μ

theorem ProbabilityTheory.integral_truncation_le_integral_of_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) (h'f : 0 ≤ f) {A : ℝ} : ∫ (x : α), ProbabilityTheory.truncation f A x ∂μ ≤ ∫ (x : α), f x ∂μ

theorem ProbabilityTheory.tendsto_integral_truncation {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) : Filter.Tendsto (fun (A : ℝ) => ∫ (x : α), ProbabilityTheory.truncation f 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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} [MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : α → ℝ} {g : β → ℝ} (h : ProbabilityTheory.IdentDistrib f g μ ν) {A : ℝ} : ProbabilityTheory.IdentDistrib (ProbabilityTheory.truncation f A) (ProbabilityTheory.truncation g A) μ ν

theorem ProbabilityTheory.sum_prob_mem_Ioc_le {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Ω → ℝ} (hint : MeasureTheory.Integrable X MeasureTheory.volume) (hnonneg : 0 ≤ X) {K : ℕ} {N : ℕ} (hKN : K ≤ N) : ∑ j ∈ Finset.range K, 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.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Ω → ℝ} (hint : MeasureTheory.Integrable X MeasureTheory.volume) (hnonneg : 0 ≤ X) : ∑' (j : ℕ), MeasureTheory.volume {ω : Ω | X ω ∈ Set.Ioi ↑j} < ⊤

theorem ProbabilityTheory.sum_variance_truncation_le {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Ω → ℝ} (hint : MeasureTheory.Integrable X MeasureTheory.volume) (hnonneg : 0 ≤ X) (K : ℕ) : ∑ j ∈ Finset.range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (ProbabilityTheory.truncation X ↑j ^ 2) a ≤ 2 * ∫ (a : Ω), X a

Proof of the strong law of large numbers (almost sure version, assuming only pairwise independence) for nonnegative random variables, following Etemadi's proof.

theorem ProbabilityTheory.strong_law_aux1 {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : ℕ → Ω → ℝ) (hint : MeasureTheory.Integrable (X 0) MeasureTheory.volume) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (X i) (X j) MeasureTheory.volume) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) (hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω) {c : ℝ} (c_one : 1 < c) {ε : ℝ} (εpos : 0 < ε) : ∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in Filter.atTop, |∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) ↑i) a| < ε * ↑⌊c ^ n⌋₊

The truncation of Xᵢ up to i satisfies the strong law of large numbers (with respect to the truncated expectation) along the sequence c^n, for any c > 1, up to a given ε > 0. This follows from a variance control.

theorem ProbabilityTheory.strong_law_aux2 {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : ℕ → Ω → ℝ) (hint : MeasureTheory.Integrable (X 0) MeasureTheory.volume) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (X i) (X j) MeasureTheory.volume) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) (hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω) {c : ℝ} (c_one : 1 < c) : ∀ᵐ (ω : Ω), (fun (n : ℕ) => ∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) ↑i) a) =o[Filter.atTop] fun (n : ℕ) => ↑⌊c ^ n⌋₊

theorem ProbabilityTheory.strong_law_aux3 {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : ℕ → Ω → ℝ) (hint : MeasureTheory.Integrable (X 0) MeasureTheory.volume) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) : (fun (n : ℕ) => (∫ (a : Ω), (∑ i ∈ Finset.range n, 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.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : ℕ → Ω → ℝ) (hint : MeasureTheory.Integrable (X 0) MeasureTheory.volume) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (X i) (X j) MeasureTheory.volume) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) (hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω) {c : ℝ} (c_one : 1 < c) : ∀ᵐ (ω : Ω), (fun (n : ℕ) => ∑ i ∈ Finset.range ⌊c ^ n⌋₊, 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.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : ℕ → Ω → ℝ) (hint : MeasureTheory.Integrable (X 0) MeasureTheory.volume) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) (hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω) : ∀ᵐ (ω : Ω), (fun (n : ℕ) => ∑ i ∈ Finset.range n, ProbabilityTheory.truncation (X i) (↑i) ω - ∑ i ∈ Finset.range n, 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.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : ℕ → Ω → ℝ) (hint : MeasureTheory.Integrable (X 0) MeasureTheory.volume) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (X i) (X j) MeasureTheory.volume) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) (hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω) {c : ℝ} (c_one : 1 < c) : ∀ᵐ (ω : Ω), Filter.Tendsto (fun (n : ℕ) => (∑ i ∈ Finset.range ⌊c ^ n⌋₊, X i ω) / ↑⌊c ^ n⌋₊) Filter.atTop (nhds (∫ (a : Ω), X 0 a))

theorem ProbabilityTheory.strong_law_aux7 {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X : ℕ → Ω → ℝ) (hint : MeasureTheory.Integrable (X 0) MeasureTheory.volume) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (X i) (X j) MeasureTheory.volume) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) (hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω) : ∀ᵐ (ω : Ω), Filter.Tendsto (fun (n : ℕ) => (∑ i ∈ Finset.range n, 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_real {Ω : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : ℕ → Ω → ℝ) (hint : MeasureTheory.Integrable (X 0) μ) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (X i) (X j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => (∑ i ∈ Finset.range n, X i ω) / ↑n) Filter.atTop (nhds (∫ (x : Ω), X 0 x ∂μ))

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 ∈ 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. Superseded by strong_law_ae, which works for random variables taking values in any Banach space.

theorem ProbabilityTheory.strong_law_ae_simpleFunc_comp {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] (X : ℕ → Ω → E) (h' : Measurable (X 0)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (X i) (X j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) (φ : MeasureTheory.SimpleFunc E E) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) Filter.atTop (nhds (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))

Preliminary lemma for the strong law of large numbers for vector-valued random variables: the composition of the random variables with a simple function satisfies the strong law of large numbers.

theorem ProbabilityTheory.strong_law_ae_of_measurable {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] (X : ℕ → Ω → E) (hint : MeasureTheory.Integrable (X 0) μ) (h' : MeasureTheory.StronglyMeasurable (X 0)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (X i) (X j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) Filter.atTop (nhds (∫ (x : Ω), X 0 x ∂μ))

Preliminary lemma for the strong law of large numbers for vector-valued random variables, assuming measurability in addition to integrability. This is weakened to ae measurability in the full version ProbabilityTheory.strong_law_ae.

theorem ProbabilityTheory.strong_law_ae {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] (X : ℕ → Ω → E) (hint : MeasureTheory.Integrable (X 0) μ) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (X i) (X j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) Filter.atTop (nhds (∫ (x : Ω), X 0 x ∂μ))

Strong law of large numbers, almost sure version: if X n is a sequence of independent identically distributed integrable random variables taking values in a Banach space, then n⁻¹ • ∑ i ∈ range n, X i 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} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {p : ENNReal} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (X : ℕ → Ω → E) (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.eLpNorm (fun (ω : Ω) => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω - ∫ (x : Ω), X 0 x ∂μ) p μ) Filter.atTop (nhds 0)

Strong law of large numbers, Lᵖ version: if X n is a sequence of independent identically distributed random variables in Lᵖ, then n⁻¹ • ∑ i ∈ range n, X i converges in Lᵖ to 𝔼[X 0].