Statistics

Motivation

In high-dimensional linear regression one observes $y = X\beta^* + w \in \mathbb R^n$ with a design matrix $X\in\mathbb R^{n\times M}$ whose number of columns $M$ may far exceed the sample size $n$. The two standard estimators of a sparse $\beta^*$, the Lasso (Tibshirani, 1996) and the Dantzig selector (Candès and Tao, 2007), both come with error bounds of order $s\log M/n$ for an $s$-sparse $\beta^*$, but only under a condition on $X$: since $X$ has a non-trivial kernel when $M>n$, some form of restricted invertibility is unavoidable.

Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 2009) introduced the restricted eigenvalue (RE) condition, which asks for invertibility of $X$ only on a cone of approximately sparse vectors. It is weaker than the conditions used before it and has since become the default assumption in the sparse-estimation literature. Section 4 of the paper relates RE to the earlier conditions:

• 2005–2007: Candès and Tao (arXiv:math/0506081) analyse the Dantzig selector under a uniform uncertainty principle involving restricted eigenvalues and restricted correlations of $X$; the condition $\phi_{\min}(2s)>\theta_{s,2s}$ is Assumption 1 below with $c_0=1$.
• 2006–2009: Meinshausen and Yu (arXiv:math/0605584) analyse the Lasso under a lower bound on sparse eigenvalues of order $s\log n$.
• 2006: Donoho, Elad and Temlyakov (doi:10.1109/TIT.2005.860430) use mutual coherence for sparse recovery; 2007: Bunea, Tsybakov and Wegkamp (doi:10.1214/07-EJS008) use coherence-type conditions for the Lasso.
• 2009: Bickel, Ritov and Tsybakov show (Lemma 4.1 and Section 4) that each of these conditions implies RE.

This mission formalizes those implications.

Setting

Fix integers $n\ge1$ and $M\ge2$ and a matrix $X\in\mathbb R^{n\times M}$ with columns $x_1,\dots,x_M$. The Gram matrix is $\Psi_n = X^TX/n$. For $\delta\in\mathbb R^M$ and $J\subseteq\{1,\dots,M\}$, $\delta_J$ is the vector equal to $\delta$ on $J$ and $0$ off $J$; $|\cdot|_1$, $|\cdot|_2$ are the $\ell_1$ and Euclidean norms; $\mathcal M(\delta)$ is the number of non-zero coordinates of $\delta$; $J_0^c$ is the complement of $J_0$.

The cone condition for $J_0$ and $c_0>0$ is

$$|\delta_{J_0^c}|_1\le c_0\,|\delta_{J_0}|_1. \tag{4.1}$$

Assumption RE$(s,c_0)$ holds with constant $\kappa>0$ if $|X\delta|_2\ge\kappa\sqrt n\,|\delta_{J_0}|_2$ for every $J_0$ with $|J_0|\le s$ and every $\delta\ne0$ satisfying (4.1). For $m\ge s$, let $J_1$ be a set of $m$ indices outside $J_0$ carrying the $m$ largest $|\delta_j|$, and $J_{01}=J_0\cup J_1$; Assumption RE$(s,m,c_0)$ replaces $|\delta_{J_0}|_2$ by $|\delta_{J_{01}}|_2$.

The restricted eigenvalues are $\phi_{\min}(u)$ and $\phi_{\max}(u)$, the minimum and maximum of $x^T\Psi_nx/|x|_2^2$ over $x$ with $1\le\mathcal M(x)\le u$. The restricted correlations $\theta_{m_1,m_2}$ are the maximum of $c_1^TX_{I_1}^TX_{I_2}c_2/(n|c_1|_2|c_2|_2)$ over disjoint index sets $I_1,I_2$ with $|I_i|\le m_i$ and non-zero $c_i\in\mathbb R^{I_i}$. Two constants are attached to them:

$$\kappa_1(s,c_0)=\sqrt{\phi_{\min}(2s)}\Big(1-\frac{c_0\theta_{s,2s}}{\phi_{\min}(2s)}\Big),\qquad \kappa_2(s,m,c_0)=\sqrt{\phi_{\min}(s+m)}\Big(1-c_0\sqrt{\tfrac{s\,\phi_{\max}(m)}{m\,\phi_{\min}(s+m)}}\Big).$$

$P_{01}$ is the orthogonal projector in $\mathbb R^n$ onto the span of the columns $x_j$, $j\in J_{01}$.

Formalization targets

Goal: Lemma 4.1 (ii)

For integers $1\le s\le M/2$, $m\ge s$, $s+m\le M$ and $c_0>0$, if Assumption 2 $m\,\phi_{\min}(s+m)>c_0^2\,s\,\phi_{\max}(m)$ holds, then $\kappa_2(s,m,c_0)>0$, RE$(s,c_0)$ and RE$(s,m,c_0)$ hold with constant $\kappa_2(s,m,c_0)$, and for every $J_0$ with $|J_0|\le s$ and every $\delta$ satisfying (4.1)

$$\frac1{\sqrt n}|P_{01}X\delta|_2\ \ge\ \kappa_2(s,m,c_0)\,|\delta_{J_{01}}|_2 .$$

Assumption 2 involves no correlations, only extreme eigenvalues of small principal submatrices of $\Psi_n$.

Lemma 4.1 (i)

For $1\le s\le M/2$ and $c_0>0$, Assumption 1 $\phi_{\min}(2s)>c_0\theta_{s,2s}$ implies the same conclusions with $m=s$ and constant $\kappa_1(s,c_0)$.

Coherence-type conditions (Section 4)

For $1\le s\le M$ and $c_0>0$, each of

$$\phi_{\min}(s)>2c_0\theta_{s,1}\sqrt s,\qquad \phi_{\min}(s)>2c_0\theta_{1,1}s,\qquad \operatorname{diag}\Psi_n=1\ \text{and}\ \theta_{1,1}<\frac1{(1+2c_0)s}$$

(Assumptions 3, 4, 5) implies RE$(s,c_0)$, with the constants $\kappa^2=\phi_{\min}(s)-2c_0\theta_{s,1}\sqrt s$, $\phi_{\min}(s)-2c_0\theta_{1,1}s$ and $1-(1+2c_0)\theta_{1,1}s$ respectively.

The milestones are the steps of the proof in Appendix A — the projection inequality (A.1), the block bound (A.2), the shelling bound (A.3), the Candès–Tao correlation bound used for part (i) — followed by part (i) and the three coherence-type implications.

Significance

RE$(s,c_0)$ with $c_0=3$ and $c_0=1$ is the hypothesis of the paper's prediction and $\ell_1$ bounds for the Lasso and the Dantzig selector (Theorems 5.1, 6.1, 7.1, 7.2), and RE$(s,m,c_0)$ is the hypothesis of its $\ell_p$ bounds. Assumptions 1–5 are stated through quantities that are standard in compressed sensing and random matrix theory, so known bounds for $\phi_{\min}$, $\phi_{\max}$ and $\theta$ of random designs transfer, through this mission's theorems, to every result stated under RE. Lemma 4.1 also shows that RE is weaker than the Candès–Tao condition used for the Dantzig selector.

The results are proved in the paper; parts of Lemma 4.1's proof (the correlation bound for part (i)) are cited from Candès and Tao without proof. None of these results is formalized: the platform has pairwise-incoherence and restricted-nullspace statements from Wainwright's textbook (a different conclusion and normalization) and restricted isometry definitions, but neither restricted eigenvalues $\phi_{\min}(u),\phi_{\max}(u)$, restricted correlations $\theta_{m_1,m_2}$, nor the RE condition in this form.

Difficulty

The naive attempt to bound $|X\delta|_2$ from below splits $\delta=\delta_{J_0}+\delta_{J_0^c}$ and applies an eigenvalue bound to each part. This fails: $\delta_{J_0^c}$ can have up to $M-s$ non-zero coordinates, and no condition on $s$- or $2s$-sparse submatrices controls $|X\delta_{J_0^c}|_2$ directly. The cone condition bounds only the $\ell_1$ norm of $\delta_{J_0^c}$, while eigenvalue conditions speak about $\ell_2$ norms of sparse vectors; bridging the two with the right constant $\sqrt{s/m}$, and keeping track of how the leading block $J_{01}$ interacts with the rest through the projector $P_{01}$, is where the work lies. For part (i), the interaction between disjoint sparse blocks has to be controlled by $\theta_{s,2s}$ rather than by $\phi_{\max}$.

Formalization scope

• Representation. $X$ is Matrix (Fin n) (Fin M) ℝ; vectors are Fin M → ℝ and Fin n → ℝ; $|X\delta|_2=(\sum_i (X\delta)_i^2)^{1/2}$. The projector $P_{01}$ is Mathlib's orthogonal projection on EuclideanSpace ℝ (Fin n) onto the span of the columns indexed by $J_{01}$.
• RE through a witness. RE X s c0 κ asserts the RE inequality with constant $\kappa$ for all admissible $J_0$ and $\delta$. The paper's $\kappa(s,c_0)$ is the largest such $\kappa$ (the minimum is attained), so "RE holds with $\kappa(s,c_0)\ge\kappa_2$" is exactly "$\kappa_2>0$ is a witness". This avoids a real infimum over an empty set when $J_0=\emptyset$.
• Ties. Every admissible choice of $J_1$ (the $m$ largest $|\delta_j|$ outside $J_0$) is quantified over.
• Restricted eigenvalues and correlations are sInf/sSup over nonempty bounded sets (a basis vector for $\phi$; two disjoint singletons for $\theta$, since $M\ge2$), so they equal the paper's attained min/max. $u$, $s$, $m$ are natural numbers; $s\le M/2$ is written $2s\le M$.
• Corrections of the printed statement. (1) Lemma 4.1 says the RE assumptions "hold with $\kappa(s,c_0)=\kappa(s,m,c_0)=\kappa_2(s,m,c_0)$" (and likewise with $\kappa_1$); the proof gives only the lower bound, and the lower bound is what is stated. (2) The paper calls $P_{01}$ "the projector in $\mathbb R^M$"; it acts on $\mathbb R^n$. (3) The Section 4 claims "Assumption 3/4/5 implies RE$(s,c_0)$" are stated with the explicit constant produced by the displayed argument, a labelled strengthening. (4) The Candès–Tao bound is stated with the hypotheses the proof uses: the blocks are disjoint, of sizes at most $s$ and $2s$, and $\phi_{\min}(2s)>0$.
• Ruling out trivializations. RE quantifies over all $J_0$ with $|J_0|\le s$ and all non-zero $\delta$ in the cone, and bounds the full $|X\delta|_2$, not $|X\delta_{J_0}|_2$; no hypothesis restricts $X$ beyond the stated assumptions. The hypotheses are satisfiable: for $n=M=4$, $X=2I$ (so $\Psi_n=I$), $s=1$, $m=2$, $c_0=1$, Assumption 2 reads $2>1$.
• Infrastructure. A sparse-vector library (restriction, support, sorting coordinates into blocks) and facts about orthogonal projections onto column spans are needed; both are reusable for the other missions of this series and for compressed-sensing results. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. arXiv:0801.1095v3. https://arxiv.org/abs/0801.1095
• E. Candès, T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6), 2313–2351, 2007. https://arxiv.org/abs/math/0506081
• N. Meinshausen, B. Yu, Lasso-type recovery of sparse representations for high-dimensional data, Ann. Statist. 37(1), 246–270, 2009. https://arxiv.org/abs/math/0605584
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Sparsity oracle inequalities for the Lasso, Electron. J. Statist. 1, 169–194, 2007. https://doi.org/10.1214/07-EJS008
• D. L. Donoho, M. Elad, V. N. Temlyakov, Stable recovery of sparse overcomplete representations in the presence of noise, IEEE Trans. Inform. Theory 52(1), 6–18, 2006. https://doi.org/10.1109/TIT.2005.860430

Motivation

The book is discriminative almost throughout: it learns predictors, not distributions, following Vapnik's advice not to solve a more general problem as an intermediate step. Chapter 24 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), presents the generative alternative: assume a parametric form for the data distribution and estimate its parameters. The maximum likelihood principle is introduced on Bernoulli and Gaussian samples, shown to be empirical risk minimization for the log-loss, and analyzed through the decomposition of the true log-loss risk into a relative entropy plus an entropy (24.5), which explains both its consistency under a correct model and its overfitting on small samples. Naive Bayes and linear discriminant analysis show how generative assumptions reduce the number of parameters and make the Bayes classifier linear (24.8). The chapter's main theorem concerns the Expectation-Maximization algorithm of Dempster, Laird and Rubin for latent-variable models such as Gaussian mixtures: EM never decreases the log-likelihood (Theorem 24.3), because it is an alternate maximization of a lower bound $G(Q, \theta)$ that touches the likelihood at the posterior (Lemma 24.2). The chapter ends with Bayesian reasoning and the rule of succession.

Setting

A Bernoulli sample $S = (x_1, \dots, x_m)$ has log-likelihood $L(S;\theta) = \log(\theta)\sum_i x_i + \log(1-\theta)\sum_i(1-x_i)$ and estimator $\hat\theta = \frac1m\sum_i x_i$ (24.1); a Gaussian sample has $L(S;(\mu,\sigma)) = -\frac1{2\sigma^2}\sum_i(x_i-\mu)^2 - m\log(\sigma\sqrt{2\pi})$. The log-loss is $\ell(\theta, x) = -\log P_\theta[x]$ (24.4); on a finite domain, $D_{RE}[P\|Q] = \sum_x P[x]\log(P[x]/Q[x])$ and $H(P) = \sum_x P[x]\log(1/P[x])$. A latent-variable model is a parametric joint $P_\theta[X = x, Y = y]$, $y \in [k]$, with $L(\theta) = \sum_i\log\sum_y P_\theta[X = x_i, Y = y]$; $F(Q,\theta) = \sum_i\sum_y Q_{i,y}\log P_\theta[X = x_i, Y = y]$, $G(Q,\theta) = F(Q,\theta) - \sum_i\sum_y Q_{i,y}\log Q_{i,y}$ over the set $\mathcal{Q}$ of row-stochastic matrices, and EM alternates the E-step $Q^{(t+1)}_{i,y} = P_{\theta^{(t)}}[Y = y \mid X = x_i]$ (24.10) with the M-step $\theta^{(t+1)} \in \operatorname{argmax}_\theta F(Q^{(t+1)}, \theta)$ (24.11).

Formalization targets

Goal: Theorem 24.3

For a positive parametric joint $P_\theta[X = x, Y = y]$, a sample $x_1, \dots, x_m$, and any run $\theta^{(0)}, \theta^{(1)}, \dots$ of EM (each M-step returning some maximizer of $F(Q^{(t+1)}, \cdot)$), the log-likelihood never decreases:

$$L(\theta^{(t+1)}) \ge L(\theta^{(t)}) \quad\text{for all } t.$$

Milestones

Equation (24.2) (Hoeffding for the Bernoulli estimator); the Gaussian maximum likelihood estimates of §24.1.1; Equation (24.5) (the risk decomposition $D_{RE}[P\|P_\theta] + H(P)$); Equation (24.8) (the LDA log-likelihood ratio is affine); Lemma 24.2 (EM as alternate maximization of $G$, with $G(Q, \theta) \le L(\theta)$ and equality at the posterior). Further items: Gibbs' inequality, the Bernoulli maximum likelihood estimator (24.1)/(24.3), Exercise 1 (the biased variance estimate), Equation (24.6), the overfitting example of §24.1.3, Exercise 3 / (24.14), the weighted-centroid M-step (24.13), and the rule of succession of §24.5.

Significance

Theorem 24.3 is the guarantee that makes EM a sensible algorithm: it does not find the maximum likelihood estimate, but it climbs monotonically, and Lemma 24.2 identifies why, the E-step chooses the tightest lower bound $G(Q, \cdot)$ at the current parameter and the M-step maximizes it. This variational view underlies a large part of modern latent-variable inference. Equation (24.5) is the information-theoretic content of maximum likelihood: the true risk is the entropy of the data plus the relative entropy to the model, so the best parameter is a projection of the data distribution onto the model class, and Gibbs' inequality is what makes that projection meaningful. The Bernoulli and Gaussian computations are the standard first examples, and Equation (24.8) is the reason linear classifiers appear in generative modeling. On the platform, the mission adds the relative entropy on finite domains, the EM objects, and Gaussian-integral identities that later probabilistic work can reuse.

Difficulty

The Bernoulli and Gaussian maximum likelihood facts are calculus, but as global maximization statements they need the concavity of $\log$ and an explicit completion of squares rather than the book's stationary-point argument; the Gaussian case reduces to minimizing $\sigma \mapsto \frac{m\hat\sigma^2}{2\sigma^2} + m\log\sigma$. Equation (24.5) is a finite-sum identity; Gibbs' inequality is Jensen for $\log$ with the equality case, or the elementary $\log t \le t - 1$. Lemma 24.2 is Jensen's inequality applied row by row to $\sum_y Q_{i,y}\log(P_\theta[X = x_i, Y = y]/Q_{i,y})$, with care at entries $Q_{i,y} = 0$, where the convention $0\log 0 = 0$ is exactly Lean's junk value; Theorem 24.3 chains the lemma's three parts as the book does. The Gaussian expectation identities (Exercise 1 and (24.6)) require the moments of gaussianReal and Fubini over the product law. Hoeffding's inequality (24.2) is Mission II's Theorem for Bernoulli variables; the overfitting example is the inequality $\log(1-\theta) \ge -2\theta$ on $[0, 1/2]$. The rule of succession is a Beta-function identity provable by integration by parts.

Formalization scope

Parametric families are functions from a parameter type to real-valued probabilities or densities, following the book's convention (p. 344) that $P[X = x]$ denotes either; no measure-theoretic densities are needed except in the two Gaussian-integral items, which use gaussianReal and the i.i.d. law of Mission I, and in the two Bernoulli probability items, which use the Bernoulli law of Mission XIV. Lean's log 0 = 0 is handled explicitly: the EM items assume a positive joint, since with junk logarithms Theorem 24.3 is false (the M-step could pick a parameter with a zero component and inflated $F$), while the entropy terms $Q\log Q$ use the convention $0\log 0 = 0$ that the book intends; the Bernoulli maximum likelihood statement ranges over $\theta \in (0,1)$; the log-loss decomposition and Gibbs' inequality take the second distribution positive. The M-step is a predicate ("some maximizer"), so Assumption 24.1 is not modeled, and an EM run is any sequence of such steps. The Gaussian maximum likelihood statement requires a nonconstant sample, without which the likelihood is unbounded; the overfitting example is stated for $\theta^\star \le 1/2$, the range on which the book's inequality $(1-\theta)^m \ge e^{-2\theta m}$ holds. Equation (24.8) is stated as a matrix identity for any symmetric $M$ in place of $\Sigma^{-1}$; the soft k-means M-step is stated as the weighted-centroid minimization it amounts to.

Not stated: Naive Bayes (24.7), which is a rewriting of Bayes' rule; the mixture density itself and the E-step formula (24.12); the Bayesian derivations (24.16) and maximum a posteriori estimation; Exercise 2.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 24. doi:10.1017/CBO9781107298019
• A. P. Dempster, N. M. Laird, D. B. Rubin, Maximum likelihood from incomplete data via the EM algorithm, Journal of the Royal Statistical Society B 39(1), 1977. doi:10.1111/j.2517-6161.1977.tb01600.x
• C. F. J. Wu, On the convergence properties of the EM algorithm, Annals of Statistics 11(1), 1983. doi:10.1214/aos/1176346060
• T. M. Cover, J. A. Thomas, Elements of Information Theory, 2nd ed., Wiley, 2006. doi:10.1002/047174882X
• C. M. Bishop, Pattern Recognition and Machine Learning, Springer, 2006.

Motivation

Chapter 5 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), asks what happens to PAC learning when the labels are unreliable. In the classification noise model of Angluin and Laird, each label returned by the oracle is flipped independently with a fixed probability $\eta < 1/2$. The algorithms of Chapter 1 collapse at once: the elimination algorithm deletes a correct literal on the strength of a single mislabeled example, and the tightest-fit rectangle may not exist. The chapter's remedy is to learn from statistics: an algorithm that forms its hypothesis only from estimates of probabilities of simple events is insensitive to occasional wrong labels. Kearns's statistical query model makes this precise, replacing the example oracle by an oracle that returns the probability of any predicate of a labeled example to within a tolerance, and the main theorem (5.3) shows that every class learnable from statistical queries is PAC learnable in the presence of classification noise. The proof rests on a single identity, Equation (5.2), that expresses the true value of a statistical query in terms of three quantities that can each be estimated from noisy examples, and on the observation that a hypothesis's disagreement with the noisy label is an affine function of its true error, which lets the best of several candidate hypotheses be recognized without clean data.

Setting

The framework is that of Mission I. The noisy example law is that of $(x, b)$ with $x \sim D$ and $b = c(x)$ flipped with probability $\eta$. A statistical query is a predicate $\chi$ of a labeled example with value $P_\chi = \Pr_{x \sim D}[\chi(x, c(x)) = 1]$. The inputs split into $X_1$, where the label matters to $\chi$, and $X_2$, where it does not; $p_1 = D(X_1)$ and $D_1$ is $D$ conditioned on $X_1$. For conjunctions over $\{0,1\}^n$, $p_0(z)$ is the probability that a literal $z$ is set to $0$ and $p_{01}(z)$ the probability that it is $0$ on a positive example; $z$ is significant if $p_0(z) \ge \epsilon/8n$ and harmful if $p_{01}(z) \ge \epsilon/8n$.

Formalization targets

Goal: Equation (5.2)

For $0 \le \eta < 1/2$ and every statistical query $\chi$,

$$P_\chi = p_1 \cdot \frac{\Pr_{EX^\eta_{CN}(c, D_1)}[\chi = 1] - \eta}{1 - 2\eta} + \Pr_{EX^\eta_{CN}(c, D)}[\chi = 1 \wedge x \in X_2],$$

the probabilities on the right being taken under the noisy oracle.

Milestones

The §5.2 analysis behind Theorem 5.2 (the conjunction of all significant, non-harmful literals has error at most $\epsilon/2$); the product estimate bound of p. 115 ($AB - 2\tau' \le \hat A\hat B \le AB + 3\tau'$); the identity of p. 117 ($\gamma_h = \eta + (1 - 2\eta)\,\mathrm{error}(h)$).

Significance

Equation (5.2) is the entire mechanism of noise-tolerant learning in the statistical query model: the noisy oracle cannot be de-noised example by example, but the probability of any predicate can be recovered exactly from noisy probabilities, because on the inputs where the label matters the noise acts as a known affine contraction and on the others it acts not at all. Together with the p. 117 identity, which turns hypothesis selection into a comparison of noisy disagreement rates, and the Chernoff bounds of Mission IV, it yields Theorem 5.3 and hence noise-tolerant algorithms for every class the book has learned so far (conjunctions, decision lists, $k$-CNF). The §5.2 analysis is the first statistical-query algorithm and shows the pattern: a hypothesis defined by thresholds on a few probabilities, with enough slack between the thresholds that estimates suffice. None of this is machine-checked. The formalization fixes the noisy example law on the platform's sample framework and proves the exact identities on which the noise-tolerant simulation depends.

Difficulty

Equation (5.2) is a computation with the pushforward of a product measure: one must express the noisy law on $X_1$ as a mixture of the clean law and its label-flipped image, solve the affine relation for the clean probability, and combine with the restriction to $X_2$, where the flipped and unflipped labels give the same value of $\chi$; the degenerate case $D(X_1) = 0$, in which the conditional measure is zero and the first term vanishes, must be handled separately. The p. 117 identity is the same computation without the split. The §5.2 analysis is two union bounds over the $2n$ literals after the observation that a literal of the target is never harmful and that a literal of the hypothesis is never insignificant. The product lemma is elementary arithmetic with a case split at $A < \tau'$.

Formalization scope

The noisy oracle is a measure on labeled examples obtained by mapping the product of $D$ and a Bernoulli($\eta$) coin; the conditional $D_1$ is Mathlib's conditional measure; queries are arbitrary measurable predicates of a labeled example, with no tolerance or query-count bookkeeping. Theorem 5.3 itself, the definitions of efficient learnability from statistical queries (Definition 14) and of efficient noisy PAC learnability (Definition 13), Theorem 5.1, Theorem 5.2 as a statement about an algorithm with oracle access, and Corollary 5.4 are not stated: they quantify over query algorithms and their running times, for which this series has no model; the mission carries their exact probabilistic content. The error-propagation analysis of §5.4.2–5.4.3 with tolerance $\tau/27$ and the guessing resolution $\Delta$ is not stated beyond the product lemma, since the factor $1/(1-2\eta)$ is not in $[0,1]$ and the book's constant does not account for it. Hypotheses: $0 \le \eta < 1/2$ for the decomposition, $0 \le \eta \le 1$ for the disagreement identity, $\epsilon > 0$ for the conjunction analysis, all reals in $[0,1]$ for the product lemma.

Trivializing readings are excluded: the decomposition is an exact identity for every measurable query, and the conjunction bound is for the exact thresholds $\epsilon/8n$ with the union bound's $\epsilon/2$. Welcome contributions: the mixture representation of the noisy law, the restriction of a pushforward to $X_2$, and the two union bounds.

Selected references

• M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 5. doi:10.7551/mitpress/3897.001.0001
• D. Angluin, P. Laird, Learning from noisy examples, Machine Learning 2(4), 1988. doi:10.1007/BF00116829
• M. Kearns, Efficient noise-tolerant learning from statistical queries, Journal of the ACM 45(6), 1998. doi:10.1145/293347.293351
• M. Kearns, M. Li, Learning in the presence of malicious errors, SIAM Journal on Computing 22(4), 1993. doi:10.1137/0222052

Motivation

Chapter 4 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), asks whether the PAC model's demand for arbitrarily small error and confidence is essential. A weak learning algorithm need only, with some fixed positive probability, output a hypothesis that beats random guessing by a fixed margin. Schapire's theorem, the chapter's main result, says that this apparently much weaker requirement is equivalent to the original one: any weak learner can be converted, by running it on carefully filtered distributions and combining its hypotheses by majority votes, into a strong learner. The construction is boosting, which became one of the most influential ideas in machine learning. The chapter proves the equivalence in two steps. Boosting the confidence is elementary: run the learner several times and validate. Boosting the accuracy is the substance: a modest procedure that combines three hypotheses, each with error at most $\beta$ on its own distribution, into a majority with error at most $g(\beta) = 3\beta^2 - 2\beta^3 < \beta$, applied recursively until the error is driven below the target. The Chernoff bounds of the Appendix, the book's workhorse for estimating probabilities from samples, are what makes the validation steps rigorous.

Setting

The framework is that of Mission I. A class $C$ is weakly learnable using $H$ if for some advantage $\gamma > 0$, confidence $\delta_0 > 0$ and sample size $m$, an algorithm outputs hypotheses in $H$ that, for every target in $C$ and every distribution, have error at most $1/2 - \gamma$ with probability at least $\delta_0$; the algorithm's prediction $L(S)(x)$ is a measurable function of the sample and the instance together, as it is for every algorithm. Given a hypothesis $h_1$, the filtered distribution $D_2$ gives weight $1/2$ to the instances on which $h_1$ errs and $1/2$ to those on which it is correct, preserving relative weights within each part, and $D_3$ is $D$ conditioned on $h_1 \ne h_2$; the modest procedure outputs $\mathrm{majority}(h_1, h_2, h_3)$. Ternary majority trees over $H$ are the closure of $H$ under the majority of three. For confidence boosting, $k$ independent samples yield $k$ hypotheses, and a fresh sample selects the one with the fewest mistakes. Bernoulli trials are $m$ independent coin flips with success probability $p$.

Formalization targets

Goal: Theorem 4.9

If $C$ is weakly PAC learnable using measurable hypotheses in $H$, then $C$ is PAC learnable using the class of ternary majority trees with leaves from $H$: for all $\epsilon, \delta \in (0, 1/2)$ some sample size and some algorithm outputting majority trees achieve error at most $\epsilon$ with probability at least $1 - \delta$, for every target in $C$ and every distribution.

Milestones

Theorem 9.2 (the additive and multiplicative Chernoff bounds); the two facts of §4.2 behind confidence boosting (independent runs all fail with probability at most $(1 - \delta_0)^k$; the fewest-mistakes selection loses at most $\gamma$ with probability at least $1 - 2k e^{-m\gamma^2/2}$); Lemma 4.1 (the modest procedure: error at most $g(\beta)$).

Significance

Theorem 4.9 is one of the landmark results of learning theory: it shows that the PAC model has no intermediate strength, that Occam learning, weak learning and strong learning coincide, and that the resources of a strong learner can be bounded polylogarithmically in $1/\epsilon$ in memory and hypothesis size. Its constructive proof is the first boosting algorithm, ancestor of AdaBoost and of gradient boosting. Lemma 4.1 is the analytic core, a clean inequality about three hypotheses and three distributions in which the filtered distribution is exactly calibrated so that $h_1$ has no advantage on it. The Chernoff bounds are the concentration inequalities invoked throughout the book, and their formalization on the product law of Bernoulli trials makes every later "estimate to within $\gamma$ with confidence $1 - \delta$" step reusable. None of these is machine-checked in this form; the boosting theorem in the sample-complexity sense is, to our knowledge, not formalized anywhere.

Difficulty

Lemma 4.1 is a computation with conditional measures: writing $\mathrm{error}_D$ of the majority as the weight of the instances on which $h_1$ and $h_2$ both err plus $\beta_3$ times the weight of their disagreement, mapping weights under $D_2$ back to $D$ by the factors $2(1 - \beta_1)$ and $2\beta_1$ (Equation (4.1)), and maximizing the resulting polynomial in $\beta_1, \beta_2, \beta_3, \gamma_1, \gamma_2$; the degenerate cases where a conditioning event is null must be handled separately. The Chernoff bounds require the exponential moment method on a finite product measure. The confidence-boosting facts are the product bound for independent blocks and Hoeffding plus a union bound. The goal is a genuine construction: from a large sample of $D$ one must simulate the recursive algorithm Strong-Learn, whose calls to the weak learner on filtered distributions are served by rejection sampling from the remaining examples, bound the depth of the recursion by the growth of $g^{-1}$ iterates (Lemma 4.2), bound the number of examples consumed at each node (Lemmas 4.3–4.7) and allocate the confidence over all the places the simulation can fail; then package the result as a deterministic function of a sample of fixed size. An alternative route is available: weak learnability with a fixed sample size forces a finite VC dimension (a class shattering a large set defeats any fixed-size learner on the uniform distribution over it), after which Theorem 3.3 gives a consistent strong learner; but its hypotheses lie in $C$, not in the majority trees over $H$, so it does not prove the stated conclusion.

Formalization scope

The weak-learning hypothesis is the book's with constants $\gamma, \delta_0$ in place of the inverse polynomials, which is what the definition says for a fixed class; hypotheses in $H$ are required to be measurable, and the weak learner jointly measurable in the sample and the instance, because Strong-Learn runs it on distributions filtered through its own earlier outputs and the analysis integrates over the earlier samples (for an arbitrary function the combined failure event need not be measurable, and outer-measure bounds on separate runs do not combine); the conclusion is the book's hypothesis class, the majority trees over $H$, built as an inductive predicate. Filtered distributions use Mathlib's conditional measure, so that a null conditioning event yields the zero measure; Lemma 4.1 is stated for $0 \le \beta \le 1/2$ and holds in those degenerate cases too. The confidence-boosting milestone states the two probabilistic facts rather than the composite algorithm, whose sample indexing across runs and validation is bookkeeping; the selection rule is any rule minimizing mistakes. Chernoff's bounds are stated with non-strict inequalities in the events, for $0 \le p \le 1$ and $0 < \gamma \le 1$. Running time, the recursion-depth and sample-size lemmas with unspecified constants (4.2–4.8), and Exercises 4.1–4.3 are not stated.

Trivializing readings are excluded: the weak-learning guarantee is uniform over all targets and distributions with an advantage strictly positive, the strong conclusion is for every $\epsilon, \delta$, and Lemma 4.1 requires all three error bounds on their respective distributions. Welcome contributions: Lemma 4.1 itself, the Hoeffding bound on the product law, and the rejection-sampling lemma that turns a sample of $D$ into a sample of a filtered distribution.

Selected references

• M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 4 and Chapter 9. doi:10.7551/mitpress/3897.001.0001
• R. E. Schapire, The strength of weak learnability, Machine Learning 5(2), 1990. doi:10.1007/BF00116037
• Y. Freund, Boosting a weak learning algorithm by majority, Information and Computation 121(2), 1995. doi:10.1006/inco.1995.1136
• W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58(301), 1963. doi:10.1080/01621459.1963.10500830
• H. Chernoff, A measure of asymptotic efficiency for tests of a hypothesis based on the sum of observations, Annals of Mathematical Statistics 23(4), 1952. doi:10.1214/aoms/1177729330

Motivation

The bandit processes that motivated the index theorem are sampling processes: an arm is a population from which one draws i.i.d. observations whose distribution has an unknown parameter, and each draw both earns something and teaches something. Chapter 7 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), develops the theory of such processes in the Bayesian setting: the state of the process is the current posterior for the parameter, continuing it samples the next value from the predictive distribution and moves to the new posterior. When the observations are themselves the rewards one has a reward process, the classical Bayesian multi-armed bandit; when the aim is to find as quickly as possible an individual whose measurement reaches a target $T$ (a compound active enough to warrant further testing, in the drug-screening problem from which the index theorem came) one has a target process, which is a job that completes when the target is reached. Two questions organize the chapter. When can the index be written down without any optimization, and when do symmetries of the model reduce the index to a function of fewer variables? The first is answered by the notion of a favourable prior (Section 7.3): if no run of observations below the target can raise the current probability of success, then the index is that probability, exactly, by Proposition 2.7. The second is answered by the invariance theorems of Section 7.4: a location parameter with a conjugate prior gives $\nu(\bar x, n) = \bar x + \nu(0, n)$, a scale parameter gives $\nu(\bar x, n) = \bar x\,\nu(1, n)$, and for target processes the target can be absorbed into the state, $\nu(\bar x, n, T) = \nu(\bar x - T, n, 0)$. These identities are what make the tables of Chapter 8 one-dimensional.

Setting

A sampling model consists of a likelihood $f(\cdot \mid \theta)$, a family of priors $\pi(\cdot \mid p)$ on the parameter indexed by the parameters $p$ of a conjugate family, and the Bayes update $p \mapsto p_x$ of those parameters after observing $x$; the family is conjugate if the posterior of $\pi(\cdot \mid p)$ given $X = x$ is $\pi(\cdot \mid p_x)$. The predictive distribution is $f(\cdot \mid p) = \int f(\cdot \mid \theta)\pi(d\theta \mid p)$. The reward process moves from $p$ to $p_x$ with $x \sim f(\cdot \mid p)$ and earns $r(p) = \int x f(x \mid p)dx$. The target process with target $T$ moves to the completion state $C$ if $x \ge T$ and to $p_x$ otherwise, earning the current probability of success $r(p) = f([T, \infty) \mid p)$, and $0$ in $C$. A state $p$ is favourable if $r(p_{x_1 \cdots x_m}) \le r(p)$ for every finite sequence of observations $x_i < T$. For the invariance theorems the parameters are $(\bar x, n)$ with the update $((n\bar x + x)/(n+1), n+1)$; $\mu$ is a location parameter of the likelihood if $f(\cdot \mid \mu + c)$ is $f(\cdot \mid \mu)$ shifted by $c$, and $\bar x$ is a location parameter of the prior family if $\pi(\cdot \mid \bar x + c, n)$ is $\pi(\cdot \mid \bar x, n)$ shifted by $c$; scale parameters are defined with $x \mapsto bx$, $b > 0$. The Gittins index is that of the Bandit Algorithms model on these chains.

Formalization targets

Goal: Theorem 7.9 (in the form of Corollary 7.10)

If $\mu$ is a location parameter of a reward process with a conjugate prior family in which $\bar x$ is a location parameter and the parameters update as the sample mean and count, then for every $n > 0$

$$r(\bar x + c, n) = r(\bar x, n) + c \quad\text{and}\quad \nu(\bar x, n) = \bar x + \nu(0, n),$$

under the standing assumptions that the observations have a mean and the discounted rewards of the chain are integrable.

Milestones

Proposition 7.4 (favourable state: $\nu = r$); Example 7.5 (Bernoulli target process, $\nu(\alpha, \beta) = \alpha/(\alpha + \beta)$); Example 7.6 (normal target process with known variance, $\nu(\bar x, n) = \Phi(\bar x (1 + n^{-1})^{-1/2})$ for $\bar x \ge 0$); Theorem 7.11 (scale parameter: $\nu(\bar x, n) = \bar x\,\nu(1, n)$); Theorem 7.17 (target process with a location parameter: $\nu(\bar x, n, T) = \nu(\bar x - T, n, 0)$).

Significance

Theorem 7.9 and its companions are the reason the Gittins index of the normal reward process is tabulated as a function of $n$ alone and that of the exponential process as a function of $n$ and one ratio; every computational method of Chapter 8 starts by reducing the state space with them. Proposition 7.4 is the source of every closed-form index in the book: it identifies the states in which sampling for information is worthless, so that the index collapses to the immediate expected reward, and Examples 7.5 and 7.6 show that for the Bernoulli target process this is every state and for the normal target process every state with a nonnegative posterior mean. The formalization gives the platform its first Bayesian sampling-process model, in which the state is a posterior and conjugacy is stated through the posterior kernel of the likelihood, and its first index identities on unbounded-reward chains, which is where the integrability assumptions of the Bandit Algorithms model do real work.

None of this is machine-checked. The invariance theorems are stated in the proper-prior form of the corollaries, with the model's symmetry as hypotheses, so that they apply to any conjugate family with the stated structure rather than to a particular density.

Difficulty

The invariance theorems require showing that the chain of parameters from the shifted (scaled) state is the image of the chain from the original state under the shift (scaling) of trajectories, which is an equivariance of the Ionescu–Tulcea construction with respect to a measurable bijection commuting with the kernel; that stopping times are carried to stopping times; that the discounted reward of a stopping time shifts by $c$ times the discounted time; and that the supremum of a nonempty bounded set of reals shifts and scales accordingly. Boundedness of the set of ratios is where the integrability assumption enters. Proposition 7.4 is the chain-level statement that all rewards along every trajectory from a favourable state are at most $r(p)$, which needs an induction on the trajectory law of the target chain, followed by the argument of Proposition 2.7. Example 7.6 needs the monotonicity of $\bar x_m (1 + 1/(n+m))^{-1/2}$ in the observations below the target, a small inequality, plus the Gaussian probability of a half-line as the current probability of success; Example 7.5 needs only that $\alpha/(\alpha + \beta + m)$ decreases.

Formalization scope

The sampling model is a structure with Markov likelihood and prior kernels and a jointly measurable update; the predictive distribution is the kernel composition; conjugacy is an almost-everywhere identity between Mathlib's posterior of the likelihood with respect to the prior and the prior at the updated parameters, and is carried as a hypothesis of the invariance theorems and of Proposition 7.4 so that their subject is the Bayesian process. For the parameters $(\bar x, n)$ it is required on $n > 0$ only (IsConjugateOn): a proper prior has $n > 0$, and conjugacy at every $(\bar x, n) \in \mathbb{R}^2$ is impossible with a location parameter, since at $n = -1$ the update divides by zero and sends every observation to one state, which made the first draft's location theorems vacuous. The chains are built with Kernel.map of product kernels, so their measurability is structural, and the target process lives on P ⊕ Unit with the completion state absorbing. The book's improper priors are replaced by proper conjugate families with the location or scale structure of Corollaries 7.10 and 7.12, as those corollaries do; the discrete-time correction factor of Section 2.8 is not applied since it cancels in every identity stated. The two examples are built directly from a uniform or Gaussian seed with the transition probabilities the book computes (the beta and normal posterior computations of Exercise 7.1 are not formalized). Hypotheses: $a \in (0, 1)$; integrable observations and L&S Assumption 35.6 for the reward processes; $n > 0$ for the invariance theorems and $\bar x > 0$ for the scale theorem; $\alpha, \beta > 0$; $\bar x \ge 0$ and $n > 0$ for the normal example.

Trivializing readings are excluded: the indices are the genuine suprema of the Bandit Algorithms definition with integrable rewards, the update rule is the book's and not a free parameter, and the favourability condition ranges over all finite observation sequences. Welcome contributions: the equivariance of the trajectory measure under a state bijection commuting with the kernel, the transport of stopping times, and the reward bound along the target chain from a favourable state.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 7. doi:10.1002/9780470980033
• J. C. Gittins, D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani, ed.), North-Holland, 1974.
• D. M. Jones, Search Procedures for Industrial Chemical Research, PhD thesis, University of Wales, 1975.
• H. Raiffa, R. Schlaifer, Applied Statistical Decision Theory, Harvard University Press, 1961.
• T. S. Ferguson, Mathematical Statistics: A Decision Theoretic Approach, Academic Press, 1967.
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapters 34–35. doi:10.1017/9781108571401

Motivation

Reinforcement learning formalizes a scenario supervised learning cannot: an agent that actively interacts with an environment, choosing actions that change both the state it observes next and the reward it receives, rather than passively receiving an i.i.d. labeled sample. Every practical treatment of this scenario — from classical dynamic programming to modern deep reinforcement learning — is built on the Markov decision process (MDP), a model in which the effect of an action depends only on the current state, not on the full history that led to it. Two questions define the theory this mission covers: given a fixed way of acting (a policy), what value does it obtain, and how is that value actually computed rather than merely characterized as the solution of a fixed-point equation? Mohri, Rostamizadeh and Talwalkar's chapter 17 answers both for the stationary, infinite-horizon discounted case, and this mission targets its two central results: that a fixed policy's value is not just characterized but uniquely determined by a linear system with an explicit closed-form solution (Theorem 17.10), and that the optimal value function — obtained instead by choosing the best action at every state — can be computed by an iterative algorithm guaranteed to converge regardless of where it starts (Theorem 17.11).

Setting

A (finite) Markov decision process consists of a finite set of states $S$, a finite set of actions $A$, a transition kernel $P[s'\mid s,a]$ giving the distribution over the next state $s'$ after taking action $a$ at state $s$, and an expected reward $\mathbb E[r(s,a)]$ for that transition. A (stationary) policy $\pi:S\to\Delta(A)$ assigns each state a distribution over actions — possibly, but not necessarily, a point mass on a single action. Fixing $\pi$ turns the MDP into an ordinary Markov chain on $S$: at each step the agent is at some state $s$, draws $a\sim\pi(s)$, receives (expected) reward $\mathbb E[r(s,a)]$, and moves to a state drawn from $P[\cdot\mid s,a]$. For a discount factor $\gamma\in[0,1)$, the value of $\pi$ at $s$ is the expected discounted sum of future rewards starting from $s$,

$$V_\pi(s) = \mathbb E_{a_t\sim\pi(s_t)}\Big[\sum_{t=0}^{+\infty}\gamma^t r(s_t,a_t) \;\Big|\; s_0=s\Big],$$

and the state-action value function $Q_\pi(s,a)$ is the analogous quantity for taking $a$ at $s$ and then following $\pi$. Marginalizing the raw kernel and reward over the mixed action $\pi(s)$ gives the induced transition matrix $P_{s,s'}=P[s'\mid s,\pi(s)]=\sum_a \pi(s)(a) P[s'\mid s,a]$ and induced reward vector $R_s=\mathbb E[r(s,\pi(s))]=\sum_a\pi(s)(a)\,\mathbb E[r(s,a)]$ — the objects that turn $\pi$'s value into a genuinely linear-algebraic quantity. A policy $\pi^*$ is optimal if $V_{\pi^*}(s)\ge V_\pi(s)$ for every policy $\pi$ and every state $s$; write $V^*$ for its value function.

Formalization targets

Theorem 17.10 (goal). For a finite MDP and a fixed policy $\pi$, the matrix $I-\gamma P$ (with $P$ the policy-induced transition matrix) is invertible, and $\pi$'s value function is the unique solution of the Bellman equations, given in closed form by

$$V_\pi = (I-\gamma P)^{-1} R.$$

Proposition 17.9 (milestone). The value function itself satisfies the linear system that Theorem 17.10 solves:

$$\forall s\in S,\quad V_\pi(s) = \mathbb E_{a\sim\pi(s)}[r(s,a)] + \gamma\sum_{s'} P[s'\mid s,\pi(s)]\,V_\pi(s').$$

Theorem 17.7 (milestone). A policy $\pi$ is optimal if and only if it places probability only on $Q_\pi$-maximizing actions: for every $(s,a)$ with $\pi(s)(a)>0$, $a\in \operatorname{argmax}_{a'} Q_\pi(s,a')$.

Theorem 17.11 (milestone). The Bellman optimality operator $\Phi$, $[\Phi(V)](s)=\max_{a} \{\mathbb E[r(s,a)]+\gamma\sum_{s'}P[s'\mid s,a]V(s')\}$, is a $\gamma$-contraction for $\lVert\cdot\rVert_\infty$; consequently, for any starting vector $V_0$, the value-iteration sequence $V_{n+1}=\Phi(V_n)$ converges to a fixed point of $\Phi$.

Significance

Theorem 17.10 is what makes policy evaluation on a finite MDP an exact, finite computation rather than an infinite limit: instead of summing an infinite discounted series or solving an implicit fixed-point equation numerically, a single $|S|\times|S|$ matrix inversion gives the policy's value at every state simultaneously. It is also the base case every planning algorithm in the chapter builds on: policy iteration alternates optimizing a policy with exactly this evaluation step. Theorem 17.11 gives the complementary guarantee for the harder problem of finding the optimal value function directly, without fixing a policy first: value iteration converges from any starting point, with a convergence rate ($O(\log(1/\epsilon))$ iterations for $\epsilon$-accuracy) that follows from the same contraction argument. Together, the two results are the mathematical content behind why dynamic-programming planning for finite MDPs is tractable at all — the discount factor $\gamma<1$, not any structural assumption on rewards or transitions, is what buys both the uniqueness in Theorem 17.10 and the convergence in Theorem 17.11. Formalizing them requires reproducing this linear-algebraic and metric content precisely, not just asserting the conclusions: an invertibility claim asserted without the operator-norm argument, or a convergence claim without the contraction property, would state something true by fiat rather than the book's actual result. No faithful prior art exists on the platform for this exact model (see Formalization scope).

Difficulty

The obvious shortcut for Theorem 17.10 is to assert $I-\gamma P$ is invertible without proof — true, but not what the book does, and not informative about why it holds. The genuine content is that $P$, being row-stochastic (every row of $P$ sums to exactly $1$, since $\pi(s)$ and $P[\cdot\mid s,a]$ are both proper distributions), has operator norm $\lVert P\rVert_\infty=1$ exactly, so $\lVert\gamma P\rVert_\infty=\gamma<1$ strictly; this rules out $1$ as an eigenvalue of $\gamma P$, which is exactly what invertibility of $I-\gamma P$ requires. The same $\gamma<1$ fact, applied differently, drives Theorem 17.11: showing $\Phi$ is $\gamma$-Lipschitz requires bounding $\Phi(V)(s)-\Phi(U)(s)$ by comparing the maximizing action for $V$ against the same action's value under $U$ (not $U$'s own maximizer), since the two suprema need not be attained at the same action — a step easy to state incorrectly as a direct comparison of two maxima. Both theorems fail if $\gamma=1$ is allowed: the discounted setting's central asset, a strict contraction, disappears exactly at that boundary.

Formalization scope

States and actions are modeled as finite types (Fintype S, Fintype A); the raw kernel and reward P : S → A → S → ℝ, Er : S → A → ℝ are unconstrained functions, with IsTransitionKernel asserting the required distribution property explicitly rather than assuming it silently. A policy is π : S → A → ℝ with IsPolicy π asserting π s is a distribution over A for every s — deliberately not π : S → A or a PMF-valued function, since Theorem 17.7's own quantifier ("for any pair (s,a) with π(s)(a) > 0") requires treating π(s) as a genuine mixture. PolicyValue is defined as the actual infinite discounted expectation (via an explicit state-occupation-distribution recursion), not as the Bellman fixed point — so that Proposition 17.9 (the value function satisfies the linear system) and Theorem 17.10 (that system has a unique, invertible-matrix solution) are both non-vacuous claims about the same object, rather than one being definitionally true of the other. The trivializing formalization this rules out is asserting IsUnit (1 - γ • P) as a bare hypothesis, or defining V_π as (1-γP)⁻¹R and calling the resulting identity a theorem; both would erase the mission's actual content. Two platform modules model related MDPs (BertsekasSSPModel, a stochastic-shortest-path model with a termination-probability deficit rather than exact row-stochasticity, and FoundationsRL.RLBasics, a finite-horizon episodic model indexed by layer) — neither specializes exactly to this chapter's stationary, always-continuing, infinite-horizon discounted convention, so every definition here is drafted fresh rather than imported. This chunk covers §17.2–17.4.2 (the MDP model, policy value, Bellman's equations, value and policy iteration); §17.4.3 (the linear-programming formulation) and §17.5 (stochastic-approximation learning algorithms — TD(0), Q-learning, SARSA) are out of scope, since they require a stochastic-approximation convergence substrate this mission does not build.

Selected references

• Mohri, M., Rostamizadeh, A., and Talwalkar, A. Foundations of Machine Learning, 2nd ed., chapter 17. MIT Press, 2018.
• Bellman, R. Dynamic Programming. Princeton University Press, 1957.
• Puterman, M. L. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, 1994.

Motivation

Every generalization bound in Chapters 2-11 depends only on the complexity of a fixed hypothesis set $H$ — Rademacher complexity, VC-dimension, growth function — and holds regardless of which algorithm within $H$ actually returns the hypothesis. This is both a strength (broad applicability) and a limitation: it throws away everything specific to how an algorithm searches $H$, and can be uninformative when $H$ itself is large or unbounded (e.g. a regularized objective that implicitly restricts the search without shrinking $H$ as a set). Chapter 14 introduces a fundamentally different route to a generalization bound — a property of the algorithm rather than the hypothesis class — first used by Devroye, Rogers and Wagner for $k$-nearest-neighbor rules and given its modern general form by Bousquet and Elisseeff (2002), whose treatment this chapter follows and (for non-differentiable convex losses) extends.

Setting

A labeled example is $z=(x,y)\in X\times Y$; for a loss function $L:Y'\times Y\to\mathbb R_+$ (where $Y'$ may differ from $Y$, e.g. $Y=\{-1,+1\}$ but $Y'=\mathbb R$ for a real-valued hypothesis), the loss of a hypothesis $h$ at $z$ is $L_z(h)=L(h(x),y)$. Given a learning algorithm $A$ that maps a sample $S$ of size $m$ to a hypothesis $h_S\in H$, the empirical error and generalization error are $\hat R_S(h)=\frac1m\sum_iL_{z_i}(h)$ and $R(h)=\mathbb E_{z\sim D}[L_z(h)]$. Uniform $\beta$-stability (Definition 14.1) says: for any two samples $S$, $S'$ differing by a single point, the algorithm's returned hypotheses satisfy $|L_z(h_S)-L_z(h_{S'})|\le\beta$ for every $z$ — replacing one training point can change the algorithm's loss on any point by at most $\beta$. For the regularized algorithms studied in §14.3, a kernel-based regularization algorithm minimizes $F_S(h)=\hat R_S(h)+ \lambda\|h\|_K^2$ over the RKHS $H$ of a positive-definite kernel $K$, and a loss $L$ is $\sigma$-admissible (Definition 14.3) if $|L(h'(x),y)-L(h(x),y)|\le\sigma|h'(x)-h(x)|$ for all hypotheses $h,h'$ — a Lipschitz-like smoothness condition satisfied by the standard regression and classification losses.

Formalization targets

Proposition 14.4 (milestone). For a PDS kernel $K$ with $K(x,x)\le r^2$ and a convex, $\sigma$-admissible loss $L$, the kernel-based regularization algorithm is $\beta$-stable with

$$\beta \le \frac{\sigma^2r^2}{m\lambda}.$$

Corollary 14.5 (milestone). For SVR (the $\epsilon$-insensitive loss $L_\epsilon$, bounded by $M$), with probability at least $1-\delta$:

$$R(h_S) \le \hat R_S(h_S) + \frac{r^2}{m\lambda} + \Big(\frac{2r^2}\lambda+M\Big)\sqrt{\frac{\log(1/\delta)}{2m}}.$$

Theorem 14.2 — the mission's goal. For a loss bounded by $M$ and a $\beta$-stable algorithm $A$, with probability at least $1-\delta$ over a sample $S$ of size $m$:

$$R(h_S) \le \hat R_S(h_S) + \beta + (2m\beta+M)\sqrt{\frac{\log(1/\delta)}{2m}}.$$

Significance

Theorem 14.2 is the book's demonstration that algorithm-dependent analysis is not merely a special-case curiosity: it is broad enough to cover an entire family (every kernel-based regularization algorithm — KRR, SVR, SVMs, and beyond) uniformly, via a single stability coefficient computation (Proposition 14.4) that is then specialized per algorithm just by plugging in that loss's admissibility constant $\sigma$. Corollary 14.5's SVR bound is the concrete payoff: a fully explicit, dimension-free generalization guarantee for a widely used regression algorithm, with every constant ($r$, $\lambda$, $m$) traceable to the algorithm's own hyperparameters, no VC-dimension or Rademacher-complexity computation required. Unlike Chapters 3-11, whose bounds are oblivious to how $H$ is searched, algorithmic stability is the first tool in the book that can, in principle, certify generalization for a hypothesis class too large or poorly understood for a complexity-based bound to be informative, provided the algorithm itself is stable. No prior art on the Prove2Me platform is faithful: GET /theorems?q=algorithmic+stability, q=uniform+stability return no hits; q=McDiarmid returns only bounded_diff_martingale_two_sided (Boucheron-Lugosi-Massart's own two-sided bounded-differences martingale inequality), which is McDiarmid's inequality's own proof engine (the background result Theorem 14.2's proof applies), not any result of this chapter — a different mathematical object entirely, not reused. All eleven items are drafted fresh.

Not formalized here: Corollary 14.6 (KRR bound), Lemma 14.7 (boundedness of kernel-regularization hypotheses) and Corollary 14.8 (SVM bound). Corollary 14.6 is structurally identical to Corollary 14.5 (a different loss function's admissibility constant plugged into the same Proposition 14.4 + Theorem 14.2 chain) and adds no new formalization content beyond Corollary 14.5, already drafted; Lemma 14.7 and Corollary 14.8 are omitted together, since 14.8's own statement needs 14.7's bound on $|h_S(x)|$ to compute its explicit $M$ (unlike Corollary 14.5, which is given $M$ as a hypothesis) — a genuine additional formalization layer (the reproducing-kernel norm bound $|h_S(x)|\le r\sqrt{B/\lambda}$) disproportionate to a single further corollary within this mission's budget.

Difficulty

The chapter's central technical step is recognizing that $\beta$-stability plus the loss bound $M$ together give exactly the bounded-difference property McDiarmid's inequality needs, applied to $\Phi(S)=R(h_S)-\hat R_S(h_S)$ as a function of the sample: replacing one point of $S$ changes $R(h_S)$ by at most $\beta$ (stability applied to the population loss, an expectation over $z$) and changes $\hat R_S(h_S)$ by at most $\beta+M/m$ (stability on the $m-1$ shared points, plus the full loss bound $M/m$ on the one point that actually changed) — two different, asymmetric arguments that must be combined correctly to get $|\Phi(S)-\Phi(S')|\le 2\beta+M/m$, not merely "stability implies boundedness" asserted directly. Proposition 14.4's own proof (not formalized here beyond its statement) needs a generalized Bregman divergence to handle a possibly non-differentiable convex loss — an extension of Bousquet-Elisseeff's original argument the book credits to itself as novel — via the reproducing-kernel property and Cauchy-Schwarz to convert a divergence bound into a bound on $\|h-h'\|_K$, then back into a pointwise loss bound.

Formalization scope

IsRKHSOf/IsMinimizer are restated locally in Stability, byte-identical to chunk 06-kernels's own copies (a draft item cannot import another chunk's draft module); H is an abstract real inner-product space with an evaluation map ev : H → X → ℝ standing for "elements of H are functions on X", the same device chunk 06's own RKHS formalization uses, since Mathlib's abstract Hilbert spaces are not themselves spaces of functions. UniformlyStable fixes the sample size m as part of the algorithm's type (A : (Fin m → X × Y) → (X → Y')), matching the book's own standing convention of a fixed sample size m throughout the chapter. Proposition 14.4 is stated pairwise — for any two samples differing by one point and any minimizers of their respective regularized objectives, the pointwise loss bound holds — rather than fixing a global choice-function algorithm A, since the book's own proof picks an arbitrary minimizer of each objective without asserting uniqueness; Corollary 14.5 does fix a choice function A (one minimizer per sample), since Theorem 14.2's own statement needs a single algorithm evaluated across the whole product-measure sample space. No numerical constant in any of the three theorems is altered from the book's own displayed form. A trivializing formalization this mission avoids: stating Theorem 14.2 only for the strict per-hypothesis loss bound (∀ h ∈ H, ∀ z, L_z(h) ≤ M) rather than the book's own weaker, algorithm-specific condition (hbound, ∀ S, ∀ z, L_z(A S) ≤ M) — the weaker hypothesis is kept, exactly matching the book's explicit statement that "a weaker condition suffices."

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 14.
• O. Bousquet, A. Elisseeff, "Stability and generalization," Journal of Machine Learning Research 2, 2002, 499-526.
• M. Kearns, D. Ron, "Algorithmic stability and sanity-check bounds for leave-one-out cross-validation," Neural Computation 11(6), 1999, 1427-1453.

Motivation

Maximum entropy (Maxent) models are a widely used family of density-estimation algorithms: given a sample and a set of features, they select the distribution that matches the empirical feature averages while being otherwise as "agnostic" (close to a prior, usually uniform) as possible — a principle that, notably, never requires specifying a parametric family of distributions to search over. This mission formalizes the theorem that explains why this works in practice: Maxent's primal optimization (over distributions, subject to feature-matching constraints) is exactly dual to an unconstrained maximum-likelihood problem over a specific, rich parametric family — the Gibbs distributions — even though the Maxent principle never mentions that family at all.

Setting

For a sample $S=(x_1,\dots,x_m)$ drawn i.i.d. from $D$ over a finite set $X$, and a feature map $\Phi:X\to\mathbb R^N$ with $\|\Phi\|_\infty\le r$, the Maxent principle seeks $p\in\Delta$ (the simplex of distributions over $X$) minimizing the relative entropy $D(p\|p_0)$ to a prior $p_0$, subject to $\|E_{x\sim p}[\Phi(x)]-E_{x\sim\hat D}[\Phi(x)]\|_\infty\le\lambda$ (problem 12.7). Introducing the indicator function $I_K$ ($0$ on $K$, $+\infty$ elsewhere) turns this into the unconstrained primal objective $F(p)=\tilde D(p\|p_0)+I_C(E_p[\Phi])$ (Eq. 12.8), with $C$ the feature-constraint set. A Gibbs distribution with parameter $w\in\mathbb R^N$ is $p_w(x)=p_0(x)e^{w\cdot\Phi(x)}/Z(w)$, $Z(w)$ the partition function (Eq. 12.9); its associated dual objective is $G(w)=\frac1m\sum_i\log\frac{p_w(x_i)}{p_0(x_i)}-\lambda\|w\|_1$ (Eq. 12.10) — note $-\frac1m\sum_i\log p_w(x_i)$ is exactly the empirical log-loss $L_S(w)$, so maximizing $G$ is minimizing an L1-regularized log-loss over the Gibbs family.

Formalization targets

Theorem 12.2 — the mission's goal (Maxent duality). $\sup_{w\in\mathbb R^N}G(w)=\min_pF(p)$. Furthermore, letting $p^*=\arg\min_pF(p)$ and $d^*=\sup_wG(w)$: for any $\epsilon>0$ and any $w$ with $|G(w)-d^*|<\epsilon$, $D(p^*\|p_w)\le\epsilon$.

Theorem 12.3 (Maxent L1-regularization generalization bound, milestone). Fix $\delta>0$. Let $\hat w$ solve the L1-regularized dual (12.12) with $\lambda=2R_m(H)+r\sqrt{\log(2/\delta)/(2m)}$. Then, with probability at least $1-\delta$,

$$L_D(\hat w) \le \inf_wL_D(w) + 2\|\hat w\|_1\Big[2R_m(H)+r\sqrt{\log(2/\delta)/(2m)}\Big].$$

Significance

Theorem 12.2 is one of the most striking dualities in the book: the Maxent principle, phrased purely in terms of closeness to a prior distribution, turns out to always produce a solution in the Gibbs family — not because that family was ever specified, but because relative entropy is the specific measure of closeness whose Fenchel conjugate is the log-partition function. This explains a whole zoo of models (log-linear models, exponential families, Gaussian and bimodal Gibbs distributions from quadratic features) as instances of a single duality theorem, and gives a computationally friendlier route to the (constrained, infinite-if-$X$-is-large) primal problem via the (unconstrained, $N$-dimensional) dual. The theorem's proof is a genuine application of conditional (Fenchel) strong duality, not an unconditional fact — this is, per the chapter's own brief, the sharpest trivialization risk in the entire mission series, since "strong duality always holds for convex problems" is false in general, and a formalization skipping the book's own qualification condition ($\lambda>0$, placing $u_0$ in the interior of the constraint set) would prove a different, potentially-false statement. No prior art on the platform is faithful: GET /theorems?q=maximum+entropy returns no hits, and Mathlib's generic Fenchel-conjugate machinery (Analysis/Convex/Conjugate) does not package the book's own specific qualification conditions as a single reusable theorem matching Theorem B.39 — reusing it inside a proof (not the audited statement) remains available to whoever proves this theorem later.

Not formalized here: Theorem 12.4 (a Bregman-divergence generalization of Theorem 12.2) and Theorem 12.5 (its L2-regularized concrete special case). BRIEF.md itself flags Theorem 12.4 as possibly too heavy and offers Theorem 12.5 as an easier alternative; this mission omits both, since even Theorem 12.5 requires a second, structurally parallel dual-objective-and-minimizer formalization (for L2 rather than L1 regularization) — disproportionate to this mission's budget once Theorem 12.2's own qualification-condition bookkeeping (the heaviest single item in this mission series) is accounted for. §12.1 (density estimation without features: ML/MAP), §12.7 (coordinate descent), and §12.8-12.9 (Bregman-divergence extensions, L2-regularization in general) are likewise out of scope, per BRIEF.md's own page-range restriction.

Difficulty

Theorem 12.2's proof is the book's own explicit application of the Fenchel duality theorem (Theorem B.39, Appendix B) to the specific triple $f(p)=\tilde D(p\|p_0)$, $g(u)=I_C(u)$, $Ap=\sum_xp(x)\Phi(x)$ — every qualification condition (A a bounded linear map, u_0\in A(\mathrm{dom}f)\cap\mathrm{cont}(g), needing \lambda>0 to place u_0 in int(C)) must be checked for this triple, not assumed generically; the conjugate computations themselves (f^*(q)=\log\sum_xp_0(x)e^{q(x)}$ via Lemma B.37, g^(w)=E_{\hat D}[w\cdot\Phi]+\lambda|w|_1 via the dual-norm identity) are specific algebraic derivations, not immediate from abstract duality alone. The second clause's proof needs a further, non-obvious algebraic identity (G(w)-D(p^|p_0)+D(p^|p_w)expanding, via Hölder's inequality applied to the primal feasibility ofp^, to something \le0) that is not a restatement of the first clause but a separate argument built on top of it. Theorem 12.3's proof structurally mirrors chunk 04's SRM bound (bounding L_D(\hat w)-L_S(\hat w)via Hölder's inequality and the Rademacher-complexity feature-concentration bound of Eq. 12.5, then using\hat w`'s optimality twice), but is applied to the log-loss of a Gibbs distribution rather than a generic bounded loss.

Formalization scope

MaxEntPrimalObjective uses EReal (the extended reals) so that the book's own +\infty values (from I_K, \tilde D) are represented exactly, matching the chapter's own explicit use of an extended-real-valued indicator function rather than a soft penalty — a trivializing formalization this mission avoids is silently replacing +\infty with a large real sentinel, which would misstate a convex-analysis object whose entire role in the proof is its infinite value outside the feasible/simplex set. hlam : 0 < lam is a genuine load-bearing hypothesis in the goal theorem, matching the book's own use of \lambda>0 to invoke Theorem B.39's qualification condition — not a free convexity assumption; this is the mission's central faithfulness guard against the chapter's own named trivialization risk. EmpiricalRademacherComplexity/ RademacherComplexity are restated locally, byte-identical to chunks 05-svm/07-boosting's own copies (a draft item cannot import another chunk's draft module). p^* in the goal theorem and \hat w in Theorem 12.3 are both quantified via explicit hypotheses (IsLeast, a minimizer inequality) rather than assumed to exist unconditionally, matching the book's own "let p^*=..."/"let \hat w be a solution of..." phrasing without asserting existence or uniqueness beyond what the book itself asserts. No numerical constant in either theorem is altered from the book's own displayed form.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 12, §12.1-12.6.
• E. T. Jaynes, "Information theory and statistical mechanics," Physical Review 106(4), 1957, 620-630.
• S. Della Pietra, V. Della Pietra, J. Lafferty, "Inducing features of random fields," IEEE Transactions on Pattern Analysis and Machine Intelligence 19(4), 1997, 380-393.