Berry–Esseen theorem

TheoremBerry–Esseen bound for finite sums#✓fully proved

Let \((\xi_j)_{j \in \mathbb{N}}\) be measurable, mutually independent real random variables on a probability space, and let \(s\) be a finite set of indices such that for each \(j \in s\) the variable \(\xi_j\) has a finite third moment and mean \(\mathbb{E}[\xi_j] = 0\), and such that \(\sum_{j \in s} \mathbb{E}[\xi_j^2] = 1\). Write \(\Phi\) for the distribution function of the standard normal distribution. If \(\gamma \ge 0\) is a real number with \(\sum_{j \in s} \mathbb{E}|\xi_j|^3 \le \gamma\), then for every real \(z\),

\[\left|\mathbb{P}\left(\sum_{j \in s} \xi_j \le z\right) - \Phi(z)\right| \le 42\gamma.\]
theorem berry_esseen_finsetSum_gaussian {Ω : Type*}
    [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {ξ : ℕ → Ω → ℝ} (hmeas : ∀ j, Measurable (ξ j))
    (hindep : iIndepFun ξ P) {s : Finset ℕ}
    (hmem : ∀ j ∈ s, MemLp (ξ j) 3 P)
    (hmean : ∀ j ∈ s, P[ξ j] = 0)
    (hvar : ∑ j ∈ s, P[fun ω => (ξ j ω) ^ 2] = 1)
    {γ : ℝ} (hγ : 0 ≤ γ)
    (hγ3 : ∑ j ∈ s, P[fun ω => |ξ j ω| ^ 3] ≤ γ)
    (z : ℝ) :
    |P.real {ω | ∑ j ∈ s, ξ j ω ≤ z} - (gaussianReal 0 1).real (Iic z)|
      ≤ 42 * γ
Used by 1
Used byBerry–Esseen theorem with constant 42

TheoremBerry–Esseen theorem with constant 42#✓fully proved

Let \(X_0, X_1, X_2, \dots\) be measurable, mutually independent real random variables on a probability space, each with the same distribution as \(X_0\), where \(X_0\) has a finite third moment, mean \(\mathbb{E}[X_0] = 0\) and variance \(\sigma^2 = \operatorname{Var}(X_0) > 0\) with \(\sigma > 0\). Write \(\rho = \mathbb{E}|X_0|^3\), \(S_n = X_0 + \dots + X_{n-1}\), and \(\Phi\) for the distribution function of the standard normal distribution. Then for every \(n \ge 1\) and every real \(x\),

\[\left|\mathbb{P}\left(\frac{S_n}{\sqrt{n\sigma^2}} \le x\right) - \Phi(x)\right| \le \frac{42\rho}{\sigma^3\sqrt{n}}.\]

Integrability of \(X_0\) is not assumed separately, since on a probability space it follows from the finite third moment.

theorem berry_esseen_explicit
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    (X : ℕ → Ω → ℝ)
    (hXmeas : ∀ n, Measurable (X n))
    (hXindep : iIndepFun X P)
    (hXid : ∀ i, IdentDistrib (X i) (X 0) P P)
    (hXmem : MemLp (X 0) 3 P)
    (hXmean : P[X 0] = 0)
    (hXvar : 0 < Var[X 0; P])
    (n : ℕ) (hn : 0 < n) (x : ℝ) :
    |((P.map (fun ω => (∑ i ∈ range n, X i ω) / Real.sqrt (n * Var[X 0; P]))).real (Iic x)
      - (gaussianReal 0 1).real (Iic x))|
      ≤ 42 * (P[fun ω => |X 0 ω| ^ 3])
        / (Real.sqrt (Var[X 0; P]) ^ 3 * Real.sqrt (n : ℝ))
Uses 1 · Used by 2
Proof usesBerry–Esseen bound for finite sums
Used byBerry–Esseen theorem · The Berry–Esseen bound with coefficient 42

TheoremBerry–Esseen theorem#✓fully proved

There is a constant \(C > 0\) with the following property. Let \(X_0, X_1, X_2, \dots\) be measurable, mutually independent real random variables on a probability space, each with the same distribution as \(X_0\), where \(X_0\) is integrable and has a finite third moment, mean \(\mathbb{E}[X_0] = 0\) and variance \(\sigma^2 = \operatorname{Var}(X_0) > 0\) with \(\sigma > 0\). Write \(\rho = \mathbb{E}|X_0|^3\), \(S_n = X_0 + \dots + X_{n-1}\), and \(\Phi\) for the distribution function of the standard normal distribution. Then for every \(n \ge 1\) and every real \(x\),

\[\left|\mathbb{P}\left(\frac{S_n}{\sqrt{n\sigma^2}} \le x\right) - \Phi(x)\right| \le \frac{C\rho}{\sigma^3\sqrt{n}}.\]
MathlibExt.Probability.BerryEsseenWanted.berry_esseen · 16 lines 
theorem berry_esseen
    : ∃ C : ℝ, 0 < C ∧
      ∀ {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
        (X : ℕ → Ω → ℝ),
        (∀ n, Measurable (X n)) →
        iIndepFun X P →
        (∀ i, IdentDistrib (X i) (X 0) P P) →
        Integrable (X 0) P →
        MemLp (X 0) 3 P →
        P[X 0] = 0 →
        0 < Var[X 0; P] →
        ∀ (n : ℕ), 0 < n →
          ∀ x : ℝ,
            |((P.map (fun ω => (∑ i ∈ range n, X i ω) / Real.sqrt (n * Var[X 0; P]))).real (Iic x)
              - (gaussianReal 0 1).real (Iic x))|
            ≤ C * (P[fun ω => |X 0 ω| ^ 3]) / (Real.sqrt (Var[X 0; P]) ^ 3 * Real.sqrt (n : ℝ))
Sources
  • A. C. Berry, Trans. AMS 49 (1941), 122-136, DOI 10.2307/1990053; and C.-G. Esseen, Arkiv för Matematik, Astronomi och Fysik 28A no. 9 (1942), 1-19.
Uses 1
Proof usesBerry–Esseen theorem with constant 42

StructureStandardized laws with finite third moment#✓fully proved

A measure \(\mu\) on \(\mathbb{R}\) is a standardized law when it is a probability measure with mean \(\int x \, d\mu(x) = 0\) and variance \(1\), and has finite third absolute moment \(\int |x|^3 \, d\mu(x) < \infty\).

structure IsStandardizedLaw (μ : Measure ℝ) : Prop where
  probability : IsProbabilityMeasure μ
  mean_zero : (∫ x, x ∂μ) = 0
  variance_one : variance id μ = 1
  third_moment : MemLp id 3 μ
Used by 22
Used byCoordinates of the i.i.d. product are distributed like the original law · Coordinates of the i.i.d. product are independent · Coordinate laws of the i.i.d. product · The i.i.d. product of a standardized law is a probability measure · CDF of the normalized sum · The normalized law with one summand · The normalized law is a probability measure · The standard Gaussian is a standardized law · The common law of an i.i.d. model is standardized · Standardized laws have an integrable third absolute moment · The third absolute moment of a standardized law is positive · Bernoulli-admissible coefficients exist · The Bernoulli Berry–Esseen constant is at most the general one · Admissible Berry–Esseen coefficient · The Berry–Esseen bound with coefficient 42 · Admissibility is upward closed · Standardized two-point law · Statement of the Korolev–Shevtsova structural Berry–Esseen bound · Statement of the Kolmogorov distance via left-continuous distribution functions · The symmetric Bernoulli law is a standardized two-point law · The symmetric Bernoulli law is standardized · The optimal Berry–Esseen coefficient satisfies the Berry–Esseen bound

DefinitionI.i.d. product law#✓fully proved

For a measure \(\mu\) on \(\mathbb{R}\), the i.i.d. product law of \(\mu\) is the measure on the sequence space \(\mathbb{R}^{\mathbb{N}}\) that is the infinite product \(\mu^{\otimes \mathbb{N}}\) of countably many copies of \(\mu\) when \(\mu\) is a probability measure, and the zero measure otherwise.

noncomputable def iidLaw (μ : Measure ℝ) : Measure (ℕ → ℝ) :=
  Measure.infinitePi (fun _ : ℕ ↦ μ)
Used by 11
Used byCoordinates of the i.i.d. product are distributed like the original law · Coordinates of the i.i.d. product are independent · Coordinate laws of the i.i.d. product · The i.i.d. product of a standardized law is a probability measure · The joint law of a standardized i.i.d. model · CDF of the normalized sum · Law of the normalized sum · Normalized sums of an i.i.d. model have the canonical law · The normalized law with one summand · The normalized law is a probability measure · The Berry–Esseen bound with coefficient 42

DefinitionNormalized sum#✓fully proved

For a positive integer \(n\) and a real sequence \(\omega = (\omega_0, \omega_1, \dots)\), the normalized sum \(S_n(\omega)\) is the sum of the first \(n\) coordinates divided by \(\sqrt{n}\): \(S_n(\omega) = (\omega_0 + \dots + \omega_{n-1})/\sqrt{n}\).

noncomputable def normalizedSum (n : ℕ+) (ω : ℕ → ℝ) : ℝ :=
  (∑ i ∈ Finset.range n.1, ω i) / Real.sqrt (n.1 : ℝ)
Used by 6
Used byCDF of the normalized sum · Law of the normalized sum · Normalized sums of an i.i.d. model have the canonical law · The normalized law with one summand · The normalized law is a probability measure · Measurability of the normalized sum

DefinitionLaw of the normalized sum#✓fully proved

For a measure \(\mu\) on \(\mathbb{R}\) and a positive integer \(n\), the normalized law of \(\mu\) at \(n\) is the pushforward of the i.i.d. law of \(\mu\) on \(\mathbb{R}^{\mathbb{N}}\) (the product measure \(\mu^{\otimes \mathbb{N}}\) when \(\mu\) is a probability measure, and the zero measure otherwise) under the normalized sum \(\omega \mapsto (\omega_0 + \dots + \omega_{n-1})/\sqrt{n}\).

noncomputable def normalizedLaw (μ : Measure ℝ) (n : ℕ+) : Measure ℝ :=
  (iidLaw μ).map (normalizedSum n)
Uses 2 · Used by 15
Statement usesI.i.d. product law · Normalized sum
Used byKolmogorov error bounds are uniform CDF bounds · The CDF errors are bounded above · Kolmogorov error · The Kolmogorov error is at most one · The Kolmogorov error is nonnegative · CDF of the normalized sum · Normalized sums of an i.i.d. model have the canonical law · The normalized law with one summand · The normalized law is a probability measure · The CDF error is at most one · Each CDF error is at most the Kolmogorov error · The Kolmogorov error vanishes for one standard Gaussian summand · Admissible coefficients bound every standardized i.i.d. sequence · The Berry–Esseen bound with coefficient 42 · Statement of the Kolmogorov distance via left-continuous distribution functions

DefinitionStandard normal CDF#✓fully proved

For \(x \in \mathbb{R}\), \(\Phi(x)\) is the value at \(x\) of the cumulative distribution function of the standard normal distribution \(\mathcal{N}(0, 1)\), that is, the probability that a standard normal random variable is at most \(x\).

noncomputable def normalCDF (x : ℝ) : ℝ := cdf (gaussianReal 0 1) x
Used by 11
Used byKolmogorov error bounds are uniform CDF bounds · The CDF errors are bounded above · Kolmogorov error · The Kolmogorov error is at most one · The Kolmogorov error is nonnegative · The CDF error is at most one · Each CDF error is at most the Kolmogorov error · The Kolmogorov error vanishes for one standard Gaussian summand · Admissible coefficients bound every standardized i.i.d. sequence · The Berry–Esseen bound with coefficient 42 · Statement of the Kolmogorov distance via left-continuous distribution functions

DefinitionThird absolute moment#✓fully proved

The third absolute moment of a measure \(\mu\) on \(\mathbb{R}\) is the real number \(\int |x|^3 \, d\mu(x)\), taken to be \(0\) when \(x \mapsto |x|^3\) is not integrable with respect to \(\mu\).

This integrand is integrable whenever \(\mu\) is a standardized law.

noncomputable def thirdMoment (μ : Measure ℝ) : ℝ := ∫ x, |x| ^ 3 ∂μ
Used by 14
Used byThird absolute moment of the common law · Nonnegativity of the third absolute moment · The third absolute moment of a standardized law is positive · Statement of Esseen's asymptotic lower bound for a two-point law · Admissible coefficients bound every standardized i.i.d. sequence · Admissible Berry–Esseen coefficient · The Berry–Esseen bound with coefficient 42 · Admissibility is upward closed · Admissible coefficients are nonnegative · Admissible Berry–Esseen coefficient for two-point laws · Bernoulli-admissible coefficients are nonnegative · Statement of the Korolev–Shevtsova structural Berry–Esseen bound · Third absolute moment of the symmetric Bernoulli law · The optimal Berry–Esseen coefficient satisfies the Berry–Esseen bound

TheoremFinite third absolute moment as an \(L^3\) condition#✓fully proved

For every measure \(\mu\) on \(\mathbb{R}\), the identity function \(x \mapsto x\) belongs to \(L^3(\mu)\) if and only if the function \(x \mapsto |x|^3\) is \(\mu\)-integrable.

theorem memLp_three_iff_integrable_absCube (μ : Measure ℝ) :
    MemLp id 3 μ ↔ Integrable (fun x : ℝ ↦ |x| ^ 3) μ

DefinitionKolmogorov error#✓fully proved

For a measure \(\mu\) on \(\mathbb{R}\) and a positive integer \(n\), the Kolmogorov error of \(\mu\) at \(n\) is the real supremum \(\sup_{x \in \mathbb{R}} |F_{\mu,n}(x) - \Phi(x)|\), where \(\Phi\) is the standard normal cumulative distribution function and \(F_{\mu,n}\) is Mathlib's cumulative distribution function of the normalized law of \(\mu\) at \(n\). When \(\mu\) is a probability measure, \(F_{\mu,n}(x)\) is the mass the normalized law gives to \((-\infty, x]\); otherwise the normalized law is the zero measure and \(F_{\mu,n}\) is a fixed but unspecified cumulative distribution function of some probability measure, not the zero function.

The values \(|F_{\mu,n}(x) - \Phi(x)|\) lie in \([0, 1]\), so the supremum is finite.

noncomputable def kolmogorovError (μ : Measure ℝ) (n : ℕ+) : ℝ :=
  sSup (Set.range (fun x : ℝ ↦ |cdf (normalizedLaw μ n) x - normalCDF x|))
Uses 2 · Used by 16
Statement usesStandard normal CDF · Law of the normalized sum
Used byKolmogorov error bounds are uniform CDF bounds · The Kolmogorov error is at most one · The Kolmogorov error is nonnegative · Each CDF error is at most the Kolmogorov error · The Kolmogorov error vanishes for one standard Gaussian summand · Statement of Esseen's asymptotic lower bound for a two-point law · Admissible coefficients bound every standardized i.i.d. sequence · Admissible Berry–Esseen coefficient · The Berry–Esseen bound with coefficient 42 · Admissibility is upward closed · Admissible coefficients are nonnegative · Admissible Berry–Esseen coefficient for two-point laws · Bernoulli-admissible coefficients are nonnegative · Statement of the Korolev–Shevtsova structural Berry–Esseen bound · Statement of the Kolmogorov distance via left-continuous distribution functions · The optimal Berry–Esseen coefficient satisfies the Berry–Esseen bound

TheoremThe i.i.d. product of a standardized law is a probability measure#✓fully proved

If \(\mu\) is a standardized law on \(\mathbb{R}\), then the i.i.d. product law of \(\mu\) on \(\mathbb{R}^{\mathbb{N}}\) is a probability measure.

theorem iidLaw_probability {μ : Measure ℝ} (hμ : IsStandardizedLaw μ) :
    IsProbabilityMeasure (iidLaw μ)
Uses 2 · Used by 2
Statement usesStandardized laws with finite third moment · I.i.d. product law
Used byThe normalized law is a probability measure · The Berry–Esseen bound with coefficient 42

TheoremMeasurability of the normalized sum#✓fully proved

For every positive integer \(n\), the map sending a real sequence \(\omega = (\omega_0, \omega_1, \dots)\) to \((\omega_0 + \dots + \omega_{n-1})/\sqrt{n}\) is measurable with respect to the product \(\sigma\)-algebra on \(\mathbb{R}^{\mathbb{N}}\).

theorem normalizedSum_measurable (n : ℕ+) : Measurable (normalizedSum n)
Uses 1 · Used by 2
Statement usesNormalized sum
Used byCDF of the normalized sum · Normalized sums of an i.i.d. model have the canonical law

TheoremThe normalized law is a probability measure#✓fully proved

For every standardized law \(\mu\) on \(\mathbb{R}\) (a probability measure with mean \(0\), variance \(1\) and finite third absolute moment) and every positive integer \(n\), the normalized law of \(\mu\) at \(n\) is a probability measure.

theorem normalizedLaw_probability {μ : Measure ℝ} (hμ : IsStandardizedLaw μ)
    (n : ℕ+) : IsProbabilityMeasure (normalizedLaw μ n)
Uses 5 · Used by 2
Statement usesStandardized laws with finite third moment · Law of the normalized sum
Proof usesI.i.d. product law · The i.i.d. product of a standardized law is a probability measure · Normalized sum
Used byCDF of the normalized sum · The Berry–Esseen bound with coefficient 42

TheoremCoordinates of the i.i.d. product are independent#✓fully proved

If \(\mu\) is a standardized law on \(\mathbb{R}\), then the coordinate maps \(\omega \mapsto \omega_i\) on \(\mathbb{R}^{\mathbb{N}}\), for \(i \in \mathbb{N}\), are mutually independent under the i.i.d. product law of \(\mu\).

theorem iidLaw_independent {μ : Measure ℝ} (hμ : IsStandardizedLaw μ) :
    iIndepFun (fun (i : ℕ) (ω : ℕ → ℝ) ↦ ω i) (iidLaw μ)
Uses 2 · Used by 1
Statement usesStandardized laws with finite third moment · I.i.d. product law
Used byThe Berry–Esseen bound with coefficient 42

TheoremCoordinate laws of the i.i.d. product#✓fully proved

If \(\mu\) is a standardized law on \(\mathbb{R}\) and \(i\) is a natural number, then the pushforward of the i.i.d. product law of \(\mu\) under the coordinate map \(\omega \mapsto \omega_i\) from \(\mathbb{R}^{\mathbb{N}}\) to \(\mathbb{R}\) is \(\mu\).

theorem iidLaw_map_eval {μ : Measure ℝ} (hμ : IsStandardizedLaw μ) (i : ℕ) :
    (iidLaw μ).map (fun ω ↦ ω i) = μ
Uses 2 · Used by 2
Statement usesStandardized laws with finite third moment · I.i.d. product law
Used byCoordinates of the i.i.d. product are distributed like the original law · The normalized law with one summand

TheoremCoordinates of the i.i.d. product are distributed like the original law#✓fully proved

Let \(\mu\) be a standardized law on \(\mathbb{R}\) and let \(i\) be a natural number. The coordinate map \(\omega \mapsto \omega_i\) on \(\mathbb{R}^{\mathbb{N}}\) under the i.i.d. product law of \(\mu\) and the identity map of \(\mathbb{R}\) under \(\mu\) are identically distributed.

theorem iidLaw_identDistrib {μ : Measure ℝ} (hμ : IsStandardizedLaw μ) (i : ℕ) :
    IdentDistrib (fun ω : ℕ → ℝ ↦ ω i) id (iidLaw μ) μ
Uses 3 · Used by 1
Statement usesStandardized laws with finite third moment · I.i.d. product law
Proof usesCoordinate laws of the i.i.d. product
Used byThe Berry–Esseen bound with coefficient 42

TheoremCDF of the normalized sum#✓fully proved

Let \(\mu\) be a standardized law on \(\mathbb{R}\) (a probability measure with mean \(0\), variance \(1\) and finite third absolute moment), let \(n\) be a positive integer and let \(x \in \mathbb{R}\). Then the cumulative distribution function of the normalized law of \(\mu\) at \(n\), evaluated at \(x\), equals the probability under the i.i.d. law \(\mu^{\otimes \mathbb{N}}\) on \(\mathbb{R}^{\mathbb{N}}\) of the event \(\{\omega \in \mathbb{R}^{\mathbb{N}} : (\omega_0 + \dots + \omega_{n-1})/\sqrt{n} \le x\}\).

theorem normalized_cdf_eq {μ : Measure ℝ} (hμ : IsStandardizedLaw μ)
    (n : ℕ+) (x : ℝ) :
    cdf (normalizedLaw μ n) x = (iidLaw μ).real {ω | normalizedSum n ω ≤ x}
Uses 6
Statement usesStandardized laws with finite third moment · I.i.d. product law · Law of the normalized sum · Normalized sum
Proof usesThe normalized law is a probability measure · Measurability of the normalized sum

TheoremStandardized laws have an integrable third absolute moment#✓fully proved

If \(\mu\) is a standardized law on \(\mathbb{R}\), then the function \(x \mapsto |x|^3\) is integrable with respect to \(\mu\).

theorem thirdMoment_integrable {μ : Measure ℝ} (hμ : IsStandardizedLaw μ) :
    Integrable (fun x : ℝ ↦ |x| ^ 3) μ
Uses 1 · Used by 1
Statement usesStandardized laws with finite third moment
Used byThe third absolute moment of a standardized law is positive

TheoremNonnegativity of the third absolute moment#✓fully proved

For every measure \(\mu\) on \(\mathbb{R}\), the third absolute moment \(\int_{\mathbb{R}} |x|^3 \, d\mu(x)\) is nonnegative.

As a real number, this integral is taken to be \(0\) when \(|x|^3\) is not \(\mu\)-integrable.

theorem thirdMoment_nonnegative (μ : Measure ℝ) : 0 ≤ thirdMoment μ
Uses 1 · Used by 2
Statement usesThird absolute moment
Used byThe third absolute moment of a standardized law is positive · Admissibility is upward closed

TheoremThe third absolute moment of a standardized law is positive#✓fully proved

If \(\mu\) is a standardized law on \(\mathbb{R}\), that is, a probability measure with mean \(0\), variance \(1\) and finite third absolute moment, then its third absolute moment \(\int |x|^3 \, d\mu(x)\) is strictly positive.

The variance condition is what excludes a zero third absolute moment.

theorem thirdMoment_positive {μ : Measure ℝ} (hμ : IsStandardizedLaw μ) :
    0 < thirdMoment μ
Uses 4 · Used by 2
Statement usesStandardized laws with finite third moment · Third absolute moment
Proof usesStandardized laws have an integrable third absolute moment · Nonnegativity of the third absolute moment
Used byAdmissible coefficients are nonnegative · The optimal Berry–Esseen coefficient satisfies the Berry–Esseen bound

TheoremThe CDF error is at most one#✓fully proved

Let \(\mu\) be a measure on \(\mathbb{R}\), \(n\) a positive integer and \(x\) a real number. Let \(F_{\mu,n}\) be the distribution function of the normalized law of \(\mu\) at \(n\) and \(\Phi\) the standard normal distribution function. Then \(|F_{\mu,n}(x) - \Phi(x)| \le 1\).

No assumption is made on \(\mu\): both distribution functions take values in \([0, 1]\).

theorem pointwise_error_le_one (μ : Measure ℝ) (n : ℕ+) (x : ℝ) :
    |cdf (normalizedLaw μ n) x - normalCDF x| ≤ 1
Uses 2 · Used by 2
Statement usesStandard normal CDF · Law of the normalized sum
Used byThe CDF errors are bounded above · The Kolmogorov error is at most one

TheoremThe CDF errors are bounded above#✓fully proved

Let \(\mu\) be a measure on \(\mathbb{R}\), let \(n\) be a positive integer, let \(F\) be the cumulative distribution function of the normalized law of \(\mu\) at \(n\), and let \(\Phi\) be the standard normal cumulative distribution function. Then the set \(\{|F(x) - \Phi(x)| : x \in \mathbb{R}\}\) is bounded above.

theorem errorRange_bddAbove (μ : Measure ℝ) (n : ℕ+) :
    BddAbove (Set.range (fun x : ℝ ↦ |cdf (normalizedLaw μ n) x - normalCDF x|))
Uses 3 · Used by 1
Statement usesStandard normal CDF · Law of the normalized sum
Proof usesThe CDF error is at most one
Used byEach CDF error is at most the Kolmogorov error

TheoremEach CDF error is at most the Kolmogorov error#✓fully proved

Let \(\mu\) be a measure on \(\mathbb{R}\), \(n\) a positive integer, \(F_{\mu,n}\) the distribution function of the normalized law of \(\mu\) at \(n\) and \(\Phi\) the standard normal distribution function. Then for every real \(x\), \(|F_{\mu,n}(x) - \Phi(x)| \le \sup_{y \in \mathbb{R}} |F_{\mu,n}(y) - \Phi(y)|\), the right side being the Kolmogorov error of \(\mu\) at \(n\).

theorem pointwise_le_kolmogorovError (μ : Measure ℝ) (n : ℕ+) (x : ℝ) :
    |cdf (normalizedLaw μ n) x - normalCDF x| ≤ kolmogorovError μ n
Uses 4 · Used by 3
Statement usesKolmogorov error · Standard normal CDF · Law of the normalized sum
Proof usesThe CDF errors are bounded above
Used byKolmogorov error bounds are uniform CDF bounds · The Kolmogorov error is nonnegative · Admissible coefficients bound every standardized i.i.d. sequence

TheoremThe Kolmogorov error is nonnegative#✓fully proved

For every measure \(\mu\) on \(\mathbb{R}\) and every positive integer \(n\), the Kolmogorov error of \(\mu\) at \(n\), that is \(\sup_{x \in \mathbb{R}} |F_{\mu,n}(x) - \Phi(x)|\) where \(F_{\mu,n}\) is Mathlib's cumulative distribution function of the normalized law of \(\mu\) at \(n\) and \(\Phi\) is the standard normal cumulative distribution function, is nonnegative.

Here \(F_{\mu,n}(x)\) is the mass the normalized law gives to \((-\infty, x]\) when \(\mu\) is a probability measure; otherwise the normalized law is the zero measure and \(F_{\mu,n}\) is a fixed but unspecified cumulative distribution function of some probability measure.

theorem kolmogorovError_nonnegative (μ : Measure ℝ) (n : ℕ+) :
    0 ≤ kolmogorovError μ n
Uses 4 · Used by 1
Statement usesKolmogorov error
Proof usesStandard normal CDF · Law of the normalized sum · Each CDF error is at most the Kolmogorov error
Used byBernoulli-admissible coefficients are nonnegative

TheoremThe Kolmogorov error is at most one#✓fully proved

For every measure \(\mu\) on \(\mathbb{R}\) and every positive integer \(n\), the Kolmogorov error of \(\mu\) at \(n\), that is \(\sup_{x \in \mathbb{R}} |F_{\mu,n}(x) - \Phi(x)|\) where \(F_{\mu,n}\) is Mathlib's cumulative distribution function of the normalized law of \(\mu\) at \(n\) and \(\Phi\) is the standard normal cumulative distribution function, is at most \(1\).

Here \(F_{\mu,n}(x)\) is the mass the normalized law gives to \((-\infty, x]\) when \(\mu\) is a probability measure; otherwise the normalized law is the zero measure and \(F_{\mu,n}\) is a fixed but unspecified cumulative distribution function of some probability measure.

theorem kolmogorovError_le_one (μ : Measure ℝ) (n : ℕ+) :
    kolmogorovError μ n ≤ 1
Uses 4
Statement usesKolmogorov error
Proof usesStandard normal CDF · Law of the normalized sum · The CDF error is at most one

TheoremKolmogorov error bounds are uniform CDF bounds#✓fully proved

Let \(\mu\) be a measure on \(\mathbb{R}\), let \(n\) be a positive integer, let \(F\) be the cumulative distribution function of the normalized law of \(\mu\) at \(n\), and let \(\Phi\) be the standard normal cumulative distribution function. Then for every real \(a\), the Kolmogorov error of \(\mu\) at \(n\) is at most \(a\) if and only if \(|F(x) - \Phi(x)| \le a\) for every real \(x\).

theorem error_le_iff (μ : Measure ℝ) (n : ℕ+) (a : ℝ) :
    kolmogorovError μ n ≤ a ↔ ∀ x : ℝ, |cdf (normalizedLaw μ n) x - normalCDF x| ≤ a
Uses 4 · Used by 1
Statement usesKolmogorov error · Standard normal CDF · Law of the normalized sum
Proof usesEach CDF error is at most the Kolmogorov error
Used byThe Berry–Esseen bound with coefficient 42

TheoremThe standard Gaussian is a standardized law#✓fully proved

The standard normal law \(N(0,1)\) on \(\mathbb{R}\) is a standardized law: it is a probability measure with mean \(0\), variance \(1\) and finite third absolute moment.

theorem standardGaussian_isStandardized : IsStandardizedLaw (gaussianReal 0 1)
Uses 1 · Used by 2
Statement usesStandardized laws with finite third moment
Used byThe Kolmogorov error vanishes for one standard Gaussian summand · Admissible coefficients are nonnegative

TheoremThe normalized law with one summand#✓fully proved

For every standardized law \(\mu\) on \(\mathbb{R}\) (a probability measure with mean \(0\), variance \(1\) and finite third absolute moment), the normalized law of \(\mu\) at \(n = 1\) is \(\mu\) itself.

theorem normalizedLaw_one {μ : Measure ℝ} (hμ : IsStandardizedLaw μ) :
    normalizedLaw μ ⟨1, by decide⟩ = μ
Uses 5 · Used by 1
Statement usesStandardized laws with finite third moment · Law of the normalized sum
Proof usesI.i.d. product law · Coordinate laws of the i.i.d. product · Normalized sum
Used byThe Kolmogorov error vanishes for one standard Gaussian summand

TheoremThe Kolmogorov error vanishes for one standard Gaussian summand#✓fully proved

Let \(F\) be the distribution function of the normalized law of the standard normal law \(N(0,1)\) at \(n = 1\), and \(\Phi\) the standard normal distribution function. Then the Kolmogorov error of \(N(0,1)\) at \(n = 1\), \(\sup_{x \in \mathbb{R}} |F(x) - \Phi(x)|\), equals \(0\).

theorem standardGaussian_error_one : kolmogorovError (gaussianReal 0 1) ⟨1, by decide⟩ = 0
Uses 5 · Used by 1
Statement usesKolmogorov error
Proof usesStandard normal CDF · Law of the normalized sum · The normalized law with one summand · The standard Gaussian is a standardized law
Used byAdmissible coefficients are nonnegative

StructureStandardized i.i.d. models#✓fully proved

Let \(\Omega\) be a measurable space with a measure \(P\), and let \((X_i)_{i \in \mathbb{N}}\) be real-valued functions on \(\Omega\). They form a standardized i.i.d. model when \(P\) is a probability measure, every \(X_i\) is measurable, the \(X_i\) are mutually independent under \(P\), every \(X_i\) has the same law under \(P\) as \(X_0\), and \(X_0\) has mean \(\int_\Omega X_0 \, dP = 0\), variance \(1\) and finite third absolute moment \(\int_\Omega |X_0|^3 \, dP < \infty\).

structure IsIIDModel {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (X : ℕ → Ω → ℝ) : Prop where
  probability : IsProbabilityMeasure P
  measurable : ∀ i, Measurable (X i)
  independent : iIndepFun X P
  identical : ∀ i, IdentDistrib (X i) (X 0) P P
  mean_zero : (∫ ω, X 0 ω ∂P) = 0
  variance_one : variance (X 0) P = 1
  third_moment : MemLp (X 0) 3 P
Used by 5
Used byThe joint law of a standardized i.i.d. model · Normalized sums of an i.i.d. model have the canonical law · The common law of an i.i.d. model is standardized · Third absolute moment of the common law · Admissible coefficients bound every standardized i.i.d. sequence

TheoremThe common law of an i.i.d. model is standardized#✓fully proved

Let \(P\) be a measure on a measurable space \(\Omega\) and \(X_0, X_1, \dots\) real-valued functions on \(\Omega\) forming an i.i.d. model: \(P\) is a probability measure, the \(X_i\) are measurable, independent and identically distributed, and \(X_0\) has mean \(0\), variance \(1\) and finite third absolute moment. Then the law of \(X_0\), the pushforward of \(P\) under \(X_0\), is a standardized law.

theorem IsIIDModel.standardizedLaw {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
    {X : ℕ → Ω → ℝ} (h : IsIIDModel P X) : IsStandardizedLaw (P.map (X 0))
Uses 2 · Used by 1
Statement usesStandardized i.i.d. models · Standardized laws with finite third moment
Used byAdmissible coefficients bound every standardized i.i.d. sequence

TheoremThe joint law of a standardized i.i.d. model#✓fully proved

If \((X_i)_{i \in \mathbb{N}}\) is a standardized i.i.d. model on a measurable space \(\Omega\) with measure \(P\), then the law under \(P\) of the sequence map \(\omega \mapsto (X_i(\omega))_{i \in \mathbb{N}}\) from \(\Omega\) to \(\mathbb{R}^{\mathbb{N}}\) equals the i.i.d. product law of the law of \(X_0\) under \(P\).

theorem IsIIDModel.jointLaw {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
    {X : ℕ → Ω → ℝ} (h : IsIIDModel P X) :
    P.map (fun ω i ↦ X i ω) = iidLaw (P.map (X 0))
Uses 2 · Used by 1
Statement usesStandardized i.i.d. models · I.i.d. product law
Used byNormalized sums of an i.i.d. model have the canonical law

TheoremNormalized sums of an i.i.d. model have the canonical law#✓fully proved

Let \(P\) be a probability measure on a measurable space \(\Omega\) and let \(X_0, X_1, \dots\) be real random variables on \(\Omega\) that are measurable, independent and identically distributed under \(P\), with \(X_0\) of mean \(0\), variance \(1\) and finite third absolute moment. Then for every positive integer \(n\), the law under \(P\) of \((X_0 + \dots + X_{n-1})/\sqrt{n}\) equals the normalized law at \(n\) of the law of \(X_0\).

theorem IsIIDModel.normalizedLaw_eq {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
    {X : ℕ → Ω → ℝ} (h : IsIIDModel P X) (n : ℕ+) :
    P.map (fun ω ↦ (∑ i ∈ Finset.range n.1, X i ω) / Real.sqrt (n.1 : ℝ)) =
      normalizedLaw (P.map (X 0)) n
Uses 6 · Used by 1
Statement usesStandardized i.i.d. models · Law of the normalized sum
Proof usesThe joint law of a standardized i.i.d. model · I.i.d. product law · Normalized sum · Measurability of the normalized sum
Used byAdmissible coefficients bound every standardized i.i.d. sequence

TheoremThird absolute moment of the common law#✓fully proved

Let \(P\) be a measure on a measurable space \(\Omega\) and \(X_0, X_1, \dots\) real-valued functions on \(\Omega\) forming an i.i.d. model: \(P\) is a probability measure, the \(X_i\) are measurable, independent and identically distributed, and \(X_0\) has mean \(0\), variance \(1\) and finite third absolute moment. Then the third absolute moment of the law of \(X_0\) equals \(\int_\Omega |X_0(\omega)|^3 \, dP(\omega)\).

theorem IsIIDModel.thirdMoment_eq {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
    {X : ℕ → Ω → ℝ} (h : IsIIDModel P X) :
    thirdMoment (P.map (X 0)) = ∫ ω, |X 0 ω| ^ 3 ∂P
Uses 2 · Used by 1
Statement usesStandardized i.i.d. models · Third absolute moment
Used byAdmissible coefficients bound every standardized i.i.d. sequence
35 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.