Chapter 2
Basic inequalities
Exponential moments and cumulants, Chernoff’s method, Hoeffding’s lemma and inequality, independent sub-Gaussian sums, finite maximal inequalities, and Bernstein-type concentration form the chapter’s formalized core.
Book map · Boucheron · Lugosi · Massart
Concentration Inequalities
A Nonasymptotic Theory of Independence (Oxford University Press, 2013).
StatsMLlib connects exponential-moment bounds, variance inequalities, entropy methods, logarithmic Sobolev inequalities, and empirical-process suprema in a reusable Lean development.
Coverage note. Each entry summarizes material with a direct formal counterpart in StatsMLlib; it is not a claim of complete chapter coverage.
Chapter-level overlap
Formalized Coverage
The map follows the chapter organization of the published book.
Chapter 3
Bounding the variance
Coordinatewise conditional expectations, variance decompositions, the Efron–Stein inequality, and Gaussian Poincaré inequalities formalize the principal variance-control mechanisms.
Chapter 4
Basic information inequalities
Entropy definitions, variational and dual formulations, conditional decomposition, Han-type inequalities, and subadditivity under product measures supply the formal information-theoretic infrastructure.
Chapter 5
Logarithmic Sobolev inequalities
The two-point inequality, Bernoulli tensorization, passage to Gaussian space, Gaussian logarithmic Sobolev and Poincaré inequalities, the Herbst argument, and Lipschitz Gaussian concentration are formalized as one connected development.
Chapter 13
Expected suprema of empirical processes
Finite-class maxima, Rademacher symmetrization, Massart’s lemma, covering and packing, metric-entropy chaining, and Dudley-type bounds formalize the expected-supremum tools used in empirical-process analysis.