Statistics

Linear Optimization Machine Learning Probability·Captain: mikedeng1

The Dantzig Selector: Statistical Estimation When p Is Much Larger than n 1: ℓ2 Error Bound for Sparse Parameters under the Uniform Uncertainty PrincipleResearch Paper

Motivation

In many statistical applications the number of unknown parameters $p$ is far larger than the number of observations $n$ : gene-expression studies with tens of samples and thousands of genes, imaging problems with fewer measurements than pixels, and nonparametric curve estimation from finitely many noisy samples. Least squares is useless in this regime, since the system $X\beta=y$ is underdetermined. If the parameter is sparse (only a few of its entries are nonzero), estimation becomes possible, and the question is how accurate a computationally tractable estimator can be.

Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) introduced the Dantzig selector, an estimator computed by a linear program, and proved that its squared error is within a factor of order $\log p$ of the error of an oracle that knows where the nonzero entries are. The paper, with its discussion in the same issue, is one of the founding results of high-dimensional sparse regression, alongside the Lasso analysis of Bickel, Ritov and Tsybakov (arXiv:0801.1095).

Timeline. Candès and Tao (2005, arXiv:math/0502327) showed that $\ell_1$ minimization recovers a sparse vector exactly from noiseless data when the restricted isometry constants of the design satisfy $\delta_S+\theta_{S,S}+\theta_{S,2S}<1$ . The Dantzig selector paper (first posted 2005, published 2007) carried this to Gaussian noise, with the $\ell_2$ error bound formalized here (Theorem 1.1) and an oracle inequality (Theorem 1.2). Bickel, Ritov and Tsybakov (2009) replaced the restricted isometry hypothesis by weaker restricted eigenvalue conditions and showed that the Lasso and the Dantzig selector behave alike.

Setting

Observe $y\in\mathbb R^n$ from the linear model

y=X\beta+z ,

where $X\in\mathbb R^{n\times p}$ is a deterministic design matrix with columns $X_1,\dots,X_p$ , each of Euclidean norm $\|X_j\|_{\ell_2}=1$ ; $\beta\in\mathbb R^p$ is an unknown deterministic parameter; and $z=(z_1,\dots,z_n)$ is a vector of independent $N(0,\sigma^2)$ random variables with $\sigma>0$ . The vector $\beta$ is $S$ -sparse if at most $S$ of its entries are nonzero.

For $T\subseteq\{1,\dots,p\}$ let $X_T$ be the submatrix of the columns indexed by $T$ . The restricted isometry constant $\delta_S$ is the smallest $\delta\ge0$ with

(1-\delta)\|c\|_{\ell_2}^2\le\|X_Tc\|_{\ell_2}^2\le(1+\delta)\|c\|_{\ell_2}^2

for all $|T|\le S$ and all coefficient vectors $c$ ; the restricted orthogonality constant $\theta_{S,S'}$ (for $S+S'\le p$ ) is the smallest $\theta\ge0$ with $|\langle X_Tc,X_{T'}c'\rangle|\le\theta\|c\|_{\ell_2}\|c'\|_{\ell_2}$ for all disjoint $T,T'$ with $|T|\le S$ , $|T'|\le S'$ .

Given a tuning parameter $\lambda_p>0$ , the Dantzig selector $\hat\beta$ is any solution of

\min_{\tilde\beta\in\mathbb R^p}\|\tilde\beta\|_{\ell_1}\quad\text{subject to}\quad\|X^*(y-X\tilde\beta)\|_{\ell_\infty}=\max_{1\le j\le p}|\langle y-X\tilde\beta,X_j\rangle|\le\lambda_p\cdot\sigma .

Formalization targets

Goal: Theorem 1.1

Let $S\ge1$ , $3S\le p$ , $\beta$ $S$ -sparse, and $\delta_{2S}+\theta_{S,2S}<1$ . For every $a\ge0$ , with $\lambda_p=\sqrt{2(1+a)\log p}$ , with probability exceeding $1-(\sqrt{\pi\log p}\cdot p^a)^{-1}$ the program has a solution and every solution satisfies

\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\cdot\lambda_p^2\cdot S\cdot\sigma^2,\qquad C_1=\frac{4}{1-\delta_{2S}-\theta_{S,2S}} .

For $a=0$ this is $\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\cdot(2\log p)\cdot S\cdot\sigma^2$ , display (1.10) of the paper. The constant is the one the paper's proof establishes (see Formalization scope).

Milestones

The cone constraint (3.2): if $\|\beta+h\|_{\ell_1}\le\|\beta\|_{\ell_1}$ and $\beta$ vanishes off $T_0$ , then $\|h_{T_0^c}\|_{\ell_1}\le\|h_{T_0}\|_{\ell_1}$ .
The tube constraint (3.3): with unit-normed columns, if $|\langle z,X_j\rangle|\le\lambda_p$ for all $j$ and $\hat\beta$ is feasible, then $\|X^*X(\hat\beta-\beta)\|_{\ell_\infty}\le2\lambda_p$ .
Lemma 3.1 (under the section’s unit-column assumption): an $\ell_2$ bound on $h$ over $T_0\cup T_1$ ( $T_1$ the $S$ largest entries of $h$ off $T_0$ ) in terms of $\|X_{T_{01}}^TXh\|_{\ell_2}$ and $\|h\|_{\ell_1(T_0^c)}$ , and $\|h\|_{\ell_2}^2\le\|h\|_{\ell_2(T_{01})}^2+S^{-1}\|h\|_{\ell_1(T_0^c)}^2$ .
The deterministic core: with $\sigma=1$ , on the event $|\langle z,X_j\rangle|\le\lambda_p$ for all $j$ , every Dantzig selector satisfies $\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\lambda_p^2S$ .
The Gaussian tail bound: for standard normal $z$ and $Z_j=\langle z,X_j\rangle$ , $\mathbb P(\sup_j|Z_j|>u)\le2p\,\varphi(u)/u$ with $\varphi(u)=(2\pi)^{-1/2}e^{-u^2/2}$ .

Significance

The result. Theorem 1.1 shows that an estimator computable by linear programming reaches, up to the factor $2\log p$ and the constant $C_1^2$ , the squared error $S\sigma^2$ that least squares would attain if the support of $\beta$ were known in advance, even when $p\gg n$ . The factor $\log p$ is the price of not knowing the support; the paper argues (p. 5) that, apart from this factor, (1.10) is unimprovable in general. The bound is non-asymptotic, with an explicit constant and an explicit failure probability, and it holds for every $S$ -sparse $\beta$ simultaneously in the sense that the good event (the noise being nearly orthogonal to every column) does not depend on $\beta$ . Its deterministic part, Lemma 3.1, is reused verbatim in the proof of the paper's oracle inequality (Theorem 1.2) and became a standard tool in compressed sensing.

Formalizing it. The result is proved, and to our knowledge no machine-checked proof exists. A formalization produces a checked version of the cone-and-tube argument behind most $\ell_1$ -recovery guarantees, a Lean statement of the restricted isometry machinery for noisy data, and a checked Gaussian maximal inequality usable for other high-dimensional estimators. It also settles the exact constant: the paper prints $C_1=4/(1-\delta_S-\theta_{S,2S})$ , while its proof gives $\delta_{2S}$ in place of $\delta_S$ .

Difficulty

Lemma 3.1 is the main obstacle. The obvious approach bounds $\|h\|_{\ell_2}$ directly through restricted isometry, and it fails because the error $h$ is not sparse: it spreads over all $p$ coordinates, and restricted isometry controls $X$ only on vectors with at most $2S$ nonzero entries. The two constraints (3.2) and (3.3) only say that $h$ is concentrated in $\ell_1$ on the $S$ coordinates of $T_0$ and that $X^*Xh$ is small coordinatewise, and turning that into an $\ell_2$ bound on all of $h$ is where the work lies. In Lean this requires bookkeeping that is routine on paper: ordering the coordinates of $h$ off $T_0$ by magnitude, with ties and a possibly incomplete last group of coordinates, and working with the span of a selected set of columns. On the probabilistic side, the tail bound needs the law of $\langle z,X_j\rangle$ (a weighted sum of independent Gaussians), a sharp Gaussian tail estimate of Mills-ratio type, and a union over $p$ events. A cruder sub-Gaussian bound $2e^{-u^2/2}$ would not give the stated failure probability.

Formalization scope

Indices are Fin n and Fin p; vectors are functions into ℝ. The norms, the column $X_j$ and the constants $\delta_S$ , $\theta_{S,S'}$ are the published definitions CandesTao_Decoding_Norms and CandesTao_Decoding_RestrictedIsometry (the smallest admissible constants, via sInf), from the formalization of Candès and Tao's Decoding by Linear Programming. The noise is a family z : Fin n → Ω → ℝ on a probability space, mutually independent (iIndepFun), each coordinate with law gaussianReal 0 σ². The $\ell_\infty$ constraint is coordinatewise. A Dantzig selector is any minimizer; uniqueness is not assumed. Section 3 works with $\sigma=1$ ; the goal is stated for general $\sigma>0$ .

Committed conventions and corrections:

Corrected constant. Theorem 1.1 is printed with $C_1=4/(1-\delta_S-\theta_{S,2S})$ , but the proof (pp. 18–19) applies Lemma 3.1, whose $\delta$ is $\delta_{2S}$ . Since $\delta_S\le\delta_{2S}$ , the printed constant is stronger than what is proved. The goal and the deterministic core are stated with $C_1=4/(1-\delta_{2S}-\theta_{S,2S})$ .
Domain. $1\le S$ and $3S\le p$ , because $\theta_{S,2S}$ is defined only for $S+2S\le p$ . This forces $p\ge3$ and $\log p>0$ .
Failure event. The probability bounded is that of the set where no Dantzig selector exists or some Dantzig selector violates the bound. A version that only constrains existing solutions, or that assumes the feasible set is nonempty, would be weaker. The bound is strict, as in the paper's "exceeding", and is on the outer measure, so no measurability of the event is assumed.
Standing assumptions are binders: unit-normed columns, independent Gaussian noise, deterministic $X$ and $\beta$ .

A trivializing formalization is excluded: the hypothesis $\delta_{2S}+\theta_{S,2S}<1$ is on the actual least constants of $X$ , not on free parameters, and it is satisfiable (for instance by $X=I_p$ , where both constants vanish).

Needed infrastructure: sums of independent real Gaussians (Mathlib has gaussianReal and its convolution), a Mills-ratio tail bound, a sorting-based block decomposition of a Finset, and orthogonal projection onto the span of finitely many columns. The block decomposition and the tail bound are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 3.1.

Selected references

E. Candès and T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6) (2007), 2313–2351. arXiv:math/0506081, doi:10.1214/009053606000001523
E. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51(12) (2005), 4203–4215. arXiv:math/0502327
P. Bickel, Y. Ritov and A. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4) (2009), 1705–1732. arXiv:0801.1095

9 thms3 active usersReviewed

Machine Learning Probability·Captain: mikedeng1

On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities III: Uniform Convergence and the Entropy per ObservationResearch Paper

Motivation

Estimating a probability by the relative frequency of the event in an independent sample is justified for one event by the law of large numbers. Statistics and learning theory need more: the frequencies of a whole class of events $S$ must approach their probabilities simultaneously, so that a quantity chosen after looking at the data (the empirical risk minimizer, the empirical distribution function) is still close to its expectation. Glivenko's theorem on the empirical distribution function is the classical instance; empirical risk minimization rests on the same property for the class of loss sets of a model.

Vapnik and Chervonenkis, On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities, Theory Probab. Appl. 16 (1971), treat this question in two parts. The first gives a distribution-free sufficient condition through the growth function (Theorems 1–3). The second, which this mission formalizes, gives a condition that is necessary and sufficient for a fixed distribution: Theorem 4, the entropy criterion.

Timeline. 1933: Glivenko and Cantelli prove uniform convergence for the class of rays $\{x \le a\}$ on the line. 1968: Vapnik and Chervonenkis announce the results in Dokl. Akad. Nauk SSSR 181. 1971: the full paper appears, with the growth-function bound and the entropy criterion. Later work (Talagrand 1987; Dudley, Giné and Zinn 1991) recasts such criteria as the theory of Glivenko–Cantelli classes.

Setting

Let $X$ be a set carrying a probability measure $P$ , and $S$ a collection of measurable subsets of $X$ (events). A sample of size $l$ is a sequence $x_1, \dots, x_l$ of independent draws from $P$ ; repetitions are allowed. For $A \in S$ the relative frequency $\nu_A^{(l)}$ is the fraction of sample terms lying in $A$ , and $P_A = P(A)$ . The maximal deviation is

\pi^{(l)}(x_1, \dots, x_l) = \sup_{A \in S} \bigl|\nu_A^{(l)} - P_A\bigr| .

The relative frequencies converge in probability to the probabilities uniformly over $S$ when $\mathbf{P}\{\pi^{(l)} > \varepsilon\} \to 0$ as $l \to \infty$ for every $\varepsilon > 0$ .

Each $A \in S$ induces in a sample the subsample of terms lying in $A$ . The index $\Delta^S(x_1, \dots, x_l)$ is the number of different subsamples induced by the sets of $S$ ; it lies between $0$ and $2^l$ . The entropy of $S$ in samples of size $l$ is

H^S(l) = \mathbf{E} \log_2 \Delta^S(x_1, \dots, x_l) .

For a sample of size $2l$ , split into halves $x_1, \dots, x_l$ and $x_{l+1}, \dots, x_{2l}$ with relative frequencies $\nu'_A$ and $\nu''_A$ , the semi-sample deviation is $\rho^{(l)} = \sup_{A \in S} |\nu'_A - \nu''_A|$ . Finally $\Phi(n, r)$ is defined by the recurrence $\Phi(n, r) = \Phi(n, r-1) + \Phi(n-1, r-1)$ , $\Phi(0, r) = \Phi(n, 0) = 1$ .

Formalization targets

Goal: Theorem 4 (p. 275)

\Bigl(\forall \varepsilon > 0:\ \lim_{l\to\infty} \mathbf{P}\{\pi^{(l)} > \varepsilon\} = 0\Bigr) \iff \lim_{l \to \infty} \frac{H^S(l)}{l} = 0 .

Milestones

Entropy rate. (12) $\Delta^S(x_1, \dots, x_l) \le \Delta^S(x_1, \dots, x_k)\Delta^S(x_{k+1}, \dots, x_l)$ ; the subadditivity $H^S(l_1 + l_2) \le H^S(l_1) + H^S(l_2)$ ; Lemma 3, $H^S(l)/l \to c \in [0, 1]$ ; Lemma 4, $\mathbf{P}(|l^{-1}\log_2 \Delta^S - c| > \varepsilon) \to 0$ .
Sufficiency. Lemma 2, $\mathbf{P}\{\pi^{(l)} > \varepsilon\} \le 2\,\mathbf{P}\{\rho^{(l)} \ge \varepsilon/2\}$ for $l \ge 2/\varepsilon^2$ ; the per-sample permutation bound $2\Delta^S(x_1, \dots, x_{2l}) e^{-\varepsilon^2 l/8}$ ; and

\mathbf{P}\{\rho^{(l)} \ge \tfrac{\varepsilon}{2}\} \le 2\Bigl(\frac{2}{e}\Bigr)^{\varepsilon^2 l/8} + \mathbf{P}\Bigl\{\tfrac{1}{2l}\log_2 \Delta^S(x_1, \dots, x_{2l}) > \tfrac{\varepsilon^2}{16}\Bigr\} .

Necessity. Lemma 1 (Sauer–Shelah in sequence form); step 1°, $1 - \mathbf{P}(C') \ge (1 - \mathbf{P}(Q))^2$ with $C' = \{\rho^{(l)} > 2\varepsilon\}$ ; (26), $\mathbf{P}\{\Delta^S > \Phi([ql], l)\} \to 1$ when $0 < q < \frac14$ and $q\log_2(2e/q) < c$ ; and (29), $\mathbf{P}\{\pi^{(l)} > \varepsilon\} \to 1$ when moreover $0 < \varepsilon < q/7$ .

Significance

Theorem 4 characterizes uniform convergence for a given distribution exactly, with no gap between the necessary and the sufficient condition. It separates the cases the growth-function bound cannot: a class may have $m^S(l) = 2^l$ for every $l$ (all open subsets of $[0,1]$ ) and still satisfy $H^S(l)/l \to 0$ under a particular $P$ , or fail it. The entropy $H^S(l)$ is the distribution-dependent quantity from which later work on Glivenko–Cantelli classes and on consistency of empirical risk minimization proceeds; the 1981 paper of the same authors extends the criterion to classes of functions. The quantitative form (29) states more than the negation of convergence: when the entropy rate is positive, the maximal deviation stays above a fixed $\varepsilon$ with probability tending to one.

The result has been proved since 1971; it has not been formalized. The platform holds Sauer–Shelah variants over sets of distinct points and PAC bounds with other constants, but no statement of the VC entropy or of Theorem 4. The mission produces machine-checked statements of the entropy criterion and of its supporting lemmas with the paper's own constants ( $l \ge 2/\varepsilon^2$ , $2e^{-\varepsilon^2 l/8}$ , $\delta = \varepsilon^2/16$ , $\varepsilon < q/7$ ).

Difficulty

The sufficiency half is a variant of the proof of the growth-function bound; its new ingredient is the concentration of $l^{-1} \log_2 \Delta^S$ (Lemma 4), which needs subadditivity and a law of large numbers over independent blocks of the sample rather than a single mean estimate. The hypergeometric tail estimate behind the permutation bound is omitted in the paper ("a simple but long computation").

Necessity is harder. The obvious attempt, bounding $\mathbf{P}\{\pi^{(l)} > \varepsilon\}$ from below by exhibiting a single bad event, fails: $S$ may be uncountable and no single $A$ deviates with non-vanishing probability. A positive entropy rate has to be converted into a combinatorial statement about typical samples ((26) combines Lemma 4 with an estimate of $\Phi([ql], l)$ ), and that statement back into a lower bound on a probability over the product measure; the constants $q < \frac14$ and $\varepsilon < q/7$ must be tracked through both conversions, and the conclusion $\lim \mathbf{P}\{\pi^{(l)} > \varepsilon\} = 1$ needs the unweakened inequality of step 1°.

Formalization scope

A sample of size $l$ is a function Fin l → X (positions $0, \dots, l-1$ ) and its law is the product measure Measure.pi (fun _ => P), with P a probability measure. A subsample is a set of positions, so the index counts distinct Finset (Fin l) of the form $\{i : x_i \in A\}$ . The halves of x : Fin (l + l) → X are x ∘ Fin.castAdd l and x ∘ Fin.natAdd l. $P_A$ is P.real A; the suprema $\pi^{(l)}$ and $\rho^{(l)}$ are real suprema over the subtype of $S$ (values in $[0,1]$ ; $0$ for $S = \emptyset$ ). $H^S(l)$ is a Bochner integral of Real.logb 2 of the index, and $[ql]$ is ⌊q * l⌋₊. Probabilities are values in $[0, \infty]$ , except in the inequalities between probabilities (step 1°, the sufficiency estimate), which use Measure.real.

Measurability. The paper assumes, and the statements carry as hypotheses, that the events of $S$ are measurable (p. 264), that $\pi^{(l)}$ is a random variable (p. 265), that $\rho^{(l)}$ is measurable (p. 268), and that the index is measurable in the sample (p. 273). Each statement carries the ones its proof uses. Without them the Bochner integral defining $H^S(l)$ can be the junk value $0$ and the equivalence can fail; replacing them by " $S$ countable" would weaken the theorem. The goal is not trivialized by degenerate cases: the equivalence is not vacuous for any class, and $S = \emptyset$ gives the true instance $H^S = 0$ , $\pi^{(l)} = 0$ .

Corrections of the printed text. Lemma 2 is printed for $l > 2/\varepsilon^2$ ; its proof gives $l \ge 2/\varepsilon^2$ , which is stated. On p. 275 Lemma 2 is recalled as " $2\mathbf{P}(C) \ge \frac12 P(Q)$ ", meaning $\mathbf{P}(C) \ge \frac12\mathbf{P}(Q)$ . On p. 276 the first display carries a stray upper limit "4" on the integral, and the region of integration is printed $\{\log_2 \Delta^S \le 2\delta\}$ where $\{\log_2\Delta^S \le 2\delta l\}$ is meant. The event $C'$ is defined with " $> 2\varepsilon$ " (p. 276) but integrated in step 3° as $\theta(\cdot - 2\varepsilon)$ , which counts " $\ge 2\varepsilon$ "; the strict form is stated, and the estimate of step 3° is itself strict. Step 1° is stated unweakened. Milestone texts are verbatim.

Contributions welcome: a reusable development of the index and its submultiplicativity, the hypergeometric tail bound for sampling without replacement, a block law of large numbers for subadditive functionals of i.i.d. samples, and the permutation-invariance argument for product measures on Fin (l + l) → X.

Selected references

V. N. Vapnik and A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and Its Applications 16(2) (1971), 264–280. https://doi.org/10.1137/1116025
V. N. Vapnik and A. Ya. Chervonenkis, Necessary and sufficient conditions for the uniform convergence of means to their expectations, Theory of Probability and Its Applications 26(3) (1981), 532–553. https://doi.org/10.1137/1126059
M. Talagrand, The Glivenko–Cantelli problem, Annals of Probability 15(3) (1987), 837–870. https://doi.org/10.1214/aop/1176992069
R. M. Dudley, E. Giné and J. Zinn, Uniform and universal Glivenko–Cantelli classes, Journal of Theoretical Probability 4(3) (1991), 485–510. https://doi.org/10.1007/BF01210321

16 thms3 active usersReviewed

Completed

Machine Learning Probability·Captain: mikedeng1

On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities II: The Uniform Deviation BoundResearch Paper

Motivation

Bernoulli's law of large numbers says that the relative frequency of a single event $A$ in $l$ independent trials converges in probability to $P(A)$ . Statistics and learning theory need more: the probabilities of a whole class $S$ of events are judged from one and the same sample, so the frequencies must converge uniformly over the class. Uniform convergence can fail even for simple classes (all open subsets of $[0,1]$ ), so one needs a criterion that says when it holds and how fast.

Vapnik and Chervonenkis gave the first distribution-free answer in On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities (Theory Probab. Appl. 16 (1971) 264–280, doi:10.1137/1116025). Its Theorem 2, now called the VC inequality, bounds the probability of a uniform deviation larger than $\varepsilon$ by a combinatorial quantity of the class times an exponentially small factor.

Timeline:

1933: Glivenko and Cantelli prove uniform almost-sure convergence of the empirical distribution function on the line (the class of rays $\{x \le a\}$ ).
1971: Vapnik and Chervonenkis publish the growth function, the VC inequality (Theorem 2), almost-sure convergence under polynomial growth (Theorem 3) and the entropy criterion (Theorem 4).
1972: Sauer and Shelah independently prove the polynomial bound on the growth function (the paper's Lemma 1).
From the late 1970s: the inequality is sharpened in its constants and extended to empirical processes (Dudley, Pollard, Talagrand).

Setting

Let $(X, P)$ be a probability space and $S$ a collection of measurable events $A \subseteq X$ , with probabilities $P_A$ . A sample of size $l$ is a sequence $x_1, \dots, x_l$ of points of $X$ drawn independently with law $P$ , so the sample has the product law $P^l$ on $X^l$ . The relative frequency of $A$ in the sample is $\nu_A^{(l)} = n_A / l$ , where $n_A$ is the number of sample terms in $A$ . The uniform deviation is

\pi^{(l)} = \sup_{A \in S} \bigl|\nu_A^{(l)} - P_A\bigr|.

Each $A \in S$ induces in a sample $x_1, \dots, x_r$ the subsample of terms lying in $A$ . The index $\Delta^S(x_1, \dots, x_r)$ is the number of different subsamples so induced (at most $2^r$ ), and the growth function is $m^S(r) = \max \Delta^S(x_1, \dots, x_r)$ over all samples of size $r$ .

For a double sample $x_1, \dots, x_{2l}$ let $\nu'_A$ and $\nu''_A$ be the frequencies of $A$ in the two semi-samples $x_1, \dots, x_l$ and $x_{l+1}, \dots, x_{2l}$ , and let

\rho^{(l)} = \sup_{A \in S} \bigl|\nu'_A - \nu''_A\bigr|.

Following the paper, $\pi^{(l)}$ and $\rho^{(l)}$ are assumed to be measurable functions of the sample for every $l$ .

Formalization targets

Goal: Theorem 2 (p. 269)

For every $\varepsilon > 0$ and every $l \ge 2/\varepsilon^2$ ,

P\bigl(\pi^{(l)} > \varepsilon\bigr) \le 4\, m^S(2l)\, e^{-\varepsilon^2 l/8}.

The constants $4$ and $1/8$ and the growth function at $2l$ are the paper's.

Milestones, in the order of the proof

Lemma 2 (p. 268): for $l \ge 2/\varepsilon^2$ , $P\{\rho^{(l)} \ge \varepsilon/2\} \ge \tfrac12 P\{\pi^{(l)} > \varepsilon\}$ .
Eq. (11) (p. 270): $P\{\rho^{(l)} \ge \varepsilon/2\} = \int \frac{1}{(2l)!} \sum_{T} \theta\bigl(\rho^{(l)}(T X_{2l}) - \varepsilon/2\bigr)\, dP$ , the sum over all permutations $T$ of the $2l$ positions ( $\theta$ the indicator of $[0, \infty)$ ).
The $\Gamma$ estimate (p. 271): for $0 \le m \le 2l$ ,

\Gamma = \sum_{k : |2k/l - m/l| \ge \varepsilon/2} \frac{\binom{m}{k}\binom{2l-m}{l-k}}{\binom{2l}{l}} \le 2e^{-\varepsilon^2 l/8}.

The per-sample permutation bound (p. 271): for every fixed double sample, $\frac{1}{(2l)!}\sum_T \theta\bigl(\rho^{(l)}(T X_{2l}) - \varepsilon/2\bigr) \le 2\Delta^S(x_1, \dots, x_{2l})\, e^{-\varepsilon^2 l/8}$ .
The semi-sample bound (p. 271): $P\{\rho^{(l)} \ge \varepsilon/2\} \le 2\, m^S(2l)\, e^{-\varepsilon^2 l/8}$ for every $l \ge 1$ .

Further items (consequences, not milestones)

Corollary (p. 269): if $m^S(l) \le l^n + 1$ for all $l$ and some finite $n$ , then $P(\pi^{(l)} > \varepsilon) \to 0$ for every $\varepsilon > 0$ .
Theorem 3 (p. 271): under the same condition, $P(\pi^{(l)} \to 0) = 1$ for an infinite i.i.d. sequence.

Significance

The bound holds for every distribution $P$ and depends on the class only through $m^S(2l)$ . Together with the paper's Theorem 1 (the growth function is either $2^r$ for every $r$ or bounded by $r^n + 1$ ), it shows that every class whose growth function is not identically $2^r$ enjoys uniform convergence at an exponential rate in probability and almost surely. The Glivenko–Cantelli theorem is the special case of rays on the line. The inequality underlies sample-complexity bounds for empirical risk minimization, the "finite VC dimension implies learnability" direction of the fundamental theorem of statistical learning, and the theory of empirical processes indexed by sets.

The result has been proved for more than fifty years; what is missing is a machine-checked proof of it in its original form. Formal libraries contain Hoeffding-type inequalities for independent variables and textbook uniform-convergence statements with other constants, stated for hypothesis classes and loss functions. This mission produces the 1971 statement itself, with its constants and its sequence-based index, together with the combinatorial tail bound for sampling without replacement that the paper states without proof.

Difficulty

The obvious argument applies Hoeffding's inequality to each $A \in S$ and takes a union bound. This fails as soon as $S$ is infinite, and the classes of interest are uncountable. The growth function can only enter after the probabilities $P_A$ have been removed from the event, because only then does the event depend on the finitely many subsamples that $S$ induces on a finite sample. Lemma 2 does this at the price of the condition $l \ge 2/\varepsilon^2$ and a factor $2$ .

The second difficulty is combinatorial. Under a random rearrangement of a fixed double sample, the number of points of an event that fall into the first half is hypergeometric, not binomial. The paper states the required tail bound $\Gamma \le 2e^{-\varepsilon^2 l/8}$ and omits the "simple but long computation". Mathlib has no tail bound for sampling without replacement.

Formalization scope

Samples are functions Fin l → X with 0-based positions; repetitions are allowed. The subsample induced by $A$ is the set of positions {i | x i ∈ A}, so the index counts distinct sets of positions and the growth function maximizes over sequences, not finite point sets (the paper's model; the two differ when $X$ has fewer than $r$ points). The sample law is Measure.pi (fun _ : Fin l => P). The double sample is Fin (l + l) → X, read through Fin.castAdd and Fin.natAdd, and $m^S(2l)$ is growth S (2 * l). Suprema are real suprema over the events of $S$ (values in $[0, 1]$ ; $0$ for $S = \emptyset$ ). Probabilities are values in $[0, \infty]$ and the bounds enter through ENNReal.ofReal. Theorem 3 uses the infinite product Measure.infinitePi and evaluates $\pi^{(l)}$ on the first $l$ coordinates.

The measurability of $\pi^{(l)}$ (p. 265) and of $\rho^{(l)}$ (p. 268) are the paper's own assumptions and are carried as hypotheses. Without them Theorem 2 can fail for uncountable classes; replacing them by a stronger condition such as countability of $S$ would weaken the theorem.

A trivializing formalization is ruled out as follows: $\varepsilon > 0$ is stated, which forces $l \ge 1$ and so avoids the value $0/0 = 0$ of the frequency. The supremum runs over the events of $S$ , not over all subsets. The index counts distinct subsamples, not sets.

Corrections of the printed text:

Lemma 2 is printed for $l > 2/\varepsilon^2$ , but its proof concludes for $l \ge 2/\varepsilon^2$ , and Theorem 2 uses $l = 2/\varepsilon^2$ . The $\ge$ form is stated, which is the stronger statement.
The text before the permutation bound describes the averaged quantity as counting arrangements with $|\nu'_A - \nu''_A| \le \tfrac12\varepsilon$ ; the indicator and the index set of $\Gamma$ count those with $\ge \tfrac12\varepsilon$ , which is what is stated.
Slips in the proof of Lemma 2 that do not affect any statement: $\varepsilon/3$ printed for $\varepsilon/2$ on p. 269, and $<$ , $>$ where Chebyshev's inequality gives $\le$ , $\ge$ .
Theorem 2 prints "more then" for "more than".

Needed infrastructure:

the invariance of Measure.pi under permutations of coordinates;
the splitting of Fin (l + l) into two halves under the product measure;
Chebyshev's inequality for binomial frequencies;
a hypergeometric (sampling without replacement) tail bound.

The last two are reusable beyond this mission. Proofs of any milestone are welcome.

Selected references

V. N. Vapnik and A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory Probab. Appl. 16(2) (1971) 264–280. https://doi.org/10.1137/1116025
W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830
N. Sauer, On the density of families of sets, J. Combin. Theory Ser. A 13 (1972) 145–147. https://doi.org/10.1016/0097-3165(72)90019-2
S. Shalev-Shwartz and S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Ch. 6 and 28. https://doi.org/10.1017/CBO9781107298019

9 thms3 active usersReviewed

Completed

Machine Learning Probability·Captain: mikedeng1

Learnability, Stability and Uniform Convergence I: A Problem Is Learnable if and only if It Admits a Uniform-RO Stable Universal AERMResearch Paper

Motivation

In supervised binary classification, a hypothesis class is learnable if and only if it has uniform convergence, meaning that empirical risks converge to true risks uniformly over the class. When that holds, empirical risk minimisation (ERM) learns. This equivalence, due to Vapnik and Chervonenkis and extended to real-valued losses by Alon, Ben-David, Cesa-Bianchi and Haussler, is the usual starting point of statistical learning theory.

Vapnik's General Learning Setting is broader. It covers stochastic convex optimisation, clustering and density estimation, and in it the equivalence breaks down. Shalev-Shwartz, Shamir, Srebro and Sridharan (JMLR 11 (2010) 2635–2670) exhibit learnable problems with no uniform convergence, and learnable problems where ERM fails. So neither uniform convergence nor the success of ERM characterises learnability there, and something else has to. This mission formalizes the paper's answer, its Theorem 7: stability.

Timeline:

1971–1995: Vapnik and Chervonenkis prove learnability ⇔ uniform convergence for binary classification. Vapnik (1995) introduces the General Learning Setting.
2002: Bousquet and Elisseeff show that uniform stability of a learning rule implies generalization.
2006: Mukherjee, Niyogi, Poggio and Rifkin show that, in the supervised setting, stability of ERM is necessary and sufficient for learnability.
2009–2010: Shalev-Shwartz, Shamir, Srebro and Sridharan (COLT 2009, JMLR 2010) prove that, in the General Learning Setting, learnability is equivalent to the existence of a uniform-RO stable, universally asymptotic empirical risk minimiser (Theorem 7).

Setting

A learning problem consists of a hypothesis class $\mathcal H$ (nonempty), an instance set $\mathcal Z$ with a $\sigma$ -algebra, and an objective $f:\mathcal H\times\mathcal Z\to\mathbb R$ with $|f(h;z)|\le B$ for all $h,z$ . Given a probability distribution $\mathcal D$ on $\mathcal Z$ and an i.i.d. sample $S=(z_1,\dots,z_m)\sim\mathcal D^m$ , the following quantities are defined:

the risk is $F(h)=\mathbb E_{z\sim\mathcal D}[f(h;z)]$ , and $F^*=\inf_{h}F(h)$ ;
the empirical risk is $F_S(h)=\frac1m\sum_{i=1}^m f(h;z_i)$ , and $F_S(\hat h_S)=\inf_h F_S(h)$ is the minimal empirical risk. Only the value is used; no minimiser need exist.

A learning rule $A$ maps each sample $S$ of each size $m$ to a hypothesis $A(S)$ . A rate $\varepsilon(m)$ is a non-increasing sequence tending to $0$ . For a rule $A$ the paper defines the following properties:

$A$ is consistent with rate $\varepsilon_{\rm cons}$ under $\mathcal D$ if $\mathbb E_S[F(A(S))-F^*]\le\varepsilon_{\rm cons}(m)$ . It is universally consistent if this holds for every $\mathcal D$ with the same rate. The problem is learnable (Definition 1) if a universally consistent rule exists.
$A$ is an AERM (asymptotic empirical risk minimiser) with rate $\varepsilon_{\rm erm}$ under $\mathcal D$ if $\mathbb E_S[F_S(A(S))-F_S(\hat h_S)]\le\varepsilon_{\rm erm}(m)$ , and universally so if this holds for every $\mathcal D$ .
$A$ generalizes with rate $\varepsilon_{\rm gen}$ under $\mathcal D$ if $\mathbb E_S[|F(A(S))-F_S(A(S))|]\le\varepsilon_{\rm gen}(m)$ .
With $S^{(i)}$ the sample $S$ with $z_i$ replaced by $z_i'$ , $A$ is uniform-RO stable with rate $\varepsilon_{\rm stable}$ (Definition 4) if, for all $S$ , all replacements $(z_1',\dots,z_m')$ and all $z'\in\mathcal Z$ ,

\frac1m\sum_{i=1}^m\bigl|f(A(S^{(i)});z')-f(A(S);z')\bigr|\le\varepsilon_{\rm stable}(m).

Average-RO stability (Definition 5) is the in-expectation analogue, with the replacement point also serving as the test point.

Formalization targets

Goal: Theorem 7

The problem is learnable if and only if there is a learning rule that is uniform-RO stable and universally an AERM. Quantitatively, if $A$ is universally consistent with rate $\varepsilon_{\rm cons}$ , then some rule $A'$ is uniform-RO stable and universally AERM with

\varepsilon_{\rm stable}(m)=\frac{2B}{\sqrt m},\qquad \varepsilon_{\rm erm}(m)=3\,\varepsilon_{\rm cons}\bigl(\lfloor m^{1/4}\rfloor\bigr)+\frac{8B}{\sqrt m},

and conversely, a uniform-RO stable universal AERM is universally consistent with rate $\varepsilon_{\rm stable}(m)+\varepsilon_{\rm erm}(m)$ .

Milestones

These follow the order of the paper's proof.

Sufficiency: Utility Lemma 12 (a bounded sample mean deviates by at most $B/\sqrt m$ in expectation), Lemma 11 (on-average generalization ⇔ average-RO stability), Claim 6 (uniform-RO ⇒ average-RO stability), Lemma 15 (an on-average generalizing AERM is consistent), and Theorem 8 (a stable AERM is consistent with rate $\varepsilon_{\rm stable}+\varepsilon_{\rm erm}$ and generalizes with rate $\varepsilon_{\rm stable}+2\varepsilon_{\rm erm}+2B/\sqrt m$ ).
Necessity: Lemma 20 (every rule has a uniform-RO stable, $3B/\sqrt m$ -generalizing version with consistency rate $\varepsilon_{\rm cons}(\lfloor\sqrt m\rfloor)$ ), Lemma 16, the Main Converse Lemma ( $\mathbb E|F_S(\hat h_S)-F^*|\le2\varepsilon_{\rm cons}(m')+2B/\sqrt m+2Bm'^2/m$ for $2\le m'\le m/2$ ), and Lemma 18 (under that bound, a consistent and generalizing rule is an AERM).

Significance

Theorem 7 shows that in the General Learning Setting, stability replaces uniform convergence as the notion that characterises learnability. It also says where to look for a learning rule: ERM may fail, but some AERM always works, and it must be stable. The rates are explicit and polynomial. Downstream, the paper uses Theorem 7 to prove Theorem 23 (randomised rules) and to design a generic learning algorithm (Theorem 25). Mission II of this series (Tikhonov-regularised ERM for stochastic convex optimisation) is a concrete instance of a stable AERM for a problem with no uniform convergence.

The theorem has been proved since 2010 but has not been formalized. The platform has the textbook side of the same authors' framework: Understanding Machine Learning Theorem 13.2, UnderstandingML.stability_identity, the replace-one identity behind Lemma 11, stated for hypotheses in $\mathbb R^d$ . The platform does not have learnability in the General Learning Setting, over an arbitrary hypothesis class, or the converse direction. That direction is the new content: learnability forces a stable AERM to exist.

Difficulty

The sufficiency direction is a chain of expectation identities. The necessity direction is harder. A universally consistent rule need not be an AERM, need not generalize and need not be stable (Example 2 of the paper), so it cannot simply be reused. ERM cannot be used either, since it can fail on learnable problems. The Main Converse Lemma is where universal consistency is used in full: the rule's guarantee has to be applied under a distribution other than $\mathcal D$ , and a naive argument under $\mathcal D$ alone fails (Example 1: consistency under one distribution does not imply generalization under it). Combining the lemmas into the stated rates requires choosing the auxiliary sample size and tracking every constant, including the regime of small $m$ where Lemma 16's hypothesis $2\le m'\le m/2$ cannot be met.

Formalization scope

Samples are Fin m → Z, the sample law $\mathcal D^m$ is Measure.pi, and $S^{(i)}$ is Function.update S i (S' i). Learning rules have type (m : ℕ) → (Fin m → Z) → H, and every property is asserted for $m\ge1$ . The minimal empirical risk and $F^*$ are real infima over the nonempty, bounded-below family, never values at a chosen minimiser. Rates are non-increasing on $m\ge1$ and tend to $0$ . $\lfloor m^{1/4}\rfloor$ and $\lfloor\sqrt m\rfloor$ are Nat.sqrt (Nat.sqrt m) and Nat.sqrt m, the paper's $\varepsilon_{\rm cons}(m^{1/4})$ read at an integer sample size. The paper's $B=\sup|f|$ is replaced by any bound $B$ (all rates increase in $B$ ).

The paper never discusses measurability. This formalization adds one standing assumption, identical across the series: each $f(h;\cdot)$ is measurable, the minimal empirical risk $S\mapsto\inf_hF_S(h)$ is measurable (true for countable $\mathcal H$ , for example), and every learning rule, whether assumed or asserted to exist, has $(S,z)\mapsto f(A(S);z)$ jointly measurable. Without this a non-measurable rule would have Bochner integrals equal to $0$ , and existence claims such as "some rule is a universal AERM" would be satisfied by junk. Every existential in the goal therefore produces a measurable rule, and learnability is quantified over measurable rules with the rate chosen before the distribution. Uniform-RO stability is pointwise over all samples, replacement vectors and test points; it is never replaced by the in-expectation Definition 5.

No statement is corrected. The proof of the converse in the paper calls $A'$ " $2B/\sqrt m$ -generalizing" where Lemma 20 gives $3B/\sqrt m$ . The stated $8B/\sqrt m$ absorbs either value, so Theorem 7 is formalized as printed.

The definitions (risks, rules, consistency, AERM, generalization, the two RO-stability notions) are reusable by the other missions of this series and by any stability-based result in the General Learning Setting. Contributions are welcome at every level: proofs of the milestones, the measure-theoretic infrastructure they need (exchangeability of i.i.d. coordinates under Measure.pi, sub-sampling and restriction of product measures, the variance bound for bounded sample means), and the remaining results of Section 5 (Theorems 9 and 10, Lemmas 14 and 17).

Selected references

S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, Stability and Uniform Convergence, Journal of Machine Learning Research 11 (2010) 2635–2670. https://jmlr.org/papers/v11/shalev-shwartz10a.html
V. N. Vapnik, The Nature of Statistical Learning Theory, Springer, 1995. https://doi.org/10.1007/978-1-4757-2440-0
N. Alon, S. Ben-David, N. Cesa-Bianchi, D. Haussler, Scale-sensitive dimensions, uniform convergence, and learnability, Journal of the ACM 44(4) (1997) 615–631. https://doi.org/10.1145/263867.263927
O. Bousquet, A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://jmlr.org/papers/v2/bousquet02a.html
S. Mukherjee, P. Niyogi, T. Poggio, R. Rifkin, Learning theory: stability is sufficient for generalization and necessary and sufficient for consistency of empirical risk minimization, Advances in Computational Mathematics 25 (2006) 161–193. https://doi.org/10.1007/s10444-004-7634-z
S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 13. https://doi.org/10.1017/CBO9781107298019

12 thms3 active usersReviewed

Completed

Machine Learning Probability·Captain: mikedeng1

Adversarially Robust Generalization Requires More Data 4: Robust Learning from One Thresholded Sample in the Bernoulli ModelResearch Paper

Motivation

Classifiers trained to high standard accuracy can be fooled by small, deliberately chosen perturbations of their inputs, so-called adversarial examples (Szegedy et al., 2014; Goodfellow et al., 2015). Training methods that aim at robustness against perturbations bounded in the $\ell_\infty$ norm reach high robust accuracy on the training set while robust test accuracy stays far lower, a gap much larger than the standard generalization gap (Madry et al., 2018). Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285) ask whether this gap is intrinsic: does learning a robust classifier need more data than learning an accurate one?

They answer with two simple data distributions. In a Gaussian model the robust sample complexity is larger than the standard one by a factor of order $\sqrt d$ , for every learning algorithm. In a Bernoulli model on the hypercube, linear classifiers suffer the same penalty, but a nonlinear classifier does not. This mission formalizes the second half of that picture: in the Bernoulli model, thresholding the input and then applying the linear classifier learned from one single sample is robust against every $\ell_\infty$ perturbation of size less than $1$ .

Setting

Points live in $\mathbb R^d$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|_2$ . Labels are $y\in\{\pm1\}$ . A binary classifier is any map $f:\mathbb R^d\to\{\pm1\}$ , and for $w\in\mathbb R^d$ the linear classifier is $f_w(x)=\operatorname{sgn}(\langle w,x\rangle)$ .

The $(\theta^\star,\tau)$ -Bernoulli model. Fix a sign vector $\theta^\star\in\{\pm1\}^d$ and a bias $\tau\in(0,\tfrac12]$ . A sample $(x,y)$ is drawn by choosing $y$ uniformly in $\{\pm1\}$ and then, independently for each coordinate $i$ , setting $x_i=y\theta^\star_i$ with probability $\tfrac12+\tau$ and $x_i=-y\theta^\star_i$ with probability $\tfrac12-\tau$ . So $x\in\{\pm1\}^d$ , and each coordinate carries a weak signal of strength $2\tau$ about the label.

Errors. The classification error of $f$ is $\mathbb P_{(x,y)}[f(x)\ne y]$ . For $\varepsilon\in\mathbb R$ the $\ell_\infty$ ball is $\mathcal B^\varepsilon_\infty(x)=\{x'\in\mathbb R^d:\|x'-x\|_\infty\le\varepsilon\}$ , and the $\ell_\infty^\varepsilon$ -robust classification error of $f$ is

\mathbb P_{(x,y)}\big[\exists\,x'\in\mathcal B^\varepsilon_\infty(x):\ f(x')\ne y\big].

The adversary may move $x$ anywhere in the ball, including off the hypercube.

Thresholding. The thresholding map $T:\mathbb R^d\to\mathbb R^d$ is $T(x)_i=+1$ if $x_i\ge0$ and $T(x)_i=-1$ otherwise. The classifier studied is $f_{\hat w}\circ T$ , with $\hat w=yx$ computed from one training sample $(x,y)$ .

Formalization targets

Goal: Theorem 10 (p. 8)

There is a universal constant $c>0$ such that, whenever $\tau\ge c\,d^{-1/4}$ and $(x,y)$ is one sample of the model with $\hat w=yx$ ,

\mathbb P_{(x,y)}\Big[\exists\,\varepsilon<1:\ \mathrm{RobErr}_\varepsilon\big(f_{\hat w}\circ T\big)>\tfrac1{100}\Big]\ \le\ \exp\!\Big(-\frac{\tau^2d}{2}\Big).

The constant $c$ is left existential; only the scaling $\tau\gtrsim d^{-1/4}$ is fixed. The failure probability is the one the paper proves for the same classifier.

Milestones

Lemma 24 (p. 31): $\mathbb P\big[\langle z,\theta^\star\rangle\le2\tau d-\sqrt{2d\log(1/\delta)}\big]\le\delta$ for $z=xy$ .
Lemma 25 (p. 31): for $\hat w=z/\|z\|_2$ , $\mathbb P[\langle\hat w,\theta^\star\rangle\le\tau\sqrt d]\le\exp(-\tau^2d/2)$ .
Lemma 26 (p. 32): for a fixed unit $w$ with $\langle w,2\tau\theta^\star\rangle\ge0$ , $\mathbb P[\langle w,z\rangle\le0]\le\exp(-2\tau^2\langle w,\theta^\star\rangle^2)$ .
Theorem 27 (p. 32): with probability at least $1-\exp(-\tau^2d/2)$ , $f_{\hat w}$ has classification error at most $\exp(-2\tau^4d)$ .
Corollary 28 (p. 33): if $\tau\ge(\log(1/\beta)/(2d))^{1/4}$ , then with probability at least $1-\exp(-\tau^2d/2)$ , $f_{\hat w}$ has classification error at most $\beta$ .
Thresholding identity (§2.2, p. 7): $T(\mathcal B^\varepsilon_\infty(x))=\{x\}$ for every $x\in\{\pm1\}^d$ and $0\le\varepsilon<1$ .

Significance

Together with the lower bound for linear classifiers in the same model (Theorem 9 of the paper), Theorem 10 shows that robust sample complexity depends on the hypothesis class and on the data distribution, not only on the perturbation size: a fixed nonlinear preprocessing step closes a gap that no linear classifier can close. The paper's Gaussian model shows the opposite behaviour, where every learner pays the $\sqrt d$ penalty, so the two models together separate "robustness is information-theoretically expensive" from "robustness is expensive for a restricted class". The authors also report that an explicit thresholding layer improves robust training on MNIST, which motivates the model.

The result is proved in the paper. To the platform's knowledge it has no machine-checked proof. Formalizing it yields a complete, finite and self-contained robust-learning upper bound, the single-sample standard-generalization bounds of Theorem 27 and Corollary 28 as reusable statements, and a worked instance of one-sided Hoeffding bounds for weighted sums of hypercube coordinates.

Difficulty

The concentration steps are standard, but the natural first approach to the goal fails: a bound on the classification error of the linear classifier $f_{\hat w}$ says nothing about its robust error, and for $\varepsilon$ of order $\tau$ the robust error of every linear classifier is close to $\tfrac12$ . The goal concerns the nonlinear classifier $f_{\hat w}\circ T$ , whose robustness rests on the data lying exactly on the hypercube and on the adversary's budget being below $1$ ; neither fact is visible to an argument about linear classifiers. A second difficulty is bookkeeping: the paper uses three forms of the estimator ( $yx$ , $z/\|z\|_2$ , $yx/\|x\|_2$ ), a training sample and a test sample with the same name, and a failure event that must hold for all $\varepsilon<1$ at once.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d). Labels and hypercube coordinates are Bool ( $+1\leftrightarrow$ true). Because the model is finite, every probability is a finite sum of the weights $\tfrac12\prod_i(\tfrac12\pm\tau)$ ; no measure theory is involved. Conventions committed to:

coordinates of $x$ are independent given $y$ (the paper's "sampling each coordinate", as its proofs use it);
$0<\tau\le\tfrac12$ in every theorem, since $\tfrac12-\tau$ must be a probability;
$\operatorname{sgn}(0)$ is taken as $+1$ (a tie is classified $+1$ ); $T$ sends $0$ to $+1$ , as printed;
the $\ell_\infty$ ball is written coordinatewise, never as the Euclidean ball;
"with probability at least $1-q$ , the error is at most $\beta$ " is stated as "the failure event has probability at most $q$ ";
the goal's "for any $\varepsilon<1$ " is inside the event, one good sample for all $\varepsilon$ ;
added hypotheses, each forced by a degenerate case where the printed statement is false: $d\ge1$ in Lemma 24, $\beta>0$ in Corollary 28, $\varepsilon\ge0$ in the thresholding identity.

A formalization that bounds only the standard error of $f_{\hat w}$ , drops $T$ , uses the Euclidean ball, or lets the estimator see $\theta^\star$ would be a different and easier statement; the goal rules each of these out.

A complete development needs one-sided Hoeffding bounds for weighted sums of independent bounded variables on a finite product space (Mathlib has the measure-theoretic version, ProbabilityTheory.measure_sum_ge_le_of_iIndepFun with hasSubgaussianMGF_of_mem_Icc) and the transfer between the finite-sum encoding and a product measure. Both are reusable beyond this mission. Proofs of any milestone, and a bridge lemma from bprob to Measure.pi, are welcome. The other missions of this series (Gaussian lower bound, Bernoulli lower bound for linear classifiers, Gaussian upper bound) formalize the paper's remaining main results.

Selected references

L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, NeurIPS 2018; arXiv:1804.11285v2. https://arxiv.org/abs/1804.11285
A. Madry, A. Makelov, L. Schmidt, D. Tsipras, A. Vladu, Towards Deep Learning Models Resistant to Adversarial Attacks, ICLR 2018. https://arxiv.org/abs/1706.06083
C. Szegedy et al., Intriguing properties of neural networks, ICLR 2014. https://arxiv.org/abs/1312.6199
I. Goodfellow, J. Shlens, C. Szegedy, Explaining and Harnessing Adversarial Examples, ICLR 2015. https://arxiv.org/abs/1412.6572
P. Rigollet, J.-C. Hütter, High Dimensional Statistics, lecture notes, MIT, 2017. https://math.mit.edu/~rigollet/PDFs/RigNotes17.pdf

8 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Are Call Center and Hospital Arrivals Well Modeled by Nonhomogeneous Poisson Processes?: Combining k Equal Subintervals of a Linear Arrival Rate Bounds the Degree of Nonhomogeneity by C/kResearch Paper

Motivation

Arrival processes to call centers and hospital emergency departments are routinely modeled as nonhomogeneous Poisson processes (NHPPs): Poisson processes whose arrival rate varies over the day. Staffing and queueing models built on this assumption are only as good as the assumption itself, so practitioners test it on data. The standard test, going back to Brown et al. (2005, doi:10.1198/016214504000001808), divides the day into short subintervals, treats the rate as constant on each, rescales the arrival times within each subinterval to $[0,1]$ , combines all the rescaled data, and applies a Kolmogorov–Smirnov (KS) test of uniformity.

Kim and Whitt (2014, doi:10.1287/msom.2014.0490) ask when this piecewise-constant approximation is justified. If the true rate is not constant on a subinterval, the rescaled arrival times are not uniform, and with enough data the KS test rejects the Poisson hypothesis even when the process really is an NHPP. Section 3 of the paper quantifies this effect through a single number, the degree of nonhomogeneity, and shows how it behaves when the interval is cut into $k$ equal pieces. This mission formalizes that section's exact computations for a linear arrival rate.

Setting

An arrival rate function $\lambda$ on an interval $[0,T]$ , $T > 0$ , is nonnegative, integrable, and strictly positive except at finitely many points. Its cumulative arrival rate is

\Lambda(t) = \int_0^t \lambda(s)\,ds .

Conditionally on $n$ arrivals in $[0,T]$ , the arrival times of an NHPP with rate $\lambda$ , divided by $T$ , are distributed as the order statistics of $n$ independent random variables on $[0,1]$ with the conditional cdf

F(t) = \frac{\Lambda(tT)}{\Lambda(T)}, \qquad 0 \le t \le 1 .

The degree of nonhomogeneity is the Kolmogorov distance of $F$ from the uniform cdf,

D = \sup_{0 \le t \le 1} |F(t) - t| .

It is zero exactly when $\lambda$ is constant, and it is the limit of the KS test statistic as the amount of data grows.

For $k \ge 1$ , divide $[0,T]$ into $k$ subintervals of length $T/k$ . For $1 \le j \le k$ the $j$ -th subinterval has cumulative rate $\Lambda_j(t) = \Lambda((j-1)T/k + t) - \Lambda((j-1)T/k)$ , conditional cdf $F_j(t) = \Lambda_j(tT/k)/\Lambda_j(T/k)$ , and share of arrivals $p_j = (\Lambda(jT/k) - \Lambda((j-1)T/k))/\Lambda(T)$ . The data of all subintervals, each rescaled to $[0,1]$ and combined, have the conditional cdf $F = \sum_{j=1}^k p_j F_j$ (LEMMA 1).

The linear arrival rate is $\lambda(t) = a + bt$ with $b \ge 0$ and $a \ge 0$ , not identically zero. When $a > 0$ its relative slope is $r = b/a$ ; on the $j$ -th subinterval the relative slope is $r_j = b/\lambda((j-1)T/k)$ .

In the Lean development these are cumRate, condCdf, degree, subCum, subCdf, weight, mixCdf, linRate and subSlope, in the namespace NHPPArrivals.LinearRate.

Formalization targets

Goal: THEOREM 5, combining equally spaced subintervals

For the linear rate, there is a constant $C$ such that for every $k \ge 1$

D = \sup_{0 \le t \le 1}|F(t) - t| = \sum_{j=1}^k p_j D_j = \sum_{j=1}^k p_j \sup_{0 \le t \le 1}|F_j(t) - t|, \tag{20}

with, if $a > 0$ ,

D = \sum_{j=1}^k \frac{p_j\, r_j T/k}{8 + 4 r_j T/k}, \tag{21}

and, if $a = 0$ ,

D = \frac{p_1}{4} + \sum_{j=2}^k \frac{p_j/(j-1)}{8 + 4/(j-1)}, \tag{22}

and in both cases $D \le C/k$ . The constant $C$ may depend on $a$ , $b$ and $T$ , but not on $k$ ; its value is left open, as in the paper.

Milestones

LEMMA 1, (17): for a general rate, the rescaled combined data have cdf $\sum_j p_j F_j$ , and the $p_j$ form a probability vector.
THEOREM 4, $a > 0$ , (14), (16): $F(t) = (tT + r(tT)^2/2)/(T + rT^2/2)$ and $D = |F(1/2) - 1/2| = rT/(8 + 4rT)$ .
THEOREM 4, $a = 0$ , (15): $F(t) = t^2$ and $D = 1/4$ .
LEMMA 1, (18): closed forms of $\Lambda_j$ , $F_j$ , $p_j$ , $r_j$ when $a > 0$ .
LEMMA 1, (19): closed forms of $\Lambda_j$ , $F_j$ , $p_j$ , $r_j$ when $a = 0$ .
THEOREM 5, (20): $D = \sum_j p_j D_j$ for one fixed $k$ .

Significance

The result gives a quantitative criterion for the piecewise-constant approximation: for a linear rate, cutting the interval into $k$ equal pieces reduces the degree of nonhomogeneity of the combined data by a factor of order $1/k$ . Since the KS critical value at sample size $n$ is of order $1/\sqrt n$ , this tells a practitioner how fine the subintervals must be, relative to the amount of data, before a KS test of the Poisson hypothesis stops rejecting merely because the rate varies within subintervals. The paper's later THEOREM 6 and its practical guidelines (§3.4, §3.6) rest on these formulas.

The results are proved in the paper by direct calculation; none of them has a machine-checked proof. The mission produces a verified library of the conditional-cdf calculus for NHPPs on an interval (the conditional cdf, its degree of nonhomogeneity, the subinterval decomposition) and the exact linear-rate formulas that the testing literature cites.

Difficulty

The computations are elementary, but two steps are not immediate. First, the supremum of $|F(t) - t|$ over $[0,1]$ is a supremum of a nonsmooth function; showing that it is attained at $t = 1/2$ requires knowing the sign of $F(t) - t$ on the whole interval, and for the combined cdf it requires that all the pieces $F_j$ attain their maximal deviation at the same point, which is special to linear rates. For a general rate the naive identity $D = \sum_j p_j D_j$ fails: the sup of a sum is at most the sum of the sups, with equality only when the maximizers coincide. Second, LEMMA 1 is a statement about the law of a rescaled random variable (the fractional part of $kX/T$ ), which requires splitting a measure along the $k$ subintervals and handling their boundary points.

Formalization scope

Rates are real functions $\lambda : \mathbb R \to \mathbb R$ ; only their values on $[0,T]$ enter. $\Lambda$ is an interval integral, subintervals are indexed by $j \in \{1, \dots, k\}$ with $k, j$ natural numbers cast to reals, and $(j-1)$ is computed in $\mathbb R$ . All quotients are real divisions; the hypotheses of every statement ( $T > 0$ , $k \ge 1$ , $b \ge 0$ , and $a > 0$ or $b > 0$ for the linear rate; integrability, nonnegativity and a finite zero set for a general rate) make every denominator $\Lambda(T)$ and $\Lambda_j(T/k)$ positive. $b \ge 0$ is the paper's standing assumption of §3.3; excluding $a = b = 0$ is §3.2's requirement that the rate be positive except at finitely many points. The degree of nonhomogeneity is sSup of the image of $[0,1]$ , and every statement that uses it also asserts that the supremum is attained, so no default value of sSup can make a statement true. The constant $C$ of THEOREM 5 is quantified before $k$ ; choosing it after $k$ would make the bound empty. The statements are about the general definitions of (17) applied to $\lambda(t) = a + bt$ , not about the closed forms (18)–(19), which are separate milestones. The formula for $r_j$ in (19) is stated for $2 \le j \le k$ only: $r_1 = b/\lambda(0)$ is undefined when $a = 0$ .

The Poisson process itself is not formalized. LEMMA 1's "i.i.d. random variables" is the paper's THEOREM 1 (the conditioning property) applied to each arrival; LEMMA 1 is stated for the law of one arrival time, the probability measure with density $\lambda/\Lambda(T)$ on $[0,T]$ . THEOREM 1, THEOREMS 2–3 and COROLLARY 1 (limits of the empirical cdf and of the KS statistic) are out of scope: they need a point-process layer, the Glivenko–Cantelli theorem and KS critical values, none of which exists in Mathlib. THEOREM 6 is out of scope because the paper gives only a sketch comparing $D$ with the KS critical value.

Contributions welcome: proofs of the milestones, general lemmas on sups of $|F(t) - t|$ for convex cdfs, and the measure-splitting argument of LEMMA 1, which is reusable for any subinterval-based test of the Poisson hypothesis.

Selected references

S.-H. Kim and W. Whitt, Are call center and hospital arrivals well modeled by nonhomogeneous Poisson processes?, Manufacturing & Service Operations Management 16(3):464–480, 2014. doi:10.1287/msom.2014.0490
L. Brown, N. Gans, A. Mandelbaum, A. Sakov, H. Shen, S. Zeltyn, L. Zhao, Statistical analysis of a telephone call center: a queueing-science perspective, Journal of the American Statistical Association 100(469):36–50, 2005. doi:10.1198/016214504000001808
F. J. Massey, The Kolmogorov–Smirnov test for goodness of fit, Journal of the American Statistical Association 46(253):68–78, 1951. doi:10.1080/01621459.1951.10500769

8 thms3 active usersReviewed

Algorithmic Game Theory Machine Learning Probability·Captain: mikedeng1

Calibrated Learning and Correlated Equilibrium III: A Randomized Forecast Calibrated against Every OpponentResearch Paper

Motivation

A forecaster who announces "70% chance of rain" is calibrated if, among the days on which that number was announced, it rained on about 70% of them. Dawid (The well-calibrated Bayesian, JASA 1982) proposed calibration as the minimal requirement of an honest probability forecaster. Oakes (Self-calibrating priors do not exist, JASA 1985) showed that no deterministic forecasting rule can be calibrated against every sequence of outcomes: an adversary who knows the rule can always choose the outcome that contradicts the forecast.

Foster and Vohra (Calibrated learning and correlated equilibrium, Games Econ. Behav. 21 (1997) 40–55) use calibration as the bridge between learning and equilibrium in repeated games. Their Theorem 1 says that if each player best-responds to calibrated forecasts of the opponent, the empirical distribution of play converges to the set of correlated equilibria. That theorem is only useful if calibrated forecasts can actually be produced whatever the opponent does. Theorem 3 of the paper, credited to an unpublished 1991 manuscript of the same authors and proved in the paper's Appendix, says they can, provided the forecaster randomizes.

Timeline. Dawid (1982) defines calibration. Oakes (1985) rules out deterministic calibrated forecasting against arbitrary sequences. Foster and Vohra (1991 manuscript; 1997 paper, Theorem 3 and Appendix) give a randomized forecaster calibrated against any opponent, through a pairwise ("internal") no-regret property. The full argument appeared in Foster and Vohra, Asymptotic calibration, Biometrika 85 (1998). Hart and Mas-Colell (A simple adaptive procedure leading to correlated equilibrium, Econometrica 2000) later made internal regret the standard route to correlated equilibrium.

Setting

Player 2 has $n\ge 1$ pure strategies $j\in\{0,\dots,n-1\}$ . In every round, player 1 announces a forecast $p\in\mathbb R^n$ , a probability vector ( $p_j\ge 0$ , $\sum_j p_j = 1$ ), and player 2 plays a strategy $j$ . The two moves are simultaneous: player 2 does not see the current forecast.

A history $h$ of length $t$ is the list of the $t$ pairs (forecast, play), oldest first. For a forecast vector $p$ and a strategy $j$ :

$N(p,t)$ is the number of rounds of $h$ in which $p$ was forecast;
$\rho(p,j,t)$ is the fraction of those rounds in which player 2 played $j$ (and $0$ if $N(p,t)=0$ );
the calibration score (Eq. (1), p. 49) is

C_t = \sum_p\sum_j \bigl|\rho(p,j,t) - p_j\bigr|\,\frac{N(p,t)}{t}.

A randomized forecaster $F$ maps each history to a probability distribution on forecasts. A learning rule $A$ of player 2 maps each history to a probability distribution on strategies. In round $t+1$ the forecast is drawn from $F(h)$ and the play from $A(h)$ , independently given the history $h$ of the first $t$ rounds. This defines the law $\mathbb P_{F,A}$ of the first $t$ rounds (histLaw F A t).

For the Appendix: with $k$ forecasts, losses $L_t^i$ and mixing weights $w_t^i$ , the pairwise regret of replacing forecast $i$ by forecast $j$ is

R_T^{i\to j} = \max\Bigl\{0,\ \sum_{t=1}^T w_t^i\,(L_t^i - L_t^j)\Bigr\}.

Formalization targets

Goal: Theorem 3 (p. 49)

There is a forecaster $F$ , with probability-vector forecasts, such that for every learning rule $A$ of player 2 and every $\varepsilon>0$ ,

\lim_{t\to\infty}\mathbb P_{F,A}\bigl(C_t<\varepsilon\bigr) = 1.

The forecaster is fixed before the opponent; no rate is claimed, and the rate may depend on $A$ .

Milestones, in the order the Appendix uses them

Flow conservation is solvable (p. 52). For every nonnegative $k\times k$ matrix $R$ , $k\ge 1$ , there is a probability vector $w$ with $w^i\sum_j R^{i\to j} = \sum_j w^j R^{j\to i}$ for all $i$ .
Lemma 1 (No-Regret) (p. 52). With losses in $[0,1]$ and weights solving flow conservation for the previous regrets,

R_T^{i\to j}\le\sqrt{2kT}\quad\text{for all } i,j,T.

Regrets sandwich L-2 calibration (p. 54). For a grid $p^1,\dots,p^k$ that is $\varepsilon$ -dense in squared distance and losses $L_t^i = |X_t - p^i|^2$ ,

\sum_i\max_j \frac{R_T^{i\to j}}{T}\ \le\ C_{2,w}(T)\ \le\ \varepsilon + \sum_i\max_j\frac{R_T^{i\to j}}{T},

with $C_{2,w}$ the fractional L-2 calibration score. 4. L-1 versus L-2 (p. 54). For each $j$ , $\sum_p|\rho(p,j,t)-p_j|\,N(p,t)/t \le \sqrt{\sum_p(\rho(p,j,t)-p_j)^2 N(p,t)/t}$ .

Significance

The result. Theorem 3 makes the hypothesis of Theorem 1 attainable: combined, they show that there are learning procedures under which play converges in probability to the set of correlated equilibria of any finite game (the paper's Corollary, p. 49). The intermediate Lemma 1 is an early internal-regret bound; internal (swap) regret minimization later became the standard algorithmic route to correlated equilibria and to calibrated prediction in online learning.

Formalizing it. The result is proved, in the 1997 Appendix in telegraphic form and in full in Foster and Vohra (1998). The Appendix leaves several steps informal (see Formalization scope), so a machine-checked proof must supply them. No formalization of calibration or of internal regret was found on Prove2Me as of 2026-09-26. The mission produces a formal model of randomized forecasters against adaptive opponents, a checked internal-regret bound with an explicit constant, and the passage from regret to calibration.

Difficulty

The obvious approach is to pick, at each round, a forecast that corrects the current miscalibration. This is a deterministic rule, and by Oakes' theorem an opponent can defeat it. Randomization alone does not help either: the forecaster must randomize in a way that controls every pairwise regret $R^{i\to j}$ at once, not only the regret against the best fixed forecast. External no-regret does not imply calibration.

Two further gaps separate Lemma 1 from Theorem 3. First, the Appendix controls a fractional score in which the event "forecast $p^i$ was issued" is replaced by its probability $w_t^i$ . The realized calibration score involves the random choices, so a concentration argument is needed against an adaptive opponent. Second, a fixed grid gives calibration only up to its mesh $\varepsilon$ . Exact convergence requires letting the grid size $k$ grow and $\varepsilon$ shrink over time, and the scores of the different phases must be combined.

Formalization scope

Model. Strategies are Fin n; forecasts are vectors Fin n → ℝ that are probability vectors (IsDist). Histories are Lean lists of (forecast, play) pairs, oldest first. Forecaster and opponent are maps from histories to Mathlib PMFs. The history law is built with PMF.bind/PMF.map, with the two draws independent given the past. $\mathbb P(C_t<\varepsilon)$ is the toOuterMeasure of the law, in ℝ≥0∞; no σ-algebra on histories is used.
Opponent. The opponent may be randomized and may depend on all past forecasts and plays; fixed sequences and deterministic rules are special cases. The opponent never sees the current forecast. Letting it see the current forecast would make the goal false, and restricting to fixed sequences would make it weaker than the paper.
Quantifiers. The forecaster is chosen before the opponent (∃ F, ∀ A). The reverse order is trivial, since one can forecast $A$ 's next play.
Conventions. Rounds are counted from $0$ , so the paper's rounds $1,\dots,t$ are the first $t$ list entries. The paper's $R_{t-1}$ is the regret over the $0$ -based rounds before $t$ . Forecasts are grouped by exact equality of real vectors. Sums over $p$ run over the forecasts that occur, and every other term vanishes. Scores divide by the history length, and are $0$ for the empty history. "Converges in probability" is the $\lim\mathbb P(C_t<\varepsilon)=1$ form the page states. The grid of milestone 3 is indexed $1,\dots,k$ (the page writes $i = 0,\dots,k$ on p. 53 and $1,\dots,k$ in Lemma 1), and "within $\varepsilon$ " is read in squared Euclidean distance.
Pinned reading. The page writes the middle term of milestone 3 as $E(C_2(t))$ with a garbled formula. The mission states the inequality for the fractional score $C_{2,w}$ , for which it holds.
Steps the paper leaves informal, not stated as milestones. (a) " $E(C_2(t))\le\varepsilon + O(k/\sqrt2)$ " when the weights solve flow conservation; the $O$ -term is garbled and should decay in $t$ . (b) "if we let $k$ grow slowly and $\varepsilon$ go slowly to zero … $C_2(t)\to 0$ in expectation which implies $C_2(t)\to0$ in probability by Jensen's inequality", together with the passage from the fractional score to the realized one. Solvers will have to formalize these steps on the way to the goal.
Not included. The Corollary on p. 49 (convergence in probability of play to the correlated equilibria when both players use the scheme). It needs the game layer and a quantitative form of Theorem 1, and the page gives no proof.
Infrastructure welcome. Finite Markov chain stationary distributions (for milestone 1), for which Prove2Me has MarkovChain.exists_isStationary for row-stochastic matrices. Also useful: martingale concentration for PMF-built processes, and Cauchy–Schwarz with weights. The history-law construction is reusable for any repeated forecasting game.

Selected references

D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997) 40–55. https://doi.org/10.1006/game.1997.0595
D. P. Foster and R. V. Vohra, Asymptotic calibration, Biometrika 85 (1998) 379–390. https://doi.org/10.1093/biomet/85.2.379
A. P. Dawid, The well-calibrated Bayesian, J. Amer. Statist. Assoc. 77 (1982) 605–613. https://doi.org/10.1080/01621459.1982.10477856
D. Oakes, Self-calibrating priors do not exist, J. Amer. Statist. Assoc. 80 (1985) 339. https://doi.org/10.1080/01621459.1985.10478117
S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68 (2000) 1127–1150. https://doi.org/10.1111/1468-0262.00153

10 thms3 active usersReviewed

Completed

Machine Learning Optimization Probability·Captain: mikedeng1

Simultaneous Analysis of Lasso and Dantzig Selector III: A Sparsity Oracle Inequality for the LassoResearch Paper

Motivation

In high-dimensional regression the number of candidate predictors $M$ can far exceed the number of observations $n$ . A regression function can then be estimated only if it is well approximated by a combination of a few elements of a large dictionary. The Lasso is the most widely used estimator in this regime. The question this mission formalizes is how well the Lasso predicts when the truth is not assumed to be sparse, or even to lie in the span of the dictionary.

A sparsity oracle inequality answers it. It bounds the prediction error of the estimator by the error of the best sparse approximation of the truth, which only an oracle knowing the truth could compute, plus a remainder proportional to the sparsity of that approximation times $\log M/n$ . Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 37(4), 2009) proved such an inequality for the Lasso under their restricted eigenvalue (RE) condition. Earlier oracle inequalities for Lasso-type estimators in fixed design (Bunea, Tsybakov and Wegkamp, 2006–2007) required the Gram matrix to be positive definite or to satisfy a mutual-coherence condition. The RE condition is weaker and allows $M\gg n$ , and it is now the standard hypothesis in this literature.

Setting

A dictionary $f_1,\dots,f_M$ is evaluated at fixed points $Z_1,\dots,Z_n$ . This gives the design matrix $X=(f_j(Z_i))\in\mathbb R^{n\times M}$ and, for an unknown regression function $f$ , the vector $f=(f(Z_1),\dots,f(Z_n))^\top$ . The observations are

y=f+W,\qquad W_1,\dots,W_n\ \text{independent}\ \mathcal N(0,\sigma^2),\ \sigma>0 .

Nothing is assumed about $f$ . For $v\in\mathbb R^n$ the empirical norm is $\|v\|_n=(\frac1n\sum_iv_i^2)^{1/2}$ , and for $\beta\in\mathbb R^M$ we write $f_\beta=X\beta$ . The column norms $\|f_j\|_n$ are assumed nonzero, with $f_{\max}=\max_j\|f_j\|_n$ and $f_{\min}=\min_j\|f_j\|_n$ . The support of $\beta$ is $J(\beta)=\{j:\beta_j\neq0\}$ and its sparsity is $\mathcal M(\beta)=|J(\beta)|$ .

The Lasso $\hat\beta_L$ is any minimiser of

\frac1n\sum_{i=1}^n\big(y_i-(X\beta)_i\big)^2+2r\sum_{j=1}^M\|f_j\|_n|\beta_j|,\qquad r=A\sigma\sqrt{\frac{\log M}{n}},\ A>2\sqrt2,

and $\hat f_L=X\hat\beta_L$ .

Assumption RE $(s,c_0)$ holds with constant $\kappa>0$ if, for every $J_0\subseteq\{1,\dots,M\}$ with $|J_0|\le s$ and every $\delta\neq0$ with $|\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1$ ,

\kappa\sqrt n\,|\delta_{J_0}|_2\le|X\delta|_2 .

The paper's $\kappa(s,c_0)$ is the largest such constant.

Formalization targets

Goal: Theorem 6.1

Fix $\varepsilon>0$ , $n\ge1$ , $M\ge2$ , $1\le s\le M$ , and let RE $(s,(3+4/\varepsilon)f_{\max}/f_{\min})$ hold with constant $\kappa$ . With probability at least $1-M^{1-A^2/8}$ , every Lasso solution satisfies, simultaneously for all $\beta$ with $\mathcal M(\beta)\le s$ ,

\|\hat f_L-f\|_n^2\le(1+\varepsilon)\Big\{\|f_\beta-f\|_n^2+C(\varepsilon)\frac{f_{\max}^2A^2\sigma^2}{\kappa^2}\,\frac{\mathcal M(\beta)\log M}{n}\Big\},\qquad C(\varepsilon)=\frac{4(2+\varepsilon)^2}{\varepsilon(1+\varepsilon)} .

Milestones

(B.4): the noise event $\mathcal A=\bigcap_j\{2|V_j|\le r\|f_j\|_n\}$ , with $V_j=n^{-1}\sum_iX_{ij}W_i$ , satisfies $P(\mathcal A^c)\le M^{1-A^2/8}$ .
(B.1) on $\mathcal A$ : for every Lasso solution and every $\beta$ ,

\|\hat f_L-f\|_n^2+r\sum_j\|f_j\|_n|\hat\beta_j-\beta_j|\le\|f_\beta-f\|_n^2+4r\sum_{j\in J(\beta)}\|f_j\|_n|\hat\beta_j-\beta_j| .

Lemma B.1: the same inequality with probability at least $1-M^{1-A^2/8}$ .
Cone step: in the case $\varepsilon\|f_\beta-f\|_n^2<4r\sum_{J(\beta)}\|f_j\|_n|\hat\beta_j-\beta_j|$ , the difference $\hat\beta_L-\beta$ lies in the cone with constant $(3+4/\varepsilon)f_{\max}/f_{\min}$ at $J(\beta)$ .
Inequality before decoupling: $\|\hat f_L-f\|_n^2\le\|f_\beta-f\|_n^2+4rf_{\max}\kappa^{-1}\sqrt{\mathcal M(\beta)}\,(\|\hat f_L-f\|_n+\|f_\beta-f\|_n)$ .
Decoupled bound: $\|\hat f_L-f\|_n^2\le\frac{b+1}{b-1}\|f_\beta-f\|_n^2+\frac{8b^2f_{\max}^2}{(b-1)\kappa^2}r^2\mathcal M(\beta)$ for all $b>1$ .
Corollary 6.2: the same oracle inequality with $\gamma$ in place of $\kappa$ and no global RE assumption. The infimum runs over those $\beta$ with $\mathcal M(\beta)\le s$ whose support alone satisfies the restricted eigenvalue inequality with constant $\gamma$ .

Significance

The theorem says that, up to the factor $1+\varepsilon$ and a remainder of order $\mathcal M(\beta)\log M/n$ , the Lasso predicts as well as the best $s$ -sparse linear combination of the dictionary. This is the case even when $f$ is not sparse and not in the span of the dictionary. The remainder is the parametric rate for $\mathcal M(\beta)$ parameters, inflated by $\log M$ and by the ill-posedness factor $f_{\max}^2/\kappa^2$ . Together with Theorem 5.1 of the same paper (mission II of this series), it shows that the Lasso and the Dantzig selector are within the same distance of the sparse oracle. The oracle inequality is used in aggregation, in model selection, and as a black box in later sparse-estimation papers.

The result is proved in the paper. It has not been formalized: at the time of writing, no Lasso oracle inequality and no probabilistic Lasso bound exist on Prove2Me or in Mathlib. What this mission contributes is a machine-checked proof of the paper's Theorem 6.1 with an explicit constant $C(\varepsilon)$ . The paper leaves $C(\varepsilon)$ unspecified, and its proof fixes the value used here. The mission also formalizes the Gaussian-tail step (B.4) and the deterministic basic inequality (B.1), both of which are shared with the paper's other Lasso results.

Difficulty

There is no sparse truth, so the usual argument does not apply. That argument places the error $\hat\beta_L-\beta^*$ in the RE cone and reads off a rate. Here the competitor $\beta$ is arbitrary, and the approximation error $\|f_\beta-f\|_n$ can dominate the penalty terms, in which case the error is not in the cone. The RE assumption can be used only where the error does lie in a cone, and the cone constant available there depends on $\varepsilon$ and on the column-norm ratio $f_{\max}/f_{\min}$ , because the penalty is weighted while RE is stated for unweighted vectors. What RE then yields is an inequality quadratic in $\|\hat f_L-f\|_n$ with a cross term, not the $(1+\varepsilon)$ form directly, and the constant $C(\varepsilon)$ is determined by how that cross term is absorbed. On the probabilistic side, the whole argument must run on one event of probability at least $1-M^{1-A^2/8}$ . That event may depend neither on $\beta$ nor on the choice of minimiser. The Lasso need not have a unique solution.

Formalization scope

The dictionary enters only through $X\in\mathbb R^{n\times M}$ (Matrix (Fin n) (Fin M) ℝ) and the target only through $f\in\mathbb R^n$ , which is arbitrary. The noise is a family W : Fin n → Ω → ℝ of measurable, independent random variables, each with law gaussianReal 0 σ², and $\sigma>0$ .
The Lasso is an argmin predicate, and every statement is made for every minimiser. "With probability at least $p$ " means a measurable event $E$ with $P(E)\ge p$ , chosen before the competitor $\beta$ and the minimiser.
RE is stated through a witness $\kappa>0$ . Since $\kappa(s,c_0)$ is attained and every bound decreases in $\kappa$ , this is equivalent to the paper's form, and it avoids a real infimum over an empty set.
The infimum over $\{\beta:\mathcal M(\beta)\le s\}$ is written as "for every such $\beta$ ". This is equivalent, because the set contains $\beta=0$ and the bracket is nonnegative.
Correction/strengthening. The printed theorem has an unspecified $C(\varepsilon)>0$ . The goal instead uses the value $C(\varepsilon)=4(2+\varepsilon)^2/(\varepsilon(1+\varepsilon))$ that the proof yields with $b=1+2/\varepsilon$ , and this implies the printed statement. Corollary 6.2 uses the same explicit constant.
The standing assumptions of Section 2 ( $M\ge2$ and every $\|f_j\|_n\neq0$ ) are hypotheses of every theorem.
Some formalizations would make the result trivial, and they are excluded here. The noise must be exactly i.i.d. $\mathcal N(0,\sigma^2)$ with $\sigma>0$ and must enter only through $y=f+W$ . The target $f$ must not be restricted to $X\beta^*$ . The event must be measurable. The constant must depend on $\varepsilon$ alone.
A single definition file provides the empirical norms, $f_{\max}$ , $f_{\min}$ , support and sparsity, the weighted Lasso, RE and its single-set version (the family $\Lambda_{s,\gamma,c_0}$ of Corollary 6.2), the Gaussian noise model and the event $\mathcal A$ . The same objects appear in the other missions of this series. Gaussian-tail and union-bound lemmas proved along the way are reusable, and contributions of such lemmas 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. Cited version: arXiv:0801.1095v3; DOI 10.1214/08-AOS620.
F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Sparsity oracle inequalities for the Lasso, Electron. J. Statist. 1, 169–194, 2007. DOI 10.1214/07-EJS008.
F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Aggregation for Gaussian regression, Ann. Statist. 35(4), 1674–1697, 2007. DOI 10.1214/009053606000001587.
R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Stat. Soc. B 58(1), 267–288, 1996. DOI 10.1111/j.2517-6161.1996.tb02080.x.

9 thms3 active usersReviewed

Completed

Linear algebra Machine Learning Optimization·Captain: mikedeng1

Simultaneous Analysis of Lasso and Dantzig Selector I: Sparse Eigenvalue and Correlation Conditions Imply the Restricted Eigenvalue ConditionResearch Paper

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

11 thms3 active usersReviewed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

Markovian Decision Processes with Uncertain Transition Probabilities II: Max-Max and Max-Min Optimal Returns Bound the Bayesian Optimal ReturnResearch Paper

Motivation

A Markovian decision process (Howard, 1960) models a controller who, in each of finitely many states, picks a decision, earns a reward and moves to a random next state according to known transition probabilities. In applications (inventory control, equipment replacement, quality control) those probabilities are estimated, not known. Satia and Lave (Operations Research 21(3), 1973) treat the uncertainty in two ways: a game-theoretic formulation, in which each unknown row only lies in a given set, and a Bayesian formulation, going back to Silver (1963) and Martin (1967), in which the controller holds a prior on the unknown matrix and learns from observed transitions.

The Bayesian problem is the natural one but its state includes the whole prior, so it cannot be solved exactly beyond small cases. The paper's contribution in the Bayesian part is a pair of computable bounds on the Bayesian optimal return in terms of the two game-theoretic values (max-max and max-min). This mission formalizes those bounds and the chain of facts they rest on.

Setting

There are $N$ states $i$ and, in state $i$ , a finite nonempty set $K_i$ of decisions. A transition $i \to j$ under decision $k$ earns $r^k_{ij}$ and rewards are discounted by $\beta$ , $0 \le \beta < 1$ . The row $p_i^k = (p^k_{ij})_j$ of transition probabilities is unknown; it is known to lie in a closed convex nonempty set $S_i^k$ of probability vectors, and $S = \{P : p_i^k \in S_i^k \text{ for all } i, k\}$ .

A prior $g$ is a probability distribution on matrices $P = (p_i^k)$ whose rows are all probability vectors. Its means are $\bar p^k_{ij} = E(p^k_{ij})$ . After a transition $l \to j$ under decision $m$ the prior is replaced by the Bayes transformation $T^m_{lj} g(P) = C\,p^m_{lj}\,g(P)$ (Eq. (8)), with $C$ the normalizing constant. The Bayesian optimal return $f(i,g)$ solves the recursion

f(i, g) = \max_{k \in K_i} \Big\{ \sum_j \bar p^k_{ij} r^k_{ij} + \beta \sum_j \bar p^k_{ij} f(j, T^k_{ij} g) \Big\}. \qquad (10)

The max-max and max-min values $V^+$ , $V^-$ solve

V_i^\pm = \max_{k \in K_i} \operatorname*{max/min}_{p_i^k \in S_i^k} \Big\{ \sum_j p^k_{ij} r^k_{ij} + \beta \sum_j p^k_{ij} V_j^\pm \Big\},

with max for $V^+$ and min for $V^-$ . Finally $\alpha = \operatorname{prob}(P \in S \mid g)$ , the prior probability that the true matrix lies in $S$ .

The Lean development lives in the namespace SatiaLave.Bayes: UncertainMDP, IsPrior, pbar, bayes, SolvesEq10, SolvesVplus, SolvesVminus, alpha, rmax, rmin, policyValue.

Formalization targets

Goal: Propositions 9 and 10

For every bounded solution $f$ of (10), all solutions $V^+$ , $V^-$ , every prior $g$ and every state $i$ ,

\alpha V_i^- + (1-\alpha)\min_{i,j,k}\frac{r^k_{ij}}{1-\beta} \;\le\; f(i,g) \;\le\; \alpha V_i^+ + (1-\alpha)\max_{i,j,k}\frac{r^k_{ij}}{1-\beta},

together with the existence of $f$ , $V^+$ and $V^-$ . Both halves are the paper's printed statements.

Milestones

Proposition 6 (Martin): (9)/(10) has a unique bounded solution (unique at priors).
No learning (p. 733): at a point-mass prior $\delta_P$ , $f(\cdot,\delta_P)$ solves the optimality equations of the process with known $P$ .
Proposition 8: $f(i,g)$ is convex in $g$ .
Jensen step (proof of Proposition 9): $f(i,g) \le \int f(i,\delta_P)\,dg(P)$ .
Policy step (proof of Proposition 10): $f(i,g) \ge \int [q + \beta P^A q + \beta^2 [P^A]^2 q + \cdots]_i\,dg(P)$ for every pure stationary policy $A$ .

Significance

The result. The bounds sandwich an intractable quantity between two quantities computable by finite algorithms (the max-max and max-min policy-iteration procedures of the same paper), weighted by a single prior probability $\alpha$ . When the prior concentrates on $S$ ( $\alpha \to 1$ ) the bounds become $V_i^- \le f(i,g) \le V_i^+$ : the Bayesian return lies between the pessimistic and optimistic robust values. They are the upper and lower bounds on the return that the paper's implicit-enumeration method (the decision tree of its Fig. 2 and Proposition 12) uses to compare decisions. The Jensen step is a value-of-information inequality (Bayesian optimal return is at most the expected full-information optimal return), which recurs throughout Bayesian control and bandit theory.

Formalizing it. The results are proved on paper (Propositions 6 and 8 by reference to Martin's book and Satia's thesis, Propositions 9 and 10 in the text); none is machine-checked. The mission produces a Lean model of Bayes-adaptive Markov decision processes with priors as measures, the Bayes transformation and its fixed-point recursion, and the link between the Bayesian and the robust (rectangular) formulations. Martin's existence-uniqueness theorem and the convexity of the Bayesian value are reusable for any Bayes-adaptive model.

Difficulty

The prior space is infinite-dimensional and not a vector space, so the recursion (10) lives on a space of measures, and the usual finite-state arguments do not apply verbatim. Proposition 8 gives convexity only along finite mixtures, while the proof of Proposition 9 applies Jensen's inequality to the integral mixture $g = \int \delta_P\,dg(P)$ of point masses; bridging the two, or proving the value-of-information inequality directly, is the central step. The paper also restricts the point masses to $x_i^k \in S_i^k$ , which cannot represent a prior with mass outside $S$ ; the formal statement integrates over every transition matrix, as the next line of the paper's display requires. Measurability of $P \mapsto f(i,\delta_P)$ is not automatic, since $f$ is only characterized by a functional equation.

Formalization scope

States are a nonempty Fintype S; decisions a dependent family D i of nonempty finite types. A matrix is P : (i : S) → D i → S → ℝ with the product Borel $\sigma$ -algebra.
Priors are measures: a probability measure giving full mass to matrices whose rows are probability vectors. This generalizes the paper's densities $g(P)$ and includes the point masses $a_x$ its proof uses.
Bayes transformation at $\bar p = 0$ : the normalizing constant does not exist; bayes then returns $g$ . That posterior is always multiplied by $\bar p = 0$ in (10), so the choice is immaterial.
Readings of informal words. "The problem reduces to a Markovian decision process" = at a point-mass prior, fixed by every Bayes transformation, $f$ solves the known- $P$ optimality equations. "Convex in $g$ " = convex along mixtures of priors. "Unique set of bounded functions" = two bounded solutions agree at every prior (values at non-priors are unconstrained). "Satisfy (9)" is formalized as (10), which the paper derives from (9) by linearity of $E$ . $\max_{P\in S}$ / $\min_{P\in S}$ in $V^\pm$ is taken over the row $p_i^k \in S_i^k$ (the only row that enters; $S$ is a product), as ⨆/⨅ over a nonempty bounded set. "Obviously $f(i,g)\ge V_i^A$ " is stated for every pure stationary policy $A$ , not only a max-min optimal one. The policy return is the componentwise series $\sum_n \beta^n (P^A)^n q$ .
Added hypotheses, not printed: $0 \le \beta < 1$ ; $S_i^k \ne \emptyset$ ; $N \ge 1$ . Printed and kept: $S_i^k$ closed and convex.
$f$ , $V^+$ , $V^-$ are quantified as solutions of their equations; $\alpha$ is computed from $g$ , never a free parameter; $\max_{i,j,k}[r^k_{ij}/(1-\beta)]$ ranges over all states $i,j$ and $k \in K_i$ . Integrability of the integrands in milestones 4 and 5 is part of their conclusions.
Trivializations ruled out. A free $\alpha \in [0,1]$ , or $f$ defined off priors, would make the goal false or vacuous; the goal also asserts that bounded $f$ and $V^\pm$ exist, so its universal part is not vacuous.
Not in scope: Proposition 7 (matrix-beta conjugacy, which needs a Dirichlet distribution), Propositions 11–13 and the numerical example.

Welcome contributions: the Banach fixed-point argument for (10) on bounded functions of priors; lemmas that bayes maps priors to priors and that point masses are fixed; continuity of the known- $P$ optimal value in $P$ ; a general Jensen inequality for functions convex along mixtures of probability measures.

Selected references

J. K. Satia and R. E. Lave, Jr., Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3), 728–740, 1973. https://doi.org/10.1287/opre.21.3.728
J. J. Martin, Bayesian Decision Problems and Markov Chains, Wiley, New York, 1967.
E. A. Silver, Markovian Decision Processes with Uncertain Transition Probabilities or Rewards, Interim Technical Report No. 1, Operations Research Center, Massachusetts Institute of Technology, August 1963.
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
J. K. Satia, Markovian Decision Process with Uncertain Transition Matrices or/and Probabilistic Observation of States, Ph.D. dissertation, Stanford University, 1968.

7 thms3 active usersReviewed

Machine Learning Probability·Captain: mikedeng1

The Power of Convex Relaxation: Near-Optimal Matrix Completion III: No Method Recovers Incoherent Rank-r Matrices below the Sampling Rate (I.20)Research Paper

Motivation

Matrix completion asks to recover a matrix from a small random subset of its entries. It models collaborative filtering (a ratings table with most entries missing), sensor-network localisation from partial distance data, and system identification. With no structure the task is hopeless, so one assumes the matrix has low rank $r$ and that its information is not concentrated in a few entries (incoherence).

Candès and Recht (Found. Comput. Math., 2009) showed that nuclear-norm minimisation recovers such a matrix from about $n^{6/5} r\log n$ random entries. Candès and Tao (IEEE Trans. Inf. Theory, 2010) lowered this to $n r\,\mathrm{polylog}(n)$ . The same paper also asks how few entries any method could possibly use, and answers it with a lower bound, Theorem 1.7: below about $\mu_0 n r\log n$ observed entries, no algorithm can succeed. This mission formalizes that lower bound. The two upper bounds of the same paper are separate missions of this series.

Setting

Work with real $n\times n$ matrices. For a matrix $M$ , let $U \subseteq \mathbb{R}^n$ be its column space and $V\subseteq \mathbb{R}^n$ its row space, and let $P_U$ , $P_V$ be the orthogonal projections onto them. Let $e_a$ be the $a$ -th standard basis vector.

Fix an integer $r$ and a real $\mu_0$ . A matrix $M$ has rank at most $r$ and obeys the incoherence property with parameter $\mu_0$ (the paper's (I.18)) if $\operatorname{rank}M \le r$ and

\|P_U e_a\|^2 \le \frac{\mu_0 r}{n},\qquad \|P_V e_b\|^2 \le \frac{\mu_0 r}{n}\qquad\text{for all } a,b\in[n].

Since $\sum_a \|P_U e_a\|^2 = \dim U$ , a matrix of rank exactly $r$ can satisfy this only when $\mu_0\ge 1$ ; the smallest possible value $\mu_0 = 1$ means the column and row spaces are spread evenly over the coordinates.

Bernoulli sampling. Fix $m \ge 1$ and set $p = m/n^2$ . The observed set $\Omega\subseteq[n]\times[n]$ contains each entry independently with probability $p$ , so $m$ is the expected number of observed entries. The sampling operator $\mathcal{P}_\Omega$ keeps the entries of a matrix that lie in $\Omega$ and sets the others to $0$ . A recovery method sees only $\mathcal{P}_\Omega(M)$ .

The sampling conditions are, with the natural logarithm,

m \ge n^2\left(1 - e^{-\frac{\mu_0 r}{n}\log\left(\frac{n}{2\delta}\right)}\right) \qquad \text{(I.20)}

m \ge (1-\epsilon)\,\mu_0 n r\log\left(\frac{n}{2\delta}\right),\qquad \epsilon := \frac12\frac{\mu_0 r}{n}\log\left(\frac{n}{2\delta}\right). \qquad \text{(I.21)}

Formalization targets

Goal: Theorem 1.7 (p. 2058)

Fix $1 \le m$ , $1 \le r \le n$ , $\mu_0\ge 1$ and $0<\delta<1/2$ , with $\ell := n/(\mu_0 r)$ an integer. If (I.20) fails, or (I.21) fails, then

\mathbb{P}_\Omega\Bigl(\text{there are infinitely many pairs } M\ne M' \text{ of rank} \le r, \text{ incoherent with parameter } \mu_0, \text{ with } \mathcal{P}_\Omega(M)=\mathcal{P}_\Omega(M')\Bigr) \ \ge\ \delta .

On that event, the observations cannot tell $M$ from $M'$ , so no method can recover every such matrix with probability greater than $1-\delta$ . The statement fixes no constant beyond those the paper prints.

Milestones (Section II)

For pairwise disjoint sets of entries $S_1,\dots,S_n$ of size $\ell$ , $\mathbb{P}(\text{every } S_a \text{ is sampled}) = (1-(1-p)^\ell)^n$ .
For $n\ge1$ , $\pi\in[0,1]$ and $0<\delta<1/2$ : $(1-\pi)^n \ge 1-\delta$ implies $\pi \le 2\delta/n$ .
With $p = m/n^2$ and the theorem's parameters: $(1-p)^\ell \le 2\delta/n$ implies (I.20).
$1-e^{-x} > x - x^2/2$ for every $x>0$ (the paper prints $x\ge0$ ; see Formalization scope).
The second part of Theorem 1.7: for the theorem's parameters, (I.20) implies (I.21).

Significance

The result. Theorem 1.7 shows that the sample complexity $n r\,\mathrm{polylog}(n)$ of the paper's upper bounds is close to optimal: about $\mu_0 n r\log n$ entries are necessary, however the matrix is reconstructed. The count exceeds the $2nr - r^2$ degrees of freedom of a rank- $r$ matrix by the factor $\mu_0\log n$ . The logarithm is a coupon-collector effect: every row has to be sampled. The factor $\mu_0$ shows that the oversampling grows in proportion to the coherence. The bound is information-theoretic, and it holds even when the rank bound and the coherence are known in advance.

Formalizing it. The theorem and its proof in Section II are published. No machine-checked version is known to exist, and the platform has no lower bound for matrix completion. A formal proof would also check the printed argument, whose steps are compressed. It would yield reusable pieces: a Lean predicate for incoherence of matrices of bounded rank built on Mathlib's orthogonal projections, the independence computation for Bernoulli sampling over disjoint entry sets, and the elementary estimates that turn a success probability into a sampling rate.

Difficulty

The probabilistic and analytic parts are elementary. The difficulty is in building the hard instances as matrices and certifying them. For each observation set one has to exhibit, on an event of probability at least $\delta$ , an infinite family of distinct pairs that agree on $\Omega$ . Every member must have rank at most $r$ and meet both incoherence bounds, measured through projections onto its column and row spaces, and the pairs must stay distinct across the family. The paper describes the instances only informally. They have to be pinned down so that whatever distinguishes $M$ from $M'$ is really invisible on $\Omega$ , while the incoherence bounds still hold for every admissible $\mu_0\ge1$ and $r\le n$ . Computing the column space and the projection norms of an explicit matrix in Lean is the main infrastructure cost.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ (the platform's MatrixCompletion.RealMatrix n n). The observation model is the platform's bernoulliEventProb with rate $m/n^2$ , the sum over all $\Omega$ of $p^{|\Omega|}(1-p)^{n^2-|\Omega|}$ . The sampling operator is the platform's samplingProjection. Logarithms and exponentials are Real.log, Real.exp. The mission's own definitions are IncoherentRankAtMost r μ₀ M (rank at most $r$ , with the projection bounds computed from Mathlib's Submodule.starProjection onto the ranges of $M$ and $M^\top$ in EuclideanSpace ℝ (Fin n)) and SamplingConditionI20, SamplingConditionI21.

The formalization commits to four readings:

Order of quantifiers. The event is "the set of bad pairs is infinite", evaluated for each $\Omega$ , so the pairs may depend on $\Omega$ . This is what Section II establishes and what the sentence after the theorem uses. The reading "fixed $M\ne M'$ with $\mathbb{P}(\mathcal{P}_\Omega(M) = \mathcal{P}_\Omega(M'))\ge\delta$ " is a different statement and is not the goal.
Integrality of $\ell$ . The hypothesis that $\ell = n/(\mu_0 r)$ is an integer is the paper's own "without loss of generality" of Section II, and it is stated explicitly. It forces $\mu_0 r \le n$ .
"Fix $1\le m, r\le n$ " is read as $1\le m$ and $1\le r\le n$ . No upper bound on $m$ is imposed, since the failure of (I.20) already gives $m<n^2$ .
Standing assumptions. Section I-H assumes $m\ge 2nr$ and $n$ larger than an absolute constant for the rest of the paper. Those assumptions serve the upper bounds. Theorem 1.7 lists its own ranges, and only those are imposed.

The hypothesis "(I.20) fails or (I.21) fails" covers both parts of the theorem. The last sentence of Section II proves the second part from $1 - e^{-x} > x - x^2/2$ , which the paper states "whenever $x \ge 0$ ". At $x=0$ the two sides are equal, so the strict inequality is false there; milestone 4 states the corrected range $x>0$ , which is all the paper uses, since its $x = \frac{\mu_0 r}{n}\log\frac{n}{2\delta}$ is positive.

Trivializing formalizations are ruled out. The set of pairs requires $M\ne M'$ , so the diagonal pairs $(M,M)$ do not count. "Infinitely many" is Set.Infinite of a set of pairs, not "at least one". Incoherence uses the theorem's $r$ and the actual column and row spaces, so the class is the paper's. The hypotheses are satisfiable, for example $n=4$ , $r=1$ , $\mu_0=1$ , $\ell=4$ , $\delta=0.1$ , $m=1$ .

Contributions are welcome on every milestone. The Bernoulli independence computation and the incoherence predicate can be reused in the other two missions of this series and in any lower bound for sampling problems.

Selected references

E. J. Candès and T. Tao, The Power of Convex Relaxation: Near-Optimal Matrix Completion, IEEE Transactions on Information Theory 56(5):2053–2080, 2010. https://doi.org/10.1109/TIT.2010.2044061
E. J. Candès and B. Recht, Exact Matrix Completion via Convex Optimization, Foundations of Computational Mathematics 9(6):717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5

12 thms3 active usersReviewed

Machine Learning Operations Research Optimization·Captain: mikedeng1

Generalization Bounds in the Predict-then-Optimize Framework II: Margin-Based Generalization Bound for the SPO Loss under the Strength PropertyResearch Paper

Motivation

In the predict-then-optimize paradigm a model first predicts the cost vector of a linear optimization problem from contextual features, and the prediction is then fed to an optimization solver that returns a decision. Examples include routing with predicted travel times and portfolio choice with predicted returns. The quality of a prediction is judged by the decision it produces. The Smart Predict-then-Optimize (SPO) loss of Elmachtoub and Grigas (Management Science 2022) measures exactly that: the excess cost of acting on the prediction instead of on the true cost vector.

El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3) ask when a model with small empirical SPO loss also has small expected SPO loss. The SPO loss is non-convex and discontinuous, so standard Lipschitz-contraction arguments do not apply to it directly. Their Section 4 introduces a margin version of the SPO loss, in the spirit of the margin theory of Koltchinskii and Panchenko (Ann. Statist. 2002) for classification. They show that it is Lipschitz under a geometric condition on the feasible region, and derive a generalization bound in terms of the multivariate Rademacher complexity of the hypothesis class. This mission formalizes that bound.

Setting

Decisions live in $\mathbb R^d$ with a norm $\|\cdot\|$ ; cost vectors are linear functionals with the dual norm $\|c\|_*=\max_{\|w\|\le1}c^\top w$ . The feasible region $S\subseteq\mathbb R^d$ is nonempty, compact and convex, and throughout Section 4 it is not a singleton. An optimization oracle $w^*$ maps each cost vector $c$ to some minimizer $w^*(c)\in\arg\min_{w\in S}c^\top w$ . The SPO loss of a prediction $\hat c$ against the realized cost $c$ is

\ell_{\rm SPO}(\hat c,c)=c^\top w^*(\hat c)-c^\top w^*(c),

and the linear optimization gap is $\omega_S(c)=\max_{w\in S}c^\top w-\min_{w\in S}c^\top w$ , with $\omega_S(\mathcal C)=\sup_{c\in\mathcal C}\omega_S(c)$ and $\rho_2(\mathcal C)=\sup_{c\in\mathcal C}\|c\|_2$ for the set $\mathcal C$ of possible true costs.

A cost vector is degenerate if $\min_{w\in S}\hat c^\top w$ has more than one optimal solution; $\mathcal C^\circ$ is the set of degenerate costs. The distance to degeneracy is $\nu_S(\hat c)=\inf_{c\in\mathcal C^\circ}\|c-\hat c\|_*$ . The region $S$ has the strength property with parameter $\mu>0$ if

\hat c^\top\big(w-w^*(\hat c)\big)\ge\frac{\mu\,\nu_S(\hat c)}{2}\,\|w-w^*(\hat c)\|^2\qquad\text{for all }w\in S\text{ and all }\hat c .

For $\gamma>0$ the $\gamma$ -margin SPO loss $\ell^\gamma_{\rm SPO}(\hat c,c)$ equals $\ell_{\rm SPO}(\hat c,c)$ when $\nu_S(\hat c)>\gamma$ and $\frac{\nu_S(\hat c)}{\gamma}\ell_{\rm SPO}(\hat c,c)+\big(1-\frac{\nu_S(\hat c)}{\gamma}\big)\omega_S(c)$ otherwise. It dominates the SPO loss.

Data $(x,c)$ are drawn from a distribution $\mathcal D$ on features $\mathcal X$ and costs in $\mathcal C$ , and $\mathcal H$ is a class of prediction functions $f:\mathcal X\to\mathbb R^d$ . The SPO risk is $R_{\rm SPO}(f)=\mathbb E_{\mathcal D}[\ell_{\rm SPO}(f(x),c)]$ and the empirical margin risk is $\hat R^\gamma_{\rm SPO}(f)=\frac1n\sum_i\ell^\gamma_{\rm SPO}(f(x_i),c_i)$ . The multivariate empirical Rademacher complexity is $\hat{\mathfrak R}^n(\mathcal H)=\mathbb E_{\boldsymbol\sigma}\big[\sup_{f\in\mathcal H}\frac1n\sum_i\boldsymbol\sigma_i^\top f(x_i)\big]$ with i.i.d. Rademacher vectors $\boldsymbol\sigma_i\in\{\pm1\}^d$ , and $\mathfrak R^n(\mathcal H)$ is its expectation over the sample.

Formalization targets

Goal: Theorem 4, second display (pp. 19–20)

In the $\ell_2$ set-up, under the strength property with $\mu>0$ and for fixed $\gamma>0$ , for every $\delta>0$ , with probability at least $1-\delta$ over an i.i.d. sample of size $n$ , for all $f\in\mathcal H$ :

R_{\rm SPO}(f)\le\hat R^\gamma_{\rm SPO}(f)+\Big(\frac{2\sqrt2\rho_2(\mathcal C)+2\sqrt2\mu\,\omega_S(\mathcal C)}{\gamma\mu}\Big)\mathfrak R^n(\mathcal H)+\omega_S(\mathcal C)\sqrt{\frac{\log(1/\delta)}{2n}} .

Milestones

Theorem 3(a): $\|w^*(\hat c_1)-w^*(\hat c_2)\|\le\frac{\|\hat c_1-\hat c_2\|_*}{\mu\min\{\nu_S(\hat c_1),\nu_S(\hat c_2)\}}$ .
Theorem 3(b): the same Lipschitz-like bound for $\ell_{\rm SPO}(\cdot,c)$ , with an extra factor $\|c\|_*$ .
Theorem 3(c): $\ell^\gamma_{\rm SPO}(\cdot,c)$ is $\frac{\|c\|_*+\mu\,\omega_S(c)}{\gamma\mu}$ -Lipschitz for the dual norm.
Eq. (7) with $C=\sqrt2$ (Maurer's vector contraction inequality): for $L$ -Lipschitz $\Phi_i$ on Euclidean $\mathbb R^d$ ,

\mathbb E_\sigma\Big[\sup_{f\in\mathcal H}\frac1n\sum_i\sigma_i\Phi_i(f(x_i))\Big]\le\sqrt2L\,\hat{\mathfrak R}^n(\mathcal H).

Theorem 4, first display: for any fixed sample with costs in $\mathcal C$ ,

\hat{\mathfrak R}^n_{\gamma\rm SPO}(\mathcal H)\le\Big(\frac{\sqrt2\rho_2(\mathcal C)+\sqrt2\mu\,\omega_S(\mathcal C)}{\gamma\mu}\Big)\hat{\mathfrak R}^n(\mathcal H).

Theorem 3 is stated for a general norm, as in the paper. Eq. (7), Theorem 4 and the goal are Euclidean. The paper's Theorem 5 (p. 20), a version of the goal uniform over $\gamma\in(0,\bar\gamma]$ , is not part of this mission.

Significance

The bound replaces the loss-class complexity of the SPO loss, which is controlled only through combinatorial dimensions (Natarajan dimension in the polyhedral case, Section 3 of the paper), by the multivariate Rademacher complexity of $\mathcal H$ itself. For norm-bounded linear hypothesis classes this complexity has mild, even logarithmic, dependence on the dimensions $p$ and $d$ (Section 4.4). The result applies to every feasible region with the strength property. By Section 5 of the paper these include strongly convex sets and polytopes, where $\nu_S$ can also be computed. When most predictions stay far from degeneracy, $\hat R^\gamma_{\rm SPO}\approx\hat R_{\rm SPO}$ and the bound is much sharper than the combinatorial one. It is also a strict generalization of margin bounds for binary classification (Example 7).

The theorem is proved in the paper, which imports two external tools without proof: the Rademacher generalization bound of Bartlett and Mendelson, applied to the margin loss, and Maurer's inequality. To our knowledge none of these results has a machine-checked proof. The mission produces a checked proof of the margin bound and a Lean statement of Maurer's inequality. It also formalizes the strength property and the Lipschitz estimates of Theorem 3, which the companion missions on strongly convex sets and polytopes rely on.

Difficulty

The SPO loss is discontinuous in $\hat c$ at degenerate predictions. The standard route, scalar Ledoux–Talagrand contraction applied to the loss class, therefore fails at the first step. It would fail even for a Lipschitz loss, because it relates the loss class only to a scalar class, and $\mathcal H$ is vector valued. Lipschitz continuity of the margin loss needs the oracle to be stable away from $\mathcal C^\circ$ . Convexity and compactness of $S$ alone do not give that: for an $\ell_p$ ball with $2<p<\infty$ the strength property fails for every $\mu>0$ (p. 14). The vector contraction inequality of Maurer (2016) is a nontrivial probabilistic inequality, and its constant $\sqrt2$ must not depend on the dimension $d$ . The final concentration step is McDiarmid's inequality for a supremum over a possibly uncountable class, which in a formal proof needs measurability of that supremum.

Formalization scope

The decision space is a finite-dimensional real normed space E. Cost vectors and predictions are continuous linear functionals, StrongDual ℝ E, whose operator norm is the paper's dual norm. In the $\ell_2$ statements E = EuclideanSpace ℝ (Fin d), where the dual norm is Euclidean. Every statement carries the standing assumptions: $S$ nonempty, compact, convex and not a singleton, an arbitrary oracle (no tie-breaking rule), and $\mu>0$ , $\gamma>0$ . The Lipschitz-like bounds of Theorem 3(a)–(b) are stated multiplied out, because the paper reads $1/0$ as $+\infty$ . Expectations over signs are finite averages over sign patterns. $\omega_S(\mathcal C)$ and $\rho_2(\mathcal C)$ are suprema over a nonempty bounded $\mathcal C$ containing the cost almost surely. "With probability at least $1-\delta$ " is the statement that the outer $\mathcal D^n$ -measure of the failure event is at most $\delta$ .

Added hypotheses, all disclosed in the statements: the multivariate Rademacher sums are bounded above (almost surely in the goal) and $\hat{\mathfrak R}^n(\mathcal H)$ is integrable, since otherwise Lean's junk value $0$ would replace an infinite complexity and make the bound false rather than vacuous. Hypotheses $f$ and $\ell_{\rm SPO}(f(x),c)$ measurable, and the uniform deviation and margin Rademacher suprema a.e.-measurable, are also added; the paper is silent on measurability. A singleton $S$ would make $\mathcal C^\circ$ empty and the strength property hold for free; this is excluded explicitly, so the strength property is not vacuous.

A complete development needs the Bartlett–Mendelson symmetrization bound for bounded losses, McDiarmid's inequality, Maurer's inequality, and the Lipschitz and distance-to-degeneracy facts of Section 4.1. Maurer's inequality and the multivariate Rademacher complexity are reusable across vector-valued learning theory. Proofs of any milestone, and of Maurer's inequality in particular, are welcome.

Selected references

O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, Mathematics of Operations Research, 2023; preprint arXiv:1905.11488v3, 2022. https://arxiv.org/abs/1905.11488
A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 2022. https://doi.org/10.1287/mnsc.2020.3922
A. Maurer, A Vector-Contraction Inequality for Rademacher Complexities, Algorithmic Learning Theory (ALT), 2016. https://arxiv.org/abs/1605.00251
P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
V. Koltchinskii, D. Panchenko, Empirical Margin Distributions and Bounding the Generalization Error of Combined Classifiers, Annals of Statistics 30(1), 2002. https://doi.org/10.1214/aos/1015362183

9 thms3 active usersReviewed

Completed

Machine Learning Probability·Captain: naimengye

Understanding Machine Learning XIX: Generative ModelsTextbook

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.

11 thms3 active usersReviewed

Completed

Combinatorics Machine Learning Probability·Captain: naimengye

An Introduction to Computational Learning Theory V: Classification Noise and Statistical QueriesTextbook

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

7 thms3 active usersReviewed

Completed

Combinatorics Machine Learning Probability·Captain: naimengye

An Introduction to Computational Learning Theory IV: Weak and Strong Learning, Boosting and Chernoff BoundsTextbook

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

7 thms3 active usersReviewed

Completed

Bandit Algorithms Operations Research Optimization+1·Captain: naimengye

Multi-armed Bandit Allocation Indices VI: Bandit Sampling Processes, Favourable Priors and Invariance of the IndexTextbook

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

9 thms3 active usersReviewed

Completed

Machine Learning Operations Research Probability+1·Captain: mikedeng1

Foundations of Machine Learning XIV: Finite Markov Decision Processes and Bellman's EquationsTextbook

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.

13 thms3 active usersReviewed

Completed

Machine Learning Probability Theoretical Computer Science·Captain: mikedeng1

Foundations of Machine Learning XII: Algorithmic StabilityTextbook

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.

11 thms3 active usersReviewed

Completed

Machine Learning Probability Theoretical Computer Science·Captain: mikedeng1

Foundations of Machine Learning XI: Maximum Entropy Models and DualityTextbook

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.

14 thms3 active usersReviewed

Completed

Machine Learning Probability Theoretical Computer Science·Captain: mikedeng1

Foundations of Machine Learning X: Regression and Rademacher Complexity BoundsTextbook

Motivation

Every generalization bound presented so far in this series is for classification, where the error of a prediction is binary (correct or not). Regression asks a different question: predictions are real-valued, and error is measured by the magnitude of the deviation from the true label, via a loss function L. Chapter 11 develops generalization theory for bounded regression, showing that the same two complexity measures used for classification — Rademacher complexity and a VC-dimension analogue — extend naturally, once the loss function itself is folded into the machinery via a Lipschitz-contraction argument (Rademacher route) or a reduction to classification via level-set thresholding (pseudo-dimension route).

Setting

A regression hypothesis h:X→ℝ is scored by a loss L:ℝ×ℝ→ℝ against a joint distribution D on X×ℝ (the stochastic scenario, since regression labels are rarely exactly reproducible); R(h) = E_{(x,y)~D}[L(h(x),y)] (Eq. 11.1) and R̂_S(h) = (1/m)∑L(h(x_i),y_i) (Eq. 11.2). For a finite hypothesis set, Theorem 11.1 gives a Hoeffding/union-bound guarantee directly, the regression analogue of chunk 02-pac's finite-hypothesis bound. For infinite H, §11.2.2 develops a Rademacher-complexity route: Proposition 11.2 shows that if L is µ-Lipschitz in its first (predicted-value) argument, the Rademacher complexity of the loss-composed family G = {(x,y)↦L(h(x),y) : h∈H} is controlled by µ times H's own Rademacher complexity, via Talagrand's contraction lemma (chunk 05-svm's Lemma 5.7); Theorem 11.3 combines this with chunk 03's Theorem 3.3 to give the chapter's headline bound. §11.2.3 develops an independent, purely combinatorial route: pseudo-dimension (Definition 11.5), a real-valued analogue of VC-dimension defined via threshold-witnessed shattering (Definition 11.4, restated via its own Eq. 11.3 as the VC-dimension of a thresholded indicator family); Theorem 11.8 gives a pseudo-dimension generalization bound by reducing regression to a family of classification problems (one per threshold t), using the tail-integral identity Eq. 11.5.

Formalization targets

Theorem 11.1 (milestone). For L bounded by M and H finite: for any δ>0, with probability at least 1-δ, for all h∈H: R(h) ≤ R̂_S(h) + M√((log|H|+log(1/δ))/(2m)).

Proposition 11.2 (milestone). For L non-negative, bounded by M, µ-Lipschitz in its first argument: for any sample S, R̂_S(G) ≤ µR̂_S(H).

Theorem 11.3 — the mission's goal. Under Proposition 11.2's hypotheses on L: for any δ>0, with probability at least 1-δ, for all h∈H: E[L(h(x),y)] ≤ (1/m)∑L(h(x_i),y_i) + 2µR_m(H) + M√(log(1/δ)/(2m)), and also with 2µR̂_S(H) + 3M√(log(2/δ)/(2m)).

Theorem 11.8 (milestone). For Pdim(G)=d, L non-negative bounded by M: for any δ>0, with probability at least 1-δ over a sample of size m, for all h∈H: R(h) ≤ R̂_S(h) + M√(2d log(em/d)/m) + M√(log(1/δ)/(2m)).

Significance

Theorem 11.3 is the chapter's own choice of headline result (§11.2's stated goal is to show "how the Rademacher complexity bounds of theorem 3.3 can be used to derive generalization bounds for regression"), and its proof genuinely reuses two pieces of prior machinery from this series — chunk 03's Theorem 3.3 and chunk 05's Talagrand's-lemma-style contraction — combined via a new observation (Proposition 11.2) specific to loss-composed families, not a restatement of either. Theorem 11.8 is the chapter's second, structurally independent technique: its em/d bound parallels chunk 03's Corollary 3.19 (both ultimately reduce to a VC-dimension-style growth-function argument), but the reduction itself — regression to a continuum of threshold classification problems, via the Lebesgue-integral tail identity Eq. (11.5) applied to |R(h)-R̂_S(h)| — is genuinely new content for this book, and pseudo-dimension has no prior art on the platform or in Mathlib. No prior art exists for this chapter's overall content either: GET /theorems?q=generalization%20bound%20regression and GET /theorems?q=pseudo-dimension both return zero hits.

Difficulty

Proposition 11.2's proof needs Talagrand's contraction lemma applied with the Lipschitz constant taken in the first argument of L only — the predicted value h(x_i), holding the true label y_i fixed — exactly the pitfall BRIEF.md names: a loss Lipschitz in the wrong argument, or in both arguments jointly, would not license this step. Theorem 11.8's proof is the chapter's most involved: it defines, for every h∈H and threshold t≥0, a classifier c(h,t):(x,y)↦1_{L(h(x),y)>t}, bounds |R(h)-R̂_S(h)| by M·sup_{t∈[0,M]}|R(c(h,t))- R̂_S(c(h,t))| via the tail-integral identity, and then applies a VC-dimension-style classification bound (Corollary 3.19) to the family of thresholded classifiers — whose VC-dimension is, by Eq. (11.3), exactly Pdim(G) by construction. A formalization that conflated pseudo-dimension with ordinary VC-dimension, or reused chunk 03's HasVCDim definition by relabeling, would misrepresent this chapter's genuinely different (real-valued, threshold-witnessed) combinatorial notion — precisely the pitfall BRIEF.md flags.

Formalization scope

Y := ℝ throughout (the book's own "Y a measurable subset of ℝ"), a harmless simplification consistent with every hypothesis, loss and Lipschitz condition in this chapter being stated for real-valued scores and labels. EmpiricalRademacherComplexity/ RademacherComplexity restate chunk 03-rademacher-vc's Definitions 3.1/3.2 locally, since a draft item cannot import another chunk's draft module. Shatters/PseudoDim are formalized via the book's own equivalent reformulation (Eq. 11.3, the thresholded-indicator form), rather than the sign-function form of Definition 11.4 directly, since the two coincide except at a measure-zero boundary the book itself does not address; PseudoDim mirrors chunk 03's HasVCDim Prop-valued pattern (does not cover Pdim(G)=+∞; every consuming theorem takes it as an explicit hypothesis) but is a structurally distinct definition built on Shatters, never a relabeling of HasVCDim, per BRIEF.md's pitfall note. Proposition 11.2's and Theorem 11.3's Lipschitz hypothesis (hLlip) is stated with the true label y' universally quantified outside the two-point comparison y1, y2 (the predicted values), matching "for any fixed y' ∈ Y, y ↦ L(y,y') is µ-Lipschitz" exactly — Lipschitzness in the first argument only, per BRIEF.md's pitfall note. RademacherComplexity (Measure.map Prod.fst D) H m gives the book's R_m(H) (H's Rademacher complexity under the marginal sampling distribution of the inputs x, i.e. D's first marginal). No numerical constant is altered from the book in any of the four theorems.

Not formalized: the L_p-loss worked example following Theorem 11.3's proof (an instantiation of the general theorem for a specific loss family, not a separate numbered theorem); Theorem 11.6 and Theorem 11.7 (worked pseudo-dimension examples for hyperplanes and vector spaces, background/illustration rather than the chapter's general machinery — drafting only these examples instead of the general Theorem 11.8 would be this chapter's trivializing formalization); the two-sided variant of Theorem 11.1 mentioned immediately after its proof (an unnumbered remark, not a separately displayed/numbered theorem); and all of §11.3 (linear regression, kernel ridge regression, SVR, Lasso and their online variants), which is applications-heavy per BRIEF.md's chapter restriction to §11.1-11.2.

Selected references

M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 11 (§11.1-11.2).
D. Haussler, "Decision theoretic generalizations of the PAC model for neural net and other learning applications," Information and Computation 100(1), 1992 (pseudo-dimension's origin).
D. Pollard, Convergence of Stochastic Processes, Springer, 1984 (the tail-integral identity Eq. 11.5's classical antecedent).

11 thms3 active usersReviewed

Completed

Machine Learning Probability Theoretical Computer Science·Captain: mikedeng1

Foundations of Machine Learning VIII: Multi-Class Classification and the Margin BoundTextbook

Motivation

Every generalization bound in chapters 2-5 is for binary classification. Most real-world classification problems have more than two classes, and the number of classes can itself be in the hundreds or thousands (topic classification, speech recognition). Chapter 9 extends the margin-based generalization theory of chapter 5 (SVMs) to this multi-class, mono-label setting, using the same Rademacher-complexity machinery as chunk 03-rademacher-vc, but with a new combinatorial ingredient — bounding the Rademacher complexity of a family built by taking a pointwise maximum over several hypothesis sets — needed because a multi-class prediction is itself an argmax over per-class scores.

Setting

A multi-class hypothesis is a scoring function $h:X\times Y\to\mathbb R$ with $Y=\{1,\dots,k\}$ (mono-label case); the predicted label is $\arg\max_y h(x,y)$ , and the margin $\rho_h(x,y)=h(x,y)-\max_{y'\ne y}h(x,y')$ (p. 215) is negative exactly when $h$ misclassifies $(x,y)$ . The empirical margin loss $\hat R_{S,\rho}(h)$ (Eq. 9.5) uses the same margin-loss function $\Phi_\rho$ (Definition 5.5) as chunk 05-svm, restated locally here. $\Pi_1(H) = \{x\mapsto h(x,y):y\in Y,h\in H\}$ (p. 217) projects a multi-class hypothesis set onto ordinary real-valued functions on $X$ — the object the chapter's Rademacher-complexity bound actually controls, since $H\subseteq\mathbb R^{X\times Y}$ has no norm of its own without such a projection. Lemma 9.1 is a purely combinatorial tool: the empirical Rademacher complexity of a family built by taking the pointwise max over $l$ hypothesis sets is bounded by the sum of their individual empirical Rademacher complexities — used to control the argmax structure of a multi-class prediction. Theorem 9.2 combines this with chunk 03's Rademacher-complexity generalization machinery (Theorem 3.3) to give the chapter's margin bound. Proposition 9.3 and Corollary 9.4 specialize this to kernel-based hypotheses, where each class has its own weight vector in a reproducing kernel Hilbert space and the $k$ weight vectors are jointly constrained by an $L^p$ -type group norm $\|W\|_{H,p}\le\Lambda$ .

Formalization targets

Lemma 9.1 (milestone). For $F_1,\dots,F_l$ hypothesis sets in $\mathbb R^X$ , $l\ge1$ , and $G=\{\max\{h_1,\dots,h_l\}:h_i\in F_i\}$ : $\hat R_S(G)\le\sum_{j=1}^l\hat R_S(F_j)$ .

Theorem 9.2 — the mission's goal. For $H\subseteq\mathbb R^{X\times Y}$ , $Y=\{1,\dots,k\}$ , fix $\rho>0$ . For any $\delta>0$ , with probability at least $1-\delta$ , for all $h\in H$ :

R(h) \le \hat R_{S,\rho}(h) + \tfrac{4k}\rho R_m(\Pi_1(H)) + \sqrt{\tfrac{\log(1/\delta)} {2m}}.

Proposition 9.3 (milestone). For a PDS kernel $K$ with feature map $\Phi$ and $K(x,x)\le r^2$ : $R_m(\Pi_1(H_{K,p})) \le \sqrt{r^2\Lambda^2/m}$ .

Corollary 9.4 (milestone). Under Proposition 9.3's hypotheses, fix $\rho>0$ . For any $\delta>0$ , with probability at least $1-\delta$ , for all $h\in H_{K,p}$ : $R(h) \le \hat R_{S,\rho}(h) + 4k\sqrt{r^2\Lambda^2/\rho^2/m} + \sqrt{\log(1/\delta)/(2m)}$ .

Significance

Theorem 9.2 is the multi-class generalization of chunk 05-svm's Theorem 5.8, and its proof is the chapter's genuine new technique rather than a restatement: it needs a $k$ -way application of Lemma 9.1 (once for the argmax structure of the margin, once summing over the $k$ possible labels), which is exactly where the $4k$ factor comes from. Corollary 9.4 is the direct theoretical basis for the multi-class SVM algorithm the chapter derives next (§9.3.1): the displayed dual optimization problem literally minimizes the right-hand side of the corollary's bound. No prior art exists on the platform: GET /theorems?q=multi-class%20classification returns zero hits, and chunk 03's Rademacher-complexity machinery (needed by the proof route) is a draft, not reusable, per the "drafts cannot import drafts" rule.

Difficulty

Lemma 9.1's proof is a genuine two-function argument (max as $\tfrac12(h_1+h_2+|h_1-h_2|)$ , Talagrand's lemma applied to $|\cdot|$ ) generalized to $l$ functions by induction, not a one-line consequence of chunk 03's single-hypothesis-set bound. Theorem 9.2's own proof (PDF pp. 234-236) is the chapter's most involved: it introduces an auxiliary margin function $\rho_{\theta,h}$ with a free parameter $\theta$ later fixed to $2\rho$ , splits the resulting Rademacher complexity into a "diagonal" term (bounded via a further one-hot decomposition across the $k$ classes, giving the first factor of $k$ ) and a "off-diagonal" term bounded via Lemma 9.1 (giving the second factor, folded into the same $4k$ constant). A formalization that stated Theorem 9.2 for $H$ itself rather than $\Pi_1(H)$ , or that treated $k$ as an unrelated free constant rather than the actual number of classes, would misstate the theorem — precisely the pitfall BRIEF.md names for this chapter. Proposition 9.3's proof is a clean Cauchy-Schwarz/Jensen argument in the RKHS but needs the $L^p$ -group-norm hypothesis class $H_{K,p}$ stated with its exact footnote definition (PDF p. 236), not a simplified $p=2$ special case.

Formalization scope

GeneralizationError, EmpiricalRademacherComplexity and RademacherComplexity are restated locally in this chunk's MultiClass namespace (the last two identical in content to chunk 03-rademacher-vc's own copies); MarginLossFunction restates chunk 05-svm's Definition 5.5 (the same function, needed here for this chapter's own EmpiricalMarginLoss); IsPDS restates chunk 06-kernels's PDS-kernel definition. All are duplicated rather than imported since a draft item cannot import another chunk's draft module, and none of 03, 05, 06 is listed as reusable in missions/README.md's "Published definitions" table at the time of this session. GeneralizationError is formalized via the book's own established equivalence " $h$ misclassifies $(x,y)$ iff $\rho_h(x,y)\le0$ " (the form Theorem 9.2's own proof displays and works with), rather than via an explicit argmax classifier construction — checked as faithful, not a weakening, since it is exactly the quantity the chapter's proof bounds. MarginFunction's ⨆_{y'≠y} is a real supremum rather than a Finset.sup', avoiding a nonempty-finset side proof at definition time; every consuming theorem supplies 2 ≤ k (Y = Fin k) to guard it against trap 5. MaxFamily's index type is Fintype+Nonempty rather than a Finset-cardinality parameter l, a harmless generalization matching "l ≥ 1 hypothesis sets" via Nonempty. IsPDS's feature map Φ and its defining property K(x,y) = ⟪Φ(x),Φ(y)⟫ are supplied as hypotheses to the two kernel theorems rather than as a separate "feature mapping associated to a kernel" definition — the book itself treats this as a given correspondence, not a construction. No numerical constant is altered: 4k/ρ and log(1/δ) in Theorem 9.2, r²Λ²/m in Proposition 9.3, and 4k and r²Λ²/ρ²/m in Corollary 9.4 are exactly as displayed.

Not formalized: §9.1's discussion of the multi-label case (Eq. 9.2/9.3, the Hamming-distance risk) and Eq. 9.4 (empirical Hamming error) — background for a case this chapter's own generalization-bound section (§9.2) does not cover (the mono-label case only); the multi-class SVM primal/dual optimization problems (§9.3.1, an algorithm derived from Corollary 9.4, not a generalization-theoretic theorem); AdaBoost.MH (§9.3.2, a boosting algorithm, analyzed via a convex-surrogate argument rather than the Rademacher-complexity route this mission formalizes); and the uniform-over- $\rho$ extension mentioned at the end of the Theorem 9.2 proof (an unnumbered remark referencing Theorem 5.9's technique from a different chapter, not restated here). Drafting only the algorithmic consequences (the multi-class SVM's optimization problem) in place of the generalization bounds themselves would be this chapter's trivializing formalization.

Selected references

M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 9.
V. Koltchinskii, D. Panchenko, "Empirical margin distributions and bounding the generalization error of combined classifiers," Annals of Statistics 30(1), 2002 (Lemma 9.1's technique).
K. Crammer, Y. Singer, "On the algorithmic implementation of multiclass kernel-based vector machines," JMLR 2, 2001 (the multi-class SVM algorithm §9.3.1 derives).

15 thms3 active usersReviewed

Completed

Machine Learning Probability Theoretical Computer Science·Captain: mikedeng1

Foundations of Machine Learning VII: On-Line Learning and On-Line-to-Batch ConversionTextbook

Motivation

Every guarantee in the preceding chapters assumes a fixed distribution and i.i.d. sampling. On-line learning drops both assumptions: an algorithm processes one example at a time, in an adversarial (worst-case) sequence, and is judged by regret against the best fixed comparator in hindsight rather than by generalization error. This chapter develops the theory for this setting — mistake bounds and regret bounds for prediction with expert advice, a margin-based mistake bound for the Perceptron — and then closes a conceptual gap: since on-line algorithms need no distributional assumption, can their guarantees be converted into ordinary distributional (batch) generalization guarantees when the data does happen to be i.i.d.? The on-line-to-batch conversion theorem answers yes, using nothing but an Azuma's-inequality martingale argument on the sequence of hypotheses the algorithm actually produces.

Setting

At round t, an on-line algorithm receives x_t, predicts ŷ_t, receives the true label y_t, and incurs loss L(ŷ_t,y_t); its regret R_T (Eq. 8.1) compares its cumulative loss to the best fixed action's in hindsight. §8.2 develops this for prediction with expert advice: the Halving algorithm (realizable case), Weighted Majority and its randomized version RWM (zero-one loss, Theorem 8.4's L_T ≤ log(N)/(1-β) + (2-β)L_T^min, proved by the chapter's recurring potential-function technique applied to W_t = ∑_i w_{t,i}), and the Exponential Weighted Average algorithm (convex losses). §8.3.1 analyzes the Perceptron, a linear classification algorithm whose margin-based mistake bound (Theorem 8.8, separable case; the non-separable Theorem 8.11, restated here, in terms of an arbitrary comparator v's hinge losses) depends only on the normalized margin, not the ambient dimension. §8.4 shows that averaging the hypotheses h_1,…,h_T an on-line algorithm produces while processing an i.i.d. sample S yields a hypothesis with controlled true risk: Lemma 8.14 bounds the average of the per-round risks R(h_t) by the average on-line loss via a martingale argument on V_t = R(h_t) - L(h_t(x_t),y_t), and Theorem 8.15 upgrades this, via the loss's convexity, to a bound on the risk of the averaged hypothesis (1/T)∑h_t.

Formalization targets

Theorem 8.4 (milestone). Fix β∈[1/2,1). For any T≥1: L_T ≤ log(N)/(1-β) + (2-β)L_T^min; for β=max{1/2,1-√(log(N)/T)}: L_T ≤ L_T^min + 2√(T log N).

Theorem 8.11 (milestone). M ≤ inf_{ρ>0,‖v‖₂≤1}[(r/ρ+√(r²/ρ²+4‖l_ρ‖₁))/2]², where l_ρ=(l_t)_{t∈I}, l_t=max{0,1-y_t(v·x_t)/ρ}.

Lemma 8.14 (milestone). For any δ>0, with probability at least 1-δ: (1/T)∑_tR(h_t) ≤ (1/T)∑_tL(h_t(x_t),y_t) + M√(2log(1/δ)/T).

Theorem 8.15 — the mission's goal (first inequality). Under Lemma 8.14's hypotheses, with L additionally convex in its first argument: for any δ>0, with probability at least 1-δ: R((1/T)∑_th_t) ≤ (1/T)∑_tL(h_t(x_t),y_t) + M√(2log(1/δ)/T).

Significance

Theorem 8.15 is the chapter's conceptual capstone: it is the only bridge in the whole book between the adversarial on-line-learning framework and the distributional PAC/statistical framework every other chapter develops, and its proof needs nothing beyond Lemma 8.14 plus convexity — no new machinery, just the right observation about the loss's structure. Theorem 8.4 is the chapter's cleanest instance of its recurring potential-function proof technique (reused, with variations, for Theorems 8.3, 8.6 and 8.7), and — checked against the platform's existing OnlineConvexOpt.Introduction.randomized_weighted_majority_mistake_bound (Hazan series) — a genuinely different result from what is already on the platform: that lemma bounds a mistake count with a (1+ε) multiplier, this bounds the RWM algorithm's own weighted-mixture loss with a 1/(1-β) term and a distinct optimal-β substitution, confirming BRIEF.md's assessment that the two are close but not interchangeable. Theorem 8.11 is the non-realizable generalization of the separable-case Perceptron bound (Theorem 8.8) that motivates soft-margin algorithms generally, expressed via an arbitrary comparator's hinge loss rather than assuming perfect separability. No prior art exists for the chapter's other content: GET /theorems?q=online%20to%20batch returns zero hits, and GET /theorems?q=perceptron returns only an unrelated neural-network topology result.

Difficulty

Theorem 8.4's proof (mirrored by Theorem 8.3's WM analogue) derives matching upper and lower bounds on the potential W_t, combines them via a logarithm, and substitutes a specific optimal β found by differentiating the resulting bound — a genuine two-step optimization argument, not a direct algebraic identity. Theorem 8.11's proof solves a quadratic inequality in √M after summing the hinge-loss-defining inequalities over the update set I and invoking the Cauchy-Schwarz step already used in Theorem 8.8's proof; keeping the inf over both ρ and v in the statement (not fixing them, per BRIEF.md's pitfall note) is what makes this a genuine bound rather than a bound for one arbitrary choice. Lemma 8.14's proof is an application of Azuma's inequality (the book's own Theorem D.7) to the martingale difference sequence V_t = R(h_t) - L(h_t(x_t),y_t), which requires h_t to be measurable with respect to the history strictly before round t — the on-line algorithm's hypothesis at round t must not depend on the pair drawn at that same round, per BRIEF.md's pitfall note. Theorem 8.15's step beyond Lemma 8.14 is the passage from the average of T individual risks to the risk of the averaged hypothesis, licensed by Jensen's inequality under the loss's convexity in its first argument — dropping convexity breaks exactly this step, not merely weakening a constant.

Formalization scope

GeneralizationError restates chunk 11-regression's Eq. (11.1) convention locally (Y := ℝ, consistent with that chunk's own harmless simplification), needed here since Theorem 8.15 requires averaging hypotheses into a single real-valued function. OnlineHypothesis A S t is formalized so that its type signature itself enforces history-adaptedness: the on-line algorithm A : (n:ℕ) → (Fin n → X × ℝ) → (X → ℝ) is a function of the prefix of the sample seen so far, and OnlineHypothesis A S t applies it only to S's first t pairs — this is what licenses Azuma's inequality's martingale-difference argument (the conditional-mean-zero property of V_t), per BRIEF.md's pitfall note. Revision (2026-09-19), correcting an earlier claim in this section: history-adaptedness does not by itself guard against GeneralizationError's Bochner integral silently junking to 0 for a non-measurable hypothesis (a distinct property — whether h_t, as a function of x, is Measurable — from whether h_t depends on round t's own draw). Moderation found this a live gap in both Lemma 8.14 and Theorem 8.15's drafted statements; both now carry an explicit hAmeas/hLmeas hypothesis in addition to the history-adapted type signature. RWM's w_{t,i}, W_t, p_{t,i}, L_t, L_T, L_{T,i}, L_T^min are modeled as their own recursively-defined algorithm state (mirroring, but never substituting into, chunk 07-boosting's AdaBoost pattern), matching this chapter's own loss-based (not mistake-count) quantities, per BRIEF.md's pitfall note distinguishing them from AdaBoost's and RWM-mistake variants. The Perceptron's w_t, update-index set I, and M = |I| are modeled the same way, using Eq. (8.23)'s equivalent sign-agreement update rule (the book's own reformulation of Figure 8.6's sgn-based rule). Theorem 8.11's inf_{ρ>0,‖v‖₂≤1} is a genuine nested restricted infimum (⨅ ρ ∈ Set.Ioi 0, ⨅ v ∈ Metric.closedBall 0 1, …), not a bound instantiated at fixed ρ, v, per BRIEF.md's explicit pitfall note. No numerical constant is altered from the book in any of the four theorems.

Not formalized: Theorems 8.1-8.3 (Halving and WM mistake bounds — the chapter's warm-up results, superseded in content by the more general RWM/EWA theorems that follow), Theorem 8.5 (a matching lower bound, a distinct impossibility result rather than an algorithm's guarantee), Theorems 8.6-8.7 (Exponential Weighted Average regret bounds — a third algorithm with its own potential-function proof, out of scope per BRIEF.md's restriction to §8.2's Halving/WM/RWM), Theorems 8.8-8.10 (the Perceptron's separable-case bound and its leave-one-out-based expected generalization bounds, both superseded in generality by Theorem 8.11 for this mission's purposes), Theorem 8.12 (Perceptron's L²-norm hinge-loss bound, the book's own note that it is implied by, and looser than, Theorem 8.11's L¹-norm bound), the dual/kernel Perceptron (an equivalent reformulation, not new generalization content), and Theorem 8.15's second displayed inequality (a regret-form corollary depending on the regret decomposition of the surrounding discussion, not drafted per BRIEF.md's own recommendation to commit to the first inequality as the goal). §8.3.2 (Winnow) and §8.5 (the game-theoretic connection) are out of scope per BRIEF.md's chapter restriction.

Selected references

M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 8 (§8.2, §8.3.1, §8.4).
N. Littlestone, M. K. Warmuth, "The weighted majority algorithm," Information and Computation 108(2), 1994 (WM/RWM's origin).
F. Rosenblatt, "The perceptron: a probabilistic model for information storage and organization in the brain," Psychological Review 65(6), 1958 (the Perceptron algorithm).
Y. Freund, R. E. Schapire, "Large margin classification using the perceptron algorithm," Machine Learning 37(3), 1999 (Theorem 8.11's hinge-loss mistake bound).

16 thms3 active usersReviewed

Completed

Machine Learning Probability·Captain: mikedeng1

High-Dimensional Statistics IX: Nuclear-Norm Regularization for Low-Rank Matrix RegressionTextbook

Motivation

Many estimation problems are naturally posed over matrices rather than vectors: recommender systems (Netflix-style matrix completion), multivariate regression with correlated responses, vector autoregressive time series, and phase retrieval all reduce to estimating an unknown matrix $\Theta^*$ that is low-rank, or well approximated by one. A rank constraint alone makes the natural least-squares estimator non-convex and generally intractable; replacing it with the nuclear norm — the sum of the matrix's singular values, the tightest convex surrogate for rank — yields a tractable semidefinite program. Wainwright's High-Dimensional Statistics (2019), Chapter 10, shows that this substitution costs nothing statistically: nuclear-norm-regularized least squares achieves error rates matching what one could hope for even knowing the rank in advance, by specializing Chapter 9's general decomposable-regularizer framework (mission 09-decomposability) directly to the nuclear norm.

Setting

For matrices $A,B\in\mathbb R^{d_1\times d_2}$ , the trace inner product is $\langle\!\langle A,B\rangle\!\rangle := \mathrm{trace}(A^TB) = \sum_{j_1,j_2}A_{j_1j_2}B_{j_1j_2}$ (Eq. 10.1), inducing the Frobenius norm $\|\!|A|\!\|_F$ . Given design matrices $X_1,\dots,X_n\in\mathbb R^{d_1\times d_2}$ and responses $y_i=\langle\!\langle X_i,\Theta^*\rangle\!\rangle+w_i$ , the observation operator $\mathcal X_n(\Theta):=(\langle\!\langle X_i,\Theta\rangle\!\rangle)_{i=1}^n$ and its adjoint $\mathcal X_n^*(u):=\sum_iu_iX_i$ (Eqs. 10.2-10.3) are the matrix analogs of a vector design matrix and its transpose. The nuclear norm $\|\!|\Theta|\!\|_{\mathrm{nuc}}:=\sum_j\sigma_j(\Theta)$ (Eq. 10.5) — the sum of singular values — is a decomposable regularizer (in the sense of Chapter 9) with respect to the subspace pair spanned by the top singular vectors of any target matrix, and its dual norm (Table 9.1) is the $\ell_2$ -operator (spectral) norm $\|\!|\cdot|\!\|_2$ . The estimator under study is nuclear-norm-regularized least squares,

\hat\Theta \in \operatorname*{arg\,min}_{\Theta\in\mathbb R^{d_1\times d_2}} \left\{ \frac{1}{2n}\|y-\mathcal X_n(\Theta)\|_2^2 + \lambda_n\|\!|\Theta|\!\|_{\mathrm{nuc}} \right\} \tag{10.16}

with $\lambda_n>0$ user-chosen.

Formalization targets

Goal (Proposition 10.6)

Suppose $\mathcal X_n$ satisfies the restricted strong convexity condition (10.17), $\|\mathcal X_n(\Delta)\|_2^2/(2n) \ge \kappa/2\|\!|\Delta|\!\|_F^2 - c_0\frac{d_1+d_2}{n}\|\!|\Delta|\!\|_{\mathrm{nuc}}^2$ for all $\Delta$ , with $\kappa>0$ , $c_0\ge 0$ . Conditioned on the good event $\mathcal G(\lambda_n)=\{\|\!|\frac1n\sum_iw_iX_i|\!\|_2 \le\lambda_n/2\}$ , any optimal $\hat\Theta$ satisfies, for any $r\in\{1,\dots,d'\}$ with $r\le\kappa n/(128c_0(d_1+d_2))$ ,

\|\!|\hat\Theta-\Theta^*|\!\|_F^2 \le \frac{9}{2}\frac{\lambda_n^2}{\kappa^2}r + \frac{1}{\kappa}\left\{2\lambda_n\sum_{j=r+1}^{d'}\sigma_j(\Theta^*) + \frac{32c_0(d_1+d_2)}{n}\left(\sum_{j=r+1}^{d'}\sigma_j(\Theta^*)\right)^2\right\}.

Milestone (Proposition 10.7)

Under the alternative $\Phi^*$ -curvature condition (10.20) (a curvature bound on the gradient map rather than the Taylor error), with $\mathrm{rank}(\Theta^*)<\kappa/(64\tau_n)$ : conditioned on $\mathcal G(\lambda_n)=\{\|\!|\frac1n\mathcal X_n^*(w)|\!\|_2\le\lambda_n/2\}$ , any optimal $\hat\Theta$ satisfies $\|\!|\hat\Theta-\Theta^*|\!\|_2 \le 3\sqrt2\,\lambda_n/\kappa$ — an operator-norm bound the book notes is, in conjunction with the cone-like constraint (10.15), strictly stronger than Proposition 10.6's Frobenius-norm bound.

Significance

Proposition 10.6 is this chapter's direct payoff from Chapter 9's general machinery: it shows that the deterministic backbone of the Lasso's guarantee (mission 07-sparse-linear) extends essentially verbatim to the matrix setting, with the sparsity level $s$ replaced by the target rank $r$ and the ambient dimension $d$ replaced by $d_1+d_2$ — exactly the "degrees of freedom" scaling one would predict by counting the parameters needed to specify a rank- $r$ matrix. Every one of the chapter's later corollaries (matrix compressed sensing, multivariate regression, matrix completion) is obtained by verifying the restricted strong convexity condition (10.17) holds with high probability for a specific random design, then reading the rate directly off Proposition 10.6 — the same two-step recipe Chapter 9's own Theorem 9.19 established abstractly. Proposition 10.7's operator-norm bound is what subsequently controls the individual singular values of the estimation error, needed for exact-rank-recovery guarantees.

Difficulty

Both results are direct specializations of Chapter 9's general oracle inequalities (Theorem 9.19 and Theorem 9.24 respectively) to the nuclear norm as regularizer and the Frobenius/operator norm pair, so their formalization difficulty lies almost entirely in getting the matrix-specific objects right rather than in new proof machinery: the nuclear norm requires an actual notion of singular values (realized via the eigenvalues of the Gram matrix $\Theta^T\Theta$ , using Mathlib's Hermitian-matrix spectral theorem), the operator norm requires the correct rectangular generalization of the symmetric-matrix Rayleigh-quotient characterization used in mission 08-pca, and the restricted-strong-convexity and curvature conditions must be instantiated against the correctly-adjointed observation operator $\mathcal X_n^*$ . A further subtlety is keeping Proposition 10.6's Frobenius-norm conclusion and Proposition 10.7's operator-norm conclusion cleanly distinct — the book itself warns against conflating the norms used across different chapters of Part II (the vector $\ell_2$ -norm of chunks 07-sparse-linear/08-pca versus the matrix Frobenius and operator norms here).

Formalization scope

Scope cut, disclosed here and in STATUS.md. BRIEF.md recommends Corollary 10.10 (the sample-complexity bound for the $\Sigma$ -Gaussian random matrix ensemble) as the goal theorem. Corollary 10.10 is a genuinely probabilistic statement — it asserts a bound holding "with probability at least $1-2e^{-2n\delta^2}$ " over $n$ i.i.d. draws of design matrices from a $\Sigma$ -Gaussian ensemble (Theorem 10.8's own high-probability restricted-strong-convexity certification for that ensemble) — and formalizing it faithfully would require a genuine multivariate-Gaussian-measure infrastructure on matrix space (a probability space, an i.i.d. sequence of $\Sigma$ -covariance-structured Gaussian matrices, and Mathlib's measure-theoretic probability API) that is disproportionate to this mission's time budget, and orthogonal to what Chapter 10 itself contributes (the chapter's own text stresses that Propositions 10.6 and 10.7 are the chapter's deterministic core, with probability entering only in Section 10.3's ensemble-specific certification — precisely mirroring chunk 09-decomposability's own "Theorem 9.19 is actually a deterministic result" framing). This mission instead takes Proposition 10.6 as its goal — explicitly named in BRIEF.md's own candidate list as "the nuclear-norm oracle inequality, an explicit corollary of Theorem 9.19" — the natural, tractable, still highly citable deterministic title result of Section 10.2, together with its companion Proposition 10.7. Theorem 10.8 (the $\Sigma$ -Gaussian ensemble's RSC certification), Corollary 10.9 (noiseless exact recovery) and Corollary 10.10 itself are left for a future mission with a dedicated probability-theory budget. The cone-like constraint (Eq. 10.15) — whose own faithful statement requires the same explicit subspace-pair machinery ( $\mathcal M(U_r,V_r),\bar{\mathcal M}(U_r,V_r)$ ) chunk 09-decomposability built for the general theory — is similarly left out, since Propositions 10.6 and 10.7's own numbered statements never expose these subspaces directly (only their proofs do, via instantiating Theorem 9.19/9.24). singularValues and nuclearNorm are noncomputable, defined via Mathlib's Hermitian-matrix eigenvalue spectral theorem; c0 ≥ 0 and λn > 0 are made explicit, matching this book's running conventions for RSC tolerance constants and regularization weights (see MODERATION_NOTES.md).

Selected references

Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 10. DOI: 10.1017/9781108627771.
Negahban, S., Wainwright, M. J. "Estimation of (near) low-rank matrices with noise and high-dimensional scaling." Annals of Statistics, 39(2), 2011, 1069–1097.
Recht, B., Fazel, M., Parrilo, P. A. "Guaranteed minimum-rank solutions of linear matrix equations via nuclear norm minimization." SIAM Review, 52(3), 2010, 471–501.

3 thms3 active usersReviewed

Machine Learning Probability·Captain: mikedeng1

Support Vector Machines VI: An Oracle Inequality for Classifying with Support Vector MachinesTextbook

Motivation

A support vector machine for classification is trained by minimizing a regularized hinge-loss objective — never the classification loss itself, which is non-convex and computationally intractable to minimize. Every earlier mission in this series supplies one piece of the argument that this substitution is nonetheless justified: 01-loss-functions shows the excess hinge risk controls the excess classification risk (Zhang's inequality); 05-concentration supplies a Hilbert-space concentration inequality; and Chapter 6 of the book (not itself a mission in this series, but cited here) combines concentration with a stability argument to bound how far the empirical SVM solution's regularized hinge risk can be from its population minimum. Steinwart & Christmann, Support Vector Machines (Springer 2008, Information Science and Statistics), Chapter 8, assembles exactly these three pieces into Theorem 8.1: an explicit, finite-sample, non-asymptotic bound on how close an SVM classifier's classification risk gets to the Bayes risk — the payoff result the whole apparatus of Chapters 2, 5 and 6 was built to deliver.

Setting

Fix a measurable space $X$ and $Y := \{-1,1\}$ . A loss $L : X \times Y \times \mathbb R \to [0,\infty)$ , a distribution $P$ on $X \times Y$ , the $L$ -risk $R_{L,P}(f) := \int L(x,y,f(x)) \,dP(x,y)$ , and the Bayes risk $R^*_{L,P} := \inf_f R_{L,P}(f)$ are exactly as in 01-loss-functions, restated locally here. The hinge loss is $L_{\mathrm{hinge}}(y,t) := \max\{0,1-yt\}$ and the classification loss is $L_{\mathrm{class}}(y,t) := \mathbf 1_{(-\infty,0]}(y\cdot\operatorname{sgn} t)$ .

Let $H$ be a reproducing kernel Hilbert space (RKHS) of a kernel $k$ over $X$ , i.e. a Hilbert space of functions $X \to \mathbb R$ in which point evaluation is represented by an inner product against a feature map $x \mapsto k_x \in H$ with $k(x,x') = \langle k_x,k_{x'}\rangle_H$ . Write $\|k\|_\infty := \sup_x \sqrt{k(x,x)}$ for the kernel's sup-bound. For a sample $D := ((x_1,y_1),\dots,(x_n,y_n)) \in (X\times Y)^n$ , the empirical risk is $R_{L,D}(f) := \tfrac1n \sum_i L(x_i,y_i,f(x_i))$ , and the SVM decision function $f_{D,\lambda}$ is the minimizer over $H$ of $g \mapsto \lambda\|g\|_H^2 + R_{L,D}(g)$ — the regularized empirical risk minimizer a practical SVM solver computes. The restricted Bayes risk on $H$ is $R^*_{L,P,H} := \inf_{f\in H} R_{L,P}(f)$ , and the approximation error function is $A_2(\lambda) := \inf_{f\in H} \lambda\|f\|_H^2 + R_{L,P}(f) - R^*_{L,P,H}$ : the price, in excess risk, of restricting attention to $H$ at regularization strength $\lambda$ .

Formalization targets

Goal: Theorem 8.1 — oracle inequality for classifying with SVMs

R_{L_{\mathrm{class}},P}(f_{D,\lambda}) - R^*_{L_{\mathrm{class}},P} < A_2(\lambda) + \lambda^{-1}\left(\sqrt{\tfrac{8\tau}{n}} + \sqrt{\tfrac{4}{n} + \tfrac{8\tau}{3n}}\right)

with $P^n$ -probability at least $1-e^{-\tau}$ , for the hinge loss, $H$ a separable RKHS with $\|k\|_\infty \le 1$ , and $P$ such that $H$ is dense in $L^1(P_X)$ . The bound is finite-sample (valid for every fixed $n$ , not just asymptotically) and fully explicit: no unspecified constants beyond $A_2(\lambda)$ itself, which is a genuine, computable-in-principle quantity depending on $H$ , $P$ and $\lambda$ , not a placeholder. Making the right-hand side small — e.g. letting $\lambda \to 0$ slowly as $n\to\infty$ — is exactly what proves an SVM classifier consistent for the classification risk, even though it never optimizes that risk directly.

Three milestones, each the specific instance of an earlier chapter's result that this proof invokes (attack order):

Theorem 6.24 instance (hinge loss): $\lambda\|f_{D,\lambda}\|_H^2 + R_{L,P}(f_{D,\lambda}) - R^*_{L,P,H} < A_2(\lambda) + \lambda^{-1}(\sqrt{8\tau/n}+\sqrt{4/n+8\tau/(3n)})$ with $P^n$ -probability at least $1-e^{-\tau}$ — the general oracle inequality for regularized SVMs (Chapter 6, not itself a mission of this series), specialized to the hinge loss, whose global Lipschitz constant $1$ collapses the general theorem's Lipschitz-constant factor away.
Theorem 5.31 instance: $R^*_{L_{\mathrm{hinge}},P,H} = R^*_{L_{\mathrm{hinge}},P}$ — the RKHS's restricted Bayes hinge risk equals the unrestricted one, using $H$ 's density in $L^1(P_X)$ and the fact (Lemma 2.25 v)) that the hinge loss is automatically a $P$ -integrable Nemitski loss.
Theorem 2.31 instance (Zhang's inequality, second clause): $R_{L_{\mathrm{class}},P}(f) - R^*_{L_{\mathrm{class}},P} \le R_{L_{\mathrm{hinge}},P}(f) - R^*_{L_{\mathrm{hinge}},P}$ for every measurable $f$ with finite hinge and classification risk — this series' own 01-loss-functions mission's zhang_inequality, second assertion, restated locally.

Chaining these three (with milestone 2 used to rewrite milestone 1's $R^*_{L,P,H}$ as $R^*_{L,P}$ , then milestone 3 applied to $f=f_{D,\lambda}$ ) is exactly the book's four-line proof of Theorem 8.1.

Significance

Theorem 8.1 is this series' capstone: every other chapter's result (loss calibration, RKHS theory, representer theorem, Hilbert-space concentration, the general SVM oracle inequality) is a prerequisite this theorem consumes, and nothing later in the book depends on formalizing it further to be meaningful in its own right — it is already a complete, citable, explicit consistency-and-rate statement for SVM classification. It is also the first result in this series whose statement combines three distinct chapters' machinery into a single inequality, making the "restate the specific instance, not the general machinery" discipline (Hard Rule 9) most visibly load-bearing here: none of Theorem 6.24, Theorem 5.31 or Theorem 2.31 in their full generality is needed, only the narrow slice each contributes to this one proof.

No machine-checked formalization of an SVM classification oracle inequality of this kind is known to exist in a public Lean/Mathlib development (see prior-art search below): statistical learning theory results of this shape (finite-sample high-probability bounds combining regularization, approximation error and concentration) are largely unformalized outside isolated concentration inequalities.

Difficulty

The difficulty here is compositional rather than computational: each of the three milestones is, in its own chapter, a short consequence of substantial earlier machinery (Theorem 6.24 rests on a stability argument plus Hilbert-space Hoeffding; Theorem 5.31 rests on continuity of the risk functional on $L^p$ ; Theorem 2.31 rests on a pointwise case analysis), but none of that earlier machinery is re-derived here — only the specific numerical instance each milestone hands to Theorem 8.1's proof. Getting the three instances to compose correctly (in particular, making sure milestone 1's restrictedBayesRisk and milestone 2's equality target the identical quantity, so the substitution the book's proof performs is literally available) is the main formalization risk, not any single proof step.

The probabilistic statement itself is genuinely over the product measure $P^n$ on samples of size $n$ , not an expectation or almost-sure claim, and the bounded-kernel hypothesis $\|k\|_\infty\le1$ is load-bearing (it is what fixes the " $8$ " and " $4$ " constants exactly, not just up to a normalization).

Formalization scope

$X$ is an arbitrary measurable space; $H$ is a general real Hilbert space (NormedAddCommGroup H, InnerProductSpace ℝ H, CompleteSpace H), not specialized to a concrete function space, matching the book's own generality. IsRKHSOfKernel, risk/bayesRisk, classLoss/hingeLoss and empiricalRisk are restated locally in this mission's own Classification sub-namespace — per Hard Rule 9, a draft mission cannot import another draft's definitions, so these duplicate (with identical mathematical content) definitions already drafted in 01-loss-functions and 04-representer. IsSVMSolution encodes " $f_{D,\lambda}$ minimizes the regularized empirical risk over $H$ " directly as a hypothesis rather than re-deriving existence and uniqueness (04-representer's territory). DenseInL1 renders " $H$ dense in $L^1(P_X)$ " as an $\varepsilon$ -approximation property in the $L^1$ seminorm rather than via the Lp subtype, to keep the statement self-contained without importing Chapter 5's own Lp-space apparatus. $\|k\|_\infty \le 1$ is ∀ x, k x x ≤ 1 (since $\|k\|_\infty := \sup_x\sqrt{k(x,x)}$ , Eq. (4.15)). "With $P^n$ -probability at least $1-e^{-\tau}$ " is stated as a lower bound on (Measure.pi (fun _ : Fin n => P)).real {D | ...}, the $n$ -fold product measure of the event.

Theorem 8.2 (Classification with benign kernels), the polynomially-decaying-entropy-number specialization of Theorem 8.1 stated immediately after it in the book, is deliberately out of scope for this mission: it requires entropy-number and covering-number machinery (dyadic entropy numbers $e_i(\mathrm{id}: H\to C(X))$ , Lemma 6.21's covering-number bound) that none of this mission's three milestones need, and formalizing it faithfully would roughly double the mission's scope for a result that is a refinement, not a prerequisite, of Theorem 8.1. A trivializing formalization of the goal would state the conclusion for an unconstrained fSVM : (Fin n → X × ℝ) → H with no connection to L, D or λ (making the bound a tautology about whatever function is supplied, independent of what an SVM actually computes); this is ruled out here by requiring hfSVM : ∀ D, IsSVMSolution H toFun hingeLoss lam n D (fSVM D), which pins fSVM D to be an actual minimizer of the regularized empirical hinge risk for that specific sample D.

Selected references

I. Steinwart & A. Christmann, Support Vector Machines, Springer, Information Science and Statistics, 2008. https://doi.org/10.1007/978-0-387-77242-4 (Chapter 8, §8.1, pp. 287-291; Chapter 6, §6.4, pp. 223-225; Chapter 5, §5.4-5.5, pp. 179, 190-191; Chapter 2, §2.3, p. 37).
T. Zhang, "Statistical behavior and consistency of classification methods based on convex risk minimization," Annals of Statistics 32(1), 2004, pp. 56-85. https://doi.org/10.1214/aos/1079120130
This series' 01-loss-functions mission (Theorem 2.31, full statement and proof) and 04-representer mission (Chapter 5's RKHS and SVM-solution machinery, in full generality).

7 thms3 active usersReviewed

Completed

Machine Learning Probability Theoretical Computer Science·Captain: mikedeng1

Foundations of Machine Learning VI: AdaBoost and Margin TheoryTextbook

Motivation

Weak learning — a base classifier only slightly better than random guessing — is easy to come by; strong learning, in the PAC sense of Chapter 2, is not. Boosting is the technique that turns the first into the second: combine many weak classifiers, each trained on a reweighted version of the sample that emphasizes previously misclassified points, into a single strong ensemble. AdaBoost, the algorithm this chapter studies, does this with a specific, closed-form weighting rule, and comes with two distinct theoretical guarantees: its training error decreases exponentially fast in the number of rounds (Theorem 7.2), and — more surprisingly — its test error can keep improving even after the training error has already reached zero, an empirical phenomenon that Chapter 3's VC-dimension bound cannot explain at all (it predicts overfitting for large numbers of rounds) but that a margin-based analysis, structurally identical to Chapter 5's SVM theory, does (Theorem 7.7). This mission formalizes both routes.

Setting

AdaBoost (Figure 7.1) takes a labeled sample $S=((x_1,y_1),\dots,(x_m,y_m))$ with $y_i\in\{-1,+1\}$ and a base classifier set $H\subseteq\{-1,+1\}^X$ , and runs for $T$ rounds. It maintains a distribution $D_t$ over the sample indices, starting uniform ( $D_1(i)=1/m$ ); at round $t$ it selects a base classifier $h_t$ with small $D_t$ -weighted error $\varepsilon_t=\Pr_{i\sim D_t}[h_t(x_i)\ne y_i]$ , sets $\alpha_t=\frac12\log\frac{1-\varepsilon_t} {\varepsilon_t}$ and $Z_t=2\sqrt{\varepsilon_t(1-\varepsilon_t)}$ , and reweights: $D_{t+1}(i)=D_t(i)\exp(-\alpha_ty_ih_t(x_i))/Z_t$ . After $T$ rounds it returns $f=\sum_{t=1}^T\alpha_th_t$ ; its normalized version is $\bar f=f/\sum_t\alpha_t$ . Since $\varepsilon_t<1/2$ makes $\alpha_t>0$ , $\bar f$ is a genuine convex combination of base classifiers, i.e. a member of the convex hull $\mathrm{conv}(H)=\{\sum_k\mu_kh_k:\mu_k\ge0, h_k\in H,\sum_k\mu_k\le1\}$ (Eq. 7.12). The chapter reuses Chapter 5's confidence-margin apparatus (empirical margin loss $\hat R_{S,\rho}$ , Rademacher complexity $\hat R_S$ / $R_m$ ) to analyze $\bar f$ 's generalization.

Formalization targets

Theorem 7.2 (AdaBoost empirical error bound, milestone). The empirical (zero-one) error of $f$ satisfies $\hat R_S(f) \le \exp(-2\sum_{t=1}^T(1/2-\varepsilon_t)^2)$ , and, if $\gamma\le1/2-\varepsilon_t$ for all $t$ , $\hat R_S(f)\le\exp(-2\gamma^2T)$ : training error decays exponentially in $T$ whenever every round beats random guessing by a fixed margin (the "edge" $\gamma$ ).

Lemma 7.4 (milestone). $\hat R_S(\mathrm{conv}(H))=\hat R_S(H)$ : the convex hull of a hypothesis set, though generally much larger, has exactly the same empirical Rademacher complexity as the set itself.

Corollary 7.5 (Ensemble Rademacher margin bound, milestone). For $H$ a set of real-valued functions and $\rho>0$ , with probability at least $1-\delta$ , every $h\in\mathrm{conv}(H)$ satisfies $R(h)\le\hat R_{S,\rho}(h)+\frac2\rho R_m(H)+\sqrt{\log(1/\delta)/(2m)}$ (and the empirical-complexity analogue with an extra additive $3\sqrt{\log(2/\delta)/(2m)}$ term) — this is Theorem 5.8's margin bound applied to $\mathrm{conv}(H)$ , then rewritten via Lemma 7.4 so its complexity term is $H$ 's own, not the (much larger) convex hull's.

Theorem 7.7 — the mission's goal. Assume $\varepsilon_t<1/2$ for every $t\in[T]$ (so $\alpha_t>0$ ). Then for any $\rho>0$ ,

\hat R_{S,\rho}(\bar f) \le 2^T\prod_{t=1}^T\sqrt{\varepsilon_t^{1-\rho}(1-\varepsilon_t)^{1+\rho}}.

Significance

Theorem 7.7's bound is what makes margin theory a genuine explanation of AdaBoost's empirical behavior: combined with Corollary 7.5 (applied to $\bar f\in\mathrm{conv}(H)$ ), it shows that if AdaBoost's edge stays bounded away from zero, the empirical margin loss at a fixed $\rho$ decreases exponentially in $T$ while the generalization bound's complexity term does not depend on $T$ at all — so continuing to boost past zero training error can still shrink the true risk, by growing the margin on the training points that are already correctly classified. This resolves the puzzle that opens §7.3.1: AdaBoost's test error is empirically observed to keep decreasing well after its training error hits zero, which the chapter's own earlier VC-dimension bound on $\mathcal F_T$ (Eq. 7.9, growing as $O(dT\log T)$ ) predicts should eventually overfit, not improve. No prior art on the Prove2Me platform is faithful: GET /theorems?q=boosting and q=AdaBoost return no hits; this chunk's Rademacher-complexity apparatus is restated locally (a draft item cannot import chunk 05-svm's or 03-rademacher-vc's own draft copies) rather than reused, matching the precedent those chunks' own STATUS.md records recommend for every later chunk needing the same machinery.

Not formalized here: Theorem 7.6 (the VC-dimension-based ensemble margin bound, a direct corollary of Corollary 7.5 via chunk 03's VC-dimension apparatus) — restating 03's own machinery a second time for a single further corollary is disproportionate within this mission's budget, and the chapter's actual capstone targets the sharper, dimension-free Rademacher-complexity route (Theorem 7.7) instead. Also out of scope: §7.2.2's coordinate- descent equivalence, §7.2.3's practical (decision-stump) use, and §7.3.4-7.3.5's margin- maximization LP and game-theoretic interpretation — discussion sections with no numbered result feeding the goal's proof.

Difficulty

Theorem 7.2's proof needs the telescoping identity $D_{T+1}(i) = e^{-y_if(x_i)}/(m\prod_tZ_t)$ (Eq. 7.2), obtained by repeatedly unfolding the recursive weight update — a genuine induction on $t$ , not a one-line algebraic manipulation — before the elementary inequality $1_{u\le0}\le e^{-u}$ turns the empirical error into a telescoping product of the $Z_t$ 's, each of which is then re-expressed in closed form via a case split on $y_ih_t(x_i)=\pm1$ . Theorem 7.7's proof reuses the same identity but with an added margin-shift term $\rho\|\alpha\|_1$ inside the exponential, requiring the same telescoping machinery plus a separate accounting of $e^{\rho\sum_t\alpha_t}$ against the product of $[\sqrt{(1-\varepsilon_t)/\varepsilon_t}]^\rho$ factors coming from each $\alpha_t$ 's own closed form — a proof that shares its main structural step with Theorem 7.2 but is not a trivial corollary of it. Corollary 7.5's proof is Lemma 7.4 (itself a careful supremum-exchange argument using the dual-norm characterization of $\ell^1$ , not a routine calculation) composed with Theorem 5.8, applied to the specific set $\mathrm{conv}(H)$ rather than a generic hypothesis class — a formalization that stated the corollary only for a "sufficiently nice" abstract class, without deriving it from Lemma 7.4's convex-hull identity, would be proving a different, weaker-provenance statement.

Formalization scope

WeightedError, AdaBoostAlpha, AdaBoostNormalizer, AdaBoostDist, AdaBoostEpsilon, AdaBoostEnsemble, AdaBoostNormalizedEnsemble, EmpiricalError and ConvHull are new, capturing AdaBoost as an actual algorithm (a genuine recursion on the round index, closed under Definitions.Def_FoundationsML_Boosting_AdaBoostDist's own recursive equation) rather than an unspecified "boosting procedure" — the trivialization trap BRIEF.md names for this chapter. AdaBoostDist takes the sequence of base classifiers actually selected at each round, h : ℕ → X → ℝ, as external data rather than deriving it via an argmin over H; this is checked in SELF_REVIEW.md to drop no content either milestone or the goal theorem's statement actually needs, since neither invokes h_t's optimality, only the weighted error ε_t it produces under AdaBoost's own distribution D_t. PhiRho, EmpiricalMarginLoss, MarginGeneralizationError, EmpiricalRademacherComplexity and RademacherComplexity are restated locally, byte-identical to chunk 05-svm's own copies of Definitions 5.5, 5.6, 2.1 (specialized), 3.1, 3.2 (a draft item cannot import another chunk's draft module); this duplication collapses once 05-svm and 03-rademacher-vc are uploaded and listed in missions/README.md's "Published definitions" table. No numerical constant in any of the four theorems is altered from the book's own displayed form. A trivializing formalization this mission avoids: stating Theorem 7.2/7.7 for an arbitrary sequence of error rates $\varepsilon_1,\dots,\varepsilon_T$ satisfying $\varepsilon_t<1/2$ , disconnected from any actual algorithm — AdaBoostEpsilon instead ties every ε_t to the weighted error AdaBoost's own recursively defined D_t assigns to its own selected h_t, so the bound is provably about this algorithm's error trajectory, not an arbitrary one.

Selected references

M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 7.
Y. Freund, R. E. Schapire, "A decision-theoretic generalization of on-line learning and an application to boosting," Journal of Computer and System Sciences 55(1), 1997, 119-139.
R. E. Schapire, Y. Freund, P. Bartlett, W. S. Lee, "Boosting the margin: a new explanation for the effectiveness of voting methods," The Annals of Statistics 26(5), 1998, 1651-1686.

18 thms3 active usersReviewed

Missions

The Dantzig Selector: Statistical Estimation When p Is Much Larger than n 1: ℓ2 Error Bound for Sparse Parameters under the Uniform Uncertainty PrincipleResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities III: Uniform Convergence and the Entropy per ObservationResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4 (p. 275)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities II: The Uniform Deviation BoundResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 269)

Milestones, in the order of the proof

Further items (consequences, not milestones)

Significance

Difficulty

Formalization scope

Selected references

Learnability, Stability and Uniform Convergence I: A Problem Is Learnable if and only if It Admits a Uniform-RO Stable Universal AERMResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 7

Milestones

Significance

Difficulty

Formalization scope

Selected references

Adversarially Robust Generalization Requires More Data 4: Robust Learning from One Thresholded Sample in the Bernoulli ModelResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 10 (p. 8)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Are Call Center and Hospital Arrivals Well Modeled by Nonhomogeneous Poisson Processes?: Combining k Equal Subintervals of a Linear Arrival Rate Bounds the Degree of Nonhomogeneity by C/kResearch Paper

Motivation

Setting

Formalization targets

Goal: THEOREM 5, combining equally spaced subintervals

Milestones

Significance

Difficulty

Formalization scope

Selected references

Calibrated Learning and Correlated Equilibrium III: A Randomized Forecast Calibrated against Every OpponentResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 49)

Milestones, in the order the Appendix uses them

Significance

Difficulty

Formalization scope

Selected references

Simultaneous Analysis of Lasso and Dantzig Selector III: A Sparsity Oracle Inequality for the LassoResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.1

Milestones

Significance