Book map · Roman Vershynin
An Introduction with Applications in Data Science, 2nd ed. (Cambridge University Press, 2026).
StatsMLlib formalizes a connected path through concentration, high-dimensional random vectors and matrices, Gaussian methods, empirical processes, and chaining.
Coverage note. Each entry consolidates material with a direct formal counterpart in StatsMLlib. It does not assert complete formalization of the chapter.
Chapter-level overlap
The map follows the chapter organization of the second edition.
Formalized coverage includes exponential-moment and cumulant methods, Hoeffding’s lemma and inequality, Chernoff bounds, sub-Gaussian scales and tails, independent sub-Gaussian linear combinations, finite maximal inequalities, Bernstein-type concentration from local cumulant control, and a bounded-density small-ball bound.
Projection-based sub-Gaussian vector scales, covariance and isotropy through second moments, standard Gaussian and Rademacher models, and concentration of norms and quadratic forms provide the chapter’s formalized random-vector toolkit.
The chapter-level development combines singular values and Courant–Fischer min–max principles; covering, packing, and Euclidean nets; Eckart–Young–Mirsky, Weyl, and Davis–Kahan perturbation results; operator-norm bounds for independent sub-Gaussian entries; and two-sided singular-value bounds for matrices with isotropic sub-Gaussian rows.
Gaussian Poincaré and logarithmic Sobolev inequalities, tensorization, the Herbst argument, and dimension-free concentration for Lipschitz functions cover the chapter’s Gaussian concentration theory. Matrix concentration is represented by Loewner-order calculus, Lieb concavity, trace-MGF recursion, and matrix Bernstein.
Hanson–Wright concentration for quadratic forms of independent centered sub-Gaussian variables is formalized together with Rademacher symmetrization machinery for empirical processes.
Sub-Gaussian processes, canonical increment metrics, finite-class maximum bounds, and countable and separable supremum infrastructure formalize the process-level foundations used by later chaining arguments.
Covering and packing numbers, metric entropy, dyadic chaining, separability reductions, Dudley’s entropy integral, its truncated form, and empirical Rademacher chaining give a unified formal treatment of the chapter.