Machine Learning

Calibrated forecasting

A forecaster announces, each day, a probability that it will rain; afterwards nature reveals whether it did. The forecaster is calibrated if, on the days on which it announced roughly 30%, it rained roughly 30% of the time, and likewise for every other announced value. Calibration is a minimal consistency requirement for probabilistic forecasts, used in meteorology, in the evaluation of probabilistic classifiers, and in game theory, where calibrated forecasts of the opponents' play lead to correlated equilibrium (Foster and Vohra, 1997).

Calibration is achievable even against an adversary who chooses the outcomes, provided the forecaster randomizes. Timeline:

• 1998. Foster and Vohra construct an asymptotically calibrated randomized forecaster against an arbitrary outcome sequence.
• 1999. Foster reduces calibration to Blackwell's approachability theorem by exhibiting, for each halfspace, a forecast that keeps the payoff inside it.
• 2009. Mannor and Stoltz give an approachability-based calibration procedure concurrently with the paper below.
• 2011. Abernethy, Bartlett and Hazan prove that Blackwell approachability and no-regret online linear optimization are equivalent, and use the equivalence to obtain an efficient calibrated forecaster: $O(\log 1/\varepsilon)$ time per round and calibration rate $O(1/\sqrt{\varepsilon T})$.

This mission formalizes the last result, Theorem 22 of the 2011 paper, in the explicit form given by its proof.

Setting

Fix a positive integer $m$ and the grid width $\varepsilon = 1/m$. Each round $t = 1, \dots, T$ the forecaster chooses a probability vector $w_t$ in the simplex $\Delta_{m+1}$ over the grid indices $i = 0, \dots, m$, draws $i_t \sim w_t$ and announces $p_t = i_t/m$. Nature then reveals $y_t \in \{0, 1\}$.

Vectors live in $\mathbb R^{m+1}$ with the Euclidean norm $\|\cdot\|_2$. The ℓ₁ norm is $\|x\|_1 = \sum_i |x_i|$, the ℓ₁ ball is $B_1(r) = \{y : \|y\|_1 \le r\}$, and the unit cube is $B_\infty(1) = \{\theta : |\theta_i| \le 1 \text{ for all } i\}$.

The calibration game (11) has payoff

$$u(w, y) = \Bigl(w(0)\bigl(y - \tfrac0m\bigr),\ w(1)\bigl(y - \tfrac1m\bigr),\ \dots,\ w(m)(y - 1)\Bigr) \in \mathbb R^{m+1}.$$

The $(\ell_1, \varepsilon)$-calibration rate (Definition 19) of the announced forecasts is $\max\{0, \sum_{i=0}^m |\frac1T\sum_{t=1}^T \mathbb I[p_t = i/m](i/m - y_t)| - \varepsilon/2\}$. Replacing each indicator by its expectation $w_t(i)$ gives the rate of the forecast distributions,

$$\bar C^\varepsilon_T = \max\Bigl\{0,\ \sum_{i=0}^m \Bigl|\frac1T \sum_{t=1}^T w_t(i)\Bigl(\frac im - y_t\Bigr)\Bigr| - \frac\varepsilon2\Bigr\},$$

which is $\max\{0, \|\bar u_T\|_1 - \varepsilon/2\}$ for the average payoff $\bar u_T = \frac1T\sum_t u(w_t, y_t)$.

The forecaster is Algorithm 5. It keeps a point $\theta_t$ in the cube, starting from $\theta_1 = 0$ with $w_1$ arbitrary. After round $t$ it takes a projected gradient step (Algorithm 4, online gradient descent) against the loss vector $f_t = -u(w_t, y_t)$:

$$\theta_{t+1} = \Pi_{B_\infty(1)}\bigl(\theta_t + \eta\, u(w_t, y_t)\bigr),$$

where $\Pi$ is the Euclidean projection. It then sets $w_{t+1}$ to the output of the oracle Algorithm 3 on $\theta_{t+1}$, which puts weight on at most two adjacent grid points where $\theta$ changes sign.

Formalization targets

Goal: Theorem 22 in the form (14)

For $m \ge 1$, $T \ge 1$, every outcome sequence $y_1, \dots, y_T \in \{0, 1\}$ and every run of Algorithm 5 with $\eta = \sqrt{(m+1)/T}$,

$$\bar C^\varepsilon_T \le \sqrt{\frac{2}{\varepsilon T}}.$$

This is the bound $C^\varepsilon_T \le GD/\sqrt T$ of display (14) with the paper's constant $G = \sqrt 2$.

Milestones

1. Claim 1 (proof): $\min_{\|y\|_1 \le \varepsilon/2}\|x - y\|_1 = \max\{0, -\varepsilon/2 + \|x\|_1\}$.
2. Display (13): for $\|x\|_1 > \varepsilon/2$, also $= -\varepsilon/2 - \min_{\|\theta\|_\infty \le 1}\langle -x, \theta\rangle$.
3. Algorithm 3: for every $\theta$ in the cube there is an output $w \in \Delta_{m+1}$, and every output satisfies $\langle u(w, y), \theta\rangle \le \varepsilon/2$ for all $y \in [0, 1]$.
4. Display (12): under that guarantee, $\max\{0, \|\bar u_T\|_1 - \varepsilon/2\} \le \frac1T\bigl(\sum_t \langle -u_t, \theta_t\rangle - \min_{\theta \in B_\infty(1)}\sum_t\langle -u_t, \theta\rangle\bigr)$.
5. Online gradient descent: regret at most $DG\sqrt T$ with step $\eta = D/(G\sqrt T)$.
6. Theorem 21 (response-satisfiability and approachability): for every $y \in [0,1]$ some $w \in \Delta_{m+1}$ has $u(w, y) \in B_1(\varepsilon/2)$; hence some algorithm choosing $w_t$ from $y_1, \dots, y_{t-1}$ drives the distance of the average payoff to $B_1(\varepsilon/2)$ to $0$ against every outcome sequence in $[0,1]$.

Significance

The bound shows that a forecaster with logarithmic per-round cost has calibration error vanishing at rate $T^{-1/2}$ against every outcome sequence. Earlier calibrated forecasters required solving a linear program or computing a fixed point each round. The construction is also the paper's worked instance of its general equivalence: a calibration problem, posed as approachability of an ℓ₁ ball, is solved by a no-regret learner on the dual unit cube together with a halfspace oracle.

The result is proved in the paper; no machine-checked version is known to exist. The formalization makes explicit three points the paper leaves informal: the step size, the sign of the gradient step, and the gap between the forecast distributions and the sampled forecasts. The milestones are reusable on their own: the ℓ₁/ℓ∞ duality, and the regret bound of online gradient descent for linear losses on a general closed convex set.

Difficulty

The chain (12)–(14) looks like a direct composition, but each link has content. The oracle guarantee needs a case analysis over the sign pattern of $\theta$, including the degenerate case $\theta(i+1) = 0$. The reduction (12) needs the duality (13) with attained minima, and it holds only outside the ball $B_1(\varepsilon/2)$. The regret bound of online gradient descent needs the non-expansiveness of the Euclidean projection and a telescoping argument. The tempting shortcut of quoting "OGD has regret $O(\sqrt T)$" does not give the stated constant without fixing the step size.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin (m+1)), with grid index $i \in \{0, \dots, m\}$ as Fin (m+1) and $i/m$ as a real quotient; the ℓ₁ norm and the cube are written out coordinatewise. Rounds are $t = 1, \dots, T$. Minima over sets are stated through IsLeast or as the infimum of the image of a nonempty bounded set. Algorithm 3 is a relation that allows every sign-change index the binary search might return. The projection is any Euclidean minimizer onto the cube.

Conventions and corrections, each disclosed in the item's Formalization Note:

• Gradient-step sign. Algorithm 4 prints $\theta_t - \eta u_t$, but the proof runs the learner on the losses $f_t = -u_t$ (condition 2), so the step is $\theta_t + \eta u_t$. With the printed sign the bound fails.
• Step size. The page sets $\eta = O(T^{-1/2})$; the goal pins $\eta = \sqrt{(m+1)/T}$, the standard tuning with radius $\sqrt{m+1}$ of the cube and $\|u_t\|_2 \le 1$. The page's $D = \sqrt{1/\varepsilon}$ is not the cube's diameter.
• Forecast distributions. The rate is that of the distributions $w_t$, the expectation of the calibration vector over the forecaster's draws (Lemma 20). The high-probability statement for the sampled forecasts is not formalized, nor is the running-time claim.
• Other misprints. Algorithm 3's header "$w \mapsto \theta$" is $\theta \mapsto w$, and the calibration vector has $m + 1$ coordinates, not $\lfloor \varepsilon^{-1} \rfloor$.
• Added hypotheses. $m \ge 1$ and $T \ge 1$.

A trivializing formalization is ruled out. The rate is defined from Definition 19's formula, not as a distance, and the step size is pinned. A free step size would make the bound false, and an empty oracle relation would make it vacuous; milestone 3's existence clause excludes the latter.

Contributions are welcome on each milestone. The online gradient descent bound and the ℓ₁/ℓ∞ duality are independent of calibration. The published one-step inequality LogRegretOCO.OGD.one_step_inequality is included as a reference item for the regret bound.

Selected references

• J. Abernethy, P. L. Bartlett, E. Hazan, Blackwell Approachability and No-Regret Learning are Equivalent, COLT 2011, JMLR W&CP 19, pp. 27–46, 2011. https://proceedings.mlr.press/v19/abernethy11b.html
• D. P. Foster, R. V. Vohra, Asymptotic calibration, Biometrika 85(2), 1998. https://doi.org/10.1093/biomet/85.2.379
• D. P. Foster, A proof of calibration via Blackwell's approachability theorem, Games and Economic Behavior 29, 1999. https://doi.org/10.1006/game.1999.0724
• D. P. Foster, R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21, 1997. https://doi.org/10.1006/game.1997.0595
• S. Mannor, G. Stoltz, A geometric proof of calibration, Mathematics of Operations Research 35(4), 2010. https://arxiv.org/abs/0908.3576
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955

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

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

1. 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$.
2. 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\} .$$

3. 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