TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Berry–Esseen bound for a finite independent array

Statement

Assume the Axiom of Choice. Let $X_{1}, \dots, X_{n}$ be independent, finite-support real random variables with $E X_{i} = 0$ and total variance $σ^{2} = \sum_{i} E X_{i}^{2} > 0$ . If $S = \sum_{i} X_{i}$ and $Φ$ is the standard-normal CDF, then $\sup_{z \in R} ∣ \Pr {S / σ \leq z} - Φ (z) ∣ \leq 1088 \frac{\sum_{i} E ∣ X_{i} ∣^{3}}{σ^{3}} .$

Facts & Assumptions

Given: The finite independent array, its mean and variance hypotheses, and the Axiom of Choice.

[A1]

The Axiom of Choice and Standard normal and normal laws: assume AC, and let $G$ have density $φ (x) = (2 π)^{- 1 / 2} e^{- x^{2} / 2}$ and total mass one.

[F1]

The exponential function is smooth and $(\exp)^{'} = \exp$ , The exponential dominates every fixed nonnegative integer power at $+ \infty$ , and The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ : $φ^{'} (x) = - x φ (x)$ , Gaussian tails vanish at infinity, and the Gaussian integral is finite with the stated normalization.

[F2]

The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive, A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , and If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ : the first fundamental theorem differentiates a continuous-integrand integral, the product rule applies, and integration by parts holds on finite intervals for integrable derivatives.

[F3]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ : on a closed interval, a differentiable function whose derivative is integrable has endpoint difference equal to the derivative's integral; apply it separately on each smooth piece of $f^{'}$ split at the two breakpoints of $h$ .

Proof

1.1givenalgebra

Divide each summand by $σ$ , so it suffices to consider independent mean-zero variables with total variance one and $β : = \sum_{i} E ∣ X_{i} ∣^{3}$ . A zero-variance summand is zero almost surely and may be removed. For $r > 0$ , let $δ_{m} (r)$ be the supremum of ${0}$ together with the normal-CDF errors $\sup_{z} ∣ \Pr {\sum_{i} X_{i} \leq z} - Φ (z)$ over all $m$ -term finite-support arrays with total variance one and third-moment sum at most $r^{3}$ . This convention also defines $δ_{m} (r) = 0$ when the class of arrays is empty.

1.2givenalgebra

If some summand has variance greater than $1 / 2$ , the needed Lyapunov inequality follows locally as follows. Put $A = ∣ X_{i} ∣$ and $m_{3} = E A^{3}$ ; then $m_{3} > 0$ . For $U = A / m_{3}^{1 / 3}$ , the pointwise identity $1 + 2 U^{3} - 3 U^{2} = (U - 1)^{2} (2 U + 1) \geq 0$ gives $E A^{2} / m_{3}^{2 / 3} \leq 1$ , so $E ∣ X_{i} ∣^{3} \geq (E X_{i}^{2})^{3 / 2}$ . Therefore $β \geq (E X_{i}^{2})^{3 / 2} > 1 / (2 \sqrt{2}) > 1 / 3$ . Since any two CDF values differ by at most one, the bound $δ_{m} (r) \leq 1088 r^{3}$ holds in this case.

1.3A1F1F2given

It remains to prove the induction step when each summand variance is at most $1 / 2$ . Fix a threshold $a$ and $ϵ > 0$ , and let $h$ equal $1$ on $(- \infty, a]$ , decrease linearly to $0$ on $[a, a + ϵ]$ , and equal $0$ afterward. Define $f (x) = e^{x^{2} / 2} \int_{- \infty}^{x} e^{- t^{2} / 2} (h (t) - E h (G)) d t,$ where $G$ has the standard-normal law. On any finite interval, [F2] differentiates the integral term and the product rule differentiates the integrating factor, giving $f^{'} (x) - x f (x) = h (x) - E h (G)$ . The total integral of the integrand is zero, so its upper-tail form also holds.

2.1F1F2F3step 1.3

For $x > 0$ , the upper-tail formula and $0 \leq h \leq 1$ give $∣ f (x) ∣ \leq e^{x^{2} / 2} \int_{x}^{\infty} e^{- t^{2} / 2} d t = \int_{0}^{\infty} e^{- x s - s^{2} / 2} d s \leq \min (2, 1 / x)$ . For $x \leq 0$ the lower-tail formula gives the same bounds. Thus $∣ x f (x) ∣ \leq 1$ and the differential equation gives $∣ f^{'} (x) ∣ \leq 2$ . Away from the two breakpoints of the piecewise-linear $h$ , differentiating the Stein equation gives $f^{''} = f + x f^{'} + h^{'}$ , so $∣ f^{''} (x) ∣ \leq 2 + 2 ∣ x ∣ + ϵ^{- 1} 1_{[a, a + ϵ]} (x)$ . On any finite segment, split at those breakpoints and apply [F3] on each smooth subinterval to the function $f^{'}$ ; it is differentiable there, its derivative $f^{''}$ is continuous up to the one-sided endpoints, and hence integrable. Continuity of $f^{'}$ lets the increments add across the breakpoints.

3.1A1F1step 2.1giveninductionalgebra

Integrating the last bound along the segment from $x$ to $x + y$ (and using $∣ f^{'} ∣ \leq 2$ when $∣ y ∣ > 1$ ) yields $∣ f^{'} (x + y) - f^{'} (x) ∣ \leq 4 ∣ y ∣ (1 + ∣ x ∣ + ϵ^{- 1} \int_{0}^{1} 1_{[a, a + ϵ]} (x + s y) d s) .$ For the sum $S_{- i}$ omitting term $i$ , its variance is at least $1 / 2$ . After dividing by its standard deviation $σ_{- i} \geq 1 / \sqrt{2}$ , its third-moment sum is at most $\sqrt{8} r^{3} < 8 r^{3} = (2 r)^{3}$ , so the induction definition bounds its CDF error by $δ_{m - 1} (2 r)$ . Comparing the two endpoints of any interval of length $ϵ$ with a normal interval, whose density is bounded by one, gives $\Pr {S_{- i} + s y \in [a, a + ϵ]} \leq 2 ϵ + 2 δ_{m - 1} (2 r)$ . Finally, $(E ∣ S_{- i} ∣)^{2} \leq E S_{- i}^{2} = Var (S_{- i}) \leq 1$ , because $E (∣ S_{- i} ∣ - E ∣ S_{- i} ∣)^{2} \geq 0$ . Taking expectations in the increment bound therefore gives $E ∣ f^{'} (S_{- i} + y) - f^{'} (S_{- i}) ∣ \leq 16 ∣ y ∣ (1 + δ_{m - 1} (2 r) / ϵ)$ .

3.2A1F1F2step 1.3step 2.1algebra

Integrating by parts on $[- A, A]$ using [F2] gives $\int_{- A}^{A} f^{'} φ = [f φ]_{- A}^{A} + \int_{- A}^{A} x f φ$ . The boundary term tends to zero because $f$ is bounded by step 2.1 and $φ (A) \to 0$ by [F2]; the integrals converge since $f, f^{'}$ are bounded and $∣ x ∣ φ (x)$ is integrable by [F1]. Hence $E f^{'} (G) = E G f (G)$ . The smoothing inequalities $1_{(- \infty, a]} \leq h_{a} \leq 1_{(- \infty, a + ϵ]}$ show that $\Pr {S \leq a} - Φ (a) \leq E h_{a} (S) - E h_{a} (G) + ϵ$ : the normal mass of an interval of length $ϵ$ is at most $ϵ$ . For the reverse difference, apply the same calculation to $h_{a - ϵ}$ and its corresponding Stein solution; the bounds in step 2.1 are uniform in the threshold. For either smoothing function, the Stein equation identifies the expectation difference as $E [f^{'} (S) - S f (S)]$ , proving the displayed uniform estimate.

4.1step 3.1step 3.2givenalgebra

For the needed moment comparison, write the finite law of $A = ∣ X_{i} ∣$ as values $a_{j}$ with weights $p_{j}$ . For every pair $j, k$ , $a_{j}^{2} a_{k} \leq (2 a_{j}^{3} + a_{k}^{3}) / 3$ , since $2 a^{3} + b^{3} - 3 a^{2} b = (a - b)^{2} (2 a + b) \geq 0$ . Averaging with weights $p_{j} p_{k}$ gives $E X_{i}^{2} E ∣ X_{i} ∣ \leq E ∣ X_{i} ∣^{3}$ . Put $Z = S_{- i}$ . Independence and mean zero give $E [X_{i} f (S)] = E [X_{i}^{2} \int_{0}^{1} f^{'} (Z + t X_{i}) d t]$ , while independence also gives $E [X_{i}^{2} f^{'} (Z)] = E X_{i}^{2} E f^{'} (Z)$ . By step 3.1, conditioning on $X_{i}$ bounds $E [X_{i}^{2} \int_{0}^{1} ∣ f^{'} (Z + t X_{i}) - f^{'} (Z) ∣ d t]$ by $8 E ∣ X_{i} ∣^{3} (1 + δ_{m - 1} (2 r) / ϵ)$ , and the same step bounds $E X_{i}^{2} E ∣ f^{'} (Z + X_{i}) - f^{'} (Z) ∣$ by $16 E X_{i}^{2} E ∣ X_{i} ∣ (1 + δ_{m - 1} (2 r) / ϵ)$ . Decomposing at $f^{'} (Z)$ and using the moment comparison shows $∣ E [X_{i} f (S)] - E X_{i}^{2} E f^{'} (S) ∣ \leq 24 E ∣ X_{i} ∣^{3} (1 + δ_{m - 1} (2 r) / ϵ) \leq 32 E ∣ X_{i} ∣^{3} (1 + δ_{m - 1} (2 r) / ϵ)$ . Summing over $i$ and using $\sum_{i} E X_{i}^{2} = 1$ bounds the difference in step 3.2 by $32 r^{3} (1 + δ_{m - 1} (2 r) / ϵ)$ .

5.1step 1.1step 1.2step 3.2step 4.1algebra∎

Choose $ϵ = 512 r^{3}$ . Steps 3.2 and 4.1 give $δ_{m} (r) \leq 544 r^{3} + \frac{1}{16} δ_{m - 1} (2 r)$ . Inductively, $δ_{m - 1} (2 r) \leq 1088 (2 r)^{3}$ , so the right side is at most $(544 + 544) r^{3} = 1088 r^{3}$ . For one summand with variance one, Lyapunov gives $r^{3} \geq β \geq 1$ , and the trivial CDF bound starts the induction. Combining with step 1.2 proves the normalized claim; undoing the variance normalization proves the Statement.

Depends on

Used by

Nondegenerate normal approximation for finite unconstrained DMCs Theorem

Dependency tree · two levels

72 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Roman Vershynin, Two friendly proofs of the Berry–Esseen theorem, arXiv:2602.06234v2 (standard reference, not scraped)