Machine Learning

Why variance-regularized risk bounds

In statistical learning, one picks a function $f$ from a class $\mathcal F$ to make the population risk $\mathbb E[f]$ small, with access only to an i.i.d. sample $x_1,\dots,x_n$ from an unknown distribution $P$. Empirical risk minimization replaces $\mathbb E[f]$ by the empirical mean $\mathbb E_{\widehat P_n}[f]$, and its classical guarantees decay like $1/\sqrt n$ regardless of how concentrated $f$ is. Bernstein-type inequalities show that the deviation of $\mathbb E_{\widehat P_n}[f]$ from $\mathbb E[f]$ scales with the standard deviation of $f$, so a procedure that minimizes "empirical risk plus a standard-deviation penalty" can, in principle, achieve faster rates when the variance at the optimum is small (Maurer and Pontil, 2009). The penalized objective is non-convex even when every $f$ is convex in its parameters, which makes it hard to optimize.

J. C. Duchi and H. Namkoong (arXiv:1610.02581v3, 2017) replace the penalty by a distributionally robust objective: the worst-case risk over all reweightings of the sample within a $\chi^2$-divergence ball. This objective is convex whenever the losses are, and (Theorem 1 of the paper) it equals the empirical mean plus a standard-deviation penalty up to an error of order $1/n$. This mission formalizes the paper's guarantee for the minimizer of that robust objective in terms of localized Rademacher complexities (Section 3.2, Theorem 4), the sharpest of the paper's three generalization analyses. It is the third of four missions on the paper.

Setting

Let $P$ be a probability measure on a measurable space $\mathcal X$ and $x_1,\dots,x_n$, $n\ge1$, an i.i.d. sample from $P$ with empirical distribution $\widehat P_n$. Let $M\ge1$ and let $\mathcal F$ be a collection of measurable functions $f:\mathcal X\to[0,M]$ (losses).

• The $\chi^2$ ball of radius $\rho\ge0$ is the set $\mathcal P_n$ of weight vectors $p\in\mathbb R^n$ with $p_i\ge0$, $\sum_ip_i=1$ and $\frac12\sum_i(np_i-1)^2\le\rho$; equivalently, the distributions $P$ on the sample with $D_\phi(P\|\widehat P_n)\le\rho/n$ for $\phi(t)=\frac12(t-1)^2$.
• The robust risk of $f$ is $\sup_{P:\,D_\phi(P\|\widehat P_n)\le\rho/n}\mathbb E_P[f]=\sup_{p\in\mathcal P_n}\sum_ip_if(x_i)$, and a robust minimizer $\widehat f$ minimizes it over $\mathcal F$.
• The empirical Rademacher complexity is $\mathfrak R_n(\mathcal F)=\mathbb E_\varepsilon\big[\sup_{f\in\mathcal F}\frac1n\sum_i\varepsilon_if(x_i)\big]$ with i.i.d. uniform signs $\varepsilon_i\in\{-1,1\}$, and $\mathbb E[\mathfrak R_n(\mathcal F)]$ averages it over the sample.
• A function $\psi:\mathbb R_+\to\mathbb R_+$ is sub-root if it is nonnegative, nondecreasing, and $r\mapsto\psi(r)/\sqrt r$ is nonincreasing on $r>0$.
• The localization inequality (20) asks that, for all $r\ge0$,

$$\psi_n(r)\ \ge\ \mathbb E\big[\mathfrak R_n(\{cf : f\in\mathcal F,\ c\in[0,1],\ \mathbb E[c^2f^2]\le r\})\big],$$

with $\psi_n$ sub-root, and $r_n^\star>0$ is a point with $r_n^\star\ge\psi_n(r_n^\star)$.

Formalization targets

Goal: Theorem 4, inequality (23), as its proof establishes it

Let $0<t<n$ and let $\rho$ satisfy (21): $\frac\rho n\ge8\big(\frac{45M}n\big(t+\log\lceil\log\frac nt\rceil\big)+18r_n^\star\big)$. With probability at least $1-4e^{-t}$, every robust minimizer $\widehat f$ satisfies

$$\mathbb E[\widehat f]\ \le\ \Big(1+2\sqrt{\tfrac{2\rho}n}\Big)\inf_{f\in\mathcal F}\Big(\mathbb E[f]+\sqrt{\tfrac{182\rho}{45n}\mathrm{Var}(f)}\Big)+\Big(14+6\sqrt{\tfrac{2\rho}n}\Big)\frac{M(3\rho+t)}n .$$

Milestones

In attack order: Bousquet's form of Talagrand's inequality (Lemma B.2); the elementary root bound (Lemma D.4); the contraction principle (Lemma D.5, a published theorem); the uniform Bernstein inequality with Rademacher complexity (Lemma D.1); its localized version in terms of $r_n^\star$ (Lemma D.2); localized second-moment bounds (Lemma D.3); the deterministic expansion (10) of Theorem 1,

$$\Big(\sqrt{\tfrac{2\rho}n s_n^2}-\tfrac{2M\rho}n\Big)_+\le\sup_{P}\mathbb E_P[Z]-\mathbb E_{\widehat P_n}[Z]\le\sqrt{\tfrac{2\rho}ns_n^2};$$

and the uniform bound (22): with probability at least $1-2e^{-t}$, for all $f\in\mathcal F$,

$$\mathbb E[f]\le\Big(1+2\sqrt{\tfrac{2\rho}n}\Big)\sup_{P:\,D_\phi(P\|\widehat P_n)\le\rho/n}\mathbb E_P[f]+\Big(13+4\sqrt{\tfrac{2\rho}n}\Big)\frac{M\rho}n .$$

Significance

The bound (23) says that the robust minimizer competes with the best trade-off between risk and standard deviation in the class, and that the complexity of the class enters only through the fixed point $r_n^\star$ of a localized complexity bound. For bounded VC classes $r_n^\star$ is of order $\frac{d\log(n/d)}n$ (Bartlett, Bousquet and Mendelson, 2005, Corollary 3.7), so when the optimal function has small variance the excess risk is of order $\rho/n$, faster than the $1/\sqrt n$ of uniform covering arguments; and localized complexities apply to classes, such as balls of reproducing kernel Hilbert spaces, whose covering numbers are too large for the covering-number analysis of the paper's Theorem 3 (mission II of this series).

The paper's result is proved, not open. No part of it, and none of the localized-complexity machinery of Bartlett, Bousquet and Mendelson, is formalized in Lean or Mathlib to our knowledge. The mission produces a checked version of the theorem with every constant explicit and, along the way, the localization lemmas D.1–D.3, which are reusable for any localized-complexity analysis. Reading the proof also exposed three arithmetic slips in the printed statements; the mission states what the proof establishes (see Formalization scope).

Difficulty

The obvious route applies a uniform concentration inequality to $\mathcal F$ and then a Bernstein bound to each $f$. Talagrand's inequality applied to the whole class gives a deviation governed by the largest variance in the class and by the global complexity $\mathbb E[\mathfrak R_n(\mathcal F)]$, which yields only $1/\sqrt n$ rates. Obtaining a deviation that scales with each function's own second moment requires peeling the class into shells of comparable second moment and a fixed-point argument on the sub-root bound, with a union bound whose cost appears as $\log\lceil\log\frac nt\rceil$. The two directions of the localized inequalities (population to sample, and sample to population for second moments) must then be combined with the deterministic expansion (10) while keeping the constants explicit. A further subtlety is the self-normalized rescaling $f\mapsto\sqrt{r/(\mathbb E[f^2]\vee r)}\,f$, which differs from the variance normalization of Bartlett et al. and is what makes the bound compatible with the robust objective.

Formalization scope

Lean conventions. The sample is the coordinate map of the product measure $P^n$ on Fin n → X. Distributions on the sample are weight vectors in the $\chi^2$ ball; the robust risk is the real supremum over that ball (attained, since the ball is nonempty and compact for $n\ge1$, $\rho\ge0$). Population means and variances are ∫ x, f x ∂P and ProbabilityTheory.variance f P for measurable bounded $f$; empirical means and variances are normalized by $1/n$. The empirical Rademacher complexity is the published UnderstandingML_Rademacher definition evaluated on $\{(f(x_1),\dots,f(x_n))\}$. Its expectation is a Bochner integral, and every hypothesis that bounds it also asserts that the integrand is integrable: otherwise the integral is $0$, (20) would hold for free, and the theorem would be false. Probability bounds are stated for the failure event under $P^n$ (an outer measure when the event is not measurable). The goal speaks about every minimizer of the robust risk, so it is not vacuous when the set of minimizers is empty. The condition $r_n^\star>0$ is part of the page's "root" (and the proof divides by $\sqrt{r_n^\star}$); with $r_n^\star=0$ allowed, $\psi(r)=\sqrt r$ would remove the complexity term from (21). The condition $t<n$ makes $\log\lceil\log\frac nt\rceil$ defined.

Corrections of printed statements, each recorded in the item's docstring and Formalization Note (the milestone texts stay verbatim):

• (22) is stated with probability $1-2e^{-t}$; the paper prints $1-e^{-t}$, and its proof (p. 41) concludes $1-2e^{-t}$.
• (23) is stated with probability $1-4e^{-t}$ (printed $1-3e^{-t}$; the proof adds two fixed-$f$ events to the two of (22)) and with $\frac{182\rho}{45n}$ (printed $\frac{91\rho}{45n}$; the proof's step $\sqrt\rho+\sqrt t\le\sqrt{91\rho/45}$ multiplies $\sqrt{2\mathrm{Var}(f)/n}$).
• Lemma D.3 is stated with the additive term $72M^2(1+\eta)r_n^\star+(4(1+\eta)+\frac{14}3)\frac{M^2t}n$ and, in the reversed direction, the coefficient $1+\frac1{1+\eta}$, as its proof yields (printed: $\frac{Mt}n(4+\frac73M)$ and $1+\frac\eta{1+\eta}$), under Theorem 4's standing hypothesis $M\ge1$.
• Lemma D.5 is linked to the published contraction lemma UnderstandingML.contraction_lemma, which states it at a fixed sample for nonempty bounded classes and allows a different Lipschitz map per coordinate.

Contributions welcome: proofs of the milestones in any order; Lemma B.2 (Bousquet's inequality) is the deepest single ingredient and is reusable well beyond this mission, as are the peeling Lemma D.1 and the sub-root fixed-point Lemma D.2.

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017. https://arxiv.org/abs/1610.02581
• P. L. Bartlett, O. Bousquet and S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. https://doi.org/10.1214/009053605000000282
• O. Bousquet, A Bennett concentration inequality and its application to suprema of empirical processes, Comptes Rendus Mathématique 334(6), 2002. https://doi.org/10.1016/S1631-073X(02)02292-6
• A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT 2009. https://arxiv.org/abs/0907.3740
• M. Ledoux and M. Talagrand, Probability in Banach Spaces, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4

Motivation

In many operational problems (shortest paths, assignment, planning) the decision solves a linear program whose cost vector is unknown at decision time and is predicted from contextual features. The predict-then-optimize pipeline fits a model $f$ that maps a feature vector $x$ to a predicted cost vector $\hat c=f(x)$, and then acts on the decision that is optimal for $\hat c$. Elmachtoub and Grigas (Smart "Predict, then Optimize", Management Science 2022) proposed to measure the quality of such a model not by the prediction error but by the SPO loss (Smart Predict-then-Optimize loss): the excess true cost of the decision induced by the prediction over the best decision in hindsight.

The question is whether a small SPO loss on the training sample implies a small SPO loss on new data, uniformly over the models a training procedure may return. The SPO loss is neither convex nor continuous in the prediction, so the standard Lipschitz-based bounds for regression do not apply. El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3, Mathematics of Operations Research 2023; a preliminary version appeared at NeurIPS 2019) give the first such generalization bounds. This mission formalizes their first one, for polyhedral feasible regions, which treats every vertex of the feasible region as a class label of a multiclass classification problem. The bound has since been used by later work, e.g. Hu, Kallus and Mao (Fast rates for contextual linear optimization, Management Science 2022), who sharpen it by a $\sqrt{\log n}$ factor (as noted on p. 4 of the paper).

Setting

A feasible region $S\subseteq\mathbb R^d$ is nonempty, compact and convex. For a cost vector $c\in\mathbb R^d$ the nominal problem is $\min_{w\in S}c^\top w$. An optimization oracle is a fixed map $w^*:\mathbb R^d\to S$ with $w^*(c)\in\arg\min_{w\in S}c^\top w$ for every $c$; nothing is assumed about how it breaks ties. The SPO loss of a prediction $\hat c$ when the realized cost is $c$ is

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

The linear optimization gap is $\omega_S(c)=\max_{w\in S}c^\top w-\min_{w\in S}c^\top w$, and for a set $\mathcal C$ of cost vectors $\omega_S(\mathcal C)=\sup_{c\in\mathcal C}\omega_S(c)$; the SPO loss of a cost in $\mathcal C$ lies in $[0,\omega_S(\mathcal C)]$.

Data are pairs $(x,c)$ drawn from a distribution $\mathcal D$ on $\mathcal X\times\mathcal C$. A hypothesis class $\mathcal H$ is a family of predictors $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 on an i.i.d. sample $(x_1,c_1),\dots,(x_n,c_n)$ the empirical SPO risk is $\hat R_{\rm SPO}(f)=\frac1n\sum_i\ell_{\rm SPO}(f(x_i),c_i)$. The empirical Rademacher complexity with respect to the SPO loss is

$$\hat{\mathfrak R}^n_{\rm SPO}(\mathcal H)=\mathbb E_\sigma\Big[\sup_{f\in\mathcal H}\frac1n\sum_{i=1}^n\sigma_i\,\ell_{\rm SPO}(f(x_i),c_i)\Big]$$

with independent uniform signs $\sigma_i\in\{\pm1\}$, and $\mathfrak R^n_{\rm SPO}(\mathcal H)$ is its expectation over the sample.

The decisions induced by $\mathcal H$ form the class $w^*(\mathcal H)=\{x\mapsto w^*(f(x)):f\in\mathcal H\}$. A class $\mathcal F$ N-shatters a finite set $\mathbb X\subseteq\mathcal X$ if there are two labelings $g_1,g_2$ that differ at every point of $\mathbb X$ such that every mixture of them (follow $g_1$ on a subset $T$, $g_2$ on the rest) is realized by some member of $\mathcal F$. The Natarajan dimension $d_N(\mathcal F)$ is the largest size of an N-shattered set. When $S$ is a polyhedron, $\mathfrak S$ denotes its finite set of extreme points.

Formalization targets

Goal: Theorem 2, second display (p. 11)

For a polyhedral $S$ and every $\delta>0$, with probability at least $1-\delta$ over an i.i.d. sample of size $n$, every $f\in\mathcal H$ satisfies

$$R_{\rm SPO}(f)\le\hat R_{\rm SPO}(f)+2\,\omega_S(\mathcal C)\sqrt{\frac{2d_N(w^*(\mathcal H))\log(n|\mathfrak S|^2)}{n}}+\omega_S(\mathcal C)\sqrt{\frac{\log(1/\delta)}{2n}} .$$

Milestones, in attack order

1. Theorem 1 (p. 9): with probability $1-\delta$, $R_{\rm SPO}(f)\le\hat R_{\rm SPO}(f)+2\mathfrak R^n_{\rm SPO}(\mathcal H)+\omega_S(\mathcal C)\sqrt{\log(1/\delta)/(2n)}$ for all $f\in\mathcal H$.
2. Massart step (Appendix B.1, p. 31): for a fixed sample with costs in $\mathcal C$, $\hat{\mathfrak R}^n_{\rm SPO}(\mathcal H)\le\omega_S(\mathcal C)\sqrt{2\log|\mathfrak F_{|\mathbb X}|/n}$, where $\mathfrak F_{|\mathbb X}$ is the set of decision vectors $(w^*(f(x_1)),\dots,w^*(f(x_n)))$.
3. Natarajan lemma (cited on p. 31; proved on the platform as UnderstandingML.natarajan_lemma): a class from an $m$-point set to $k$ labels with Natarajan dimension $d$ has at most $m^d k^{2d}$ members.
4. Empirical bound (Appendix B.1, p. 31): for a fixed sample, $\hat{\mathfrak R}^n_{\rm SPO}(\mathcal H)\le\omega_S(\mathcal C)\sqrt{2d_N(w^*(\mathcal H))\log(n|\mathfrak S|^2)/n}$.
5. Theorem 2, first display (p. 11): the same bound for the expected complexity $\mathfrak R^n_{\rm SPO}(\mathcal H)$.

Significance

The bound controls the out-of-sample decision cost of every predictor in the class, not only of an empirical risk minimizer, so it applies to any training procedure (SPO+ surrogate minimization, decision trees, heuristics) that returns a member of $\mathcal H$. Its dependence on the feasible region is only through $\omega_S(\mathcal C)$ and $\log|\mathfrak S|$: the number of vertices of a combinatorial polytope is typically exponential in $d$, and enters only logarithmically. For linear predictors $x\mapsto Bx$ the paper's Corollary 2 bounds $d_N(w^*(\mathcal H_{\rm lin}))$ by $dp$, giving a rate of order $\sqrt{dp\log(n|\mathfrak S|)/n}$.

The results are proved in the paper; this mission formalizes them. No statement about predict-then-optimize or the SPO loss is known to have a machine-checked proof. The platform already has the Natarajan lemma (proved) and several Massart-type lemmas for generic classes; this mission connects that multiclass machinery to decision losses, and its Theorem 1 is a reusable Rademacher generalization bound for a loss with range $[0,\omega]$.

Difficulty

The obvious route through Lipschitz contraction fails: the SPO loss jumps when the prediction crosses a point where the optimum is not unique, so the Rademacher complexity of the composed class cannot be bounded by that of $\mathcal H$ times a Lipschitz constant. Any argument through the finitely many vertices of $S$ needs the decisions $w^*(f(x_i))$ to take finitely many values on a sample, i.e. the oracle to return vertices; for an oracle that returns a non-vertex optimal point under ties, $w^*(\mathcal H)$ may take infinitely many values on a sample. On the probabilistic side, the passage from the empirical to the expected complexity and the McDiarmid concentration step (Theorem 1) require the suprema over an uncountable class to be measurable, which the paper does not discuss.

Formalization scope

Lean works in $\mathbb R^d$ = EuclideanSpace ℝ (Fin d); cost vectors and decisions live in the same space and $c^\top w$ is the inner product. The standing assumptions of §2 are hypotheses of every theorem: $S$ nonempty, compact and convex; $w^*$ an arbitrary oracle (a hypothesis IsOracle S w, never a specific selection); $\mathcal C$ nonempty and bounded, with the cost component of $\mathcal D$ in $\mathcal C$ almost surely (or, for fixed-sample statements, every $c_i\in\mathcal C$); $n\ge1$. "Polyhedron" means the solution set of finitely many linear inequalities; with compactness it is a polytope, and $|\mathfrak S|$ is the cardinality of Set.extremePoints ℝ S. The expectation over signs is the exact average over the $2^n$ sign vectors; $R_{\rm SPO}$ and $\mathfrak R^n_{\rm SPO}$ are Bochner integrals. "With probability at least $1-\delta$" is stated as: the product measure of the set of samples on which some $f\in\mathcal H$ violates the bound is at most $\delta$.

The formalization commits to the following disclosed additions:

• In the empirical bound, Theorem 2 and its first display, the oracle returns extreme points of $S$. This is the proof's own "w.l.o.g." (p. 31), made explicit because p. 10 allows non-vertex outputs under ties. The hypothesis is needed: on the unit square, an oracle that returns distinct interior points of an edge under ties can have $d_N(w^*(\mathcal H))=1$ and empirical complexity near $\frac12$, which exceeds the printed bound for large $n$.
• The Natarajan dimension is not defined as a number (a supremum in $\mathbb N$ would silently be $0$ for unboundedly large shattered sets). Statements carry a natural number $k$ bounding the size of every N-shattered set, in place of $d_N(w^*(\mathcal H))$. This is equivalent when $d_N$ is finite; the printed bound is vacuous otherwise.
• Theorem 1 and the goal carry three measurability hypotheses: each loss function $z\mapsto\ell_{\rm SPO}(f(z_1),z_2)$ is measurable; the uniform deviation $\sup_f(R_{\rm SPO}(f)-\hat R_{\rm SPO}(f))$ and, for each sign vector, the signed supremum $\sup_f\frac1n\sum_i\sigma_i\ell_{\rm SPO}(f(x_i),c_i)$ are almost-everywhere measurable functions of the sample. Without them the integral defining $\mathfrak R^n_{\rm SPO}$ could default to $0$.
• The Massart step assumes $\mathfrak F_{|\mathbb X}$ finite, the case in which its printed right-hand side is finite.

A formalization that let $d_N$ be an sSup in $\mathbb N$, or chose a specific tie-breaking oracle inside the definitions, would prove a different and in part trivial statement; both are excluded.

Infrastructure needed: McDiarmid's bounded-differences inequality and symmetrization for the product measure; Massart's finite-class lemma (a proved version is on the platform as RademacherMassart.rad_le_massart, with its own normalization); the Natarajan lemma (proved, UnderstandingML.natarajan_lemma, stated with its own but identical notion of N-shattering over finite types); finiteness and nonemptiness of the extreme points of a nonempty polytope. Theorem 1 and the Massart step do not use polyhedrality and are reusable for any bounded decision loss. Contributions of these infrastructure lemmas are welcome.

Selected references

• O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, arXiv:1905.11488v3, 2022; Mathematics of Operations Research, 2023. https://arxiv.org/abs/1905.11488
• A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 9–26, 2022. https://arxiv.org/abs/1710.08005
• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian complexities: risk bounds and structural results, Journal of Machine Learning Research 3, 463–482, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
• B. K. Natarajan, On learning sets and functions, Machine Learning 4(1), 67–97, 1989. https://doi.org/10.1007/BF00114804
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014 (Lemma 29.4). https://doi.org/10.1017/CBO9781107298019
• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018 (Theorem 3.3, Corollary 3.8). https://cs.nyu.edu/~mohri/mlbook/

Motivation

Many regression problems have far more unknown coefficients $p$ than observations $n$: gene expression studies with tens of samples and thousands of genes, imaging from few measurements, nonparametric curve recovery from a finite number of noisy samples. Estimation is hopeless in general, but becomes possible when the parameter is sparse, that is, has few nonzero entries. Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) proposed the Dantzig selector, an estimator computed by a single linear program, and showed that its squared error is within a logarithmic factor of what an oracle that knew which coefficients matter could achieve.

The estimator became one of the two standard $\ell_1$ methods for high-dimensional regression, alongside the Lasso; the comparison of the two by Bickel, Ritov and Tsybakov (arXiv:0801.1095, 2009) is built on it. This mission targets the paper's main result, the oracle inequality (Theorem 1.2). A companion mission covers the simpler $\ell_2$ bound for sparse parameters (Theorem 1.1).

Setting

Observations follow 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)$ has independent $N(0,\sigma^2)$ coordinates, $\sigma>0$. The vector $\beta$ is $S$-sparse if at most $S$ of its entries are nonzero.

Two constants of $X$ measure how close sparse sets of columns are to being orthonormal. The restricted isometry constant $\delta_S$ is the smallest $\delta\ge0$ such that $(1-\delta)\|c\|_{\ell_2}^2\le\|Xc\|_{\ell_2}^2\le(1+\delta)\|c\|_{\ell_2}^2$ for every $c$ supported on at most $S$ indices. The restricted orthogonality constant $\theta_{S,S'}$ (defined for $S+S'\le p$) is the smallest $\theta\ge0$ with $|\langle Xc,Xc'\rangle|\le\theta\|c\|_{\ell_2}\|c'\|_{\ell_2}$ whenever $c,c'$ are supported on disjoint sets of sizes at most $S$ and $S'$. Below $\delta:=\delta_{2S}$ and $\theta:=\theta_{S,2S}$.

For a tuning level $\lambda_p>0$, a 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}=\sup_{1\le j\le p}|\langle y-X\tilde\beta,X_j\rangle|\le\lambda_p\sigma .$$

The ideal mean squared error is $\sum_{i=1}^p\min(\beta_i^2,\sigma^2)$: the risk of an oracle that keeps exactly the coordinates above the noise level.

Formalization targets

Goal: Theorem 1.2 (pp. 8–9)

Let $t>0$, $a\ge0$, and $\lambda_p:=(\sqrt{1+a}+t^{-1})\sqrt{2\log p}$. If $\beta$ is $S$-sparse and $\delta_{2S}+\theta_{S,2S}<1-t$, then with probability exceeding $1-(\sqrt{\pi\log p}\cdot p^a)^{-1}$ every Dantzig selector obeys

$$\|\hat\beta-\beta\|_{\ell_2}^2\le C_2^2\cdot\lambda_p^2\cdot\Big(\sigma^2+\sum_{i=1}^p\min(\beta_i^2,\sigma^2)\Big),$$

with the explicit constant (1.14)

$$C_2=\frac{2C_0}{1-\delta-\theta}+\frac{2\theta(1+\delta)}{(1-\delta-\theta)^2}+\frac{1+\delta}{1-\delta-\theta},\qquad C_0=2\sqrt2\Big(1+\frac{1-\delta^2}{1-\delta-\theta}\Big)+\Big(1+\frac1{\sqrt2}\Big)\frac{(1+\delta)^2}{1-\delta-\theta}.$$

Milestones

1. Lemma 3.2: $\|X\beta\|_{\ell_2}\le\sqrt{1+\delta}\,(\|\beta\|_{\ell_2}+(2S)^{-1/2}\|\beta\|_{\ell_1})$ for every $\beta$.
2. Lemma A.1 (dual sparse reconstruction, $\ell_2$ version): for $c$ supported on $|T|\le2S$, a vector $\beta$ on $T$ whose correlations $\langle X\beta,X_j\rangle$ equal $c_j$ on $T$ and are small off $T$ except on an exceptional set of size at most $S$, with bounds (6.1)–(6.6).
3. Corollary A.2 ($\ell_\infty$ version): the same without exceptional set, constants $1/(1-\delta-\theta)$.
4. Corollary A.3 (constrained thresholding): an $S$-sparse $\beta$ with $\|\beta\|_{\ell_2}<\lambda\sqrt S$ splits as $\beta'+\beta''$ with $\beta'$ small in $\ell_2$ and $\ell_1$ and $\|X^*X\beta''\|_{\ell_\infty}<\frac{1-\delta^2}{1-\delta-\theta}\lambda$.
5. Gaussian tail bound (Section 3, p. 15): $P(\sup_j|\langle z,X_j\rangle|>u)\le2p\,\varphi(u)/u$ for standard Gaussian noise.
6. Lemma 3.1: the $\ell_2$ mass of $h$ on $T_0$ and its top $S$ positions outside $T_0$ is controlled by $\|X^T_{T_{01}}Xh\|_{\ell_2}$ and $\|h\|_{\ell_1(T_0^c)}$.

Significance

The result. Theorem 1.2 says that a single linear program, which knows neither the support of $\beta$ nor which coefficients exceed the noise, matches the oracle risk $\sum_i\min(\beta_i^2,\sigma^2)$ up to a factor $O(\log p)$, uniformly over $S$-sparse parameters and with explicit, nonasymptotic constants. For coefficients well below the noise level it is far sharper than the $\sigma^2 S\log p$ bound of Theorem 1.1. It is the template for later oracle inequalities for $\ell_1$-penalized estimators under restricted isometry or restricted eigenvalue conditions.

Formalizing it. The theorem is proved in the paper, but parts of the argument are only sketched: Corollary A.2 refers to the 2005 Decoding by Linear Programming paper for its convergence argument, and Corollary A.3's $\ell_1$ bound is printed with a constant its own proof does not deliver. A machine-checked proof settles these steps. The restricted isometry and orthogonality constants used here are already published on the platform from the decoding series; the appendix lemmas on dual vectors are reusable for any compressed-sensing result in that framework. No formalization of the Dantzig selector's oracle inequality is known to us.

Difficulty

The natural proof compares $\hat\beta$ with the hard-thresholded parameter $\beta^{(1)}$ that keeps only the large coefficients: if $\beta^{(1)}$ were feasible for the Dantzig constraint, the analysis of Theorem 1.1 would apply directly. It is not feasible in general, because the small coefficients $\beta^{(2)}$, though individually below the noise level, can add up to a large correlation $X^*X\beta^{(2)}$. The central difficulty is to split $\beta^{(2)}$ into a part with controlled $\ell_1$ and $\ell_2$ norm and a part invisible to the constraint; this requires constructing dual vectors with prescribed correlations (Lemma A.1, Corollary A.2), via an iterative, geometrically convergent correction. The probabilistic part is a Gaussian tail estimate plus a union bound, and the bookkeeping of constants must be carried through exactly.

Formalization scope

Vectors are functions Fin p → ℝ, the design is Matrix (Fin n) (Fin p) ℝ, and the noise is a family z : Fin n → Ω → ℝ of mutually independent random variables (iIndepFun) each with law gaussianReal 0 σ². $\delta_{2S}$ and $\theta_{S,2S}$ are the published CandesTao.Decoding.restrictedIsometryConst X (2*S) and restrictedOrthogonalityConst X S (2*S) (infima, absolute value in the orthogonality condition). Domain: $S\ge1$ and $3S\le p$ (the paper defines $\theta_{S,S'}$ for $S+S'\le p$), which forces $p\ge3$ and $\log p>0$. A Dantzig selector is any $\ell_1$ minimizer over the feasible set; the $\ell_\infty$ constraint is a bound on every coordinate.

The goal bounds from above the (outer) probability of the bad event "no Dantzig selector exists, or some Dantzig selector violates (1.13)". Because the event includes non-existence, a definition no vector satisfies cannot make the theorem vacuous; and the constant $C_2$ is the printed (1.14), evaluated at $\delta_{2S}$, $\theta_{S,2S}$ of $X$, not a free constant chosen after the fact.

Corrected constant: Corollary A.3 is stated with $\|\beta'\|_{\ell_1}\le2\frac{1+\delta}{1-\delta-\theta}\|\beta\|_{\ell_2}^2/\lambda$, the bound its proof gives once Corollary A.2 is applied at an integer sparsity level; the printed statement omits the factor $2$. Corollary A.2 carries Lemma A.1's standing hypothesis $\delta+\theta<1$. The deterministic lemmas (3.1, 3.2, A.1–A.3) assume nothing about column norms, since their statements do not need it.

Useful infrastructure: monotonicity of $\delta_S$ and $\theta_{S,S'}$ in their indices (the proof applies the lemmas at a smaller sparsity level), the Gaussian tail bound $1-\Phi(u)<\varphi(u)/u$, existence of minimizers of the Dantzig linear program, and a sorting/blocking toolkit for "the $S$ largest positions". Proofs of individual milestones are welcome independently.

Selected references

• E. Candès and T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6):2313–2351, 2007. arXiv:math/0506081v3, doi:10.1214/009053606000001523
• E. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51(12):4203–4215, 2005. arXiv:math/0502327, doi:10.1109/TIT.2005.858979
• P. Bickel, Y. Ritov and A. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4):1705–1732, 2009. arXiv:0801.1095, doi:10.1214/08-AOS620
• D. Donoho and I. Johnstone, Ideal spatial adaptation by wavelet shrinkage, Biometrika 81(3):425–455, 1994. doi:10.1093/biomet/81.3.425

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

1. 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}$.
2. 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$.
3. 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$.
4. 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$.
5. 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

Motivation

Many algorithms in operations research and computer science have tunable parameters: sequence-alignment weights, clustering linkage interpolations, branch-and-bound branching rules, auction reserve prices. In data-driven algorithm design the parameters are chosen by optimizing average performance over a training set of problem instances drawn from an unknown application-specific distribution. The question this mission is about is statistical: how many training instances suffice for the empirical average performance of every parameter setting to be close to its expected performance?

Classical learning theory answers this through the pseudo-dimension of the class of utility functions (Pollard, 1984): a bound on the pseudo-dimension gives a uniform convergence bound of order $H\sqrt{(\mathrm{Pdim} + \ln(1/\delta))/N}$. The difficulty is that utility functions of combinatorial algorithms are wildly discontinuous in the parameters, so standard tools (Lipschitz arguments, linear classes) do not apply. Balcan, DeBlasio, Dick, Kingsford, Sandholm and Vitercik (arXiv:1908.02894v4, STOC 2021) observed that for a large family of algorithms the utility on each fixed instance is a piecewise-structured function of the parameters, and proved a single general theorem converting that structure into a pseudo-dimension bound. Earlier analyses (for example Gupta and Roughgarden 2017; Balcan, Nagarajan, Vitercik and White 2017) derived such bounds one algorithm family at a time; Theorem 3.3 unifies them.

Setting

Let $\mathcal X$ be a set of problem instances and $\mathcal U \subseteq \mathbb R^{\mathcal X}$ a class of utility functions; in the paper $\mathcal U = \{u_\rho : \rho \in \mathcal P\}$ for a parameter space $\mathcal P \subseteq \mathbb R^d$, with $u_\rho(x)$ the performance of the algorithm with parameter $\rho$ on instance $x$.

Pseudo-dimension. A class $\mathcal H$ of real functions on a domain $\mathcal Y$ shatters points $y_1, \dots, y_N$ if there are targets $z_1, \dots, z_N \in \mathbb R$ such that every one of the $2^N$ patterns of "above / not above $z_i$" at the points $y_i$ is realized by some $h \in \mathcal H$. The pseudo-dimension $\mathrm{Pdim}(\mathcal H)$ is the largest $N$ for which some $N$ points are shattered. For $\{0,1\}$-valued classes it is the VC-dimension $\mathrm{VCdim}(\mathcal H)$.

Dual class (Definition 3.1). For $\mathcal H \subseteq \mathbb R^{\mathcal Y}$, each $y \in \mathcal Y$ gives an evaluation map $h^*_y : \mathcal H \to \mathbb R$, $h^*_y(h) = h(y)$, and $\mathcal H^* = \{h^*_y : y \in \mathcal Y\}$. For utility functions, $u^*_x(u_\rho) = u_\rho(x)$: the dual function of instance $x$ records performance on $x$ as the algorithm varies.

Piecewise decomposability (Definition 3.2). Given a class $\mathcal G \subseteq \{0,1\}^{\mathcal Y}$ of boundary functions, a class $\mathcal F \subseteq \mathbb R^{\mathcal Y}$ of piece functions and $k \in \mathbb N$, a class $\mathcal H \subseteq \mathbb R^{\mathcal Y}$ is $(\mathcal F, \mathcal G, k)$-piecewise decomposable if every $h \in \mathcal H$ admits $g^{(1)}, \dots, g^{(k)} \in \mathcal G$ and, for each bit vector $\boldsymbol b \in \{0,1\}^k$, some $f_{\boldsymbol b} \in \mathcal F$, with $h(y) = f_{\boldsymbol b_y}(y)$ where $\boldsymbol b_y = (g^{(1)}(y), \dots, g^{(k)}(y))$. The theorem applies this to $\mathcal H = \mathcal U^*$, so $\mathcal F \subseteq \mathbb R^{\mathcal U}$ and $\mathcal G \subseteq \{0,1\}^{\mathcal U}$, and their duals $\mathcal F^*$, $\mathcal G^*$ are classes of functions on $\mathcal F$ and $\mathcal G$.

Formalization targets

Goal: Theorem 3.3, explicit form

Suppose $\mathcal U^*$ is $(\mathcal F, \mathcal G, k)$-piecewise decomposable, $k \ge 1$, $d_F = \mathrm{Pdim}(\mathcal F^*)$, $d_G = \mathrm{VCdim}(\mathcal G^*)$ and $D = d_F + d_G$. With $a = D/\ln 2$ and $b = (D + d_G\ln k)/\ln 2$,

$$\mathrm{Pdim}(\mathcal U) \le 4a\ln(2a) + 2b = O\bigl(D\ln D + d_G \ln k\bigr).$$

This is the explicit bound behind the printed $O(\cdot)$; it is what the paper's proof establishes.

Milestones, in the order the proof uses them

1. Lemma 3.4. For $h_1, \dots, h_N$ in a $\{0,1\}$-valued class $\mathcal H$ ($N \ge 1$),

$$|\{(h_1(y), \dots, h_N(y)) : y \in \mathcal Y\}| \le (eN)^{\mathrm{VCdim}(\mathcal H^*)}.$$

2. Claim 3.5. For instances $x_1, \dots, x_N$, the class $\mathcal U$ splits into $M \le (ekN)^{d_G}$ cells (strictly fewer when $d_G \ge 1$) on each of which every $u^*_{x_i}$ coincides with one fixed piece function $f_i \in \mathcal F$.
3. Eq. (7). On any cell, fixed piece functions $f_1, \dots, f_N$ realize at most $(eN)^{d_F}$ label vectors $(\mathbb 1[f_i(u) > z_i])_i$.
4. Eq. (5). The whole class realizes at most $(ekN)^{d_G}(eN)^{d_F}$ label vectors $(\mathbb 1[u(x_i) > z_i])_i$.
5. Shattering inequality. If $\mathcal U$ shatters $x_1, \dots, x_N$ ($N \ge 1$), then $2^N \le (ekN)^{d_G}(eN)^{d_F}$.
6. Lemma A.1. For $a \ge 1$, $b > 0$: $y < a\ln y + b$ implies $y < 4a\ln(2a) + 2b$.

Significance

Theorem 3.3 is the engine behind every generalization guarantee in the paper. It is instantiated for piecewise-constant and piecewise-linear duals over $\mathbb R^d$ (Lemmas 3.8–3.10), and through them for sequence alignment, RNA folding, hierarchical clustering, integer programming (branch-and-bound), greedy algorithms and auction design. Combined with the classical uniform convergence bound, it says that $\tilde O(H^2(D + d_G\ln k)/\varepsilon^2)$ training instances suffice to tune any such algorithm to within $\varepsilon$ of its optimal expected performance. The matching lower bounds in the paper (Theorems 4.3 and 5.2) show that the bound is tight up to logarithmic factors.

The result is proved in the paper; to the best of available records it has not been machine-checked. The mission formalizes the known proof, including the dual-class version of Sauer's lemma and the counting argument over the partition induced by the boundary functions. The published Sauer's lemma FoundationsML.RademacherVC.sauer_lemma is included as a reference item, as it is the tool Lemma 3.4 cites.

Difficulty

The obvious approach, bounding the pseudo-dimension of $\mathcal U$ directly from the complexity of $\mathcal F$ and $\mathcal G$, fails: the piecewise structure lives on the dual side, and nothing about $\mathcal F$ or $\mathcal G$ themselves controls how $\mathcal U$ labels instances. The bound has to pass through dual classes twice and through the dual of a dual once, and Sauer's lemma, which counts labelings of fixed points by varying functions, must be applied in the transposed direction. Formally, the counting step needs bookkeeping of label vectors under a partition indexed by $kN$ boundary functions, and a conversion from a pseudo-dimension bound on $\mathcal F^*$ to a VC-dimension bound on the thresholded class $\{(f, z) \mapsto \mathbb 1[f(u) > z]\}$, which needs the observation that a shattered tuple of pairs has distinct first coordinates.

Formalization scope

• Pseudo- and VC-dimension are the published FoundationsML predicates Shatters, PseudoDim, GrowthFunction, HasVCDim. The exact-value predicates fix finite dimensions $d_F$, $d_G$, which the paper's bound presupposes. "$\mathrm{Pdim}(\mathcal U) \le B$" is stated as "every shattered tuple has length at most $B$". $\{0,1\}$ is Bool.
• Sign convention. Shattering uses strict thresholds $u(x_i) > z_i$; the paper leaves $\mathrm{sign}(0)$ unspecified, and strict and non-strict thresholds shatter the same tuples, so the dimension is unchanged. Label vectors in the counting milestones use the same reading.
• Domains. The dual classes are classes of functions on the subtype of the primal class. Parameters $\rho$ are indexed by the functions $u_\rho$ themselves, and Claim 3.5's partition of $\mathcal P$ becomes a partition of $\mathcal U$; nothing in the theorem depends on $\rho$ except through $u_\rho$.
• Corrections of the printed statements. (i) Theorem 3.3's $O(\cdot)$ is replaced by the explicit bound $4a\ln(2a) + 2b$ derived from the paper's own last step and Lemma A.1, with $k \ge 1$ added (the printed $\ln k$ is undefined at $k = 0$); the case $D = 0$ is covered, where the bound is $0$. (ii) Lemma 3.4 and the counting milestones assume $N \ge 1$; at $N = 0$ the printed bounds read $1 \le 0$. (iii) Claim 3.5's strict $M < (ekN)^{\mathrm{VCdim}(\mathcal G^*)}$ is kept for $\mathrm{VCdim}(\mathcal G^*) \ge 1$ and weakened to $\le$ only when $\mathrm{VCdim}(\mathcal G^*) = 0$, where the strict form is false ($M = 1$). The milestone texts are quoted verbatim.
• Dropped hypothesis. The range $[0, H]$ of the utility functions is not used by the theorem or its proof and is omitted, which makes the statement more general.
• Ruling out trivializations. The goal carries the explicit constant, never an $O(\cdot)$ with a constant chosen after the classes; the hypotheses are jointly satisfiable on a nontrivial example (one instance, $u_\rho(x) = \rho$, $k = 1$, $d_F = 1$, $d_G = 0$, in which $\mathcal U$ does shatter one point), checked by a sorry-free local verification file; all counts are of subsets of $\{0,1\}^N$, so no cardinality silently defaults to zero.
• Contributions welcome: proofs of each milestone; a dual-class Sauer lemma reusable for other data-driven design papers; the passage from pseudo-dimension of $\mathcal F^*$ to the VC-dimension of its thresholded class.

Selected references

• M.-F. Balcan, D. DeBlasio, T. Dick, C. Kingsford, T. Sandholm, E. Vitercik, How Much Data Is Sufficient to Learn High-Performing Algorithms? Generalization Guarantees for Data-Driven Algorithm Design, STOC 2021; arXiv:1908.02894v4, 2021. https://arxiv.org/abs/1908.02894
• P. Assouad, Densité et dimension, Annales de l'Institut Fourier 33(3), 1983. https://doi.org/10.5802/aif.938
• D. Pollard, Convergence of Stochastic Processes, Springer, 1984. https://doi.org/10.1007/978-1-4612-5254-2
• N. Sauer, On the density of families of sets, Journal of Combinatorial Theory A 13(1), 1972. https://doi.org/10.1016/0097-3165(72)90019-2
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014. https://doi.org/10.1017/CBO9781107298019
• R. Gupta, T. Roughgarden, A PAC approach to application-specific algorithm selection, SIAM Journal on Computing 46(3), 2017. https://doi.org/10.1137/15M1050276