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

  βˆ‘_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 #

def ProbabilityTheory.truncation {Ξ± : Type u_1} (f : Ξ± β†’ ℝ) (A : ℝ) :
Ξ± β†’ ℝ

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

Equations
Instances For
    theorem ProbabilityTheory.abs_truncation_le_bound {Ξ± : Type u_1} (f : Ξ± β†’ ℝ) (A : ℝ) (x : Ξ±) :
    @[simp]
    theorem ProbabilityTheory.truncation_zero {Ξ± : Type u_1} (f : Ξ± β†’ ℝ) :
    theorem ProbabilityTheory.abs_truncation_le_abs_self {Ξ± : Type u_1} (f : Ξ± β†’ ℝ) (A : ℝ) (x : Ξ±) :
    theorem ProbabilityTheory.truncation_eq_self {Ξ± : Type u_1} {f : Ξ± β†’ ℝ} {A : ℝ} {x : Ξ±} (h : |f x| < A) :
    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) :
    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 : ℝ} :
    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_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) :
    βˆ€α΅ (Ο‰ : Ξ©), Filter.Tendsto (fun (n : β„•) => (βˆ‘ i ∈ Finset.range n, 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 ∈ 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} [MeasureTheory.MeasureSpace Ξ©] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {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) MeasureTheory.volume) (hident : βˆ€ (i : β„•), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) (Ο† : MeasureTheory.SimpleFunc E E) :
    βˆ€α΅ (Ο‰ : Ξ©), Filter.Tendsto (fun (n : β„•) => (↑n)⁻¹ β€’ βˆ‘ i ∈ Finset.range n, ↑φ (X i Ο‰)) Filter.atTop (nhds (∫ (a : Ξ©), (↑φ ∘ X 0) a))

    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} [MeasureTheory.MeasureSpace Ξ©] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] (X : β„• β†’ Ξ© β†’ E) (hint : MeasureTheory.Integrable (X 0) MeasureTheory.volume) (h' : MeasureTheory.StronglyMeasurable (X 0)) (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) :
    βˆ€α΅ (Ο‰ : Ξ©), Filter.Tendsto (fun (n : β„•) => (↑n)⁻¹ β€’ βˆ‘ i ∈ Finset.range n, X i Ο‰) Filter.atTop (nhds (∫ (a : Ξ©), X 0 a))

    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} [MeasureTheory.MeasureSpace Ξ©] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] (X : β„• β†’ Ξ© β†’ E) (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) :
    βˆ€α΅ (Ο‰ : Ξ©), Filter.Tendsto (fun (n : β„•) => (↑n)⁻¹ β€’ βˆ‘ i ∈ Finset.range n, X i Ο‰) 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 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} [MeasureTheory.MeasureSpace Ξ©] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {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 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) :
    Filter.Tendsto (fun (n : β„•) => MeasureTheory.snorm (fun (Ο‰ : Ξ©) => (↑n)⁻¹ β€’ βˆ‘ i ∈ Finset.range n, X i Ο‰ - ∫ (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 random variables in Lα΅–, then n⁻¹ β€’ βˆ‘ i ∈ range n, X i converges in Lα΅– to 𝔼[X 0].