1. Add the dependency
Add StatsMLlib to your project’s lakefile.toml.
[[require]]
name = "StatsMLlib"
git = "https://github.com/Lean-MoDS/StatsMLlib.git"A Lean 4 library
StatsMLlib
Formal foundations for probability, statistics, and machine learning, from concentration inequalities and random matrices to finite-sample learning guarantees.
Abstract. StatsMLlib develops concentration of measure, metric entropy and chaining, empirical processes, Rademacher complexity, random matrix theory, and finite-sample learning guarantees as formal mathematics in Lean 4. Together, these results provide a unified foundation for probability, statistics, and machine learning, with every proof checked by the Lean 4 kernel.
666Theorems
1,219Lemmas
352Definitions
89Lean files
64,695Lines of Lean
0Sorries
Organizers
Fanghui LiuOrganizer
Jason D. LeeOrganizer
Peter BartlettOrganizer
Weijie SuOrganizer
Aleksandar MijatovicOrganizer
Taiji SuzukiOrganizer
Yuekai SunOrganizer
Sho SonodaOrganizerInstallation
2. Import a chapter
Import only the part of the library you need.
import StatsMLlib.Probability.Process.Dudley
import StatsMLlib.LearningTheory.UniformDeviation.Bounds
import StatsMLlib.Statistics.Regression.LeastSquares.Linear.MinimaxRateFormalized literature map
Book Map
Navigate StatsMLlib through five foundational books, with each chapter map highlighting related formal developments in Lean 4.
High-Dimensional ProbabilityAn Introduction with Applications in Data Science, 2nd ed.7 mapped chapters
High-Dimensional StatisticsA Non-Asymptotic Viewpoint9 mapped chapters
Concentration InequalitiesA Nonasymptotic Theory of Independence5 mapped chapters
Foundations of Machine Learning2nd ed.4 mapped chapters
Learning Theory from First PrinciplesMIT Press, 20244 mapped chapters
Selected Theorems
Uniform law via Rademacher complexity
For a separable, first-countable parameter space indexing measurable functions bounded in absolute value by \(b>0\), with pointwise-continuous parametrization, empirical means track their expectations uniformly.
\[
\mathbb{P}_{S\sim\mu^{\otimes n}}\!\left(
\sup_{f\in\mathcal{F}}\left|P_n f-Pf\right|
\ge 2\mathfrak{R}_n(\mathcal{F})+\varepsilon
\right)
\le \exp\!\left(-\frac{n\varepsilon^2}{2b^2}\right).
\]
StatsMLlib/LearningTheory/UniformDeviation/Bounds.lean · theorem uniform_deviation_tail_bound_separable_of_pos
Finite-sample guarantee for linear regression
For a \(d\)-dimensional linear class and injective design, least squares achieves a nonasymptotic rate of order \(\sigma^2 d/n\).
\[
\exists\,C_1,C_2>0:\qquad
\mathbb{P}_{w\sim\mathcal{N}(0,I_n)}\!\left(
\left\lVert \widehat{f}(w)-f^\star\right\rVert_n^2
\le C_1\frac{\sigma^2 d}{n}
\right)
\ge 1-\exp(-C_2d).
\]
StatsMLlib/Statistics/Regression/LeastSquares/Linear/MinimaxRate.lean · theorem LeastSquares.linear_minimax_rate
Gaussian logarithmic Sobolev inequality
\[
\operatorname{Ent}_{\gamma_n}(g^2)
\le 2\int_{\mathbb{R}^n}
\left\lVert \nabla g(x)\right\rVert_2^2
\,\mathrm{d}\gamma_n(x).
\]
StatsMLlib/Probability/Concentration/LogSobolev/GaussianTensorization.lean · theorem GaussianLSI.gaussian_logSobolev_W12_pi
Expected supremum of a sub-Gaussian process
For an anchored sub-Gaussian process indexed by a totally bounded set of diameter at most \(D\), the expected supremum is controlled by metric entropy.
\[
\mathbb{E}_{\mu}\!\left[\sup_{t\in s} X_t\right]
\le 12\sqrt{2}\,\sigma
\int_{0}^{D}\sqrt{\log \mathcal{N}(s,d,\varepsilon)}\,\mathrm{d}\varepsilon .
\]
StatsMLlib/Probability/Process/Dudley.lean · theorem dudley