Machine Learning

Motivation

The sample complexity of a learning problem is the number of labelled examples needed to learn to a prescribed accuracy with a prescribed confidence. In Valiant's probably approximately correct (PAC) model it is the basic quantity of statistical learning theory: it says how much data is necessary and sufficient, as a function of the complexity of the hypothesis class, when the target concept belongs to that class (the realizable case).

For a class of Vapnik–Chervonenkis (VC) dimension $d$ the answer was known up to a logarithmic factor for about 25 years:

• 1982–1989. Vapnik (1982) and Blumer, Ehrenfeucht, Haussler and Warmuth (J. ACM 1989) showed that any learner that outputs a classifier consistent with the sample succeeds with $O\left(\frac1\varepsilon\left(d\log\frac1\varepsilon+\log\frac1\delta\right)\right)$ examples.
• 1989. Ehrenfeucht, Haussler, Kearns and Valiant (Inform. Comput. 1989) together with Blumer et al. proved the lower bound $\Omega\left(\frac1\varepsilon\left(d+\log\frac1\delta\right)\right)$ for every learner.
• 1994. Haussler, Littlestone and Warmuth (Inform. Comput. 1994) showed $\mathcal M(\varepsilon,\delta)=O\left(\frac d\varepsilon\mathrm{Log}\frac1\delta\right)$ with a variant of the one-inclusion graph predictor, which is sometimes better but also does not match the lower bound.
• 2007–2015. The gap was closed for restricted classes, such as intersection-closed classes (Auer and Ortner 2007; Darnstädt 2015), but not for classes such as linear separators.
• 2015. Simon (COLT 2015) analysed a majority vote of consistent classifiers trained on disjoint parts of the data and reduced the logarithmic factor to a very slowly growing function of $1/\varepsilon$.
• 2016. Hanneke (JMLR 17(38), 2016; arXiv:1507.00473) removed the logarithmic factor for every class, with an explicit learner: a majority vote of consistent classifiers trained on recursively constructed, overlapping subsamples.

Setting

Let $\mathcal X$ be a set with a $\sigma$-algebra and $\mathcal Y=\{-1,+1\}$. A classifier is a measurable map $h:\mathcal X\to\mathcal Y$; the concept space $\mathbb C$ is a set of classifiers with $|\mathbb C|\ge3$. A finite sequence $x_1,\ldots,x_k$ is shattered by $\mathbb C$ if every labelling $y_1,\ldots,y_k$ is realized by some $h\in\mathbb C$; the VC dimension $d$ is the largest such $k$, assumed finite (then $d\ge1$).

A data set is a finite sequence $S$ of pairs in $\mathcal X\times\mathcal Y$, and $\mathbb C[S]$ is the set of $h\in\mathbb C$ with $h(x)=y$ for all $(x,y)\in S$. For a probability measure $P$ and a target $f^\star\in\mathbb C$, the error of $h$ is $\mathrm{er}_P(h;f^\star)=P(\mathrm{ER}(h))$, where $\mathrm{ER}(h)=\{x:h(x)\ne f^\star(x)\}$. A learning algorithm maps data sets to classifiers.

For $\varepsilon,\delta\in(0,1)$, the sample complexity $\mathcal M(\varepsilon,\delta)$ (Definition 1) is the least $m$ such that some algorithm $\mathcal A$ satisfies, for every probability measure $\mathcal P$ on $\mathcal X$ and every $f^\star\in\mathbb C$, with $X_1,\ldots,X_m$ independent with law $\mathcal P$,

$$\mathbb P\left(\mathrm{er}_{\mathcal P}\left(\mathcal A\big((X_i,f^\star(X_i))_{i\le m}\big);f^\star\right)\le\varepsilon\right)\ge1-\delta,$$

and $\mathcal M(\varepsilon,\delta)=\infty$ if there is no such $m$.

The learner of the paper uses three ingredients. A sample-consistent learner $L$ returns an element of $\mathbb C[S]$ whenever that set is nonempty. The majority vote is $\mathrm{Majority}(h_1,\ldots,h_k)(x)=2\mathbb 1\left[\sum_i h_i(x)\ge0\right]-1$. The subsample algorithm $\mathbb A(S;T)$ returns $\{S\cup T\}$ if $|S|\le3$; otherwise it splits $S$ into a head $S_0$ of $|S|-3\lfloor|S|/4\rfloor$ points and three blocks $S_1,S_2,S_3$ of $\lfloor|S|/4\rfloor$ points, and returns the concatenation of $\mathbb A(S_0;S_2\cup S_3\cup T)$, $\mathbb A(S_0;S_1\cup S_3\cup T)$ and $\mathbb A(S_0;S_1\cup S_2\cup T)$. The learned classifier is $\hat h=\mathrm{Majority}(L(\mathbb A(S;\emptyset)))$.

Formalization targets

Goal: Theorem 2 with its explicit constant

$$\mathcal M(\varepsilon,\delta)\le\frac{1800}{\varepsilon}\left(d+\ln\left(\frac{18}{\delta}\right)\right)\qquad(\varepsilon,\delta\in(0,1)).$$

The paper states Theorem 2 as $\mathcal M(\varepsilon,\delta)=O\left(\frac1\varepsilon\left(d+\mathrm{Log}\frac1\delta\right)\right)$ with a numerical constant; its proof establishes the bound above with $c=1800$, and that explicit form is the goal. Improving the constant would give a stronger theorem; this statement stays valid.

Milestones, in attack order

1. Lemma 4 (Blumer et al. 1989): with probability $1-\delta$, every $h\in\mathbb C[\{(Z_i,f^\star(Z_i))\}_{i\le m}]$ has $\mathrm{er}_P(h;f^\star)\le\frac2m\left(d\,\mathrm{Log}_2\frac{2em}d+\mathrm{Log}_2\frac2\delta\right)$.
2. Lemma 5: $a\ln(c_1(c_2+b/a))\le a\ln(c_1(c_2+e))+b/e$ for $a,b,c_1\ge1$, $c_2\ge0$.
3. Structure of $\mathbb A$: every subsample $\hat S$ satisfies $T\subseteq\hat S\subseteq S\cup T$, and the number of subsamples does not depend on $T$.
4. The Chernoff event $E_i''$: if $Q(E)\ge\frac{23}n\ln\frac9\delta$, then with probability $1-\delta/9$ at least $\frac7{10}Q(E)n$ of $n$ i.i.d. points fall in $E$.
5. The bound (8) and its comparison with $\frac{150}{m+1}\left(d+\ln\frac{18}\delta\right)$.
6. Majority averaging: $\mathrm{er}(h_{\mathrm{maj}})\le12\,\mathbb E\left[\mathcal P(\mathrm{ER}(h_I)\cap\mathrm{ER}(\tilde h))\right]$ for three equal-size committees.
7. Claim (9): with probability $1-\delta$, $\mathrm{er}_{\mathcal P}(\hat h_{m,T};f^\star)\le\frac{1800}{m+1}\left(d+\ln\frac{18}\delta\right)$.
8. Sample size (10): $\mathrm{Majority}(L(\mathbb A(\cdot;\emptyset)))$ is $(\varepsilon,\delta)$-PAC from $\left\lfloor\frac{1800}\varepsilon\left(d+\ln\frac{18}\delta\right)\right\rfloor$ examples.

Significance

Together with the classical lower bound, Theorem 2 gives $\mathcal M(\varepsilon,\delta)=\Theta\left(\frac1\varepsilon\left(d+\log\frac1\delta\right)\right)$: the realizable PAC sample complexity is determined up to a numerical constant by the VC dimension alone. It settles a question open since 1989, shows that the $\log\frac1\varepsilon$ factor in the classical bounds is an artifact of empirical risk minimization rather than of the learning problem, and supplies an explicit, simple learner that attains the optimal rate. Later work on optimal learners (majority votes over bagged or subsampled ERMs, optimal learning in other settings) builds on this construction.

The result is proved on paper. To our knowledge no proof assistant contains it, and the formal libraries lack parts of its infrastructure: the classical bound for consistent learners (Lemma 4), multiplicative Chernoff bounds for empirical counts, and conditioning on independent parts of an i.i.d. sample. This mission produces a machine-checked statement of the optimal bound with the paper's explicit constant, a verified formal model of the learner, and reusable components for these three.

Difficulty

The obvious approach is to sharpen the analysis of a single consistent classifier, as in the classical bound. Decades of effort along these lines did not remove the $\log\frac1\varepsilon$ factor, and the paper removes it only by aggregating many classifiers. The error of a majority vote is not controlled by the errors of its voters one at a time. The proof controls the probability that two voters trained on overlapping subsamples err at the same point, which requires tracking which parts of the sample are independent of which trained classifiers through a recursion of depth $\log_4 m$. In a formal development the difficult parts are the conditional-independence bookkeeping for random subsamples of a product measure, the induction over the sample size with a data set $T$ that varies with the level, and the numerical constants, which are tight (the key comparison is $149.9997<150$).

Formalization scope

• Representation. Labels are Bool (true for $+1$); data sets are lists and $\cup$ is concatenation; $\mathbb C$ is a set of measurable functions with $|\mathbb C|\ge3$; the VC dimension is a supremum in $\mathbb N\cup\{\infty\}$, assumed equal to a natural number $d$. The i.i.d. sample is the product measure $\mathcal P^m$ on $\mathrm{Fin}\,m\to\mathcal X$. "With probability at least $1-\delta$" is stated as a bound $\le\delta$ on the outer measure of the failure event. $\mathcal M$ takes values in $\mathbb N\cup\{\infty\}$, so the goal is stated as $\mathcal M(\varepsilon,\delta)\le\left\lfloor\frac{1800}\varepsilon\left(d+\ln\frac{18}\delta\right)\right\rfloor$, which is equivalent. Ties in the majority vote go to $+1$, as printed.
• Algorithms. $\mathcal M$ quantifies over deterministic algorithms that output measurable classifiers, chosen before $\mathcal P$ and $f^\star$ and seeing only the labelled sample. The paper also admits randomized algorithms (footnote 2), which can only lower $\mathcal M$, so the goal implies the paper's statement.
• Measurability. The paper assumes that every event in its probability claims is measurable (p. 3). The formalization makes this explicit with two hypotheses: the class is well-behaved (the event of Lemma 4 and the double-sample event of Blumer et al. are null-measurable for every distribution), and the base learner $L$ is jointly measurable in the sample and the point. Both hold for every countable class of measurable classifiers, with $L$ returning the first consistent classifier of an enumeration. Without the first hypothesis Lemma 4 fails for some classes of VC dimension 1.
• Ruled out. The following formalizations would make the goal trivial or weaker, and are not used here:
  • a sample complexity whose algorithm may depend on $\mathcal P$ or $f^\star$, which gives $\mathcal M\equiv0$;
  • a goal with an existential constant or a ceiling in place of $1800$ and the floor;
  • measurability hypotheses that no infinite class satisfies;
  • milestones 7–8 stated for an arbitrary family of subsamples instead of the algorithm $\mathbb A$.
• Needed infrastructure. VC theory for consistent learners (Lemma 4, via the double-sample argument), multiplicative Chernoff bounds for binomial counts, and conditioning of product measures on coordinate blocks. These are reusable beyond this mission. Contributions welcome: a proof of Lemma 4, the Chernoff milestone, the numerical milestone 5, and the majority-vote averaging step, each of which is independent of the others.

Selected references

• S. Hanneke, The Optimal Sample Complexity of PAC Learning, Journal of Machine Learning Research 17(38):1–15, 2016. arXiv:1507.00473v4
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Learnability and the Vapnik–Chervonenkis dimension, Journal of the ACM 36(4):929–965, 1989. doi:10.1145/76359.76371
• A. Ehrenfeucht, D. Haussler, M. Kearns, L. Valiant, A general lower bound on the number of examples needed for learning, Information and Computation 82(3):247–261, 1989. doi:10.1016/0890-5401(89)90002-3
• H. U. Simon, An almost optimal PAC algorithm, Proceedings of the 28th Conference on Learning Theory (COLT), PMLR 40:1552–1563, 2015. proceedings.mlr.press/v40/Simon15a
• D. Haussler, N. Littlestone, M. K. Warmuth, Predicting {0,1}-functions on randomly drawn points, Information and Computation 115(2):248–292, 1994. doi:10.1006/inco.1994.1097
• P. Auer, R. Ortner, A new PAC bound for intersection-closed concept classes, Machine Learning 66(2–3):151–163, 2007. doi:10.1007/s10994-006-8638-3
• V. Vapnik, Estimation of Dependences Based on Empirical Data, Springer, 1982.

Motivation

In stochastic linear optimization under bandit feedback a learner repeatedly chooses a point $x_t$ from a compact decision set $D\subset\mathbb R^n$ and observes only the random cost $\ell_t$ of that point, whose mean is $\mu\cdot x_t$ for an unknown vector $\mu$. The problem models online routing, ad placement and other sequential decisions with linearly structured costs. The quality of a learner is measured by its regret against the best fixed decision.

For the $K$-armed bandit the achievable regret for a fixed instance is logarithmic in the horizon $T$ (Lai and Robbins 1985; Auer, Cesa-Bianchi and Fischer 2002). Dani, Hayes and Kakade (COLT 2008) showed that for linear costs the picture depends on the geometry of $D$. Their Theorem 1 gives polylogarithmic regret when the decision set has a positive gap between the best and second-best extreme point (a polytope, for instance), and their Theorem 2 gives $O^*(n\sqrt T)$ regret for every decision set. Their Theorem 3 shows that the second rate cannot be improved in general: on a decision set with zero gap, every algorithm pays $\Omega(\sqrt T)$ in expectation.

Timeline:

• 2002: Auer, Using confidence bounds for exploitation–exploration trade-offs (JMLR 3), introduces confidence-bound algorithms for linear bandits on finite decision sets.
• 2008: Dani, Hayes and Kakade prove the $O^*(n\sqrt T)$ upper bound for ConfidenceBall₂ and the $\Omega(\sqrt T)$ lower bound on a product of circles, the subject of this mission. A hypercube lower bound for the adversarial setting appears in their NIPS 2007 paper.
• 2010: Rusmevichientong and Tsitsiklis, Linearly parameterized bandits (Math. OR 35), give $\Omega(n\sqrt T)$ lower bounds on the unit sphere.
• 2020: Lattimore and Szepesvári, Bandit Algorithms, Theorems 24.1 and 24.2, give minimax lower bounds on the hypercube and the unit ball with Gaussian noise.

Setting

The decision set is the unit circle $D_2=S^1=\{x\in\mathbb R^2: x_1^2+x_2^2=1\}$. An unknown mean vector $\mu\in\mathbb R^2$ is drawn once, uniformly from the circle $D_2/2$ of radius $1/2$; concretely $\mu=\mu(\theta)=\tfrac12(\cos\theta,\sin\theta)$ with $\theta$ uniform on $[0,2\pi)$.

On each round $t=1,\dots,T$ the algorithm plays $x_t\in D_2$ and observes a cost $\ell_t\in\{-1,+1\}$ with $\Pr(\ell_t=+1)=(1+\mu\cdot x_t)/2$, so that $\mathbb E[\ell_t]=\mu\cdot x_t$. Given the decision, the cost is independent of the past.

An algorithm may be randomised. It draws a seed $s$ once from a probability measure $\rho$ on a measurable space $S$, and chooses $x_t$ as a function of $s$ and the costs $\ell_1,\dots,\ell_{t-1}$ observed so far, measurably in $s$.

The regret over $T$ rounds is

$$R=\sum_{t=1}^T(\mu\cdot x_t-\mu\cdot x^*),\qquad \mu\cdot x^*=\min_{x\in D_2}\mu\cdot x,$$

so each round costs $r_t=\mu\cdot x_t+\tfrac12\ge0$ when $\|\mu\|=1/2$. The expected regret $\mathbb E R=\mathbb E_\mu\,\mathbb E(R\mid\mu)$ averages over the seed, the prior and the costs.

In the Lean development these objects are unitCircle, meanVec, optCost, RandomizedPolicy and expectedRegret in the namespace StochLinOpt.LowerBound.

Formalization targets

Goal: Theorem 3 for $n=2$

There is a universal constant $c>0$ such that for every randomised algorithm and every $T\ge1$,

$$\mathbb E R\ \ge\ c\sqrt T.$$

The constant is left existential, which is the form that survives any later improvement of the constant; it is chosen before the algorithm and before $T$.

Milestones

1. Section 6.1, Eq. (3). For $\|\mu_1\|=\|\mu_2\|=1/2$, $x\in S^1$, a posterior probability $p\in[0,1]$ of $\mu=\mu_1$ and a cost $\ell\in\{\pm1\}$, the Bayes-updated bias $b_{t+1}$ satisfies $|b_{t+1}-b_t|\le|(\mu_1-\mu_2)\cdot x|$, where $b_t=2p-1$.
2. Lemma 15. With $\varepsilon=\|\mu_1-\mu_2\|>0$ and the same data,

$$\mathbb E_\mu(r_t\mid\mathcal H_t)\ge\frac1{16}\Big(\varepsilon^2+\frac{|b_{t+1}-b_t|^2}{\varepsilon^2}\Big)\mathbf 1\{|b_t|\le1/2\}.$$

3. Theorem 4 (Freedman). For a martingale difference sequence $X_1,\dots,X_T$ bounded above by $b$, with conditional variance sum $V$, and all $a,v>0$,

$$\Pr\Big(\sum_i X_i\ge a,\ V\le v\Big)\le\exp\Big(\frac{-a^2}{2v+2ab/3}\Big).$$

Significance

The lower bound shows that the $\sqrt T$ dependence of the problem-independent upper bound (Theorem 2 of the same paper) is necessary. It also shows that the gap-dependent polylogarithmic rate of Theorem 1 cannot extend to decision sets without a gap, such as the sphere. Together with the upper bound it characterises the minimax regret of stochastic linear bandits in $T$ up to logarithmic factors, and in the paper's general-$n$ form it also underlies the claim that the price of bandit information is $\Theta^*(\sqrt n)$.

The result is proved in the paper for $n=2$ and has not been machine-checked. The mission produces a checked Bayesian lower bound over all randomised algorithms, with an explicit probability model for the protocol. Two related platform results are different theorems: BanditAlgorithm.linear_bandit_unit_ball_minimax_lower_bound (Lattimore–Szepesvári Theorem 24.2: unit ball, Gaussian noise, a worst-case $\mu$) and BanditAlgorithm.linear_bandit_hypercube_minimax_lower_bound (Theorem 24.1: hypercube). The $\{-1,+1\}$ costs, the circle and the uniform prior used here are not covered by either.

Difficulty

The obvious attempt is a two-point change-of-measure argument with a fixed pair of means at distance $\varepsilon$. It fails as stated because the decision set has no gap: an algorithm that plays close to the optimum of both candidates learns slowly but also pays little. The per-round trade-off between regret and information (Lemma 15) is exact only while the posterior is undecided, $|b_t|\le1/2$. Turning it into a bound on the whole horizon requires controlling how long the posterior stays undecided, which is a statement about a martingale whose step sizes are chosen by the algorithm; a concentration bound that ignores the accumulated conditional variance (Azuma–Hoeffding with worst-case steps) is too weak for this. The averaging step from a two-point prior to the uniform prior on the circle is also part of the formal work.

Formalization scope

Vectors are Fin 2 → ℝ with the dot product ⬝ᵥ; Euclidean norms are written through dot products, never with Lean's sup norm. Rounds are 0-indexed internally: the Lean index $t$ is the paper's round $t+1$. The expected regret is the exact finite expectation

$$\mathbb E R=\int_S\frac1{2\pi}\int_0^{2\pi}\sum_{\ell\in\{\pm1\}^T}\prod_{t=1}^T\frac{1+\ell_t\,\mu(\theta)\cdot x_t}{2}\;R\;d\theta\,d\rho(s),$$

so no infinite product of measures is needed. A randomised algorithm is a seeded policy, which covers every randomised algorithm. The optimal cost is the infimum of $\mu\cdot x$ over the compact circle and is attained. Every junk value in the model (a non-integrable integrand) could only make the lower bound harder to prove, never easier.

A statement over deterministic algorithms only, over a worst-case $\mu$ instead of the uniform prior, or with the constant allowed to depend on the algorithm or on $T$ would be a weaker theorem. The goal quantifies $\exists c>0$ before the algorithm and $T$, and fixes the prior.

Corrections relative to the printed paper:

• General $n$ is not stated. Theorem 3 as printed claims $\mathbb E R\ge\frac1{10}n\sqrt T$ for every even $n$. It is false for $n>10$: on $D_n$ with $\mu\in D_n/n$ each round has regret at most $1$, so at $T=1$ the claim would need $\mathbb E R\ge n/10>1$. The general case rests on Lemma 16, which has no proof. The goal is the $n=2$ case, which Section 6.1 proves.
• The constant. For $n=2$ the paper prints $\frac15\sqrt T$; its proof gives $c=\frac1{16}\min(\frac12-\frac1e,\frac1{64})=\frac1{1024}$. The proof's Freedman step prints $2\exp(-\frac{1/4}{1/8+\varepsilon/3})\le 2/e^2$; with $v=1/32$ the denominator is $1/16+\varepsilon/3$, and the bound $2/e^2$ then needs $\varepsilon=T^{-1/4}\le3/16$. Small $T$ is covered by the first round, whose expected regret is $1/2$. The goal leaves $c$ existential.
• Theorem 4. The printed variance sum runs to $n$; it runs to $T$. The conditioning is on a general filtration, and square-integrability of the steps is assumed so that the conditional variance is defined.
• Lemma 15. Its right side depends on the round-$t$ cost $\ell_t$, which is not part of $\mathcal H_t$; the Lean statement holds for either value of $\ell_t$.

Welcome contributions: a Lean proof of Freedman's inequality (reusable across the bandit and concentration missions on the platform); the averaging argument from two-point priors to the uniform prior; and the stopped-martingale bookkeeping for the bias sequence.

Selected references

• Varsha Dani, Thomas P. Hayes, Sham M. Kakade, Stochastic Linear Optimization under Bandit Feedback, Proceedings of the 21st Annual Conference on Learning Theory (COLT), 2008.
• David A. Freedman, On tail probabilities for martingales, The Annals of Probability 3(1):100–118, 1975. https://doi.org/10.1214/aop/1176996452
• Colin McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer, 1998. https://doi.org/10.1007/978-3-662-12788-9_6
• Peter Auer, Using confidence bounds for exploitation–exploration trade-offs, JMLR 3:397–422, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• Paat Rusmevichientong, John N. Tsitsiklis, Linearly parameterized bandits, Mathematics of Operations Research 35(2):395–411, 2010. https://doi.org/10.1287/moor.1100.0446
• Tor Lattimore, Csaba Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 24. https://doi.org/10.1017/9781108571401

Motivation

Modern machine-learning systems are routinely assembled by grafting: pretrained components (an encoder, a decoder) are re-used inside a new architecture, parts of them are frozen, and only selected coordinates are trained. When the full computation does not fit in memory, practitioners cut the loss into tiles (microbatches, row blocks, vocabulary shards), accumulate gradient contributions, and apply the optimizer once. Every memory-constrained trainer assumes this tiled schedule computes the same update as the monolithic one — but the folklore proof hides real failure modes: updating parameters after each tile, averaging tile means, clipping per tile, detaching a frozen component's input, or saving a weights-only checkpoint all silently change the learner.

This mission turns that folklore into a theorem with explicit hypotheses. The design source is the Vathek Graft white paper (Davis, 2026), which proposes an open-predicate extractor trained as a graft and makes the schedule-preservation claim its first proof obligation (Theorem T0). The architectural precedents are established: parallel set-based extraction (DetIE), set-prediction objectives, pointer-generator copying, and low-rank adaptation of frozen bases. What none of them supplies is the exact-arithmetic statement that the memory-saving row schedule preserves the mathematical update — that is the target here.

Setting

Fix finite-dimensional spaces: logical parameters $w \in W = \mathbb{R}^d$, of which only coordinates $j \in T$ are trainable ($P_T$ zeroes frozen coordinates), and a shared-state space $V = \mathbb{R}^m$. One training frame $\xi$ carries a differentiable shared computation $h_\xi : W \to V$ (the donor encoder plus shared projections), finitely many occurrence losses $f_i : W \times V \to \mathbb{R}$ with fixed coefficients $\alpha_i$ over a finite occurrence set $I$, and all discrete choices, fixed during one logical update. The monolithic objective is

$$L_\xi(w) = \sum_{i \in I} \alpha_i\, f_i\big(w, h_\xi(w)\big).$$

A tile partition $\mathcal{B} = (B_1, \dots, B_q)$ splits $I$ into pairwise-disjoint tiles. The tiled evaluator streams the tiles through an accumulator of three slots — running loss, direct parameter-gradient contribution $A$, shared cotangent $C$ — everything read at the same pre-update point $w_0$, and finishes with one reverse pass:

$$g_{\mathrm{tile}} = A + Dh_\xi(w_0)^{\top} C.$$

Then the gradient is projected to trainable coordinates, globally clipped at radius $c$, and a deterministic optimizer $U$ is applied exactly once: $\operatorname{Step}(S, \xi) = U\big(S, C_c(P_T\, g)\big)$, where $S$ is the complete transition-relevant state (parameters, optimizer moments, step counter). One concrete masked-optimizer instance (masked AdamW) is included so "no decay on frozen coordinates" is a theorem, not a hope.

Formalization targets

The goal theorem packages exact one-step, trajectory, and restart preservation:

$$L_{\mathrm{tile}}(w_0) = L_\xi(w_0), \qquad g_{\mathrm{tile}} = \nabla L_\xi(w_0), \qquad \operatorname{Step}_{\mathrm{tile}}(S,\xi) = \operatorname{Step}_{\mathrm{mono}}(S,\xi),$$

and, by induction over a deterministic frame sequence, equality of the tiled and monolithic state trajectories, plus restart equality: saving at any completed update boundary $a \le n$ and reloading the round-tripped structural snapshot preserves the remaining trajectory,

$$\operatorname{Run}_{\mathrm{tile}}\big(\operatorname{reload}(S_a),\, a{:}n\big) = \operatorname{Run}_{\mathrm{mono}}(S_0,\, 0{:}n).$$

Twelve milestones build the result: partition flattening; weighted partition sums; the shared-path chain rule $\nabla[f \circ (\mathrm{id}, h)] = \nabla_1 f + Dh^{\top} \nabla_2 f$; linearity of the reverse pass over summed cotangents; the streaming-accumulator invariant and order independence; frozen-input differentiation with a concrete nonzero witness ($\theta \mapsto 6\theta$ through a frozen donor gives gradient $66$ at $\theta = 2$); projection–clipping–optimizer congruence; one-step equivalence; trajectory equivalence; checkpoint round trip; restart equivalence; and the full two-tile non-vacuity witness, whose tiled gradient is the nonzero $105/2$ while its detached (input-frozen) variant falsely gives $0$.

Significance

The result itself. Each clause rules out a real implementation bug: per-tile means change the objective on uneven tiles; updating after each tile reads moved parameters; clipping per tile differs from global clipping (gradients $10$ and $-9$ sum to $1$, but clipped-then-summed give $0$); a weights-only checkpoint loses optimizer state and changes the resumed trajectory. A verified tiled trainer — or a verified compiler schedule for one — can cite this mission's lemmas as its exactness certificate.

What formalizing it adds. The paper states Theorem T0 informally with a proof sketch; no machine-checked version exists. The load-bearing content is precisely the discipline of hypotheses: the certificates that per-occurrence gradients are genuine derivatives (partial derivatives alone do not give the chain rule), the single pre-update point for all tiles, and the complete transition state. Follow-on missions in the same vocabulary (source-byte integrity, masked normalization, matching invariance, numerical refinement, resource bounds) can import these definitions.

Difficulty

The analysis is elementary; the danger is vacuity and silent strengthening. A statement that hypothesizes "the tiled gradient is correct" proves nothing; one that hypothesizes differentiability of every branch at every point in a way no real frame satisfies proves nothing either. The encoding must let tiles be empty and uneven, let the occurrence set be empty (zero objective, not division by zero), quantify certificates only at the points used, and keep the optimizer deterministic-but-arbitrary. The counterexamples above are disproof fixtures: a correct statement survives all of them without ad-hoc exclusions.

Formalization scope

Parameters are EuclideanSpace ℝ (Fin d); gradients use HasGradientAt with genuine Fréchet derivatives paired by inner-product duality, and the reverse pass is ContinuousLinearMap.adjoint — no uninterpreted gradient oracle appears anywhere. Partitions are lists of Finsets; the accumulator is an executable fold. The checkpoint is a real-valued structural snapshot (coordinate lists); finite-byte codecs and floating-point associativity are explicitly out of scope — the theorem is exact-arithmetic. A trivializing formalization (defining the tiled gradient as the monolithic one, or hypothesizing the conclusion) is ruled out: milestone M12 exhibits a concrete instance with nonzero gradient that satisfies every hypothesis, and the detachment mutant shows the hypotheses have teeth.

Definitions are shared across the whole mission series under the VathekProof namespace: the frame, derivative-certificate, state, and optimizer files are reusable beyond this mission. Contributions welcome on any milestone; the witness computations (M06, M12) are self-contained entry points.

Selected references

• Davis, Vathek Graft: A Proof and Evidence Programme, mission-source white paper v1.0, 2026 (§4–6, Appendix A) — the theorem source; private document, cited by section.
• Vasilkovsky et al., DetIE: Multilingual Open Information Extraction Inspired by Object Detection, 2022. https://arxiv.org/abs/2206.12514
• See, Liu, Manning, Get To The Point: Summarization with Pointer-Generator Networks, ACL 2017. https://aclanthology.org/P17-1099/
• Hu et al., LoRA: Low-Rank Adaptation of Large Language Models, 2021. https://arxiv.org/abs/2106.09685
• Loshchilov, Hutter, Decoupled Weight Decay Regularization, ICLR 2019. https://arxiv.org/abs/1711.05101

Motivation

The book has characterized learnability through uniform convergence and through stability; Chapter 30 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), gives a third sufficient condition, compression: if a learning algorithm's output can be reconstructed from a small subsequence of $k$ training examples, then the error on the remaining examples estimates the true error, and the algorithm generalizes with a bound of order $k\log(m/\delta)/m$ (Theorem 30.2, Littlestone and Warmuth). The bound is a union bound over the $m^k$ possible index sequences of a held-out estimate that follows from Bernstein's inequality (Lemma 30.1), and in the consistent case it gives $L_D \le 8k\log(m/\delta)/m$ (Corollary 30.3). Classes admitting such compression schemes include axis-aligned rectangles ($k = 2d$), homogeneous halfspaces ($k = d$, through the minimal-norm point of the convex hull and Carathéodory's theorem), separating polynomials by reduction, and any margin-separable data ($k \le 1/\gamma^2$, through the Perceptron). Whether every class of finite VC dimension has a compression scheme of size $O(d)$ is Warmuth's problem, open when the book was written.

Setting

A sample $S = (z_1, \dots, z_m)$ is drawn i.i.d. from $D$; a selection rule picks $(i_1, \dots, i_k) \in [m]^k$ (repetitions allowed), a reconstruction map $B : Z^k \to H$ produces $A(S) = B(z_{i_1}, \dots, z_{i_k})$, and $V$ is the set of positions not selected, with $L_V$ the average loss over them. The loss takes values in $[0,1]$. A class $H$ has a compression scheme of size $k$ (Definition 30.4) if for every $m \ge 1$ there are such $A$ and $B$ with $B(S_{A(S)})$ correct on every sample labeled by a member of $H$; the unrealizable version (Definition 30.5) asks $B(S_{A(S)})$ to be an empirical risk minimizer on every sample.

Formalization targets

Goal: Theorem 30.2

For a $[0,1]$-valued loss, $k \ge 1$, $m \ge 2k$, any reconstruction map $B$ and any selection rule, with probability at least $1 - \delta$ over $S \sim D^m$,

$$L_D(A(S)) \le L_V(A(S)) + \sqrt{L_V(A(S))\,\frac{4k\log(m/\delta)}{m}} + \frac{8k\log(m/\delta)}{m}.$$

Milestones

Lemma 30.1 (the held-out Bernstein bound); Corollary 30.3 (the consistent case); Lemma 30.6 (realizable schemes give unrealizable schemes); the compression scheme of size $2d$ for axis-aligned rectangles (§30.2.1); the separation property of the minimal-norm point of the convex hull (§30.2.2). Further items: the size-$d$ scheme for homogeneous halfspaces and the margin scheme of §30.2.4.

Significance

Compression bounds are the cleanest generalization argument in the book: no complexity measure of the class enters, only the number of examples needed to encode the output, and the resulting bound is data-dependent through $L_V$. They explain why support vector machines and the Perceptron generalize in terms of the number of support vectors or updates, and they underlie the sample-compression view of learning that connects to Chapters 9 and 15. Lemma 30.6 shows that compression is robust to label noise in the binary case. The halfspace scheme is a small piece of convex geometry of independent interest, and Warmuth's question about VC classes, settled in the affirmative for finite size by Moran and Yehudayoff after the book appeared, remains open in the form $O(d)$.

Difficulty

Lemma 30.1 is Bernstein's inequality for the $n$ held-out losses with variance at most $L_D(h_T)$, followed by solving the resulting quadratic in $\sqrt{L_D}$ to move the risk from the right-hand side to $L_V$; the constant $4$ comes out of that step (the exact value is about $3.19$). Theorem 30.2 is a union bound over the $m^k$ index sequences with $\delta' = m^k\delta$, using $|V| \ge m - k \ge m/2$ and $\log(m^k/\delta') \le k\log(m/\delta')$, which needs $k \ge 1$; formally the event for the learner is contained in the union of the events of Lemma 30.1 for each fixed index sequence, so no measurability of the selection rule is needed. Corollary 30.3 is immediate. Lemma 30.6 applies the realizable scheme to the subsample on which an ERM hypothesis is correct. The rectangle scheme is bookkeeping about extremal coordinates. The halfspace scheme needs three facts: the minimal-norm point of the hull separates (a one-line perturbation argument), it lies on a face and hence is a convex combination of $d$ sample points (Carathéodory's theorem, in Mathlib, applied to a face), and it is the minimal-norm point of the hull of those $d$ points (uniqueness of the projection onto a convex set); the existence of the minimizer uses compactness of the hull. The margin scheme is the Perceptron convergence theorem of Mission VI applied to the batch algorithm, whose output is the sum of the updated examples.

Formalization scope

Samples are Fin m-indexed under Mission I's iidLaw, and probability statements bound the outer measure of the failure event. Lemma 30.1 splits a sample of size $k + n$ into its first $k$ and last $n$ entries; Theorem 30.2 takes an arbitrary selection rule $\mathrm{sel} : Z^m \to [m]^k$ and reconstruction map $B$, the held-out set being the positions not in the range of the selection, and requires $k \ge 1$ and $m \ge 1$ in addition to the book's $m \ge 2k$: for $k = 0$ the bound reads $L_D \le L_V$, which fails, and the book's derivation uses $k \ge 1$ in $\log(m^k/\delta') \le k\log(m/\delta')$. Compression schemes are defined for every $m \ge 1$, since for $m = 0$ there is no index to select, with indices allowed to repeat as in $[m]^k$ and with $B$'s outputs in $H$; the unrealizable version uses Mission XXIII's multiclass 0–1 loss. The halfspace results are stated for strictly separable $\pm1$-labeled samples, $y_i\langle w^\star, x_i\rangle > 0$, the book's "w.l.o.g. all labels positive" normalization; this avoids the boundary negatives that a realizable sample may contain under the $\operatorname{sign}(0)$ convention of Mission VI, and it is the setting in which the minimal-norm argument works. The scheme is stated as the existence of $d$ indices whose signed examples have a minimal-norm hull point separating the whole sample, which is the content of $A$ and $B$ without fixing how ties among faces are broken. Rectangles are closed boxes. The margin scheme uses Theorem 9.1's normalization.

Not stated: §30.2.3 (polynomials, a reduction), the bibliographic remarks, and the intermediate Carathéodory step as a separate item.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 30. doi:10.1017/CBO9781107298019
• N. Littlestone, M. K. Warmuth, Relating data compression and learnability, technical report, University of California, Santa Cruz, 1986.
• S. Floyd, M. K. Warmuth, Sample compression, learnability, and the Vapnik-Chervonenkis dimension, Machine Learning 21, 1995. doi:10.1007/BF00993593
• S. Ben-David, A. Litman, Combinatorial variability of Vapnik-Chervonenkis classes with applications to sample compression schemes, Discrete Applied Mathematics 86, 1998. doi:10.1016/S0166-218X(98)00000-6
• S. Moran, A. Yehudayoff, Sample compression schemes for VC classes, Journal of the ACM 63(3), 2016. doi:10.1145/2890490

Motivation

Chapter 17 introduced multiclass prediction; Chapter 29 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), asks the two questions the fundamental theorem answered for binary classes: which classes of multiclass predictors are PAC learnable with respect to the 0–1 loss, and with what sample complexity. Natarajan's dimension generalizes the VC dimension by shattering with two disagreeing label functions, and the multiclass fundamental theorem (Theorem 29.3) bounds the uniform-convergence, agnostic and realizable sample complexities in terms of it, up to logarithmic factors in the number of labels $k$; the only new ingredient in its proof is Natarajan's lemma, the multiclass substitute for Sauer's lemma. The chapter then computes or bounds the Natarajan dimension of the classes that matter, One-versus-All and general reductions to binary classifiers, and linear multiclass predictors (Theorem 29.7). Its last section is a warning: unlike the binary case, not all ERMs are equal, and with infinitely many labels a class can be learnable by one ERM and not by another, so learnability and uniform convergence come apart (Claim 29.9).

Setting

$H$ is a class of functions from $X$ to a finite label set $Y$ with $|Y| = k$. $C \subseteq X$ is shattered by $H$ if there are $f_0, f_1 : C \to Y$ with $f_0(x) \ne f_1(x)$ everywhere on $C$ such that every $B \subseteq C$ is realized by some $h \in H$ agreeing with $f_0$ on $B$ and with $f_1$ on $C \setminus B$ (Definition 29.1); $\operatorname{Ndim}(H)$ is the largest size of a shattered set (Definition 29.2). One-versus-All builds $T(\bar h)(x) = \operatorname{argmax}_i h_i(x)$ from $k$ binary classifiers, the smaller label on ties; a general reduction applies a rule $r : \{0,1\}^l \to [k]$ to $l$ binary classifiers; the linear class $H_\Psi$ predicts $\operatorname{argmax}_i\langle w, \Psi(x, i)\rangle$ for a class-sensitive feature map $\Psi : X \times [k] \to \mathbb{R}^d$ (29.1). The class of §29.4 has labels $P_f(X) \cup \{\ast\}$, the finite and cofinite subsets of $X$ plus a special label, and hypotheses $h_A(x) = A$ if $x \in A$ and $\ast$ otherwise; $A_{good}$ returns $h_\emptyset$ on an all-$\ast$ sample and $A_{bad}$ returns $h_{\{x_1, \dots, x_m\}^c}$.

Formalization targets

Goal: Theorem 29.3

There are absolute constants $C_1, C_2 > 0$ such that every class $H \subseteq Y^X$ with $\operatorname{Ndim}(H) = d$ satisfies

$$C_1\frac{d + \log(1/\delta)}{\epsilon^2} \le m^{UC}_H(\epsilon,\delta),\ m_H(\epsilon,\delta) \le C_2\frac{d\log k + \log(1/\delta)}{\epsilon^2}, \qquad C_1\frac{d + \log(1/\delta)}{\epsilon} \le m^{\mathrm{real}}_H(\epsilon,\delta) \le C_2\frac{d\log(kd/\epsilon) + \log(1/\delta)}{\epsilon},$$

the upper bounds by every ERM learner and the lower bounds for small $\epsilon, \delta$ and $d \ge 2$, in the format of Mission IV's Theorem 6.8.

Milestones

Lemma 29.4 (Natarajan: $|H| \le |X|^{\operatorname{Ndim}(H)}k^{2\operatorname{Ndim}(H)}$); Lemma 29.5 (the Natarajan dimension of One-versus-All is $O(kd\log(kd))$); Theorem 29.7 ($\operatorname{Ndim}(H_\Psi) \le d$); Claim 29.9(1) ($A_{good}$ needs $\frac1\epsilon\log\frac1\delta$ examples); Claim 29.9(2) ($A_{bad}$ fails with constant probability on $(|X|-1)/(6\epsilon)$ examples). Further items: the equality $\operatorname{Ndim} = \operatorname{VCdim}$ for two classes, and Lemma 29.6 for general reductions.

Significance

Theorem 29.3 is the multiclass fundamental theorem of Natarajan (1989) and Ben-David, Cesa-Bianchi, Haussler and Long (1995): finite Natarajan dimension characterizes multiclass learnability, and the sample complexity is linear in it, with the dependence on $k$ confined to logarithms. Natarajan's lemma is the combinatorial core, and the dimension bounds of §29.3 are what make the theorem usable: a One-versus-All scheme over a class of VC dimension $d$ costs $\tilde O(kd)$, and a linear multiclass predictor costs at most its number of parameters, so the multivector construction of Chapter 17 is learnable with $\tilde O(nk/\epsilon^2)$ examples. Claim 29.9 is a genuine phenomenon of Daniely, Sabato, Ben-David and Shalev-Shwartz (2011): in multiclass classification the choice of ERM matters, and the equivalence "learnable iff uniform convergence" of the binary theory is false, which is why Conjecture 29.10 about good ERMs is open in the form the chapter states it.

Difficulty

The equality with the VC dimension for two labels is a direct comparison of the two shattering definitions. Natarajan's lemma is a Sauer-type induction on $|X|$, in which a shattered set must be produced from two hypotheses that differ at a point; the exercise-level proof of the book becomes a careful double induction formally. Theorem 29.3's upper bounds follow the binary proof of Chapter 28 with Natarajan's lemma in place of Sauer's, hence Massart's lemma and Theorem 26.5 for the agnostic case and the double-sample argument for the realizable case; the lower bounds reduce to the binary ones by embedding a binary class into a multiclass one on a shattered set. These are long formal developments, and the theorem is stated with unspecified constants for that reason. Lemmas 29.5 and 29.6 are counting: a shattered $C$ has $2^{|C|} \le |H_C| \le |(H_{bin})_C|^k$, Sauer's lemma bounds the right side by $\big(\sum_{i \le d}\binom{|C|}{i}\big)^{k}$, and the resulting inequality is solved. For Lemma 29.5's printed $3kd\log(kd)$ this fails only at $(k, d) = (2, 1), (3, 1)$. There a shattered set splits by the label pair $\{f_0(x), f_1(x)\}$ into parts shattered by $\{B \setminus A : A, B \in H_{bin}\}$ (pairs $\{0, b\}$) or by $H_{bin}$ (other pairs). The first class has at most $31$ traces on $5$ points. Theorem 29.7 maps a shattered set into $\mathbb{R}^d$ by $\rho(x) = \Psi(x, f_0(x)) - \Psi(x, f_1(x))$, up to sign, and shows the image is shattered by homogeneous halfspaces; the tie-breaking rule decides which sign and which halfspace convention to use. Claim 29.9(1) is the bound $(1-\epsilon)^m \le \delta$; Claim 29.9(2) needs only that at most $(d-1)/2$ of the $d-1$ light points appear in the sample, an event of probability at least $1/3$ by Markov's inequality when $m \le (d-1)/(6\epsilon)$, which exceeds the claimed $e^{-1}/6$.

Formalization scope

Labels are an arbitrary finite type, shattering and the Natarajan dimension are stated with witnesses $f_0, f_1$ defined on all of $X$, and the dimension is a supremum in $\mathbb{N} \cup \{\infty\}$. The multiclass 0–1 loss, the ERM property, agnostic PAC learnability and uniform convergence are Mission I's generic notions; the realizable multiclass PAC property is defined here in the shape of Definition 3.1 with $D(\{h \ne f\})$ as the error, since Mission I's binary version is $\{0,1\}$-specific. Theorem 29.3 is stated exactly as Mission IV states Theorem 6.8, with existential constants, upper bounds for every ERM learner of a nonempty measurable class with the countable-approximation property (the measurability device of Remark 3.1), and lower bounds for $\epsilon < \epsilon_0$, $\delta < \delta_0$, $d \ge 2$. Argmax predictors, both One-versus-All and $H_\Psi$, break ties towards the smallest label; the book states this rule for One-versus-All, and some fixed rule is necessary for Theorem 29.7, since with arbitrary tie-breaking every function is an argmax predictor of the zero mapping. Lemmas 29.5 and 29.6 are stated per shattered set. Lemma 29.5 keeps the printed $3kd\log(kd)$, which is true although the book's step $|(H_{bin})_C| \le |C|^d$ fails for small $|C|$. Lemma 29.6 uses $2ld\log_2(2ld)$, which the counting supports, because the printed $3ld\log(ld)$ is false at $l = d = 1$. Theorem 29.3's uniform-convergence upper bound is stated for $d \ge 1$. At $d = 0$ the confidence term $\log(1/\delta)$ vanishes as $\delta \to 1$, the bound reaches $m = 1$, and a single example is not representative. The class of §29.4 has labels Option of the subtype of finite-or-cofinite sets, with the discrete σ-algebra, and the two ERMs are predicates fixing the output on all-$\ast$ samples; Claim 29.9(1) is stated for countable $X$ with measurable singletons and Claim 29.9(2) for finite $X$ of size at least $2$, with the proof's own distribution, $h_\emptyset$ as target, and every $\epsilon \in (0, 1/2)$ in place of the book's unspecified constant $a$.

Not stated: Corollary 29.8 (its lower bound $(k-1)(n-1)$ is cited, not proved), Conjecture 29.10, the exercises.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 29. doi:10.1017/CBO9781107298019
• B. K. Natarajan, On learning sets and functions, Machine Learning 4, 1989. doi:10.1007/BF00114804
• S. Ben-David, N. Cesa-Bianchi, D. Haussler, P. M. Long, Characterizations of learnability for classes of {0, …, n}-valued functions, Journal of Computer and System Sciences 50(1), 1995. doi:10.1006/jcss.1995.1008
• D. Haussler, P. M. Long, A generalization of Sauer's lemma, Journal of Combinatorial Theory A 71(2), 1995. doi:10.1016/0097-3165(95)90001-2
• A. Daniely, S. Sabato, S. Ben-David, S. Shalev-Shwartz, Multiclass learnability and the ERM principle, COLT 2011; Journal of Machine Learning Research 16, 2015.
• A. Daniely, S. Sabato, S. Shalev-Shwartz, Multiclass learning approaches: a theoretical comparison with implications, NIPS 2012.

Motivation

Chapter 6 stated the fundamental theorem of statistical learning: a binary class is learnable if and only if its VC dimension is finite, with sample complexity $\Theta((d + \ln(1/\delta))/\epsilon^2)$ in the agnostic case and $\Theta((d\ln(1/\epsilon) + \ln(1/\delta))/\epsilon)$ in the realizable case. Chapter 28 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), proves it. The agnostic upper bound is obtained from the Rademacher machinery of Chapter 26 with Sauer's lemma and Massart's lemma, up to a $\log(d/\epsilon)$ factor that only chaining removes (28.1). The agnostic lower bound comes in two parts: a two-point construction giving $m \ge 0.5\log(1/(4\delta))/\epsilon^2$, and a $d$-point construction giving $m \ge d/(512\epsilon^2)$ at confidence $1/8$, whose heart is Lemma 28.1, the optimality of the Maximum-Likelihood rule against the family of noisy distributions $D_b$. The realizable upper bound is proved through $\epsilon$-nets: with $m \ge \frac8\epsilon(2d\log(16e/\epsilon) + \log(2/\delta))$ examples a random sample hits every set of measure at least $\epsilon$ in the class (Theorem 28.3), so any hypothesis consistent with the sample has error below $\epsilon$. Mission IV states these bounds with unnamed constants; this mission gives the chapter's explicit ones.

Setting

$H$ is a class of functions $X \to \{0,1\}$ with the 0–1 loss and $\operatorname{VCdim}(H) = d$. For the upper bound, $A = \{(\mathbb{1}[h(x_i) \ne y_i])_i : h \in H\}$ is the loss set of a sample and $R(A)$ its Rademacher complexity. For the lower bounds, $C = \{c_1, \dots, c_d\}$ is a set shattered by $H$ and, for $b \in \{\pm1\}^d$ and $\rho \in (0,1)$, $D_b$ draws $c_i$ uniformly and labels it $b_i$ with probability $(1+\rho)/2$; for $d = 1$ these are the distributions $D_\pm$ of §28.2.1. The Maximum-Likelihood rule $A_{ML}$ predicts at each $c_i$ the majority of the labels seen at $c_i$. An $\epsilon$-net for $H$ with respect to $D$ is a sample meeting every $h \in H$ with $D(h) \ge \epsilon$ (Definition 28.2).

Formalization targets

Goal: Theorem 28.3

Let $\operatorname{VCdim}(H) = d$, $\epsilon \in (0,1)$, $\delta \in (0, 1/4)$ and $m \ge \frac8\epsilon\big(2d\log\frac{16e}{\epsilon} + \log\frac2\delta\big)$. Then with probability at least $1 - \delta$ over $S \sim D^m$, $S$ is an $\epsilon$-net for $H$.

Milestones

The two-sided deviation bound of §28.1 ($|L_D(h) - L_S(h)| \le 2\sqrt{(8d\log(em/d) + 2\log(4/\delta))/m}$ uniformly over $H$); the lower bound $m(\epsilon,\delta) \ge 0.5\log(1/(4\delta))/\epsilon^2$ of §28.2.1; Lemma 28.1; the lower bound $m(\epsilon, 1/8) \ge d/(512\epsilon^2)$ of §28.2.2; the realizable upper bound of §28.3 (ERM has error at most $\epsilon$ with probability $1 - \delta$ for the sample size of Theorem 28.3). Further items: the Rademacher bound $R(A) \le \sqrt{2d\log(em/d)/m}$, the explicit uniform-convergence sample complexity of §28.1, and the expectation lower bound $\rho/4$ of §28.2.2.

Significance

These are the theorems that make the VC dimension the right measure of learnability, with constants. The upper bounds show what the abstract machinery of Missions II, IV, XX buys when instantiated: Sauer plus Massart plus Theorem 26.5 gives the agnostic rate, and the double-sample symmetrization plus Sauer gives the realizable rate, sharper by a factor $1/\epsilon$ because $\epsilon$-nets need only one-sided control. The lower bounds are the No-Free-Lunch argument refined to quantify $\epsilon$ and $\delta$: the two-point distribution shows that confidence costs $\log(1/\delta)/\epsilon^2$, and the $d$-point family with Lemma 28.1 shows that the dimension costs $d/\epsilon^2$, through the exact optimality of majority voting and a binomial anti-concentration bound. Theorem 28.3 is also the basic $\epsilon$-net theorem of Haussler and Welzl, a result of independent importance in computational geometry.

Difficulty

The Rademacher bound is Sauer's lemma (Mission IV) plus Massart's lemma (Mission XX) with $\|a - \bar a\| \le \sqrt m$; the deviation bound is Theorem 26.5 applied to $\ell$ and $-\ell$ with a union bound; the explicit sample complexity is Lemma A.2, $x \ge 4a\log(2a) + 2b \Rightarrow x \ge a\log x + b$, which a formal proof must establish (the tangent inequality for $\log$ at $2a$). The two-point lower bound requires the binomial lower-tail estimate of Lemma B.11 and the algebra $\frac12(1 - \sqrt{1 - \sqrt{4\delta}}) \ge \delta$, valid for $\delta < 1/4$, the only nonvacuous range. Lemma 28.1 is a conditioning argument: fixing the instance indices and the labels off $c_i$, the contribution of $c_i$ is minimized by predicting the more likely $b_i$ given the labels at $c_i$, which is the majority; the formal proof must decompose the product measure $D_b^m$ over the positions $r$ with $x_r = c_i$. The expectation bound $\rho/4$ then needs Lemma B.11 again, $1 - e^{-a} \le a$, Jensen for $\sqrt{\cdot}$ and $\mathbb{E}[n_i] = m/d$, and the probability bound $1/8$ follows by Mission III's reverse Markov inequality with $\rho = 8\epsilon$. Theorem 28.3 is the double-sample argument: Claim 1 ($P[S \in B] \le 2P[(S,T) \in B']$, via a Chernoff bound that only needs $m\epsilon \ge 2\log 2$), Claim 2 (symmetrization by a random half, $P[(S,T) \in B'] \le e^{-\epsilon m/4}\tau_H(2m)$), Sauer's lemma, and Lemma A.2 once more. The realizable upper bound applies Theorem 28.3 to the error sets $\{x : h(x) \ne f(x)\}$, a class of the same VC dimension.

Formalization scope

All objects are those of the earlier missions: risks, samples and learners from Mission I, vcDim and the countable-approximation property PointwiseSeparable from Mission IV (the measurability device for suprema over $H$, used wherever a symmetrization or Rademacher argument is invoked), condLaw from Mission XIV for the distributions $D_b$, and rademacher, evalSet, lossClass from Mission XX. Probability statements bound the outer measure of the failure event under iidLaw. The Rademacher and deviation items require $m > d + 1$, the range in which Mission IV states Sauer's lemma in the form $(em/d)^d$; the explicit sample complexity of §28.1 implies this range, since its first term $432d\log(64d/\epsilon^2)/\epsilon^2$ dominates the possibly negative $8d\log(e/d)$, and Lemma A.2 holds for any real $b$, so the book's constants are used verbatim. The lower bounds take a shattered set as an injective $c : \mathrm{Fin}\ d \to X$ with the shattering property written out, use $D_b$ as condLaw of the uniform law on $C$, and state the excess risk against $\min_{h \in H}L_{D_b}(h)$ as $\exists h \in H$ with $L(h) + \epsilon \le L(A(S))$, or as a real infimum over $H$ in the expectation item; no measurability of the learner is needed because $D_b^m$ is atomic. Lemma 28.1 compares the sums over $b$ of the expected risks, the common term $\min_h L_{D_b}$ cancelling, for every majority rule with arbitrary tie-breaking. Theorem 28.3 and the realizable bound are stated for $\delta \in (0, 1/4)$, the theorem's own range; the realizable bound is the inner clause of Mission I's IsPACWith on that range rather than a sample-complexity function, since the theorem does not cover $\delta \ge 1/4$ with its formula.

Not stated: the realizable lower bound (an exercise), the remark that chaining removes the logarithm in (28.1), and the intermediate claims of the proof of Theorem 28.3 as separate items.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 28. doi:10.1017/CBO9781107298019
• V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and its Applications 16(2), 1971. doi:10.1137/1116025
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Learnability and the Vapnik-Chervonenkis dimension, Journal of the ACM 36(4), 1989. doi:10.1145/76359.76371
• D. Haussler, E. Welzl, ε-nets and simplex range queries, Discrete and Computational Geometry 2, 1987. doi:10.1007/BF02187876
• M. Anthony, P. L. Bartlett, Neural Network Learning: Theoretical Foundations, Cambridge University Press, 1999. doi:10.1017/CBO9780511624216