Machine Learning

Motivation

At infinite width a randomly initialized network is a Gaussian process (Mission I of this series). Real networks have finite width $n$, and the leading departure from Gaussianity is measured by the connected four-point function $\kappa_4$. It captures both correlations between neurons and non-Gaussian fluctuations. Lecture 4 of the Les Houches lectures (arXiv:2309.01592, lectures by B. Hanin) states the central finite-width result, Theorem 4.2: $\kappa_4$ is of order $1/n$ and obeys an explicit layer-to-layer recursion up to $O(n^{-2})$. At criticality this gives the effective depth $L/n$ as the parameter controlling finite-width effects. The result was first derived at a physics level of rigor by Yaida (2020) and in Roberts–Yaida–Hanin (2022), and later derived more mathematically by Hanin (reference [19] of the notes).

Setting

A network of depth $L$ with widths $n_0,\dots,n_{L+1}$ and nonlinearity $\sigma$ has preactivations $z^{(1)}=b^{(1)}+W^{(1)}x$ and $z^{(\ell+1)}=b^{(\ell+1)}+W^{(\ell+1)}\sigma(z^{(\ell)})$. The parameters are independent, with $W^{(\ell)}_{ij}\sim\mathcal N(0,C_W/n_{\ell-1})$ and $b^{(\ell)}_i\sim\mathcal N(0,C_b)$, where $C_b\ge0$ and $C_W>0$ (eqs. (118)–(119)). At a single input $x$, write $\langle f\rangle_K$ for the average of $f$ against $\mathcal N(0,K)$. The infinite-width kernel is $K^{(1)}=C_b+C_W|x|^2/n_0$ and $K^{(\ell+1)}=C_b+C_W\langle\sigma^2\rangle_{K^{(\ell)}}$ (eq. (120)). The parallel susceptibility is $\chi_\parallel^{(\ell)}=C_W\,\partial_K\langle\sigma^2\rangle_K|_{K=K^{(\ell)}}$. The normalized connected four-point function is

$$\kappa^{(\ell)}_4=\tfrac13\Big(\mathbb E\big[(z^{(\ell)}_i)^4\big]-3\,\mathbb E\big[(z^{(\ell)}_i)^2\big]^2\Big).$$

Formalization targets

Goal: Theorem 4.2, recursion for $\kappa_4$

If the hidden widths satisfy $n\le n_\ell\le An$, then $\kappa^{(\ell)}_4=O(n^{-1})$ and

$$\kappa^{(\ell+1)}_4=\frac{C_W^2}{n_\ell}\,\mathrm{Var}_{K^{(\ell)}}\big[\sigma^2\big]+\big(\chi^{(\ell)}_\parallel\big)^2\kappa^{(\ell)}_4+O(n^{-2}),$$

with constants independent of the widths.

Milestones

1. Proposition 4.3: $AW\sim\mathcal N(A\mu,A\Sigma A^{T})$ for $W\sim\mathcal N(\mu,\Sigma)$.
2. Lemma 4.4: conditional on $z^{(\ell)}$, the vector $z^{(\ell+1)}$ is Gaussian with covariance $\Sigma^{(\ell)}I$, where $\Sigma^{(\ell)}=C_b+\frac{C_W}{n_\ell}\sum_j\sigma(z^{(\ell)}_j)^2$; moreover $\kappa^{(\ell+1)}_4=\mathrm{Var}[\Sigma^{(\ell)}]$.
3. Section 4.8, exercise: $\kappa^{(\ell)}_4=\mathrm{Cov}\big((z^{(\ell)}_i)^2,(z^{(\ell)}_j)^2\big)$ for $i\neq j$.
4. Theorem 4.2, criticality (ReLU, $C_b=0$, $C_W=2$, uniform width): $\kappa^{(L+1)}_4/(K^{(L+1)})^2=C_\sigma L/n+O_L(n^{-2})$.
5. Theorem 4.2, expansion of observables: $\mathbb E f(z^{(\ell)}_1,\dots,z^{(\ell)}_m)=\langle f\rangle_{G^{(\ell)}}+\frac{\kappa^{(\ell)}_4}{8}\big\langle\big(\sum_j\partial_j^4+\sum_{j_1\neq j_2}\partial_{j_1}^2\partial_{j_2}^2\big)f\big\rangle_{K^{(\ell)}}+O(n^{-2})$.

Significance

Theorem 4.2 is the first quantitative statement that finite-width networks at initialization are not Gaussian processes. The size of the deviation is $1/n$ per layer, and it accumulates linearly in depth at criticality. This is the basis for the claim of Lecture 4 that $L/n$ controls correlations between neurons, fluctuations and, in later lectures, feature learning. As far as the drafter knows these statements have not been machine-checked. Lemma 4.4 and the covariance exercise are exact finite-width identities and are natural first targets.

Difficulty

The next layer is Gaussian only conditionally, with a random variance $\Sigma^{(\ell)}$ that is an average over $n_\ell$ dependent neurons. Establishing the recursion to order $n^{-2}$ requires expanding Gaussian averages around the mean of $\Sigma^{(\ell)}$ and controlling all higher cumulants of this collective observable uniformly in the widths. The nonlinearity is only assumed polynomially bounded, so smoothness must come from Gaussian averaging, not from $\sigma$.

Formalization scope

• Mission I's definitions (LesHouchesWidth_GaussianMLP: the network mlpZ, stdGaussianParams, nngpKernel, uniformWidths) are reused. Mission I must be launched first, and its definition then added to this proposal as a reference item.
• New definitions (LesHouchesWidth_FiniteWidth): gaussAvg, gaussAvgVec, gaussVarSq, chiParallel, PolyBounded, kappa4, dressedTwoPoint, collectiveSigma.
• "$n_1,\dots,n_L\simeq n$" is encoded as $n\le n_\ell\le An$ for a fixed $A\ge1$. The $O(\cdot)$ constants may depend on all fixed data ($C_b,C_W,\sigma,L,n_0,n_{L+1},x,A$, and $m,f$ where relevant) but not on $n$ or on the widths.
• "Reasonable" $\sigma$ is taken to mean measurable and polynomially bounded, and the kernel is assumed nondegenerate: $K^{(\ell)}>0$ for $1\le\ell\le L+1$, as the density-based definition of $\langle\cdot\rangle_K$ in Section 4.2 requires. "Reasonable" test functions $f$ are taken to be smooth with polynomially bounded derivatives of all orders.
• The expansion of observables is stated with $\kappa^{(\ell)}_4$ in front of the correction. The printed $\kappa^{(\ell+1)}_4$ appears to be an index slip: with $\kappa^{(\ell)}_4$ the formula reproduces $\mathbb E[z^4]=3G^2+3\kappa_4$ and $\mathbb E[z_1^2z_2^2]=G^2+\kappa_4$ exactly.
• The criticality statement is formalized for ReLU at $C_b=0$, $C_W=2$, the one critical example in the notes where $K^{(\ell)}$ is constant. For $\sigma=\tanh$ the notes' "$\simeq$" is asymptotic in depth and is not formalized here.

Selected references

• Y. Bahri, B. Hanin, A. Brossollet, V. Erba, C. Keup, R. Pacelli, J. B. Simon, Les Houches Lectures on Deep Learning at Large & Infinite Width, 2023. arXiv:2309.01592
• S. Yaida, Non-Gaussian processes and neural networks at finite widths, MSML 2020. arXiv:1910.00019
• D. A. Roberts, S. Yaida, B. Hanin, The Principles of Deep Learning Theory, Cambridge University Press, 2022. arXiv:2106.10165
• B. Hanin, Random Fully Connected Neural Networks as Perturbatively Solvable Hierarchies, 2022. arXiv:2204.01058

Motivation

A fully connected neural network with random Gaussian weights defines a random function of its input. Lecture 1 of the Les Houches lectures on deep learning at large and infinite width (arXiv:2309.01592, lectures by Y. Bahri) explains that, when the hidden layers become infinitely wide, this random function becomes a Gaussian process (the "neural network Gaussian process", NNGP). Its covariance kernel is computed by an explicit layer-to-layer recursion. The observation goes back to Neal (1996) for one hidden layer. It was extended to deep networks by Matthews et al. and Lee et al. (2018). It underlies Bayesian inference with infinitely wide networks (Section 1.6) and the analysis of signal propagation at large depth (Section 1.7). Lecture 2 introduces Wick's theorem, the tool for computing moments of Gaussian vectors that the lectures then use for finite-width corrections.

Setting

A network of depth $L$ with widths $n_0,\dots,n_{L+1}$ and nonlinearity $\varphi$ maps an input $x\in\mathbb R^{n_0}$ to preactivations

$$z^{(1)}_i=b^{(1)}_i+\sum_{j}W^{(1)}_{ij}x_j,\qquad z^{(\ell+1)}_i=b^{(\ell+1)}_i+\sum_{j}W^{(\ell+1)}_{ij}\,\varphi\big(z^{(\ell)}_j\big),$$

with independent $b^{(\ell)}_i\sim\mathcal N(0,\sigma_b^2)$ and $W^{(\ell)}_{ij}\sim\mathcal N(0,\sigma_w^2/n_{\ell-1})$ (eqs. (1)–(3) and (5); layers are indexed as in Lectures 4–5, so $z^{l}$ of Lecture 1 is $z^{(l+1)}$ here). For a $2\times2$ covariance $\Sigma$ write $F_\varphi(\Sigma_{11},\Sigma_{12},\Sigma_{22})=\mathbb E_{(u_1,u_2)\sim\mathcal N(0,\Sigma)}[\varphi(u_1)\varphi(u_2)]$ (eq. (15)). The NNGP kernel is

$$K^{(1)}(x,x')=\sigma_b^2+\sigma_w^2\,\frac{x\cdot x'}{n_0},\qquad K^{(\ell+1)}(x,x')=\sigma_b^2+\sigma_w^2F_\varphi\big(K^{(\ell)}(x,x),K^{(\ell)}(x,x'),K^{(\ell)}(x',x')\big).$$

A pairing of $\{1,\dots,2m\}$ is a partition into $m$ two-element blocks.

Formalization targets

Goal: Result 1 (single hidden layer)

For a network with one hidden layer of width $n$, fixed inputs $x_1,\dots,x_m$ and output width $n_2$, as $n\to\infty$ the vector $(z^{(2)}_i(x_a))_{i\le n_2,\,a\le m}$ converges in distribution to a centered Gaussian with covariance

$$\mathbb E\big[z^{(2)}_i(x_a)z^{(2)}_j(x_b)\big]\to\delta_{ij}K^{(2)}(x_a,x_b).$$

Milestones

1. Eq. (10): $\mathbb E[z^{(1)}_i(x)z^{(1)}_i(x')]=K^{(1)}(x,x')$.
2. Eqs. (9), (11): $\mathbb E[z^{(2)}_i(x)z^{(2)}_i(x')]=K^{(2)}(x,x')$ at every finite width.
3. Eq. (16): closed form of $F_{\mathrm{ReLU}}$ (the arc-cosine kernel).
4. Result 2 (Wick's theorem): $\mathbb E[z_{\mu_1}\cdots z_{\mu_{2m}}]=\sum_{\text{pairings}}\prod K_{\mu_k\mu_{k'}}$ for $z\sim\mathcal N(0,K)$, and odd moments vanish.

A further item states the deep version of the limit, eqs. (13)–(14), in the simultaneous-width limit. It is included as a supporting theorem rather than a milestone.

Significance

Result 1 and its deep extension identify the prior over functions induced by random initialization. They also make the NNGP kernel the central computational object of the infinite-width theory. The finite-width covariance identities (9)–(11) are exact and explain where the recursion comes from. Formula (16) makes the recursion explicit for ReLU. Wick's theorem is the basic tool of the finite-width perturbation theory of later lectures. These are classical results. The mission asks for their formal proofs against a single shared model of random networks that the later missions of this series reuse.

Difficulty

Result 1 is a multivariate central limit theorem for sums of $n$ i.i.d. vectors whose entries are products of a Gaussian weight and a nonlinear function of Gaussian first-layer preactivations. No assumption beyond square-integrability of $\varphi$ against the relevant Gaussians is imposed, so the CLT must be applied in its $L^2$ form. The deep limit is harder: for $L\ge2$ the hidden preactivations are not Gaussian at finite width, and one must control a triangular array in which the widths of all layers grow together. The ReLU formula (16) is an explicit but delicate Gaussian integral over a cone.

Formalization scope

• The parameters are coordinates of i.i.d. standard Gaussians (stdGaussianParams), scaled by $\sigma_b$ and $\sigma_w/\sqrt{n_{\ell-1}}$ (mlpBias, mlpWeight). This is equality in law with the prior (5).
• Bivariate Gaussian averages use Mathlib's multivariateGaussian. Convergence in distribution is stated with bounded continuous test functions: $\mathbb E\,g(Z_n)\to\int g\,d\mathcal N(0,C)$ for every bounded continuous $g$.
• The one-hidden-layer goal assumes only that $\varphi$ is measurable and that $\varphi^2$ is integrable against $\mathcal N(0,K^{(1)}(x_a,x_a))$ for each input. The deep statement assumes $\varphi$ continuous with a linear envelope $|\varphi(u)|\le c+M|u|$, the condition used by Matthews et al. (2018). The notes defer to the references for these conditions.
• Pairings are fixed-point-free involutions of $\{0,\dots,2m-1\}$.

Selected references

• Y. Bahri, B. Hanin, A. Brossollet, V. Erba, C. Keup, R. Pacelli, J. B. Simon, Les Houches Lectures on Deep Learning at Large & Infinite Width, 2023. arXiv:2309.01592
• R. M. Neal, Bayesian Learning for Neural Networks, Springer, 1996. doi:10.1007/978-1-4612-0745-0
• A. G. de G. Matthews, M. Rowland, J. Hron, R. E. Turner, Z. Ghahramani, Gaussian Process Behaviour in Wide Deep Neural Networks, ICLR 2018. arXiv:1804.11271
• Y. Cho, L. K. Saul, Kernel Methods for Deep Learning, NeurIPS 2009.

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

A recommendation system learns from the users it serves: the diner who tries a restaurant produces the review the next diner reads. Each user would rather exploit what is already known than explore for the benefit of those who come later, so a population of self-interested agents under-explores, and an alternative that looks bad on sparse early evidence may never be tried again even when it is the best. Chapter 11 of Slivkins, Introduction to Multi-Armed Bandits (arXiv:1904.07272), treats incentivized exploration: a principal who cannot force the agents but can recommend, and who, because it aggregates what earlier agents observed, knows more than any one of them. The question is whether recommendations alone can induce enough exploration to learn as fast as an ordinary bandit algorithm. The model is that of Kremer, Mansour and Perry (JPE 2014) and the results are those of Mansour, Slivkins and Syrgkanis (EC 2015, Operations Research 2020), specialized to two arms; the single-round problem is Bayesian persuasion in the sense of Kamenica and Gentzkow (AER 2011).

Setting

There are $K$ arms and $T$ rounds. A mean reward vector $\mu \in [0,1]^K$ is drawn from a known prior $P$, and each pull of arm $a$ yields a reward drawn from a known family $D_{\mu_a}$ with mean $\mu_a$. In round $t$ the principal recommends an arm $\mathrm{rec}_t$; agent $t$, who knows the prior, the family, the algorithm and the round but not the past, sees only $\mathrm{rec}_t$, chooses $a_t$, collects $r_t \sim D_{\mu_{a_t}}$ and leaves; the principal observes $(a_t, r_t)$. The chapter works with two arms, ordered so that the prior means satisfy $\mu^0_1 \ge \mu^0_2$, with a prior of finite support and finitely many reward values.

An algorithm is Bayesian incentive-compatible (BIC, Definition 11.4) if following its recommendation is in every agent's interest given what the agent knows: for every round $t$ and arms $a \ne a'$ with $\Pr[\mathrm{rec}_t = a, E_{t-1}] > 0$,

$$\mathbb{E}[\mu_a - \mu_{a'} \mid \mathrm{rec}_t = a,\ E_{t-1}] \ge 0, \tag{11.1}$$

where $E_{t-1}$ is the event that all previous agents complied. A BIC algorithm is then an ordinary bandit algorithm whose recommendations are followed, and the run has the law of the Bayesian bandit of Chapter 3. Two contrasting policies frame the chapter. GREEDY reveals the history and lets agents exploit, $a_t \in \arg\max_a \mathbb{E}[\mu_a \mid H_t]$ (11.2); it is BIC and it fails. HiddenExploration (Algorithm 11.1) hides a little exploration in a lot of exploitation: on a signal $\mathrm{sig}$, with probability $\varepsilon$ it recommends a target arm $a_{\mathrm{trg}}(\mathrm{sig})$, otherwise the arm maximizing $\mathbb{E}[\mu_a \mid \mathrm{sig}]$, ties to arm 1. Its posterior gap is $G = \mathbb{E}[\mu_2 - \mu_1 \mid \mathrm{sig}]$. RepeatedHE (Algorithm 11.2) runs it round after round with an arbitrary bandit algorithm $\mathrm{ALG}$ as the target: $N_0$ initial rounds recommend arm 1; afterwards, with probability $\varepsilon$ the round is an exploration round in which $\mathrm{ALG}$ chooses (and is fed the reward), and otherwise the exploitation branch recommends $\min\arg\max_a \mathbb{E}[\mu_a \mid S_t]$, where $S_t$ is the data of all exploration rounds so far (11.10). The quantity that governs everything is $G_{1,n} = \mathbb{E}[\mu_2 - \mu_1 \mid S_{1,n}]$ (11.11), the posterior gap after $n$ samples of arm 1, and Property (11.12), that $\Pr[G_{1,n} > 0] > 0$ for some $n$: arm 2 can appear better after enough samples of arm 1.

Formalization targets

Goal: Theorem 11.15

RepeatedHE with exploration probability $\varepsilon > 0$ and $N_0$ initial samples of arm 1 is BIC as long as

$$\varepsilon < \tfrac13\,\mathbb{E}\big[G \cdot \mathbf 1\{G > 0\}\big], \qquad G = G_{N_0+1} = \mathbb{E}[\mu_2 - \mu_1 \mid S_{1,N_0}],$$

for any bandit algorithm $\mathrm{ALG}$ and any horizon. The threshold depends on the prior alone.

Milestones

Theorem 11.7 (GREEDY never chooses arm 2 with probability at least $\mu^0_1 - \mu^0_2$) and Corollary 11.8 (linear Bayesian regret of GREEDY under independent priors); Lemma 11.10 (HiddenExploration is BIC when $\varepsilon \le \frac13\mathbb{E}[G\mathbf 1\{G > 0\}]$) with Claim 11.12 (the arm-2 side of the constraint suffices); Corollary 11.14 (RepeatedHE is BIC under the round-by-round condition); Theorem 11.19 (without Property (11.12) no BIC algorithm ever plays arm 2, ties to arm 1).

Significance

The results say when exploration can be incentivized at all and how. Theorem 11.7 shows that revealing everything is not a solution: the greedy dynamics gets stuck on arm 1 with a probability that does not shrink with $T$, and Corollary 11.8 turns that into $\Omega(T)$ Bayesian regret. Theorem 11.15 shows that a recommendation-only principal can induce any amount of exploration it wants, with $\mathrm{ALG}$ arbitrary, at a per-round rate $\varepsilon$ fixed by the prior; Theorem 11.17 (stated with a proof sketch, and omitted here) then transfers $\mathrm{ALG}$'s regret to RepeatedHE up to the prior-dependent factors $N_0$ and $1/\varepsilon$, so $\tilde O(\sqrt T)$ regret is attainable subject to incentives. Theorem 11.19 closes the picture: Property (11.12) is necessary as well as sufficient. Together they characterize which priors admit incentivized exploration and give an algorithm that works for all of them.

Nothing of this is machine-checked. The mission adds to the Bayesian layer of mission III (prior, posterior by Bayes' rule, Bayesian regret) the BIC constraint on a joint law, GREEDY as a policy, the single-round HiddenExploration on an abstract finite signal, and the law of RepeatedHE; all of it is reusable for the $K$-arm and the "explore all explorable arms" extensions of the literature review.

Difficulty

Theorem 11.7 is a martingale argument: the posterior gap along the history is a Doob martingale, the first round in which arm 2 is chosen is a bounded stopping time, and optional stopping gives $\mathbb{E}[Z_\tau] = \mu^0_1 - \mu^0_2$; all of this has to be set up on the joint law of $(\mu, H_T)$ of mission III, where the posterior is defined by Bayes' rule and the identification with a conditional expectation is itself a theorem (posterior_eq_condProb). Lemma 11.10 is the heart of the chapter and is not a computation about $\mathrm{rec}$: it works with $F(E) = \mathbb{E}[G\mathbf 1_E]$, splits along the two branches, uses that the exploitation branch recommends arm 2 exactly when $G > 0$, and closes with $F(G > 0) + F(G < 0) = \mathbb{E}[\mu_2 - \mu_1] \le 0$; the only place where the analysis uses that both branches are functions of the signal is the step $\mathbb{E}[\mu_2 - \mu_1 \mid \mathrm{rec} = 2] = \mathbb{E}[G \mid \mathrm{rec} = 2]$, and a formalization has to make that step explicit. Theorem 11.15 requires seeing each later round of RepeatedHE as a HiddenExploration with signal $S_t$, where $\mathrm{ALG}$'s choice is a randomized function of $S_t$, and then the monotonicity of $\mathbb{E}[G_t\mathbf 1\{G_t > 0\}]$ in $t$, a two-line consequence of $S_{t+1}$ determining $S_t$ that presupposes the posterior given $S_t$ is the Bayes posterior of the exploration data alone, which is true because the exploration decisions do not depend on $\mu$ given that data. Corollary 11.8 needs the independence of the event "$\mu_1 < 1 - 2\alpha$ and arm 2 is never chosen" from $\mu_2$. Theorem 11.19 is an induction in which the inductive hypothesis is a probability-zero statement about all earlier rounds.

Formalization scope

Arms are Fin 2, the book's arm 1 being index 0; rounds are Fin T. The prior is a probability measure on mean vectors supported on a finite set $F \subseteq [0,1]^2$, with $\mu^0_1 \ge \mu^0_2$ as a hypothesis; the reward family is mission III's RewardFamily (finitely many values, mean $\nu$ for $\nu \in [0,1]$). BIC is defined on a joint law of $(\mu, \text{record})$ of the run in which every agent complies, with the recommendation of each round read off the record; the compliance event $E_{t-1}$ of (11.1) is the sure event of that law, which is the standard reading of "the agents believe all previous agents complied". For a bandit policy the law is mission III's jointMeasure. Conditional expectations are written as finite sums over $F$, so there are no integrals and no integrability side conditions; a posterior mean off the support is a junk $0$ that never enters a theorem. GREEDY allows arbitrary tie-breaking; HiddenExploration's exploitation branch breaks ties toward arm 1 as Algorithm 11.1 does; the tie convention of Theorem 11.19 is the strict form of BIC for arm 2. The law of RepeatedHE is an explicit finitely supported measure, $\mu$ and record weighted by the prior times the product of the round probabilities (initial rounds forced to arm 1, then the $\varepsilon$-coin, $\mathrm{ALG}$'s kernel on its own history, or the exploitation arm, then $D_{\mu_{a_t}}$); it is written this way because $\mathrm{ALG}$ is fed a history of variable length. Two conditions are stated exactly as printed: Lemma 11.10 with $\varepsilon \le \frac13\mathbb{E}[G\mathbf 1\{G > 0\}]$ (non-strict, checked at equality) and Theorem 11.15 with the strict inequality.

Trivializations are excluded: $\varepsilon > 0$ throughout; the BIC condition is asserted only where the recommendation has positive probability, and the sums in it are over the finite support, so an unsatisfiable hypothesis cannot hide in a measure-zero set. Welcome contributions: the optional-stopping argument on jointMeasure, the identification of explPostMean with the conditional expectation given the exploration data, the Bayes-rule algebra behind Lemma 11.10, and the counting lemmas on heRecords.

Selected references

• A. Slivkins, Introduction to Multi-Armed Bandits, Foundations and Trends in Machine Learning 12(1-2), 2019, Chapter 11. arXiv:1904.07272, doi:10.1561/2200000068
• I. Kremer, Y. Mansour, M. Perry, Implementing the "Wisdom of the Crowd", Journal of Political Economy 122(5), 2014. doi:10.1086/676597
• Y. Mansour, A. Slivkins, V. Syrgkanis, Bayesian Incentive-Compatible Bandit Exploration, Operations Research 68(4), 2020 (EC 2015). doi:10.1287/opre.2019.1919
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. doi:10.1257/aer.101.6.2590
• M. Sellke, A. Slivkins, The Price of Incentivizing Exploration: A Characterization via Thompson Sampling and Sample Complexity, Operations Research 71(5), 2023. doi:10.1287/opre.2022.2401

Motivation

Every data-driven decision problem faces the same trap. A decision-maker estimates a risk functional $R(P,\ell) = \mathbb{E}_P[\ell(\xi)]$ from a nominal distribution $\hat P_N$ built from $N$ training samples, then optimizes a loss function $\ell$ against $\hat P_N$ instead of the unknown true distribution $P$. Because the optimizer adapts to the noise in $\hat P_N$, the in-sample risk of the optimizer systematically understates its true, out-of-sample risk — a phenomenon Smith and Winkler named the optimizer's curse (Smith & Winkler, Management Science, 2006). The remedy explored here is to hedge against a whole neighborhood of plausible distributions around $\hat P_N$, rather than trusting the point estimate. Kuhn, Mohajerin Esfahani, Nguyen and Shafieezadeh-Abadeh's INFORMS TutORials chapter (2019) develops this neighborhood using the Wasserstein distance, and the present mission formalizes its foundational duality theory: the machinery every later result in the chapter (finite-sample guarantees, elliptical tractability, regularization) builds on.

Setting

Fix a norm $\|\cdot\|$ on a finite-dimensional real vector space $E$ (representing $\mathbb{R}^m$). For $p \in [1,\infty)$, the type-$p$ Wasserstein distance between two Borel probability measures $Q, Q'$ on $E$ is

$$W_p(Q,Q') = \left(\inf_{\pi \in \Pi(Q,Q')} \int_{E\times E} \|\xi-\xi'\|^p\, \pi(d\xi,d\xi')\right)^{1/p},$$

where $\Pi(Q,Q')$ is the set of couplings of $Q$ and $Q'$ — joint probability measures on $E \times E$ whose marginals are $Q$ and $Q'$. The optimal $\pi$ can be read as a transportation plan moving one pile of dirt ($Q$) into another ($Q'$) at minimum cost, which is why $W_p$ is also called the earth mover's distance; the underlying linear program was formalized by Kantorovich (1942) after Monge's 1781 original.

Given $N$ training samples $\hat\xi_1,\dots,\hat\xi_N$, the empirical distribution is $\hat P_N = \frac1N\sum_{i=1}^N \delta_{\hat\xi_i}$. Centered at $\hat P_N$, the Wasserstein ambiguity set of radius $\varepsilon \ge 0$ is

$$B_{\varepsilon,p}(\hat P_N) = \{Q \in \mathcal{P}(\Xi) : W_p(Q,\hat P_N) \le \varepsilon\},$$

where $\Xi \subseteq E$ is a closed set known to contain the support of the true distribution. The worst-case risk of a loss function $\ell$ is

$$R_{\varepsilon,p}(\hat P_N,\ell) = \sup_{Q \in B_{\varepsilon,p}(\hat P_N)} \mathbb{E}_Q[\ell(\xi)],$$

and minimizing it over a class of admissible loss functions $\mathcal{L}$ is a distributionally robust optimization problem. $\varepsilon$ measures the estimation error one insures against; a larger ambiguity set gives a more conservative (and more expensive) guarantee.

Formalization targets

Goal — Theorem 7, strong duality

$$R_{\varepsilon,p}(\hat P_N,\ell) = \inf_{\gamma \ge 0}\ \mathbb{E}_{\hat P_N}[\ell_\gamma(\xi)] + \gamma\varepsilon^p,\qquad \ell_\gamma(\xi) = \sup_{z\in\Xi} \ell(z) - \gamma\|z-\xi\|^p.$$

This is the Lagrangian dual of the worst-case risk evaluation problem, with $\gamma$ the multiplier of the Wasserstein constraint $W_p(Q,\hat P_N)\le\varepsilon$: it converts a supremum over an infinite-dimensional space of measures into a one-dimensional minimization of the Moreau-Yosida regularization $\ell_\gamma$. Every tractability result later in the chapter (finite convex reformulations, SDP relaxations) specializes this duality by choosing a loss class for which $\ell_\gamma$ is computable.

Supporting dual representations of $W_p$ — Theorems 1 and 2

$$W_p^p(Q,Q') = \sup\left\{\int \psi\,dQ' - \int \varphi\,dQ : \varphi,\psi \text{ bounded continuous},\ \psi(\xi)-\varphi(\xi') \le \|\xi-\xi'\|^p\right\}$$ $$W_1(Q,Q') = \sup_{\mathrm{Lip}(\varphi)\le 1} \int \varphi\,dQ - \int \varphi\,dQ'$$

These identify $W_p$ as a linear program's strong dual (Theorem 1) and, for $p=1$, specialize it to the Kantorovich-Rubinstein form (Theorem 2), which is what lets the worst-case-risk analysis reason about Lipschitz loss functions directly.

Upper and lower bounds — Theorems 5 and 6

$$R_{\varepsilon,p}(\hat P_N,\ell) \le R(\hat P_N,\ell) + \varepsilon\cdot\mathrm{Lip}(\ell)$$ $$R_{\varepsilon,p}(\hat P_N,\ell) \ge \sup\left\{\tfrac1N\textstyle\sum_i \ell(\hat\xi_i+\theta_i) : \hat\xi_i+\theta_i\in\Xi,\ \tfrac1N\textstyle\sum_i\|\theta_i\|^p\le\varepsilon^p\right\}$$

These are the tractable, easily-computed bracket that Theorems 7 and 10 later show is tight in important special cases.

Exact case — Theorem 10

$$\Xi = \mathbb{R}^m,\ \ell \text{ convex},\ p=1 \implies R_{\varepsilon,1}(\hat P_N,\ell) = R(\hat P_N,\ell) + \varepsilon\,\mathrm{Lip}(\ell)$$

Theorem 5's inequality becomes exact under convexity — the cleanest closing corollary of the duality theory, obtained from Theorem 7 by evaluating the Moreau-Yosida regularization of a convex function explicitly.

Significance

Theorem 7 is the hinge on which the entire computational program of Wasserstein distributionally robust optimization turns: every tractable reformulation in the source chapter (piecewise-concave losses via conic duality, quadratic losses via semidefinite programming, the shrinkage-estimator connection) is obtained by substituting a specific loss class into the right-hand side of Theorem 7 and showing the resulting Moreau-Yosida regularization is computable. Kuhn et al. themselves derive it as a corollary of Blanchet & Murthy (2019) and Gao & Kleywegt (2016) for the empirical case, generalized to Polish spaces by Blanchet & Murthy and Gao & Kleywegt independently — the paper cites [12] and [37] for the general statement. Formalizing it is what makes every later, more computational result in the chapter — the ones a solver is more likely to reach for next — rest on a mechanically verified foundation rather than a citation chain.

Status. The mathematical result is well established (multiple independent published proofs cited above); nothing here is open research. What this mission contributes is the first machine-checked formal statement of the duality theorem and its supporting dual representations (Theorems 1, 2, 5, 6, 10) on the Prove2Me platform — none of Wp's dual representation, the Wasserstein ambiguity set, or the worst-case risk functional exist there prior to this mission (see Formalization scope).

Difficulty

The obvious proof strategy — write down the Lagrangian of the semi-infinite program (6), swap the order of the outer supremum over $Q$ and the inner minimization over the multiplier $\gamma$, and invoke ordinary Lagrangian strong duality — fails because (6) is an infinite- dimensional linear program over measures, not a finite convex program: there is no compact feasible set or Slater point in a form that ordinary finite-dimensional duality applies to directly. The actual proof goes through the dual representation of the Wasserstein distance itself (Theorem 1, which is why it is a prerequisite milestone), reformulating the constraint $W_p(Q,\hat P_N)\le\varepsilon$ via its own dual variables and swapping the resulting sup-inf using minimax theorems for semi-infinite programs, not ordinary Lagrangian duality for finite programs.

Formalization scope

$E$ is a generic finite-dimensional real normed space (NormedAddCommGroup, NormedSpace ℝ, Borel-measurable), representing $\mathbb{R}^m$ with the paper's arbitrary fixed norm as a parameter rather than fixing the Euclidean norm. A coupling is formalized directly via MeasureTheory.Measure.map: π.map Prod.fst = Q ∧ π.map Prod.snd = Q'. Constrained infima/suprema (over couplings, over the ambiguity set, over Lipschitz test functions, over perturbation matrices) use Mathlib's guarded-binder idiom ⨅ x (_ : P x), f x, which correctly returns $\top$ (resp. $\bot$) outside the feasible set rather than a finite junk value.

Two deliberate, disclosed conventions keep the extremal-value definitions faithful without extended-real integration machinery, both recorded in MODERATION_NOTES.md:

1. worstCaseRisk and the dual representations (Theorems 1, 2) are valued in EReal, not ℝ, so an unbounded supremum is recorded as $+\infty$ rather than collapsed to Mathlib's real-valued junk value 0 on an unbounded family.
2. The goal theorem (7) and its Moreau-Yosida regularization restrict the loss function to bounded continuous $\ell$ (BoundedContinuousFunction E ℝ), narrower than the paper's general upper-semicontinuous, $\hat P_N$-integrable loss class $\mathcal{L}$ (Assumption 1). This keeps $\ell_\gamma(\xi) = \sup_{z\in\Xi}\ell(z)-\gamma\|z-\xi\|^p$ a finite real number for every nonempty $\Xi$, so the right-hand side's Bochner integral is well-posed; the milestones (Theorems 5, 6, 10) keep the more general real-valued (not necessarily bounded) loss class, since their statements do not require evaluating a pointwise supremum over $\Xi$.
3. Ξ is required closed in Theorems 5, 6 and 7, matching the paper's own standing assumption (p. 6: "we let $\Xi\subseteq\mathbb{R}^m$ be a closed set that is known to contain the support of $P$") for the whole worst-case-risk framework, which is used silently in the paper wherever a theorem takes $\Xi$ as an argument but was not carried into these theorems' own hypothesis lists in an earlier draft.
4. The goal theorem (7) additionally requires $\hat P_N$ itself supported on $\Xi$ ($\hat P_N(\Xi^c)=0$, the same "supported on $\Xi$" convention ambiguitySet uses for $Q\in\mathcal P(\Xi)$), which the paper's framework presupposes for the nominal distribution throughout §2. Combined with $\ell$ bounded, this makes $\ell_\gamma$ bounded on the full-measure set $\Xi$ (above by $\sup\ell$ unconditionally, below by $\ell(\xi)$ itself via $z=\xi$ for $\xi\in\Xi$), which is what makes the right-hand side's integral genuinely well-posed rather than liable to Mathlib's non-integrable junk value $0$.

There is no trivializing formalization risk from a vacuous hypothesis: Ξ.Nonempty and 0 < N are both required exactly where the paper's own indexing and support assumptions require them, and every extremal value uses the extended-real convention above rather than a convention that would make an inequality vacuously true.

No definition in this mission exists on the platform prior to this series (GET /theorems?q=Wasserstein, q=Kantorovich, q=optimal transport, q=coupling return only unrelated discrete/finite-type constructions); all seven definitions and six theorems are drafted fresh. WassersteinDRO.Duality.wassersteinDistance, .ambiguitySet and .worstCaseRisk are the substrate every later mission in this five-part series (Gelbrich tractability, finite-sample guarantees, regularization, shrinkage estimation) either imports directly or redefines locally per the series' reuse rule.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research, 130–166. https://doi.org/10.1287/educ.2019.0198
• Villani, C. (2009). Optimal Transport: Old and New. Springer. (Cited as [108] for Theorems 1 and 2.)
• Smith, J. E., & Winkler, R. L. (2006). The optimizer's curse: Skepticism and postdecision surprise in decision analysis. Management Science, 52(3), 311–322. https://doi.org/10.1287/mnsc.1050.0451
• Gao, R., & Kleywegt, A. J. (2016). Distributionally Robust Stochastic Optimization with Wasserstein Distance. arXiv:1604.02199.
• Blanchet, J., & Murthy, K. (2019). Quantifying Distributional Model Risk via Optimal Transport. Mathematics of Operations Research, 44(2), 565–600. https://doi.org/10.1287/moor.2018.0936

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.