A Lean 4 library for reusable, formalized statistics — 1,807 theorems, checked end to end.

Abstract. statlib builds the foundational layer that statistical and machine-learning formalization needs: stochastic-order asymptotics, uniform integrability, empirical-process tools, high-dimensional concentration, low-rank matrix recovery, matrix analysis, conformal prediction, and nonparametric approximation on top of Mathlib. Every entry is checked end to end by the Lean compiler — no gaps, no hand-waving.

Browse the library
470
Lean files
452,823
Lines of Lean
1,807
Theorems proved
1,035
Supporting lemmas
1

What's inside

statlib is built around three main boards, each a tree of topic areas formalized against Mathlib, with supporting packages in the full library tree. Today the work centers on these boards:

1.1

Statistical foundations

Statlib.StatFoundation

The probability and statistics core the rest of the library builds on: stochastic-order asymptotics (big-O/little-o in probability, Slutsky), uniform integrability and integral convergence, conformal prediction, sufficiency and statistical inference, convergence and limit theorems, empirical-process tools, sub-Gaussian and sub-exponential variables, finite-dimensional Gaussian functional inequalities, Lipschitz concentration, and concentration inequalities.

Statistical inference & sufficiency

5 thm · 5 lem

A measure-theoretic foundation for sufficient, ancillary, and complete statistics, culminating in the Lehmann-Scheffé and Basu theorems of classical estimation theory.

Convergence & limit theorems

32 thm · 51 lem

Formalizes the central limit theorems (IID, Lindeberg-Feller, multivariate), the Lévy continuity and Cramér-Wold tools behind weak convergence, and uniform laws of large numbers including Glivenko-Cantelli.

Stochastic-order asymptotics

82 thm · 4 lem

Big-O and little-o in probability, rate bounds, Slutsky-type product theorems, and convergence bridges connecting stochastic orders to classical limit theorems.

Uniform integrability

25 thm · 0 lem

Uniformly integrable families, Vitali convergence, integral-convergence bridges, and conditions ensuring L¹ convergence from convergence in probability.

Empirical processes

9 thm · 6 lem

Rademacher complexity, contraction and symmetrization tools, Dudley entropy, bounded-difference controls, and quantitative Glivenko-Cantelli statements for uniform deviation arguments.

Tail behavior of random variables

94 thm · 70 lem

Concentration and tail-bound theory for sub-Gaussian and sub-exponential random variables, plus Gaussian functional inequalities culminating in dimension-free Lipschitz concentration.

Concentration inequalities

37 thm · 2 lem

Tail and moment bounds controlling how sums and functions of independent (or martingale) random variables deviate from their means.

Conformal prediction

13 thm · 0 lem

Reusable score-coverage and event-inclusion interfaces for conformal prediction, plus measurable finite-score ranking vocabulary.

Roadmap. Grow shared vocabulary as concepts get reused across areas, broaden the estimation, testing, empirical-process, and asymptotic foundations, and expand stochastic-order and conformal-inference toolchains.

1.2

High-dimensional statistics

Statlib.HighDim

Statistics in the high-dimensional regime: matrix concentration (Hanson–Wright, matrix Bernstein), Wedin sin-theta perturbation, covariance estimation, L1 quadratic-process analysis, L1 RSE bounds from covariance, high-dimensional geometry, low-rank matrix recovery and completion tools, regression, and debiased LASSO inference.

Matrix analysis

70 thm · 101 lem

Operator-convexity, trace exponential, Lieb concavity, variational, quantum-relative-entropy, and Wedin sin-theta infrastructure supporting matrix concentration and spectral perturbation.

Low-rank matrix recovery and completion tools

24 thm · 9 lem

Nuclear-norm recovery under restricted isometry, compact-factor subgradients, and reusable tangent-space tools for matrix completion. The completion proof chain is still being developed.

High-dimensional concentration

38 thm · 110 lem

Concentration inequalities for high-dimensional random objects — sub-Gaussian maxima, the matrix Bernstein inequality for sums of independent random matrices, and the Hanson-Wright bound for quadratic forms.

Covariance estimation

7 thm · 24 lem

Concentration and unbiasedness guarantees for the sample second-moment (covariance) matrix estimator of high-dimensional sub-Gaussian random vectors.

High-dimensional geometry

11 thm · 53 lem

Geometric foundations of high-dimensional statistics: covering numbers, Johnson-Lindenstrauss dimension reduction, isotropic and anisotropic RIP, and restricted eigenvalue transfers.

High-dimensional regression

59 thm · 9 lem

Oracle inequalities and debiased-inference guarantees for sparse high-dimensional linear models, from restricted-eigenvalue LASSO bounds to asymptotic Wald coverage.

Spectral perturbation

4 thm · 48 lem

Quantitative bounds on how a matrix's eigenvalues and eigenvectors move under perturbation, applied to high-dimensional PCA via sample-covariance concentration.

Roadmap. Strengthen the operator-convexity, matrix-concentration, covariance, RIP, spectral-perturbation, debiasing, and regression theorem chains; extend L1-process results to broader design matrix families.

1.3

Nonparametric statistics

Statlib.Nonparametric

Approximation and risk vocabulary for nonparametric statistics: finite sieves, Holder classes, high-order tensor-product B-spline and wavelet approximation, RKHS and neural-network rates, and oracle interfaces.

Nonparametric approximation

276 thm · 2 lem

Approximation-error bounds for finite sieves, Holder balls, splines, wavelets, RKHS balls, and neural-network candidate classes.

Oracle interfaces

1 thm · 0 lem

Risk and oracle-comparison interfaces for estimator classes, prediction losses, and candidate families.

Roadmap. Fill in the remaining nonparametric approximation chains while keeping the sieve and risk interfaces reusable across estimators; extend conformal-prediction results to broader nonparametric settings.

2

Selected results

Low-rank matrix recovery and completion tools

Stable nuclear-norm matrix recovery under RIP

∥A^−A⋆∥F≤C0(δ) ∥A⋆−Ar⋆∥∗r+C1(δ) ε\|\widehat A-A^\star\|_F\le C_0(\delta)\,\frac{\|A^\star-A_r^\star\|_*}{\sqrt r}+C_1(\delta)\,\varepsilon

Under rank-4r restricted isometry with δ below √2−1, a feasible nuclear-norm minimizer has Frobenius error bounded by the rank-r approximation tail and observation noise. The positive constants depend on δ.

matrix_rip_recovery_bound
High-dimensional regression

Debiased LASSO standard Wald interval coverage

P ⁣(βj∈b^j±c s^j/an)→1−α\mathbb{P}\!\left(\beta_j\in \hat b_j \pm c\,\hat s_j/a_n\right)\to 1-\alpha

An iid-score debiased LASSO theorem: row-approximation error, L1 consistency, studentization, and Gaussian critical-value calibration imply asymptotic standard Wald confidence-interval coverage.

tendsto_measure_debiasedLasso_standardWaldCI_coverage_iidScoreSum_real
Nonparametric approximation

Holder-smooth ReLU approximation at the -2s/d rate

f∈Hr+β([0,1]d)  ⟹  ∃g∈NL,W: sup⁡x∈[0,1]d∣g(x)−f(x)∣≤c (LW2)−2(r+β)/df\in\mathcal{H}^{r+\beta}([0,1]^d) \implies \exists g\in\mathcal{N}_{L,W}:\ \sup_{x\in[0,1]^d}|g(x)-f(x)|\le c\,(LW^2)^{-2(r+\beta)/d}

An explicit fixed-width construction is converted into the architecture-scale ReLU approximation rate (L W^2)^(-2(r+beta)/d) for high-dimensional Holder-smooth functions.

holderSmoothBall_unitCube_LW2_rate_from_fixed_width_M_rate
Nonparametric approximation

High-order multivariate B-spline Holder rate

f0∈Hr+β([0,1]d)  ⟹  EmK(f0)≤M mK−2(r+β)/df_0\in\mathcal{H}^{r+\beta}([0,1]^d) \implies \mathcal{E}_{m_K}(f_0) \le M\,m_K^{-2(r+\beta)/d}

A positive-degree tensor-product B-spline system on the high-dimensional unit cube achieves the uniform squared-error sieve rate m^(-2(r+beta)/d) over the trace Holder-smooth ball.

unit_cube_bspline_high_order_holder_smooth_uniform_sieve_approximation_rate
High-dimensional concentration

Rectangular matrix Bernstein inequality

P ⁣(∥∑kXk∥≥t)≤(p+q) exp⁡ ⁣(−t2/2σ2+Rt/3)\mathbb{P}\!\left(\Big\|\sum_k X_k\Big\| \ge t\right) \le (p+q)\,\exp\!\left(\frac{-t^2/2}{\sigma^2 + Rt/3}\right)

The matrix Bernstein bound extended to sums of independent centered rectangular p×q random matrices via Hermitian dilation, with variance the max of the two one-sided second-moment norms.

matrix_bernstein_rect
Tail behavior of random variables

Gaussian concentration for Lipschitz functions

P ⁣(∣f(X)−Ef(X)∣≥t)≤2exp⁡ ⁣(−t22L2)\mathbb{P}\!\left(|f(X)-\mathbb{E}f(X)|\ge t\right) \le 2\exp\!\left(-\frac{t^2}{2L^2}\right)

An L-Lipschitz function of a vector with independent standard Gaussian coordinates has a dimension-free two-sided Gaussian tail around its mean.

gaussian_lipschitz_concentration
Convergence & limit theorems

Gaussian maximum comparison (diagonal case)

sup⁡t∣Pr⁡(max⁡jVj≤t)−Pr⁡(max⁡jYj≤t)∣≤C(c1,C1) Δ1/3(1∨log⁡(p/Δ))2/3\sup_t\left|\Pr(\max_j V_j\le t)-\Pr(\max_j Y_j\le t)\right|\le C(c_1,C_1)\,\Delta^{1/3}\left(1\vee\log(p/\Delta)\right)^{2/3}

For independent centered Gaussian vectors with diagonal variances bounded above and away from zero, a covariance gap Δ in (0, 1) controls the difference between their maximum distributions.

gaussianMax_cube_root_comparison_diagonal

Built to be reused — and extended

statlib aims to fill a foundation gap: reusable, machine-checked infrastructure for statistics and machine learning, built only on Mathlib. Explore the library catalog and read how it is designed.

About statlib