Optimal Berry–Esseen constant

DefinitionAdmissible Berry–Esseen coefficient#✓fully proved

A real number \(C\) is an admissible Berry–Esseen coefficient when, for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment \(\rho = \int |x|^3 \, d\mu(x)\), and every positive integer \(n\), the Kolmogorov error \(\sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)|\) is at most \(C \rho / \sqrt{n}\). Here \(F_n\) is the distribution function of \((X_1 + \dots + X_n)/\sqrt{n}\) for independent random variables \(X_1, X_2, \dots\) with law \(\mu\), and \(\Phi\) is the standard normal distribution function.

def IsAdmissible (C : ℝ) : Prop :=
  ∀ μ : Measure ℝ, IsStandardizedLaw μ → ∀ n : ℕ+,
    kolmogorovError μ n ≤ C * thirdMoment μ / Real.sqrt (n.1 : ℝ)
Uses 3 · Used by 13
Statement usesStandardized laws with finite third moment · Kolmogorov error · Third absolute moment
Used byThe admissible Berry–Esseen coefficients are bounded below · Admissible Berry–Esseen coefficients exist · Admissible coefficients bound every standardized i.i.d. sequence · The Berry–Esseen bound with coefficient 42 · Admissible coefficients are exactly those above the optimal one · Admissibility is upward closed · Admissible coefficients are nonnegative · The optimal Berry–Esseen constant · The optimal Berry–Esseen coefficient satisfies the Berry–Esseen bound · The optimal Berry–Esseen coefficient is admissible · The Berry–Esseen constant is the least admissible coefficient · The optimal Berry–Esseen coefficient is at most every admissible one · The optimal Berry–Esseen coefficient is nonnegative

DefinitionThe optimal Berry–Esseen constant#✓fully proved

Call a real number \(C\) admissible if for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment \(\rho = \int |x|^3 \, d\mu\), and every positive integer \(n\),

\[\sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)| \le \frac{C \rho}{\sqrt{n}},\]

where \(F_n\) is the distribution function of \((X_1 + \dots + X_n)/\sqrt{n}\) for independent random variables \(X_1, X_2, \dots\) with law \(\mu\), and \(\Phi\) is the standard normal distribution function. The optimal Berry–Esseen constant is the infimum of the admissible \(C\).

The set of admissible constants is nonempty (it contains \(42\)) and bounded below by \(0\), so this is a genuine real infimum.

noncomputable def value : ℝ := sInf {C : ℝ | IsAdmissible C}
Uses 1 · Used by 19
Statement usesAdmissible Berry–Esseen coefficient
Used byThe Bernoulli Berry–Esseen constant is at most the general one · Statement of Esseen's lower bound for the Berry–Esseen constant · Admissible coefficients are exactly those above the optimal one · Statement of the Korolev–Shevtsova upper bound · Statement of Lin's 2026 Berry–Esseen bound · Statement of Shevtsova's 2006 Berry–Esseen bound · Statement of Shevtsova's 2011 Berry–Esseen bound · Statement of Shevtsova's 2013 Berry–Esseen bound · Statement of Shiganov's Berry–Esseen bound · Statement of Tyurin's Berry–Esseen bound · The optimal Berry–Esseen coefficient satisfies the Berry–Esseen bound · The optimal Berry–Esseen coefficient is admissible · The Berry–Esseen constant is the least admissible coefficient · The optimal Berry–Esseen coefficient is at most 42 · The optimal Berry–Esseen coefficient is at most every admissible one · The optimal Berry–Esseen coefficient is nonnegative · Statement of van Beek's Berry–Esseen bound · Statement of the unverified Berry–Esseen bound 0.4395 · Statement of Zolotarev's Berry–Esseen bound

DefinitionEsseen's lower-bound constant#✓fully proved

Esseen's constant is the real number \((\sqrt{10} + 3)/(6\sqrt{2\pi})\).

Esseen showed that the Berry–Esseen constant for i.i.d. sums is at least this number; the definition records the value only, not that lower bound.

noncomputable def esseenConstant : ℝ :=
  (Real.sqrt 10 + 3) / (6 * Real.sqrt (2 * Real.pi))
Used by 4
Used byStatement of Esseen's asymptotic lower bound for a two-point law · Esseen's lower-bound constant is positive · Statement of Esseen's lower bound for the Berry–Esseen constant · Statement of Schulz's Bernoulli Berry–Esseen optimum

TheoremEsseen's lower-bound constant is positive#✓fully proved

The number \((\sqrt{10} + 3)/(6\sqrt{2\pi})\) is positive.

theorem esseenConstant_positive : 0 < esseenConstant
Uses 1
Statement usesEsseen's lower-bound constant

TheoremAdmissible coefficients are nonnegative#✓fully proved

Every admissible Berry–Esseen coefficient \(C \in \mathbb{R}\) satisfies \(C \ge 0\).

theorem isAdmissible_nonnegative {C : ℝ} (hC : IsAdmissible C) : 0 ≤ C
Uses 6 · Used by 2
Statement usesAdmissible Berry–Esseen coefficient
Proof usesKolmogorov error · The Kolmogorov error vanishes for one standard Gaussian summand · The standard Gaussian is a standardized law · Third absolute moment · The third absolute moment of a standardized law is positive
Used byThe admissible Berry–Esseen coefficients are bounded below · The optimal Berry–Esseen coefficient is nonnegative

TheoremThe Berry–Esseen bound with coefficient 42#✓fully proved

The number \(42\) is an admissible Berry–Esseen coefficient: for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment \(\rho = \int |x|^3 \, d\mu(x)\), and every positive integer \(n\), the Kolmogorov error \(\sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)|\) is at most \(42 \rho / \sqrt{n}\), where \(F_n\) is the distribution function of \((X_1 + \dots + X_n)/\sqrt{n}\) for independent random variables \(X_1, X_2, \dots\) with law \(\mu\), and \(\Phi\) is the standard normal distribution function.

theorem isAdmissible_fortyTwo : IsAdmissible 42
Uses 13 · Used by 3
Statement usesAdmissible Berry–Esseen coefficient
Proof usesStandardized laws with finite third moment · Kolmogorov error bounds are uniform CDF bounds · I.i.d. product law · Coordinates of the i.i.d. product are distributed like the original law · Coordinates of the i.i.d. product are independent · The i.i.d. product of a standardized law is a probability measure · Kolmogorov error · Standard normal CDF · Law of the normalized sum · The normalized law is a probability measure · Third absolute moment · Berry–Esseen theorem with constant 42
Used byAdmissible Berry–Esseen coefficients exist · Bernoulli-admissible coefficients exist · The optimal Berry–Esseen coefficient is at most 42

TheoremAdmissible Berry–Esseen coefficients exist#✓fully proved

The set of real numbers \(C\) that are admissible Berry–Esseen coefficients (common Berry–Esseen coefficients for all standardized laws and all positive sample sizes) is nonempty.

theorem admissible_nonempty : ({C : ℝ | IsAdmissible C} : Set ℝ).Nonempty
Uses 2 · Used by 2
Statement usesAdmissible Berry–Esseen coefficient
Proof usesThe Berry–Esseen bound with coefficient 42
Used byThe optimal Berry–Esseen coefficient satisfies the Berry–Esseen bound · The optimal Berry–Esseen coefficient is nonnegative

TheoremThe admissible Berry–Esseen coefficients are bounded below#✓fully proved

The set of real numbers \(C\) that are admissible Berry–Esseen coefficients (common Berry–Esseen coefficients for all standardized laws and all positive sample sizes) is bounded below.

theorem admissible_bddBelow : BddBelow {C : ℝ | IsAdmissible C}
Uses 2 · Used by 1
Statement usesAdmissible Berry–Esseen coefficient
Proof usesAdmissible coefficients are nonnegative
Used byThe optimal Berry–Esseen coefficient is at most every admissible one

TheoremThe optimal Berry–Esseen coefficient is nonnegative#✓fully proved

The infimum \(C^*\) of all admissible Berry–Esseen coefficients satisfies \(0 \le C^*\).

theorem value_nonnegative : 0 ≤ value
Uses 4
Statement usesThe optimal Berry–Esseen constant
Proof usesAdmissible Berry–Esseen coefficient · Admissible Berry–Esseen coefficients exist · Admissible coefficients are nonnegative

TheoremThe optimal Berry–Esseen coefficient is at most every admissible one#✓fully proved

If \(C\) is an admissible Berry–Esseen coefficient, then the infimum \(C^*\) of all admissible coefficients satisfies \(C^* \le C\).

theorem value_le_of_isAdmissible {C : ℝ} (hC : IsAdmissible C) : value ≤ C
Uses 3 · Used by 3
Statement usesAdmissible Berry–Esseen coefficient · The optimal Berry–Esseen constant
Proof usesThe admissible Berry–Esseen coefficients are bounded below
Used byAdmissible coefficients are exactly those above the optimal one · The Berry–Esseen constant is the least admissible coefficient · The optimal Berry–Esseen coefficient is at most 42

TheoremThe optimal Berry–Esseen coefficient is at most 42#✓fully proved

The infimum \(C^*\) of all admissible Berry–Esseen coefficients satisfies \(C^* \le 42\).

theorem value_le_fortyTwo : value ≤ 42
Uses 3
Statement usesThe optimal Berry–Esseen constant
Proof usesThe Berry–Esseen bound with coefficient 42 · The optimal Berry–Esseen coefficient is at most every admissible one

TheoremAdmissibility is upward closed#✓fully proved

If \(C \le D\) are real numbers and \(C\) is an admissible Berry–Esseen coefficient, then \(D\) is an admissible Berry–Esseen coefficient.

theorem isAdmissible_mono {C D : ℝ} (hC : IsAdmissible C) (hCD : C ≤ D) :
    IsAdmissible D
Uses 5 · Used by 1
Statement usesAdmissible Berry–Esseen coefficient
Proof usesStandardized laws with finite third moment · Kolmogorov error · Third absolute moment · Nonnegativity of the third absolute moment
Used byAdmissible coefficients are exactly those above the optimal one

TheoremThe optimal Berry–Esseen coefficient satisfies the Berry–Esseen bound#✓fully proved

Let \(C^*\) be the infimum of all admissible Berry–Esseen coefficients. For every standardized law \(\mu\) on \(\mathbb{R}\) and every positive integer \(n\), the Kolmogorov error of \(\mu\) at sample size \(n\) is at most \(C^* \rho(\mu) / \sqrt{n}\), where \(\rho(\mu) = \int |x|^3 \, d\mu(x)\) is the third absolute moment of \(\mu\).

theorem value_bound (μ : Measure ℝ) (hμ : IsStandardizedLaw μ) (n : ℕ+) :
    kolmogorovError μ n ≤ value * thirdMoment μ / Real.sqrt (n.1 : ℝ)
Uses 7 · Used by 1
Statement usesThe optimal Berry–Esseen constant · Standardized laws with finite third moment · Kolmogorov error · Third absolute moment
Proof usesAdmissible Berry–Esseen coefficient · Admissible Berry–Esseen coefficients exist · The third absolute moment of a standardized law is positive
Used byThe optimal Berry–Esseen coefficient is admissible

TheoremThe optimal Berry–Esseen coefficient is admissible#✓fully proved

The infimum \(C^*\) of all admissible Berry–Esseen coefficients is itself an admissible coefficient.

theorem value_isAdmissible : IsAdmissible value
Uses 3 · Used by 3
Statement usesAdmissible Berry–Esseen coefficient · The optimal Berry–Esseen constant
Proof usesThe optimal Berry–Esseen coefficient satisfies the Berry–Esseen bound
Used byThe Bernoulli Berry–Esseen constant is at most the general one · Admissible coefficients are exactly those above the optimal one · The Berry–Esseen constant is the least admissible coefficient

TheoremThe Berry–Esseen constant is the least admissible coefficient#✓fully proved

The infimum \(C^*\) of all admissible Berry–Esseen coefficients is the least element of the set of admissible coefficients: \(C^*\) is admissible, and \(C^* \le C\) for every admissible coefficient \(C\).

theorem value_isLeast : IsLeast {C : ℝ | IsAdmissible C} value
Uses 4
Statement usesAdmissible Berry–Esseen coefficient · The optimal Berry–Esseen constant
Proof usesThe optimal Berry–Esseen coefficient is admissible · The optimal Berry–Esseen coefficient is at most every admissible one

TheoremAdmissible coefficients are exactly those above the optimal one#✓fully proved

A real number \(C\) is an admissible Berry–Esseen coefficient if and only if \(C_0 \le C\), where \(C_0\) is the optimal Berry–Esseen coefficient, the infimum of the set of admissible coefficients.

theorem isAdmissible_iff_value_le (C : ℝ) : IsAdmissible C ↔ value ≤ C
Uses 5
Statement usesAdmissible Berry–Esseen coefficient · The optimal Berry–Esseen constant
Proof usesAdmissibility is upward closed · The optimal Berry–Esseen coefficient is admissible · The optimal Berry–Esseen coefficient is at most every admissible one

TheoremAdmissible coefficients bound every standardized i.i.d. sequence#✓fully proved

Let \(C\) be an admissible Berry–Esseen coefficient. Let \(X_0, X_1, X_2, \dots\) be measurable real random variables on a probability space \((\Omega, P)\) that are independent and identically distributed, with \(\mathbb{E}[X_0] = 0\), \(\operatorname{Var}(X_0) = 1\) and \(\mathbb{E}|X_0|^3 < \infty\). Then for every positive integer \(n\) and every real \(x\),

\[ \left| P\left( \frac{X_0 + \dots + X_{n-1}}{\sqrt{n}} \le x \right) - \Phi(x) \right| \le \frac{C \, \mathbb{E}|X_0|^3}{\sqrt{n}}, \]

where \(\Phi\) is the distribution function of the standard normal law.

theorem iid_bound {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} {X : ℕ → Ω → ℝ}
    {C : ℝ} (hC : IsAdmissible C) (h : IsIIDModel P X) (n : ℕ+) (x : ℝ) :
    |cdf (P.map (fun ω ↦ (∑ i ∈ Finset.range n.1, X i ω) /
        Real.sqrt (n.1 : ℝ))) x - normalCDF x| ≤
      C * (∫ ω, |X 0 ω| ^ 3 ∂P) / Real.sqrt (n.1 : ℝ)
Uses 10
Statement usesAdmissible Berry–Esseen coefficient · Standardized i.i.d. models · Standard normal CDF
Proof usesNormalized 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 · Kolmogorov error · Law of the normalized sum · Each CDF error is at most the Kolmogorov error · Third absolute moment

DefinitionStandardized two-point law#✓fully proved

A measure \(\mu\) on \(\mathbb{R}\) is a standardized two-point law when it is a probability measure with mean \(0\), variance \(1\) and finite third absolute moment, and there are real numbers \(a \ne b\) with \(\mu(\mathbb{R} \setminus \{a, b\}) = 0\).

def IsBernoulliLaw (μ : Measure ℝ) : Prop :=
  IsStandardizedLaw μ ∧ ∃ a b : ℝ, a ≠ b ∧ μ ({a, b}ᶜ) = 0
Uses 1 · Used by 5
Statement usesStandardized laws with finite third moment
Used byBernoulli-admissible coefficients exist · The Bernoulli Berry–Esseen constant is at most the general one · Statement of Esseen's asymptotic lower bound for a two-point law · Admissible Berry–Esseen coefficient for two-point laws · The symmetric Bernoulli law is a standardized two-point law

DefinitionSymmetric Bernoulli law#✓fully proved

The symmetric Bernoulli law is the measure \(\frac12 \delta_{-1} + \frac12 \delta_1\) on \(\mathbb{R}\), where \(\delta_a\) denotes the Dirac mass at \(a\); it puts mass \(1/2\) at each of the points \(-1\) and \(1\).

noncomputable def symmetricBernoulliLaw : Measure ℝ :=
  ((1 / 2 : ℝ≥0) : ENNReal) • Measure.dirac (-1) +
    ((1 / 2 : ℝ≥0) : ENNReal) • Measure.dirac 1
Used by 6
Used byBernoulli-admissible coefficients are nonnegative · Integrals against the symmetric Bernoulli law · The symmetric Bernoulli law is a standardized two-point law · The symmetric Bernoulli law is standardized · The symmetric Bernoulli law has moments of all orders · Third absolute moment of the symmetric Bernoulli law

TheoremThe symmetric Bernoulli law has moments of all orders#✓fully proved

For every exponent \(p \in [0, \infty]\), the identity function of \(\mathbb{R}\) belongs to \(L^p\) of the symmetric Bernoulli law.

theorem symmetricBernoulli_memLp (p : ENNReal) : MemLp id p symmetricBernoulliLaw
Uses 1 · Used by 1
Statement usesSymmetric Bernoulli law
Used byThe symmetric Bernoulli law is standardized

TheoremIntegrals against the symmetric Bernoulli law#✓fully proved

For every function \(f : \mathbb{R} \to \mathbb{R}\), the integral of \(f\) against the symmetric Bernoulli law \(\frac12 \delta_{-1} + \frac12 \delta_1\) equals \(\frac12 f(-1) + \frac12 f(1)\).

theorem symmetricBernoulli_integral (f : ℝ → ℝ) :
    (∫ x, f x ∂symmetricBernoulliLaw) = (1 / 2) * f (-1) + (1 / 2) * f 1
Uses 1 · Used by 2
Statement usesSymmetric Bernoulli law
Used byThe symmetric Bernoulli law is standardized · Third absolute moment of the symmetric Bernoulli law

TheoremThe symmetric Bernoulli law is standardized#✓fully proved

The symmetric Bernoulli law, which puts mass \(1/2\) at each of the points \(-1\) and \(1\), is a standardized law: it is a probability measure on \(\mathbb{R}\) with mean \(0\) and variance \(1\), and it has a finite third absolute moment.

theorem symmetricBernoulli_isStandardized : IsStandardizedLaw symmetricBernoulliLaw
Uses 4 · Used by 1
Statement usesSymmetric Bernoulli law · Standardized laws with finite third moment
Proof usesIntegrals against the symmetric Bernoulli law · The symmetric Bernoulli law has moments of all orders
Used byThe symmetric Bernoulli law is a standardized two-point law

TheoremThe symmetric Bernoulli law is a standardized two-point law#✓fully proved

The law \(\frac12 \delta_{-1} + \frac12 \delta_1\) on \(\mathbb{R}\) is a probability measure with mean \(0\), variance \(1\) and finite third absolute moment, and it is concentrated on the two distinct points \(-1\) and \(1\).

theorem symmetricBernoulli_isBernoulli : IsBernoulliLaw symmetricBernoulliLaw
Uses 4 · Used by 1
Statement usesStandardized two-point law · Symmetric Bernoulli law
Proof usesThe symmetric Bernoulli law is standardized · Standardized laws with finite third moment
Used byBernoulli-admissible coefficients are nonnegative

TheoremThird absolute moment of the symmetric Bernoulli law#✓fully proved

The third absolute moment \(\int |x|^3 \, d\mu(x)\) of the symmetric Bernoulli law \(\mu\) equals \(1\).

theorem symmetricBernoulli_thirdMoment : thirdMoment symmetricBernoulliLaw = 1
Uses 3 · Used by 1
Statement usesSymmetric Bernoulli law · Third absolute moment
Proof usesIntegrals against the symmetric Bernoulli law
Used byBernoulli-admissible coefficients are nonnegative

DefinitionAdmissible Berry–Esseen coefficient for two-point laws#✓fully proved

A real number \(C\) is an admissible Berry–Esseen coefficient for standardized two-point laws when, for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment \(\rho = \int |x|^3 \, d\mu(x)\) that is concentrated on two distinct points, and every positive integer \(n\), the Kolmogorov error \(\sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)|\) is at most \(C \rho / \sqrt{n}\). Here \(F_n\) is the distribution function of \((X_1 + \dots + X_n)/\sqrt{n}\) for independent random variables \(X_1, X_2, \dots\) with law \(\mu\), and \(\Phi\) is the standard normal distribution function.

def IsBernoulliAdmissible (C : ℝ) : Prop :=
  ∀ μ : Measure ℝ, IsBernoulliLaw μ → ∀ n : ℕ+,
    kolmogorovError μ n ≤ C * thirdMoment μ / Real.sqrt (n.1 : ℝ)
Uses 3 · Used by 6
Statement usesStandardized two-point law · Kolmogorov error · Third absolute moment
Used byThe Bernoulli-admissible coefficients are bounded below · Bernoulli-admissible coefficients exist · Bernoulli Berry–Esseen constant · The Bernoulli Berry–Esseen constant is at most the general one · The Bernoulli Berry–Esseen constant is nonnegative · Bernoulli-admissible coefficients are nonnegative

DefinitionBernoulli Berry–Esseen constant#✓fully proved

The Bernoulli Berry–Esseen constant is the infimum, in \(\mathbb{R}\), of the set of real numbers \(C\) that are admissible Berry–Esseen coefficients for the Bernoulli subclass: for every standardized law \(\mu\) (a probability measure on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment) concentrated on two distinct points, and every positive integer \(n\), the supremum over \(x \in \mathbb{R}\) of the distance between the distribution function of \((X_0 + \dots + X_{n-1})/\sqrt{n}\) at \(x\), for independent \(\mu\)-distributed \(X_0, \dots, X_{n-1}\), and the standard normal distribution function at \(x\) is at most \(C \rho(\mu) / \sqrt{n}\), where \(\rho(\mu) = \int |x|^3 \, d\mu(x)\).

noncomputable def bernoulliValue : ℝ := sInf {C : ℝ | IsBernoulliAdmissible C}
Uses 1 · Used by 3
Statement usesAdmissible Berry–Esseen coefficient for two-point laws
Used byThe Bernoulli Berry–Esseen constant is at most the general one · The Bernoulli Berry–Esseen constant is nonnegative · Statement of Schulz's Bernoulli Berry–Esseen optimum

TheoremBernoulli-admissible coefficients are nonnegative#✓fully proved

Every real number \(C\) that is an admissible Berry–Esseen coefficient for standardized two-point laws satisfies \(C \ge 0\).

The class of standardized two-point laws is nonempty: it contains the law with mass \(1/2\) at each of \(-1\) and \(1\).

theorem isBernoulliAdmissible_nonnegative {C : ℝ} (hC : IsBernoulliAdmissible C) :
    0 ≤ C
Uses 7 · Used by 2
Statement usesAdmissible Berry–Esseen coefficient for two-point laws
Proof usesSymmetric Bernoulli law · The symmetric Bernoulli law is a standardized two-point law · Third absolute moment of the symmetric Bernoulli law · Kolmogorov error · The Kolmogorov error is nonnegative · Third absolute moment
Used byThe Bernoulli-admissible coefficients are bounded below · The Bernoulli Berry–Esseen constant is nonnegative

TheoremBernoulli-admissible coefficients exist#✓fully proved

The set of real numbers \(C\) that are admissible Berry–Esseen coefficients for the Bernoulli subclass (common Berry–Esseen coefficients for all standardized laws concentrated on two points and all positive sample sizes) is nonempty.

The coefficient \(42\), admissible for all standardized laws, is one such coefficient.

theorem bernoulliAdmissible_nonempty : ({C : ℝ | IsBernoulliAdmissible C} : Set ℝ).Nonempty
Uses 4 · Used by 1
Statement usesAdmissible Berry–Esseen coefficient for two-point laws
Proof usesStandardized two-point law · The Berry–Esseen bound with coefficient 42 · Standardized laws with finite third moment
Used byThe Bernoulli Berry–Esseen constant is nonnegative

TheoremThe Bernoulli-admissible coefficients are bounded below#✓fully proved

The set of real numbers \(C\) that are admissible Berry–Esseen coefficients for the Bernoulli subclass (common Berry–Esseen coefficients for all standardized laws concentrated on two points and all positive sample sizes) is bounded below.

theorem bernoulliAdmissible_bddBelow : BddBelow {C : ℝ | IsBernoulliAdmissible C}
Uses 2 · Used by 1
Statement usesAdmissible Berry–Esseen coefficient for two-point laws
Proof usesBernoulli-admissible coefficients are nonnegative
Used byThe Bernoulli Berry–Esseen constant is at most the general one

TheoremThe Bernoulli Berry–Esseen constant is nonnegative#✓fully proved

The infimum of the real numbers that are admissible Berry–Esseen coefficients for the Bernoulli subclass is nonnegative.

theorem bernoulliValue_nonnegative : 0 ≤ bernoulliValue
Uses 4
Statement usesBernoulli Berry–Esseen constant
Proof usesAdmissible Berry–Esseen coefficient for two-point laws · Bernoulli-admissible coefficients exist · Bernoulli-admissible coefficients are nonnegative

TheoremThe Bernoulli Berry–Esseen constant is at most the general one#✓fully proved

The infimum of the real numbers that are admissible Berry–Esseen coefficients for the Bernoulli subclass is at most the infimum of the real numbers that are admissible Berry–Esseen coefficients for all standardized laws.

theorem bernoulliValue_le_value : bernoulliValue ≤ value
Uses 7
Statement usesBernoulli Berry–Esseen constant · The optimal Berry–Esseen constant
Proof usesAdmissible Berry–Esseen coefficient for two-point laws · Standardized two-point law · The Bernoulli-admissible coefficients are bounded below · The optimal Berry–Esseen coefficient is admissible · Standardized laws with finite third moment

DefinitionStatement of Zolotarev's Berry–Esseen bound#✓fully proved

The proposition that the Berry–Esseen constant \(C_0\) is at most \(0.82\). Here \(C_0\) is the infimum of the real numbers \(C\) such that for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment \(\beta_3 = \int |x|^3 \, d\mu(x)\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), where \(X_1, \dots, X_n\) are independent with law \(\mu\), satisfies \(\sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)| \le C \beta_3 / \sqrt{n}\); here \(\Phi\) is the standard normal distribution function.

def zolotarev1967UpperBound : Prop := value ≤ (82 / 100 : ℝ)
Sources
  • catalogue C19a, upper row Z1967; the non-i.i.d. 0.9051 is context only.
Uses 1 · Used by 1
Statement usesThe optimal Berry–Esseen constant
Used byZolotarev's upper bound for the Berry–Esseen constant

DefinitionStatement of van Beek's Berry–Esseen bound#✓fully proved

The proposition that the Berry–Esseen constant \(C_0\) is at most \(0.7975\). Here \(C_0\) is the infimum of the real numbers \(C\) such that for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment \(\beta_3 = \int |x|^3 \, d\mu(x)\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), where \(X_1, \dots, X_n\) are independent with law \(\mu\), satisfies \(\sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)| \le C \beta_3 / \sqrt{n}\); here \(\Phi\) is the standard normal distribution function.

def vanBeek1972UpperBound : Prop := value ≤ (7975 / 10000 : ℝ)
Sources
  • catalogue C19a, upper row vB1972; original primary text is not retained here.
Uses 1 · Used by 1
Statement usesThe optimal Berry–Esseen constant
Used byVan Beek's upper bound for the Berry–Esseen constant

DefinitionStatement of Shiganov's Berry–Esseen bound#✓fully proved

The proposition that the Berry–Esseen constant \(C_0\) is at most \(0.7655\). Here \(C_0\) is the infimum of the real numbers \(C\) such that for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment \(\beta_3 = \int |x|^3 \, d\mu(x)\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), where \(X_1, \dots, X_n\) are independent with law \(\mu\), satisfies \(\sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)| \le C \beta_3 / \sqrt{n}\); here \(\Phi\) is the standard normal distribution function.

def shiganov1986UpperBound : Prop := value ≤ (7655 / 10000 : ℝ)
Sources
  • catalogue C19a, upper row Shi1986; retained Shevtsova2011 introduction reports it.
Uses 1 · Used by 1
Statement usesThe optimal Berry–Esseen constant
Used byShiganov's upper bound for the Berry–Esseen constant

DefinitionStatement of Shevtsova's 2006 Berry–Esseen bound#✓fully proved

Let \(C_0\) be the infimum of all real \(C\) such that for every real probability law \(\mu\) with mean \(0\), variance \(1\) and finite third absolute moment \(\rho = \int |x|^3\,d\mu\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), for independent \(X_1, \dots, X_n\) with law \(\mu\), satisfies \(\sup_x |F_n(x) - \Phi(x)| \le C \rho / \sqrt{n}\), where \(\Phi\) is the standard normal distribution function. This is the proposition \(C_0 \le 0.7056\).

def shevtsova2006UpperBound : Prop := value ≤ (7056 / 10000 : ℝ)
Sources
  • catalogue C19a, upper row She2006; retained Shevtsova2011 introduction reports it.
Uses 1 · Used by 1
Statement usesThe optimal Berry–Esseen constant
Used byShevtsova's 2006 Berry–Esseen bound

DefinitionStatement of the Korolev–Shevtsova upper bound#✓fully proved

For a probability measure \(\mu\) on \(\mathbb{R}\) and an integer \(n \ge 1\), let \(F_n\) be the distribution function of \((X_1 + \dots + X_n)/\sqrt{n}\) for independent random variables \(X_1, X_2, \dots\) each with law \(\mu\), let \(\Delta_n(\mu) = \sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)|\), where \(\Phi\) is the standard normal distribution function, and let \(\beta_3(\mu) = \int |x|^3 \, d\mu\). Let \(C_0\) be the optimal i.i.d. Berry–Esseen constant, the infimum of all real \(C\) such that \(\Delta_n(\mu) \le C \beta_3(\mu) / \sqrt{n}\) for every integer \(n \ge 1\) and every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment. This is the proposition that \(C_0 \le 0.5129\).

def korolevShevtsova2009UpperBound : Prop := value ≤ (5129 / 10000 : ℝ)
Sources
  • catalogue C19a, upper row KS2009; retained Shevtsova2011 lines 141-148.
Uses 1 · Used by 1
Statement usesThe optimal Berry–Esseen constant
Used byKorolev–Shevtsova upper bound for the Berry–Esseen constant

DefinitionStatement of Tyurin's Berry–Esseen bound#✓fully proved

The proposition that the Berry–Esseen constant \(C_0\) is at most \(0.4785\). Here \(C_0\) is the infimum of the real numbers \(C\) such that for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment \(\beta_3 = \int |x|^3 \, d\mu(x)\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), where \(X_1, \dots, X_n\) are independent with law \(\mu\), satisfies \(\sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)| \le C \beta_3 / \sqrt{n}\); here \(\Phi\) is the standard normal distribution function.

def tyurin2009UpperBound : Prop := value ≤ (4785 / 10000 : ℝ)
Sources
  • catalogue C19a, upper row Tyu2009; retained Shevtsova2011 lines 150-154.
Uses 1 · Used by 1
Statement usesThe optimal Berry–Esseen constant
Used byTyurin's upper bound for the Berry–Esseen constant

DefinitionStatement of Shevtsova's 2011 Berry–Esseen bound#✓fully proved

Let \(C_0\) be the infimum of all real \(C\) such that for every real probability law \(\mu\) with mean \(0\), variance \(1\) and finite third absolute moment \(\rho = \int |x|^3\,d\mu\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), for independent \(X_1, \dots, X_n\) with law \(\mu\), satisfies \(\sup_x |F_n(x) - \Phi(x)| \le C \rho / \sqrt{n}\), where \(\Phi\) is the standard normal distribution function. This is the proposition \(C_0 \le 0.4748\).

def shevtsova2011UpperBound : Prop := value ≤ (4748 / 10000 : ℝ)
Sources
  • catalogue C19a, upper row She2011; retained arXiv1111.6554 Corollary 1.
Uses 1 · Used by 1
Statement usesThe optimal Berry–Esseen constant
Used byShevtsova's 2011 Berry–Esseen bound

DefinitionStatement of Shevtsova's 2013 Berry–Esseen bound#✓fully proved

Let \(C_0\) be the infimum of all real \(C\) such that for every real probability law \(\mu\) with mean \(0\), variance \(1\) and finite third absolute moment \(\rho = \int |x|^3\,d\mu\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), for independent \(X_1, \dots, X_n\) with law \(\mu\), satisfies \(\sup_x |F_n(x) - \Phi(x)| \le C \rho / \sqrt{n}\), where \(\Phi\) is the standard normal distribution function. This is the proposition \(C_0 \le 0.4690\).

def shevtsova2013UpperBound : Prop := value ≤ (4690 / 10000 : ℝ)
Sources
  • catalogue C19a, upper row She2013. The original primary text and the correct structural formula remain unresolved; this is only the literal bound request.
Uses 1 · Used by 1
Statement usesThe optimal Berry–Esseen constant
Used byShevtsova's 2013 Berry–Esseen bound

DefinitionStatement of the unverified Berry–Esseen bound 0.4395#✓fully proved

The proposition that the Berry–Esseen constant \(C_0\) is at most \(0.4395\). Here \(C_0\) is the infimum of the real numbers \(C\) such that for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment \(\beta_3 = \int |x|^3 \, d\mu(x)\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), where \(X_1, \dots, X_n\) are independent with law \(\mu\), satisfies \(\sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)| \le C \beta_3 / \sqrt{n}\); here \(\Phi\) is the standard normal distribution function.

def xiaoLi2026UnverifiedUpperBound : Prop := value ≤ (4395 / 10000 : ℝ)
Sources
  • catalogue C19a, upper row XL2026, explicitly unverified. No external repository certificate or compiler-trusting proof is accepted by this request.
Uses 1 · Used by 1
Statement usesThe optimal Berry–Esseen constant
Used byThe unverified upper bound 0.4395 for the Berry–Esseen constant

DefinitionStatement of Lin's 2026 Berry–Esseen bound#✓fully proved

Let \(C_0\) be the infimum of all real \(C\) such that for every real probability law \(\mu\) with mean \(0\), variance \(1\) and finite third absolute moment \(\rho = \int |x|^3\,d\mu\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), for independent \(X_1, \dots, X_n\) with law \(\mu\), satisfies \(\sup_x |F_n(x) - \Phi(x)| \le C \rho / \sqrt{n}\), where \(\Phi\) is the standard normal distribution function. This is the proposition \(C_0 \le 0.423\).

def lin2026UnverifiedUpperBound : Prop := value ≤ (423 / 1000 : ℝ)
Sources
  • catalogue C19a, upper row Lin2026, explicitly unverified. No external repository certificate or comparator result is asserted here.
Uses 1 · Used by 1
Statement usesThe optimal Berry–Esseen constant
Used byLin's 2026 Berry–Esseen bound

DefinitionStatement of the Korolev–Shevtsova structural Berry–Esseen bound#✓fully proved

For a probability measure \(\mu\) on \(\mathbb{R}\) and an integer \(n \ge 1\), let \(F_n\) be the distribution function of \((X_1 + \dots + X_n)/\sqrt{n}\) for independent random variables \(X_1, X_2, \dots\) each with law \(\mu\), let \(\Delta_n(\mu) = \sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)|\), where \(\Phi\) is the standard normal distribution function, and let \(\beta_3(\mu) = \int |x|^3 \, d\mu\). This is the proposition that for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment and every integer \(n \ge 1\),

\[\Delta_n(\mu) \le \frac{0.34445\,(\beta_3(\mu) + 0.489)}{\sqrt{n}}.\]
def korolevShevtsova2009Structural : Prop :=
  ∀ μ : Measure ℝ, IsStandardizedLaw μ → ∀ n : ℕ+,
    kolmogorovError μ n ≤ (34445 / 100000 : ℝ) *
      (thirdMoment μ + 489 / 1000) / Real.sqrt (n.1 : ℝ)
Sources
  • catalogue C19a, KS2009 upper-row comment, and the exact retained Shevtsova2011 quotation at lines 141-148. The additive offset is 0.489, not 0.429.
Uses 3 · Used by 1
Statement usesStandardized laws with finite third moment · Kolmogorov error · Third absolute moment
Used byKorolev–Shevtsova structural Berry–Esseen bound

DefinitionStatement of Esseen's lower bound for the Berry–Esseen constant#✓fully proved

For a probability measure \(\mu\) on \(\mathbb{R}\) and an integer \(n \ge 1\), let \(F_n\) be the distribution function of \((X_1 + \dots + X_n)/\sqrt{n}\) for independent random variables \(X_1, X_2, \dots\) each with law \(\mu\), let \(\Delta_n(\mu) = \sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)|\), where \(\Phi\) is the standard normal distribution function, and let \(\beta_3(\mu) = \int |x|^3 \, d\mu\). Let \(C_0\) be the optimal i.i.d. Berry–Esseen constant, the infimum of all real \(C\) such that \(\Delta_n(\mu) \le C \beta_3(\mu) / \sqrt{n}\) for every integer \(n \ge 1\) and every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment. This is the proposition that \((\sqrt{10} + 3)/(6\sqrt{2\pi}) \le C_0\).

def esseen1956LowerBound : Prop := esseenConstant ≤ value
Sources
  • catalogue C19a, lower row E1956, and retained Shevtsova2011 lines 185-194. The symbolic endpoint is not replaced by its decimal approximation.
Uses 2 · Used by 1
Statement usesEsseen's lower-bound constant · The optimal Berry–Esseen constant
Used byEsseen's lower bound for the Berry–Esseen constant

DefinitionStatement of Esseen's asymptotic lower bound for a two-point law#✓fully proved

For a probability measure \(\mu\) on \(\mathbb{R}\) and an integer \(n \ge 1\), let \(F_n\) be the distribution function of \((X_1 + \dots + X_n)/\sqrt{n}\) for independent random variables \(X_1, X_2, \dots\) each with law \(\mu\), let \(\Delta_n(\mu) = \sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)|\), where \(\Phi\) is the standard normal distribution function, let \(\beta_3(\mu) = \int |x|^3 \, d\mu\), and let \(C_E = (\sqrt{10} + 3)/(6\sqrt{2\pi})\). This is the proposition that there is a probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\) and variance \(1\) that is concentrated on two distinct points, such that for every real \(\varepsilon > 0\) and every \(N \in \mathbb{N}\) there is a positive integer \(n \ge N\) with

\[\Delta_n(\mu) \ge \frac{(C_E - \varepsilon)\,\beta_3(\mu)}{\sqrt{n}}.\]
def esseenBernoulliAsymptoticLowerBound : Prop :=
  ∃ μ : Measure ℝ, IsBernoulliLaw μ ∧ ∀ ε : ℝ, 0 < ε → ∀ N : ℕ,
    ∃ n : ℕ+, N ≤ n.1 ∧
      (esseenConstant - ε) * thirdMoment μ / Real.sqrt (n.1 : ℝ) ≤ kolmogorovError μ n
Sources
  • catalogue C19a, lower-row Bernoulli asymptotic comment. A single actual standardized two-point law is chosen before epsilon and the sample-size threshold. Its normalized sums approach the lower coefficient along arbitrarily large sample sizes; an original Esseen primary comparison remains a source gap.
Uses 4 · Used by 1
Statement usesStandardized two-point law · Esseen's lower-bound constant · Kolmogorov error · Third absolute moment
Used byEsseen's asymptotic lower bound for a two-point law

DefinitionStatement of Schulz's Bernoulli Berry–Esseen optimum#✓fully proved

Let \(C_B\) be the infimum of all real \(C\) such that for every real probability law \(\mu\) with mean \(0\), variance \(1\) and finite third absolute moment \(\rho = \int |x|^3\,d\mu\) that is concentrated on two points, that is, \(\mu(\mathbb{R} \setminus \{a, b\}) = 0\) for some reals \(a \ne b\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), for independent \(X_1, \dots, X_n\) with law \(\mu\), satisfies \(\sup_x |F_n(x) - \Phi(x)| \le C \rho / \sqrt{n}\), where \(\Phi\) is the standard normal distribution function. This is the proposition \(C_B = (\sqrt{10} + 3)/(6\sqrt{2\pi})\).

def schulz2016BernoulliOptimum : Prop := bernoulliValue = esseenConstant
Sources
  • catalogue C19a, Bernoulli/binomial comment and Sch2016 reference. The actual subclass consists of centered variance-one two-point laws. The full Schulz primary proof has not been acquired or verified in this lane.
Uses 2 · Used by 1
Statement usesBernoulli Berry–Esseen constant · Esseen's lower-bound constant
Used bySchulz's Bernoulli Berry–Esseen optimum

DefinitionStatement of the Kolmogorov distance via left-continuous distribution functions#✓fully proved

This is the proposition that for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment and every integer \(n \ge 1\), if \(S_n = X_1 + \dots + X_n\) for independent random variables \(X_1, X_2, \dots\) each with law \(\mu\), then

\[ \sup_{x \in \mathbb{R}} \bigl|P(S_n/\sqrt{n} < x) - \Phi(x)\bigr| = \sup_{x \in \mathbb{R}} \bigl|P(S_n/\sqrt{n} \le x) - \Phi(x)\bigr|, \]

where \(\Phi\) is the standard normal distribution function.

def leftRightCDFErrorEquivalence : Prop :=
  ∀ μ : Measure ℝ, IsStandardizedLaw μ → ∀ n : ℕ+,
    sSup (Set.range (fun x : ℝ ↦
      |(normalizedLaw μ n).real (Set.Iio x) - normalCDF x|)) = kolmogorovError μ n
Sources
  • the right-CDF catalogue definition and retained Shevtsova2011 lines 104-108, which explicitly use a left-continuous CDF. This probability bridge is requested, not inferred by replacing strict with non-strict events.
Uses 4 · Used by 1
Statement usesStandardized laws with finite third moment · Kolmogorov error · Standard normal CDF · Law of the normalized sum
Used byKolmogorov distance via left-continuous distribution functions

TheoremZolotarev's upper bound for the Berry–Esseen constant#●ready to prove

The Berry–Esseen constant \(C_0\) is at most \(0.82\). Here \(C_0\) is the infimum of the real numbers \(C\) such that for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment \(\beta_3 = \int |x|^3 \, d\mu(x)\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), where \(X_1, \dots, X_n\) are independent with law \(\mu\), satisfies \(\sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)| \le C \beta_3 / \sqrt{n}\); here \(\Phi\) is the standard normal distribution function.

theorem_wanted zolotarev1967UpperBound_holds : zolotarev1967UpperBound
Sources
  • catalogue C19a, Z1967 upper row.
Uses 1
Statement usesStatement of Zolotarev's Berry–Esseen bound

TheoremVan Beek's upper bound for the Berry–Esseen constant#●ready to prove

The Berry–Esseen constant \(C_0\) is at most \(0.7975\). Here \(C_0\) is the infimum of the real numbers \(C\) such that for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment \(\beta_3 = \int |x|^3 \, d\mu(x)\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), where \(X_1, \dots, X_n\) are independent with law \(\mu\), satisfies \(\sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)| \le C \beta_3 / \sqrt{n}\); here \(\Phi\) is the standard normal distribution function.

theorem_wanted vanBeek1972UpperBound_holds : vanBeek1972UpperBound
Sources
  • catalogue C19a, vB1972 upper row.
Uses 1
Statement usesStatement of van Beek's Berry–Esseen bound

TheoremShiganov's upper bound for the Berry–Esseen constant#●ready to prove

The Berry–Esseen constant \(C_0\) is at most \(0.7655\). Here \(C_0\) is the infimum of the real numbers \(C\) such that for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment \(\beta_3 = \int |x|^3 \, d\mu(x)\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), where \(X_1, \dots, X_n\) are independent with law \(\mu\), satisfies \(\sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)| \le C \beta_3 / \sqrt{n}\); here \(\Phi\) is the standard normal distribution function.

theorem_wanted shiganov1986UpperBound_holds : shiganov1986UpperBound
Sources
  • catalogue C19a, Shi1986 upper row.
Uses 1
Statement usesStatement of Shiganov's Berry–Esseen bound

TheoremShevtsova's 2006 Berry–Esseen bound#●ready to prove

Let \(C_0\) be the infimum of all real \(C\) such that for every real probability law \(\mu\) with mean \(0\), variance \(1\) and finite third absolute moment \(\rho = \int |x|^3\,d\mu\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), for independent \(X_1, \dots, X_n\) with law \(\mu\), satisfies \(\sup_x |F_n(x) - \Phi(x)| \le C \rho / \sqrt{n}\), where \(\Phi\) is the standard normal distribution function. Then \(C_0 \le 0.7056\).

theorem_wanted shevtsova2006UpperBound_holds : shevtsova2006UpperBound
Sources
  • catalogue C19a, She2006 upper row.
Uses 1
Statement usesStatement of Shevtsova's 2006 Berry–Esseen bound

TheoremKorolev–Shevtsova upper bound for the Berry–Esseen constant#●ready to prove

For a probability measure \(\mu\) on \(\mathbb{R}\) and an integer \(n \ge 1\), let \(F_n\) be the distribution function of \((X_1 + \dots + X_n)/\sqrt{n}\) for independent random variables \(X_1, X_2, \dots\) each with law \(\mu\), let \(\Delta_n(\mu) = \sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)|\), where \(\Phi\) is the standard normal distribution function, and let \(\beta_3(\mu) = \int |x|^3 \, d\mu\). Let \(C_0\) be the optimal i.i.d. Berry–Esseen constant, the infimum of all real \(C\) such that \(\Delta_n(\mu) \le C \beta_3(\mu) / \sqrt{n}\) for every integer \(n \ge 1\) and every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment. Then \(C_0 \le 0.5129\).

theorem_wanted korolevShevtsova2009UpperBound_holds : korolevShevtsova2009UpperBound
Sources
  • catalogue C19a, KS2009 upper row; retained Shevtsova2011 quotation.
Uses 1
Statement usesStatement of the Korolev–Shevtsova upper bound

TheoremTyurin's upper bound for the Berry–Esseen constant#●ready to prove

The Berry–Esseen constant \(C_0\) is at most \(0.4785\). Here \(C_0\) is the infimum of the real numbers \(C\) such that for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment \(\beta_3 = \int |x|^3 \, d\mu(x)\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), where \(X_1, \dots, X_n\) are independent with law \(\mu\), satisfies \(\sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)| \le C \beta_3 / \sqrt{n}\); here \(\Phi\) is the standard normal distribution function.

theorem_wanted tyurin2009UpperBound_holds : tyurin2009UpperBound
Sources
  • catalogue C19a, Tyu2009 upper row.
Uses 1
Statement usesStatement of Tyurin's Berry–Esseen bound

TheoremShevtsova's 2011 Berry–Esseen bound#●ready to prove

Let \(C_0\) be the infimum of all real \(C\) such that for every real probability law \(\mu\) with mean \(0\), variance \(1\) and finite third absolute moment \(\rho = \int |x|^3\,d\mu\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), for independent \(X_1, \dots, X_n\) with law \(\mu\), satisfies \(\sup_x |F_n(x) - \Phi(x)| \le C \rho / \sqrt{n}\), where \(\Phi\) is the standard normal distribution function. Then \(C_0 \le 0.4748\).

theorem_wanted shevtsova2011UpperBound_holds : shevtsova2011UpperBound
Sources
  • catalogue C19a, She2011 upper row; retained primary Corollary 1.
Uses 1
Statement usesStatement of Shevtsova's 2011 Berry–Esseen bound

TheoremShevtsova's 2013 Berry–Esseen bound#●ready to prove

Let \(C_0\) be the infimum of all real \(C\) such that for every real probability law \(\mu\) with mean \(0\), variance \(1\) and finite third absolute moment \(\rho = \int |x|^3\,d\mu\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), for independent \(X_1, \dots, X_n\) with law \(\mu\), satisfies \(\sup_x |F_n(x) - \Phi(x)| \le C \rho / \sqrt{n}\), where \(\Phi\) is the standard normal distribution function. Then \(C_0 \le 0.4690\).

theorem_wanted shevtsova2013UpperBound_holds : shevtsova2013UpperBound
Sources
  • catalogue C19a, She2013 upper row; the primary correction is unresolved.
Uses 1
Statement usesStatement of Shevtsova's 2013 Berry–Esseen bound

TheoremThe unverified upper bound 0.4395 for the Berry–Esseen constant#●ready to prove

The Berry–Esseen constant \(C_0\) is at most \(0.4395\). Here \(C_0\) is the infimum of the real numbers \(C\) such that for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment \(\beta_3 = \int |x|^3 \, d\mu(x)\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), where \(X_1, \dots, X_n\) are independent with law \(\mu\), satisfies \(\sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)| \le C \beta_3 / \sqrt{n}\); here \(\Phi\) is the standard normal distribution function.

theorem_wanted xiaoLi2026UnverifiedUpperBound_holds : xiaoLi2026UnverifiedUpperBound
Sources
  • catalogue C19a, explicitly unverified XL2026 row.
Uses 1
Statement usesStatement of the unverified Berry–Esseen bound 0.4395

TheoremLin's 2026 Berry–Esseen bound#●ready to prove

Let \(C_0\) be the infimum of all real \(C\) such that for every real probability law \(\mu\) with mean \(0\), variance \(1\) and finite third absolute moment \(\rho = \int |x|^3\,d\mu\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), for independent \(X_1, \dots, X_n\) with law \(\mu\), satisfies \(\sup_x |F_n(x) - \Phi(x)| \le C \rho / \sqrt{n}\), where \(\Phi\) is the standard normal distribution function. Then \(C_0 \le 0.423\).

theorem_wanted lin2026UnverifiedUpperBound_holds : lin2026UnverifiedUpperBound
Sources
  • catalogue C19a, explicitly unverified Lin2026 row.
Uses 1
Statement usesStatement of Lin's 2026 Berry–Esseen bound

TheoremKorolev–Shevtsova structural Berry–Esseen bound#●ready to prove

For a probability measure \(\mu\) on \(\mathbb{R}\) and an integer \(n \ge 1\), let \(F_n\) be the distribution function of \((X_1 + \dots + X_n)/\sqrt{n}\) for independent random variables \(X_1, X_2, \dots\) each with law \(\mu\), let \(\Delta_n(\mu) = \sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)|\), where \(\Phi\) is the standard normal distribution function, and let \(\beta_3(\mu) = \int |x|^3 \, d\mu\). Then for every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment and every integer \(n \ge 1\),

\[\Delta_n(\mu) \le \frac{0.34445\,(\beta_3(\mu) + 0.489)}{\sqrt{n}}.\]
theorem_wanted korolevShevtsova2009Structural_holds : korolevShevtsova2009Structural
Sources
  • catalogue C19a, KS2009 structural comment; retained 2011 equation.
Uses 1
Statement usesStatement of the Korolev–Shevtsova structural Berry–Esseen bound

TheoremEsseen's lower bound for the Berry–Esseen constant#●ready to prove

For a probability measure \(\mu\) on \(\mathbb{R}\) and an integer \(n \ge 1\), let \(F_n\) be the distribution function of \((X_1 + \dots + X_n)/\sqrt{n}\) for independent random variables \(X_1, X_2, \dots\) each with law \(\mu\), let \(\Delta_n(\mu) = \sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)|\), where \(\Phi\) is the standard normal distribution function, and let \(\beta_3(\mu) = \int |x|^3 \, d\mu\). Let \(C_0\) be the optimal i.i.d. Berry–Esseen constant, the infimum of all real \(C\) such that \(\Delta_n(\mu) \le C \beta_3(\mu) / \sqrt{n}\) for every integer \(n \ge 1\) and every probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment. Then \((\sqrt{10} + 3)/(6\sqrt{2\pi}) \le C_0\).

theorem_wanted esseen1956LowerBound_holds : esseen1956LowerBound
Sources
  • catalogue C19a, E1956 lower row; retained 2011 exact benchmark.
Uses 1
Statement usesStatement of Esseen's lower bound for the Berry–Esseen constant

TheoremEsseen's asymptotic lower bound for a two-point law#●ready to prove

For a probability measure \(\mu\) on \(\mathbb{R}\) and an integer \(n \ge 1\), let \(F_n\) be the distribution function of \((X_1 + \dots + X_n)/\sqrt{n}\) for independent random variables \(X_1, X_2, \dots\) each with law \(\mu\), let \(\Delta_n(\mu) = \sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)|\), where \(\Phi\) is the standard normal distribution function, let \(\beta_3(\mu) = \int |x|^3 \, d\mu\), and let \(C_E = (\sqrt{10} + 3)/(6\sqrt{2\pi})\). There is a probability measure \(\mu\) on \(\mathbb{R}\) with mean \(0\) and variance \(1\) that is concentrated on two distinct points, such that for every real \(\varepsilon > 0\) and every \(N \in \mathbb{N}\) there is a positive integer \(n \ge N\) with

\[\Delta_n(\mu) \ge \frac{(C_E - \varepsilon)\,\beta_3(\mu)}{\sqrt{n}}.\]

In other words, \(\limsup_{n \to \infty} \sqrt{n}\,\Delta_n(\mu) / \beta_3(\mu) \ge C_E\).

theorem_wanted esseenBernoulliAsymptoticLowerBound_holds : esseenBernoulliAsymptoticLowerBound
Sources
  • catalogue C19a, the asymptotic normalized Bernoulli lower-row clause.
Uses 1
Statement usesStatement of Esseen's asymptotic lower bound for a two-point law

TheoremSchulz's Bernoulli Berry–Esseen optimum#●ready to prove

Let \(C_B\) be the infimum of all real \(C\) such that for every real probability law \(\mu\) with mean \(0\), variance \(1\) and finite third absolute moment \(\rho = \int |x|^3\,d\mu\) that is concentrated on two points, that is, \(\mu(\mathbb{R} \setminus \{a, b\}) = 0\) for some reals \(a \ne b\), and every integer \(n \ge 1\), the distribution function \(F_n\) of \((X_1 + \dots + X_n)/\sqrt{n}\), for independent \(X_1, \dots, X_n\) with law \(\mu\), satisfies \(\sup_x |F_n(x) - \Phi(x)| \le C \rho / \sqrt{n}\), where \(\Phi\) is the standard normal distribution function. Then \(C_B = (\sqrt{10} + 3)/(6\sqrt{2\pi})\).

theorem_wanted schulz2016BernoulliOptimum_holds : schulz2016BernoulliOptimum
Sources
  • catalogue C19a, Bernoulli/binomial comment, Schulz2016.
Uses 1
Statement usesStatement of Schulz's Bernoulli Berry–Esseen optimum

TheoremKolmogorov distance via left-continuous distribution functions#●ready to prove

Let \(\mu\) be a probability measure on \(\mathbb{R}\) with mean \(0\), variance \(1\) and finite third absolute moment, let \(n \ge 1\) be an integer, and let \(S_n = X_1 + \dots + X_n\) for independent random variables \(X_1, X_2, \dots\) each with law \(\mu\). Then

\[ \sup_{x \in \mathbb{R}} \bigl|P(S_n/\sqrt{n} < x) - \Phi(x)\bigr| = \sup_{x \in \mathbb{R}} \bigl|P(S_n/\sqrt{n} \le x) - \Phi(x)\bigr|, \]

where \(\Phi\) is the standard normal distribution function.

theorem_wanted leftRightCDFErrorEquivalence_holds : leftRightCDFErrorEquivalence
Sources
  • catalogue C19a right CDF and Shevtsova2011's explicit left convention.
Uses 1
Statement usesStatement of the Kolmogorov distance via left-continuous distribution functions
46 fully proved15 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.