ProbabilityApproximation: Berry–Esseen Bounds for Independent Sums

ProbabilityApproximation is a Lean 4 and Mathlib library for the Berry–Esseen theorem, quantitative normal approximation, and the multivariate central limit theorem. It formalizes the nonuniform scalar bound of Chen and Shao via Stein's method and Bentkus's dimension-dependent Gaussian approximation over convex sets.

Read the interactive Blueprint, or download the complete mathematical text as a PDF.

Main results

Nonuniform Berry–Esseen bound

Let $X_1,\ldots,X_n$ be independent real-valued random variables satisfying $\mathbb E X_i=0$, $\sum_{i=1}^n\mathrm{Var}(X_i)=1$, and $\beta_3:=\sum_{i=1}^n\mathbb E|X_i|^3<\infty$. For $W:=\sum_{i=1}^n X_i$, there is a universal constant $C>0$ such that

$$ \left|\Pr(W\le x)-\Phi(x)\right| \le \frac{C\beta_3}{1+|x|^3}, \qquad x\in\mathbb R. $$

Here $\Phi$ denotes the standard normal distribution function.

Bentkus's multivariate convex-set bound

Let $X_1,\ldots,X_n$ be independent centered random vectors in $\mathbb R^d$, set $W:=\sum_{i=1}^n X_i$, and suppose that $\Sigma:=\mathrm{Cov}(W)$ is positive definite. If $Z\sim\mathcal N_d(0,\Sigma)$ and $\beta:=\sum_{i=1}^n\mathbb E\lVert\Sigma^{-1/2}X_i\rVert_2^3<\infty$, then there is a universal constant $C>0$ such that

$$ \sup_{A\in\mathcal C_d} \left|\Pr(W\in A)-\Pr(Z\in A)\right| \le C d^{1/4}\beta, $$

where $\mathcal C_d$ is the class of Borel convex subsets of $\mathbb R^d$.

Mathematical infrastructure

The library also develops reusable foundations for probability, analysis, and convex geometry:

• Stein's method and scalar probability: the half-line Stein equation, derivative estimates, leave-one-out concentration, Bennett--Hoeffding bounds, one-sided truncation, residual decompositions, large-jump estimates, and reflection of distribution functions.
• Gaussian analysis: independent Gaussian companions, covariance algebra, multivariate Gaussian pushforwards, whitening, Gaussian-density derivatives, integration by parts, and second-order Taylor remainder estimates.
• Convex and geometric measure theory: convex parallel sets, metric projection, signed distance, smooth approximations of convex indicators, Hausdorff and spherical measure, coarea formulas, Ball's Gaussian perimeter theorem, and Gaussian shell bounds.
• Multivariate normal approximation: smoothing inequalities, rotation and Fubini arguments, small- and large-angle estimates, Gaussian replacement induction, and transport from identity covariance to arbitrary positive-definite covariance.

Using the library

The current release is v0.9.5, built with Lean and Mathlib v4.32.0. Add the tagged package to a downstream lakefile.toml:

[[require]]
name = "ProbabilityApproximation"
git = "https://github.com/Polarnova/ProbabilityApproximation.git"
rev = "v0.9.5"

Then update and build:

lake update
lake exe cache get
lake build

Lake automatically downloads the matching precompiled ProbabilityApproximation release archive on Linux x86-64 and macOS arm64. If an archive is unavailable for a platform, Lake falls back to the same tagged source and builds it locally.

Import all public declarations with:

import ProbabilityApproximation

The principal declarations are:

#check ProbabilityTheory.nonuniformBerryEsseen
#check ProbabilityTheory.exists_bentkus_convex_set_constant

To build the repository itself:

git clone https://github.com/Polarnova/ProbabilityApproximation.git
cd ProbabilityApproximation
lake exe cache get
lake build ProbabilityApproximation

Blueprint

The Verso Blueprint presents both proofs as a mathematical text with complete statements, source citations, Lean declarations, and dependency graphs. The same text is available as a downloadable PDF.

Contributing

Read AGENTS.md for the source-fidelity, Mathlib-reuse, proof, and Blueprint conventions.

Citation

If you use the Lean formalization, cite the specific software release through GitHub's Cite this repository menu or CITATION.cff. Cite the original mathematical source as well: Bikelis (1966) for the classical finite-third-moment nonuniform bound, Chen--Shao (2001) for the stronger truncated-moment theorem, Chen--Shao (2005) for the proof presentation used here, or Bentkus (2004) for the multivariate convex-set theorem. Work using the auxiliary geometric or explicit-constant results should additionally cite the corresponding source listed below.

Authors

Asher Yan with ChatGPT 5.6.

References

• A. Bikelis, On estimates of the remainder term in the central limit theorem, Lithuanian Mathematical Journal 6(3) (1966), 323--346.
• Herbert Federer, Geometric Measure Theory, Springer, Grundlehren der mathematischen Wissenschaften 153 (1969).
• Keith Ball, The reverse isoperimetric problem for Gaussian measure, Discrete and Computational Geometry 10(4) (1993), 411--420.
• Louis H. Y. Chen and Qi-Man Shao, A non-uniform Berry--Esseen bound via Stein's method, Probability Theory and Related Fields 120(2) (2001), 236--254.
• Louis H. Y. Chen and Qi-Man Shao, Stein's method for normal approximation, in An Introduction to Stein's Method, Lecture Notes Series 4, Institute for Mathematical Sciences, National University of Singapore (2005), 1--59.
• Vidmantas Bentkus, On the dependence of the Berry--Esseen bound on dimension, Journal of Statistical Planning and Inference 113(2) (2003), 385--402.
• Vidmantas Bentkus, A Lyapunov-type bound in R^d, Teoriya Veroyatnostei i ee Primeneniya 49(2) (2004), 400--410.
• Martin Raič, A multivariate Berry--Esseen theorem with explicit constants, Bernoulli 25(4A) (2019), 2824--2853.

The Blueprint bibliography is generated from references.bib.

Related projects

Mathlib supplies the mathematical foundation. FABL is the initial downstream consumer of the scalar theorem.

License

ProbabilityApproximation is released under the Apache License 2.0. See LICENSE.