Optimization

Motivation

Many decision problems contain a constraint whose coefficients are an expectation under a probability vector that is not known exactly: an expected cost under uncertain scenario probabilities, an expected payoff of an asset under an estimated distribution, the expected demand in a newsvendor model. The probabilities are usually estimated from data, and a solution that is feasible for the estimate can be infeasible for the true distribution. Robust optimization protects against this by requiring the constraint to hold for every probability vector in an uncertainty region around the estimate.

A natural region is a ball in a φ-divergence, a family of statistical distances between probability vectors that contains the Kullback–Leibler divergence, the Burg entropy, the χ² distances, the Hellinger distance and the variation distance. Such balls arise as asymptotic confidence sets for the true distribution given observed frequencies (Pardo 2006), so the radius has a statistical meaning. Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) showed that the robust version of a linear constraint over such a ball is equivalent to a finite convex system involving the convex conjugate of φ. This reformulation is a standard tool in the later literature on distributionally robust optimization.

Setting

A φ-divergence function is a function $\phi:\mathbb R\to\mathbb R\cup\{+\infty\}$ that is convex on $[0,\infty)$, finite on $(0,\infty)$, and satisfies $\phi(1)=0$; the value $\phi(0)$ may be $+\infty$. Examples are $\phi(t)=t\log t-t+1$ (Kullback–Leibler), $\phi(t)=-\log t+t-1$ (Burg), $\phi(t)=(t-1)^2$ (modified χ²) and $\phi(t)=|t-1|$ (variation). For $p,q\in\mathbb R^m$ with $q>0$ the φ-divergence is

$$I_\phi(p,q)=\sum_{i=1}^m q_i\,\phi\!\left(\frac{p_i}{q_i}\right),$$

and the conjugate of $\phi$ is $\phi^*(s)=\sup_{t\ge0}\{st-\phi(t)\}$, a function with values in $\mathbb R\cup\{+\infty\}$.

Fix $a\in\mathbb R^n$, $B\in\mathbb R^{n\times m}$ with columns $b_i$, $\beta\in\mathbb R$, $C\in\mathbb R^{k\times m}$ with columns $c_i$, $d\in\mathbb R^k$, a nominal vector $q\in\mathbb R^m$ and a radius $\rho>0$. The uncertainty region is

$$U=\{p\in\mathbb R^m\mid p\ge0,\ Cp\le d,\ I_\phi(p,q)\le\rho\},$$

where the linear constraints $Cp\le d$ can encode $e^\top p=1$ and any further information on $p$. A decision $x\in\mathbb R^n$ satisfies the robust linear constraint if

$$(a+Bp)^\top x\le\beta\qquad\text{for all }p\in U. \tag{11}$$

Inequalities between vectors are componentwise throughout.

Formalization targets

Goal: Theorem 1

Assume $q>0$ and $q\in U$. Then $x$ satisfies (11) if and only if there are $\eta\in\mathbb R^k$ and $\lambda\in\mathbb R$ with

$$a^\top x+d^\top\eta+\rho\lambda+\lambda\sum_{i}q_i\,\phi^*\!\left(\frac{b_i^\top x-c_i^\top\eta}{\lambda}\right)\le\beta,\qquad\eta\ge0,\ \lambda\ge0, \tag{13}$$

where $0\phi^*(s/0):=0$ for $s\le0$ and $0\phi^*(s/0):=+\infty$ for $s>0$. The statement fixes no constants and no particular φ; it holds for the whole class.

Milestones

The proof in the paper has three displayed steps, which are the milestones. With the Lagrange function $L(p,\lambda,\eta)=(a+Bp)^\top x+\rho\lambda-\lambda I_\phi(p,q)+\eta^\top(d-Cp)$ and the dual objective $g(\lambda,\eta)=\sup_{p\ge0}L(p,\lambda,\eta)$:

1. Closing identity. For $\lambda\ge0$, $(\lambda\phi)^*(s)=\sup_{t\ge0}\{st-\lambda\phi(t)\}$ equals $\lambda\phi^*(s/\lambda)$, with the convention above at $\lambda=0$.
2. Eq. (15). For $q>0$ and $\lambda\ge0$,

$$g(\lambda,\eta)=a^\top x+d^\top\eta+\rho\lambda+\sum_{i=1}^m q_i(\lambda\phi)^*(b_i^\top x-c_i^\top\eta).$$

3. Duality. Under the hypotheses of Theorem 1, $x$ satisfies (11) if and only if $g(\lambda,\eta)\le\beta$ for some $\lambda\ge0$, $\eta\ge0$. This is split into the weak-duality direction and the strong-duality direction with attainment.

An additional item states Corollary 1, the specialization to $U=\{p\ge0,\ e^\top p=1,\ I_\phi(p,q)\le\rho\}$, where the multiplier $\eta\in\mathbb R$ of the normalization is free in sign.

Significance

Theorem 1 turns a semi-infinite constraint, one inequality for each $p$ in a convex set, into a single convex inequality in $(x,\lambda,\eta)$. The left side of (13) is jointly convex because $\lambda\phi^*(s/\lambda)$ is the perspective of a convex function. For the divergences of Table 4 of the paper the conjugate has a closed form, and the robust constraint becomes a linear, conic quadratic or self-concordant-barrier-representable constraint. The paper's applications (robust asset pricing, a robust newsvendor, and the tractability results of its §5) all start from this theorem, as do its Corollaries 2–5.

The theorem is proved in the paper; no machine-checked proof of it is known. Formalizing it adds a checked robust-counterpart theorem for φ-divergence regions, a reusable encoding of φ-divergences with extended values, and a strong-duality statement with attainment for convex programs whose constraint function takes the value $+\infty$ on the boundary of the orthant. It also records a correction: the paper states the theorem for $q\ge0$, and that version is false (see Formalization scope).

Difficulty

The separation step (15) and the conjugate identity are elementary manipulations of suprema, but in extended arithmetic: $\phi$ may be $+\infty$ at $0$, the conjugate may be $+\infty$, and the case $\lambda=0$ follows its own convention. The central difficulty is the duality step. The worst-case problem is a convex program whose constraint $I_\phi(p,q)\le\rho$ is not a finite convex function on a closed set: for the Burg or χ² divergence it is $+\infty$ on the boundary of the orthant, and $U$ itself need not be closed. Textbook statements of Slater-type strong duality usually assume finite-valued convex functions on a closed domain, so they do not apply as stated. The statement also requires attainment of the dual minimum, not only the absence of a duality gap, and this is the part a naive limiting argument does not give.

Formalization scope

Conventions:

• Vectors are Fin n → ℝ with the componentwise order; $B$ and $C$ are Matrix (Fin n) (Fin m) ℝ and Matrix (Fin k) (Fin m) ℝ; $b_i$ and $c_i$ are the columns fun j => B j i and fun j => C j i.
• $\phi$ is ℝ → EReal, never $-\infty$, finite on $(0,\infty)$, with $\phi(1)=0$ and convexity on $[0,\infty)$ written out in EReal. $\phi(0)=+\infty$ is allowed, so the Burg, χ² and J divergences are covered.
• $I_\phi(p,q)$, $\phi^*$, $(\lambda\phi)^*$, $L$, $g$ and the left side of (13) are EReal-valued. $\lambda\phi(t)$ is the EReal product, in which $0\cdot(+\infty)=0$. The term $\lambda\phi^*(s/\lambda)$ is defined by an explicit case split at $\lambda=0$, and $\lambda\sum_i q_i\phi^*(\cdot/\lambda)$ in (13) is read as $\sum_i q_i\,(\lambda\phi^*(\cdot/\lambda))$ with the convention applied term by term.
• The paper's $\max_{p\ge0}$ in $g$ is a supremum; $\min_{\lambda,\eta\ge0}g\le\beta$ is stated in its attained form, $\exists\,\lambda\ge0,\eta\ge0$ with $g(\lambda,\eta)\le\beta$.
• $m$ and $k$ may be $0$.

Corrected slip. The paper's standing assumption is $q\ge0$. The third equality of (15) substitutes $p_i=q_it$, which needs $q_i>0$, and Theorem 1 is false for $q\ge0$: with $m=k=2$, $n=1$, $\phi(t)=|t-1|$, $q=(1,0)$, both columns of $C$ equal to $(1,-1)^\top$, $d=(1,-1)$, $a=0$, $B=(0\ \ 1)$, $x=1$, $\rho=1$, $\beta=0$, the vector $p=(1/2,1/2)$ lies in $U$ and violates (11), while $\eta=0$, $\lambda=0$ satisfy (13). Every statement of the mission therefore assumes $q_i>0$ for all $i$. The hypothesis $q\in U$ (the paper's "such that $q\in U$") and $\rho>0$ are kept.

Ruled-out trivializations: a conjugate taken as a supremum over all $t\in\mathbb R$ of a real-valued φ with junk values at $t<0$ is a different function; computing the $\lambda=0$ term as $0\cdot\phi^*(s/0)$ with Lean's $s/0=0$ makes it identically $0$; a real-valued, everywhere finite φ silently excludes the Burg, χ² and J divergences; dropping $q\in U$ or $\rho>0$ removes the Slater point and changes the theorem. The mission's definitions avoid all four.

Needed infrastructure: suprema of EReal-valued families over half-lines and orthants, the interchange of a supremum over a product with a finite sum, and a Lagrangian strong-duality theorem with attainment for a convex program with finitely many affine inequality constraints and one convex, possibly infinite-valued, inequality constraint with a Slater point in the interior of its domain. That duality theorem, and the φ-divergence definitions, are reusable beyond this mission, in particular for the paper's Corollaries 2–5 and for other distributionally robust formulations. Contributions of any of these pieces as separate theorems are welcome.

Selected references

• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2):341–357, 2013. https://doi.org/10.1287/mnsc.1120.1641
• L. Pardo, Statistical Inference Based on Divergence Measures, Chapman & Hall/CRC, 2006. https://doi.org/10.1201/9781420034813
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

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

In PAC learning the learner receives a batch of examples, learns, and only then predicts. Online learning has no such separation: on each round the learner receives an instance, predicts its label, and then sees the true label, and the goal is to make few mistakes over the whole sequence, with no statistical assumption whatsoever on how the sequence is generated, adversarially if need be. Chapter 21 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), develops this model along the same lines as the PAC theory. In the realizable case, mistake bounds replace sample complexity, and a combinatorial dimension due to Littlestone, $\operatorname{Ldim}(H)$, characterizes the best achievable bound exactly (Lemmas 21.6 and 21.7), playing the role the VC dimension plays for PAC learning, with $\operatorname{VCdim}(H) \le \operatorname{Ldim}(H)$ and an arbitrarily large gap (Theorem 21.9). In the unrealizable case regret replaces excess risk; deterministic learners can be forced to regret $T/2$ (Cover), but randomized predictions restore sublinear regret through the Weighted-Majority algorithm of Littlestone, Warmuth and Vovk (Theorem 21.11). The chapter closes with online convex optimization, where Online Gradient Descent (Zinkevich) attains regret $O(\sqrt T)$ (Theorem 21.15), and with the online Perceptron, whose mistake bound follows from a round-specific surrogate loss (Theorem 21.16).

Setting

An online algorithm is a deterministic map from the history of past examples and the current instance to a prediction. For a sequence $S$ labeled by some $h^\star \in H$, $M_A(S)$ is the number of mistakes and $M_A(H)$ the supremum over all such sequences (Definition 21.1). The Consistent algorithm predicts with any hypothesis of the version space $V_t$ (the hypotheses consistent with the past), Halving with its majority label, and SOA with the label $r$ for which $\{h \in V_t : h(x_t) = r\}$ has the larger Littlestone dimension, ties to $1$. An $H$-shattered tree of depth $d$ assigns an instance to every node of a complete binary tree so that every labeling $(y_1, \dots, y_d)$ is realized by some $h \in H$ along the path it determines; $\operatorname{Ldim}(H)$ is the maximal such depth (Definitions 21.4–21.5). In the unrealizable case predictions are $p_t \in [0,1]$, the loss is $|p_t - y_t|$, and the regret against $h$ is $\sum_t |p_t - y_t| - \sum_t |h(x_t) - y_t|$ (21.1). Weighted-Majority maintains $w^{(t)}_i \propto \exp(-\eta\sum_{s<t} v_{s,i})$ over $d$ experts with costs $v_t \in [0,1]^d$ and pays $\langle w^{(t)}, v_t\rangle$. Online Gradient Descent on a closed convex $H$ predicts $w^{(t)}$, receives a convex $f_t$, takes a subgradient $v_t$ at $w^{(t)}$ and projects $w^{(t)} - \eta v_t$ back onto $H$; the online Perceptron is the special case $w^{(t+1)} = w^{(t)} + y_t x_t$ on rounds with $y_t\langle w^{(t)}, x_t\rangle \le 0$.

Formalization targets

Goal: Theorem 21.11

For $d \ge 1$ experts, cost vectors $v_t \in [0,1]^d$, $T > 2\log d$ and $\eta = \sqrt{2\log(d)/T}$,

$$\sum_{t=1}^T \langle w^{(t)}, v_t\rangle - \min_{i \in [d]}\sum_{t=1}^T v_{t,i} \le \sqrt{2\log(d)\,T}.$$

Milestones

Theorem 21.3 (Halving makes at most $\log_2|H|$ mistakes); Lemma 21.6 ($M_A(H) \ge \operatorname{Ldim}(H)$ for every $A$); Lemma 21.7 ($M_{\mathrm{SOA}}(H) \le \operatorname{Ldim}(H)$); Theorem 21.15 (the three regret bounds of Online Gradient Descent); Theorem 21.16 (the online Perceptron bound $|M| \le \sum_t f_t(w^\star) + R\|w^\star\|\sqrt{\sum_t f_t(w^\star)} + R^2\|w^\star\|^2$ and its separable case). Further items: Corollary 21.2, Theorem 21.9, Example 21.4, Cover's impossibility, Corollary 21.12 and the $\operatorname{Ldim}$ half of Theorem 21.10.

Significance

Corollary 21.8 is one of the cleanest characterizations in learning theory: the Littlestone dimension is exactly the optimal mistake bound, with SOA attaining it and Lemma 21.6 forbidding anything better. Theorem 21.11 is the engine of the unrealizable case and of a large part of online learning: the multiplicative-weights analysis with the potential $\log Z_t$ gives regret $\sqrt{2\log(d)T}$ against the best of $d$ experts, and with the experts of pp. 298–299 it yields Theorem 21.10, regret $\sqrt{2\operatorname{Ldim}(H)\log(eT)\,T}$ for any class of finite Littlestone dimension. Theorem 21.15 is the online counterpart of the SGD analysis of Chapter 14, and the derivation of Theorem 21.16 from it shows how a surrogate loss chosen per round turns a regret bound into a mistake bound, the Perceptron bound of Chapter 9 falling out as the separable case. On the platform, these items give the first online-learning model, reusing Mission X's subgradients and projections.

Difficulty

Corollary 21.2 and Theorem 21.3 are counting arguments on the version space, but formally they require tracking the version space along the history and the fact that a mistake by Halving halves it. Lemma 21.6 is the adversary argument: given a shattered tree, feed the instance at the current node and the label opposite to the prediction; the resulting sequence is labeled by some $h \in H$ by the shattering property, and the algorithm errs on every round. Lemma 21.7 needs the combinatorial core of the chapter: if both restricted version spaces had Littlestone dimension equal to $\operatorname{Ldim}(V_t)$, their shattered trees could be glued under a new root to a deeper tree. Theorem 21.9 builds a shattered tree with all nodes at depth $i$ equal to $x_i$; Example 21.4 builds the dyadic tree. Theorem 21.11's proof is the book's: $e^{-a} \le 1 - a + a^2/2$ for $a \ge 0$, $\log(1 - b) \le -b$, the telescoping potential $\log(Z_{t+1}/Z_t)$, the lower bound $\log Z_{T+1} \ge -\eta\min_i\sum_t v_{t,i}$, and the choice of $\eta$; the hypothesis $T > 2\log d$ makes $\eta < 1$. Corollary 21.12 is the reduction of hypotheses to experts, and Theorem 21.10 is the expert construction with the counting bound (21.4) $\sum_{L \le \operatorname{Ldim}} \binom{T}{L} \le (eT/\operatorname{Ldim})^{\operatorname{Ldim}}$ (Lemma A.5) and Lemma 21.13, which simulates SOA on the labels of $h$; small horizons are covered by the trivial bound $\text{regret} \le T$. Theorem 21.15 is the telescoping argument of Lemma 14.1 with the projection lemma of Chapter 14 at every step; Theorem 21.16 applies it to $f_t = \mathbb{1}[t \in M][1 - y_t\langle w, x_t\rangle]_+$ with $\eta = \|w^\star\|/(R\sqrt{|M|})$ and solves the quadratic inequality (21.6).

Formalization scope

Online algorithms are deterministic functions List (X × Y) → X → Y; a sequence is Fin T-indexed and the history at round $t$ is its first $t$ examples. Mistake bounds and the Littlestone dimension are suprema in ℕ∞, so mistakeBound, ldim and their comparisons are meaningful when infinite. Shattered trees are indexed by paths rather than by the book's node numbers $i_t = 2^{t-1} + \sum_{j<t} y_j 2^{t-1-j}$, whose binary expansion is exactly the path; the two descriptions are the same tree. Halving and SOA break ties towards $1$ as in the book; Consistent is stated as a property of an algorithm. The unrealizable case uses real-valued predictions with the loss $|p_t - y_t|$ as the book does, and the theorems of that section assert the existence of an algorithm for each horizon $T$, because Weighted-Majority takes $T$ as input. Weighted-Majority's distribution is written in unrolled form, $w^{(t)}_i \propto \exp(-\eta\sum_{s<t}v_{s,i})$, which is the update rule iterated from $\tilde w^{(1)} = (1, \dots, 1)$. Theorem 21.10 is stated for classes with $\operatorname{Ldim}(H) < \infty$ and in its $\operatorname{Ldim}(H)\log(eT)$ form, the $\log|H|$ form being Corollary 21.12; its lower bound, proved in Ben-David, Pál and Shalev-Shwartz (2009), is not stated. Online Gradient Descent is driven by a subgradient selector $g_t(w) \in \partial f_t(w)$ (Mission X's global subgradients), from $w^{(0)} = 0$, on a closed convex $H$ containing the comparator; the Lipschitz parts take LipschitzWith ρ (f t) and $T \ge 1$. The Perceptron's $M$ is the set of update rounds $y_t\langle w^{(t)}, x_t\rangle \le 0$, which contains every prediction mistake whatever $\operatorname{sign}(0)$ is and is the set the book's derivation actually uses; $R$ is any bound on $\|x_t\|$ for $t < T$. Cover's impossibility is stated for deterministic $\{0,1\}$-valued algorithms, the setting in which the book states it.

Not stated: the Doubling Trick (Exercise 4), Exercises 1–3 (specific tight examples), the SOA-based Expert algorithm as a separate definition (it is internal to the proof of Theorem 21.10), Lemma 21.13 and Corollary 21.14 as items, and the lower bound of Theorem 21.10.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 21. doi:10.1017/CBO9781107298019
• N. Littlestone, Learning quickly when irrelevant attributes abound: a new linear-threshold algorithm, Machine Learning 2, 1988. doi:10.1007/BF00116827
• N. Littlestone, M. K. Warmuth, The weighted majority algorithm, Information and Computation 108(2), 1994. doi:10.1006/inco.1994.1009
• S. Ben-David, D. Pál, S. Shalev-Shwartz, Agnostic online learning, COLT 2009.
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003.
• N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. doi:10.1017/CBO9780511546921
• S. Shalev-Shwartz, Online learning and online convex optimization, Foundations and Trends in Machine Learning 4(2), 2011. doi:10.1561/2200000018

Motivation

Binary classification is the exception in practice; most prediction tasks have many labels, a structured label space, or ask for a ranking. Chapter 17 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) extends linear predictors to these settings through one idea: a class-sensitive feature mapping $\Psi(x, y)$ that scores a candidate label, with the prediction $h_w(x) = \operatorname{argmax}_y \langle w, \Psi(x, y)\rangle$. A cost-sensitive loss $\Delta(y', y)$ replaces the 0–1 loss, and the generalized hinge loss (17.3), $\max_{y'}(\Delta(y', y) + \langle w, \Psi(x, y') - \Psi(x, y)\rangle)$, is its convex surrogate: it upper bounds $\Delta(h_w(x), y)$, is tight under margin, and is convex and Lipschitz in $w$. Multiclass SVM is then regularized loss minimization for this loss, and Corollaries 17.1 and 17.2 transfer the guarantees of Chapters 13 and 14 with no dependence on the number of labels. The same construction handles ranking: a linear ranking predictor scores each item, the Kendall tau loss has a pairwise hinge surrogate, and the NDCG surrogate reduces to an assignment problem whose linear relaxation is exact by the Birkhoff–von Neumann theorem (Claim 17.3, Lemma 17.4).

Setting

Labels form a finite nonempty type $Y$; the feature mapping takes values in $\mathbb{R}^d$ as in Mission VI, and the RLM rule and the SGD of Chapters 13 and 14 are those of Missions IX and X. An argmax predictor for $(\Psi, w)$ is any $h$ with $h(x)$ maximizing $\langle w, \Psi(x, y)\rangle$; a canonical one is fixed by choosing among the maximizers, and likewise a canonical maximizer $\hat y$ in the generalized hinge loss, which gives the SGD direction $\Psi(x, \hat y) - \Psi(x, y)$. The cost $\Delta$ is nonnegative with $\Delta(y, y) = 0$. For ranking, an example is a list $x_1, \dots, x_r$ of instances with a score vector $y \in \mathbb{R}^r$; the linear predictor is $(\langle w, x_i\rangle)_i$, the Kendall tau loss is the fraction of pairs ordered differently, using the three-valued real sign, and permutations of $[r]$ are Mathlib's permutations of Fin r, with doubly stochastic and permutation matrices from Mathlib.

Formalization targets

Goal: Corollary 17.1

For $D$ over $X \times Y$, $\|\Psi(x, y)\| \le \rho/2$, $B > 0$, and the Multiclass SVM learner with $\lambda = \sqrt{2\rho^2/(B^2 m)}$: $\mathbb{E}_S[L^\Delta_D(h_w)] \le \mathbb{E}_S[L^{g\text{-}hinge}_D(w)]$, and for every $u$ with $\|u\| \le B$, $\mathbb{E}_S[L^{g\text{-}hinge}_D(w)] \le L^{g\text{-}hinge}_D(u) + \sqrt{8\rho^2B^2/m}$.

Milestones

Equation (17.3). The generalized hinge loss bounds $\Delta(h_w(x), y)$ for every argmax predictor, equals it under the margin condition, and is convex and $\rho$-Lipschitz in $w$ with $\rho = \max_{y'}\|\Psi(x, y') - \Psi(x, y)\|$.

Corollary 17.2. SGD for multiclass learning with $T \ge B^2\rho^2/\epsilon^2$ examples has $\mathbb{E}[L^\Delta_D(h_{\bar w})] \le \mathbb{E}[L^{g\text{-}hinge}_D(\bar w)] \le L^{g\text{-}hinge}_D(u) + \epsilon$ for every $\|u\| \le B$.

Equation (17.7). The permutation induced by sorting $y$ maximizes $\sum_i v_i y_i$ over permutation vectors (the rearrangement inequality).

Claim 17.3. The doubly stochastic matrices are the convex hull of the permutation matrices.

Lemma 17.4. The assignment LP over doubly stochastic matrices has an optimal solution that is a permutation matrix.

Further items: Remark 17.2 (the binary case recovers the hinge loss) and the Kendall tau surrogate of §17.4.1 with its convexity and Lipschitz constant.

Significance

The generalized hinge loss is the device that lets the whole convex-learning machinery of Part II run on arbitrary finite label sets and on structured outputs, and Remark 17.3's observation that the bounds of Corollaries 17.1 and 17.2 do not depend on $|Y|$ is what makes structured prediction (§17.3) and ranking with exponentially many labelings feasible. The ranking half of the chapter shows the pattern at work: the induced permutation is an argmax over a combinatorial set (17.7), so the NDCG loss admits a generalized hinge surrogate, and its subgradient is an assignment problem, solvable by the Hungarian method or, thanks to Birkhoff–von Neumann, by linear programming.

Nothing here is machine-checked except that Mathlib contains the Birkhoff–von Neumann theorem, which the corresponding item restates in the book's form. The statements are faithful with the clarifications that ties are broken canonically, that the Kendall tau surrogate is stated for tie-free score vectors (the book's rewriting of the pairwise indicator assumes $\operatorname{sign}(y_i - y_j) \ne 0$), and that Corollary 17.1 is stated with the measurability conventions of Mission IX.

Difficulty

Remark 17.2 is a two-element maximum and the entry point, and Equation (17.7) is Mathlib's rearrangement inequality for monovarying functions. The properties of the generalized hinge loss are elementary: the bound by choosing $y' = h_w(x)$, the equality by showing every term is at most $0$ and the term $y' = y$ is $0$, convexity as a maximum of affine functions, and the Lipschitz bound by Cauchy–Schwarz on each term. Corollary 17.1 is Mission IX's Corollary 13.9 for the generalized hinge loss, which requires verifying convexity, the $\rho$-Lipschitz property from $\|\Psi\| \le \rho/2$, nonnegativity and boundedness at the origin (by $\max\Delta$, finite), the measurability of the loss and of the canonical argmax predictor as functions of $(w, x)$, and the pointwise comparison with the $\Delta$-loss; Corollary 17.2 is the same with Mission X's Corollary 14.12 and Claim 14.6 for the subgradient. The Kendall tau surrogate is the pairwise hinge bound under no ties, plus the convexity and Lipschitz constant of an average of hinge terms. Lemma 17.4 follows from Birkhoff–von Neumann by the averaging argument of the book, or directly from the finiteness of the permutation matrices together with the fact that a linear function on a convex hull is minimized at an extreme point.

Formalization scope

The label set is finite, so maxima over $Y$ are attained and the losses are well defined; maximizers are chosen canonically, and every statement about argmax predictors holds for any choice. The multivector and TF-IDF constructions of §17.2.1, the reductions of §17.1, structured output prediction (§17.3), the NDCG loss and its surrogate (17.8), and bipartite ranking (§17.5) are not stated; the NDCG construction would need the sorting permutation and the discount function and is left for a later revision. Exercises are not stated except 17.4 through Equation (17.7).

Trivializing readings are excluded: the $\Delta$-risk in Corollaries 17.1 and 17.2 is that of a genuine argmax predictor, the Lipschitz constants are the book's, and the assignment lemma asserts optimality against every doubly stochastic matrix. Welcome contributions: the Lipschitz constant of a maximum of affine functions, the measurability of a canonical argmax over a finite label set, and the extreme-point argument of Lemma 17.4.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 17. doi:10.1017/CBO9781107298019
• K. Crammer, Y. Singer, On the algorithmic implementation of multiclass kernel-based vector machines, Journal of Machine Learning Research 2, 2001.
• I. Tsochantaridis, T. Joachims, T. Hofmann, Y. Altun, Large margin methods for structured and interdependent output variables, Journal of Machine Learning Research 6, 2005.
• G. Birkhoff, Tres observaciones sobre el algebra lineal, Universidad Nacional de Tucumán, Revista A 5, 1946.
• H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2, 1955. doi:10.1002/nav.3800020109

Motivation

Chapter 15 bounded the sample complexity of large-margin halfspaces by the norms of the data and of the separator, independently of the dimension. Chapter 16 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) removes the remaining obstacle to using halfspaces in very high-dimensional feature spaces: computation. After embedding the data by a feature map $\psi$ into a Hilbert space, every SVM-like problem has the form $\min_w f(\langle w, \psi(x_1)\rangle, \dots, \langle w, \psi(x_m)\rangle) + R(\|w\|)$ (16.2), and the representer theorem (Theorem 16.1) says that an optimal solution lies in the span of the mapped examples. Consequently the problem can be rewritten in terms of the $m$ coefficients and the kernel $K(x, x') = \langle\psi(x), \psi(x')\rangle$ alone (16.3): this is the kernel trick. The chapter exhibits the polynomial and Gaussian kernels (Examples 16.1 and 16.2), characterizes the functions that are kernels as the positive semidefinite ones (Lemma 16.2), and shows that the SGD solver for Soft-SVM of §15.5 can be run entirely on kernel evaluations (Lemma 16.3).

Setting

A feature map $\psi : X \to F$ takes values in a real Hilbert space, a complete real inner product space; its kernel is $K(x, x') = \langle\psi(x), \psi(x')\rangle$, and a function $K$ implements an inner product in some Hilbert space if it is the kernel of some feature map into some Hilbert space, quantified existentially in the universe of the domain. The Gram matrix of a sample is $G_{ij} = K(x_i, x_j)$. The general objective (16.2) is $f(\langle w, \psi(x_1)\rangle, \dots, \langle w, \psi(x_m)\rangle) + R(\|w\|)$ with $f$ arbitrary and $R$ nondecreasing on $[0, \infty)$. The SGD procedure of §15.5 in the feature space keeps $\theta^{(t)}$ with $w^{(t)} = \theta^{(t)}/(\lambda(t+1))$ (iterates indexed from $0$) and, at each step, for the chosen index $i$, adds $y_i\psi(x_i)$ to $\theta$ when $y_i\langle w^{(t)}, \psi(x_i)\rangle < 1$; its kernelized version keeps coefficients $\beta^{(t)}$ with $\alpha^{(t)} = \beta^{(t)}/(\lambda(t+1))$ and tests $y_i\sum_j\alpha^{(t)}_j K(x_j, x_i) < 1$. Both are driven by the same sequence of chosen indices, which stands for the uniformly random choices of the book.

Formalization targets

Goal: Theorem 16.1 (Representer Theorem)

If $R$ is nondecreasing on $[0,\infty)$ and the problem (16.2) has an optimal solution, then there is $\alpha \in \mathbb{R}^m$ such that $\sum_i \alpha_i\psi(x_i)$ is an optimal solution.

Milestones

Equation (16.3). For $w = \sum_j\alpha_j\psi(x_j)$ the objective equals $f\big(\sum_j\alpha_jK(x_j, x_1), \dots\big) + R\big(\sqrt{\sum_{i,j}\alpha_i\alpha_jK(x_j, x_i)}\big)$.

Example 16.1. The polynomial kernel $(1 + \langle x, x'\rangle)^k$ on $\mathbb{R}^n$ is $\langle\psi(x), \psi(x')\rangle$ for the monomial map into $\mathbb{R}^{(n+1)^k}$.

Example 16.2. On $\mathbb{R}$, the map $\psi(x)_n = e^{-x^2/2}x^n/\sqrt{n!}$ into $\ell^2$ has $\langle\psi(x), \psi(x')\rangle = e^{-(x-x')^2/2}$; the Gaussian kernel $e^{-\|x-x'\|^2/(2\sigma)}$ on $\mathbb{R}^n$ is a kernel for every $\sigma > 0$.

Lemma 16.2. A symmetric $K$ is a kernel iff all its Gram matrices are positive semidefinite.

Lemma 16.3. The kernelized SGD reproduces the feature-space SGD: $\theta^{(t)} = \sum_j\beta^{(t)}_j\psi(x_j)$ for all $t$, hence the outputs coincide.

Further items: Exercise 16.3 (kernel ridge regression: minimizers of the coefficient objective give minimizers of the ridge objective, and $(2\lambda mI + G)\alpha = y$ gives one), Exercise 16.4 ($\min\{x, x'\}$ is a kernel), Exercise 16.6 (the nearest-class-mean rule is a halfspace).

Significance

The representer theorem is the reason kernel methods exist: it reduces an optimization over an arbitrary Hilbert space to one over $\mathbb{R}^m$, and Lemma 16.2 says the reduction needs nothing but a positive semidefinite similarity function, so one may design the kernel directly, as in the string example of §16.2.1. Lemma 16.3 makes the connection to Chapter 14 concrete: a first-order method never leaves the span of the examples, so it too can be run on the Gram matrix. Together with Chapter 15, the chapter closes the book's treatment of linear predictors: expressive through the embedding, statistically controlled through the margin, and computable through the kernel.

Nothing here is machine-checked. The statements are faithful to the book with two clarifications: the representer theorem assumes the existence of an optimal solution, which the book's proof also assumes, and the kernel-SGD equivalence is stated for a fixed sequence of chosen indices, which is the content of the book's inductive proof.

Difficulty

Equation (16.3) and Exercise 16.6 are inner-product algebra and the entry points. The representer theorem needs the orthogonal decomposition $w^\star = \sum_i\alpha_i\psi(x_i) + u$ with $u$ orthogonal to the span, which is available in Mathlib for the finite-dimensional, hence complete, subspace spanned by the $\psi(x_i)$, together with the Pythagorean identity and the monotonicity of $R$. Example 16.1 is the multinomial expansion of $(1 + \langle x, x'\rangle)^k$ as a sum over index vectors, packaged as an inner product in the Euclidean space indexed by $\{0, \dots, n\}^k$. Example 16.2 needs the summability of $x^n(x')^n/n!$ and the exponential series, and, for the general Gaussian kernel, either an explicit construction or Lemma 16.2 together with the positive semidefiniteness of the Gaussian Gram matrix. Lemma 16.2 in the nontrivial direction is the construction of the reproducing kernel Hilbert space: the pre-Hilbert space of finite combinations of the functions $K(\cdot, x)$, the inner product defined through $K$, its well-definedness and positive definiteness from the Gram matrices, and the completion, which Mathlib provides for inner product spaces. Lemma 16.3 is an induction on $t$ with the identity $\langle w^{(t)}, \psi(x_i)\rangle = \sum_j\alpha^{(t)}_jK(x_j, x_i)$. Exercise 16.3 combines the representer theorem with the identity between the two objectives on the span and the first-order condition for a convex quadratic; Exercise 16.4 needs a feature map such as $\psi(x) = (\mathbb{1}[1 \le j \le x])_j$, or the positive semidefiniteness of the min matrix.

Formalization scope

Hilbert spaces are real, complete inner product spaces; the existential in IsKernel ranges over Hilbert spaces in the universe of the domain, which the reproducing kernel construction respects. The objective (16.2) has real-valued $f$, so the hard-SVM instance with $f \in \{0, \infty\}$ is not covered by the representer item as stated. The SGD procedures are deterministic given the index sequence; the random choice of indices is not modelled, exactly as in Lemma 16.3's proof. The string kernel of §16.2.1 and Exercise 16.1, the kernelized Perceptron (Exercise 16.2), Exercise 16.5 and part (2) of Exercise 16.6 are not stated.

Trivializing readings are excluded: the representer theorem asserts optimality against every $w$, Lemma 16.2 is a biconditional with symmetry assumed as the book does, and the kernels of the examples are exhibited with explicit feature spaces where the book gives them. Welcome contributions: the orthogonal decomposition against a finite span, the multinomial identity of Example 16.1, and the reproducing kernel Hilbert space construction behind Lemma 16.2.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 16. doi:10.1017/CBO9781107298019
• B. Schölkopf, R. Herbrich, A. J. Smola, A generalized representer theorem, Proceedings of COLT, 2001. doi:10.1007/3-540-44581-1_27
• N. Aronszajn, Theory of reproducing kernels, Transactions of the American Mathematical Society 68(3), 1950. doi:10.1090/S0002-9947-1950-0051437-7
• B. Schölkopf, A. J. Smola, Learning with Kernels, MIT Press, 2002.
• M. A. Aizerman, E. M. Braverman, L. I. Rozonoer, Theoretical foundations of the potential function method in pattern recognition learning, Automation and Remote Control 25, 1964.

Motivation

The sample complexity of learning halfspaces in $\mathbb{R}^d$ grows with $d$, which is bad news when features are many or infinite. Chapter 15 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) introduces the support vector machine, the learning rule that replaces dimension by geometry. Among the halfspaces separating a sample, Hard-SVM picks the one of largest margin, the distance from the hyperplane to the nearest example (Claim 15.1, Lemma 15.2); if the data are separable with margin $\gamma$ and lie in a ball of radius $\rho$, the resulting classifier has error $O(\rho/(\gamma\sqrt m))$ whatever the dimension (Theorem 15.4), and the Perceptron of Chapter 9 makes at most $(\rho/\gamma)^2$ updates (Remark 15.1). Soft-SVM drops separability by allowing slack variables, and Claim 15.5 identifies it with regularized hinge-loss minimization, so that the stability theory of Chapter 13 applies: the hinge loss is $\|x\|$-Lipschitz (Claim 15.6), and Corollary 15.7 gives an expected-risk bound depending only on the norms of the data and of the comparison halfspace. The chapter closes with the optimality conditions that explain the name: the Hard-SVM solution is a combination of the examples on the margin (Theorem 15.8, via the Fritz John conditions, Lemma 15.9).

Setting

Vectors live in $\mathbb{R}^d$ as in Mission VI; labels are real numbers, with $y \in \{\pm 1\}$ as a hypothesis wherever the book needs it. A sample is linearly separable if some halfspace $(w, b)$ has $y_i(\langle w, x_i\rangle + b) > 0$ for all $i$, and the margin of $(w, b)$ on the sample is $\min_i y_i(\langle w, x_i\rangle + b)$. Hard-SVM solutions are minimizers of $\|w\|$ subject to $y_i(\langle w, x_i\rangle + b) \ge 1$, formalized as a relation; the minimizer is unique whenever the constraints are feasible, and the homogenous version sets $b = 0$. A distribution over $\mathbb{R}^d \times \{\pm 1\}$ is separable with a $(\gamma, \rho)$-margin if some unit $w^\star$ (and $b^\star$) has $y(\langle w^\star, x\rangle + b^\star) \ge \gamma$ and $\|x\| \le \rho$ almost surely. Soft-SVM is the problem $\lambda\|w\|^2 + \frac1m\sum\xi_i$ under $y_i(\langle w, x_i\rangle + b) \ge 1 - \xi_i$, $\xi_i \ge 0$; its homogenous form is the regularized loss minimization rule of Mission IX for the hinge loss $\max\{0, 1 - y\langle w, x\rangle\}$, and the 0–1 loss is $\mathbb{1}[y\langle w, x\rangle \le 0]$. Expectations over samples are integrals against $D^m$, with the measurability conventions of Mission IX.

Formalization targets

Goal: Corollary 15.7, last part

For $D$ on $\{\|x\| \le \rho\} \times \{\pm 1\}$ almost surely, $B > 0$, and the Soft-SVM learner with $\lambda = \sqrt{2\rho^2/(B^2 m)}$: $\mathbb{E}_S[L^{0-1}_D(A(S))] \le \mathbb{E}_S[L^{hinge}_D(A(S))]$, and for every $w$ with $\|w\| \le B$, $\mathbb{E}_S[L^{hinge}_D(A(S))] \le L^{hinge}_D(w) + \sqrt{8\rho^2 B^2/m}$.

Milestones

Claim 15.1. The distance from $x$ to $\{v : \langle w, v\rangle + b = 0\}$ with $\|w\| = 1$ is $|\langle w, x\rangle + b|$.

Lemma 15.2. For a sample with both labels present, the normalized Hard-SVM output has unit norm and margin at least that of every unit-norm halfspace.

Theorem 15.4. Under homogenous $(\gamma, \rho)$-separability, with probability at least $1 - \delta$ the 0–1 risk of the Hard-SVM output is at most $\sqrt{4(\rho/\gamma)^2/m} + \sqrt{2\log(2/\delta)/m}$.

Claim 15.5. Every feasible slack vector has average at least the hinge loss, and the hinge losses are feasible slacks.

Claim 15.6. For $y \in \{\pm 1\}$, $w \mapsto \max\{0, 1 - y\langle w, x\rangle\}$ is $\|x\|$-Lipschitz.

Corollary 15.7, first parts. For every $u$, $\mathbb{E}_S[L^{hinge}_D(A(S))]$ and $\mathbb{E}_S[L^{0-1}_D(A(S))]$ are at most $L^{hinge}_D(u) + \lambda\|u\|^2 + 2\rho^2/(\lambda m)$.

Theorem 15.8. The homogenous Hard-SVM solution is $\sum_{i \in I}\alpha_i x_i$ with $I = \{i : |\langle w_0, x_i\rangle| = 1\}$.

Lemma 15.9. Fritz John conditions, in the correct form with a multiplier on $\nabla f$.

Further items: Exercise 15.1 (the two Hard-SVM formulations agree) and Exercise 15.2 (the Perceptron makes at most $(\rho/\gamma)^2$ updates).

Significance

SVM is the bridge between the statistical theory of Part I and the kernel methods of Chapter 16: because the bounds of Theorem 15.4 and Corollary 15.7 involve only $\rho$, $\gamma$ and $B$, the same algorithm can be run after an embedding into a huge or infinite-dimensional feature space, and Theorem 15.8, that the solution lies in the span of the examples, is what makes the embedding computable. Corollary 15.7 is also the first place where the abstract machinery of Chapter 13 is applied to a specific learning rule.

Nothing here is machine-checked. One correction is built in: the Fritz John lemma is stated with the multiplier $\alpha_0 \ge 0$ on $\nabla f(w^\star)$ and nonnegative multipliers not all zero, since the printed form, with $\nabla f(w^\star)$ unweighted and $\alpha$ unrestricted, fails already for $f(w) = w$ and $g_1(w) = w^2$ on the line. Theorem 15.8 is unaffected: its constraints are affine, so the multiplier on $\nabla f$ can be taken to be $1$.

Difficulty

Claim 15.6 and Claim 15.5 are short inequalities and the intended entry points, and Exercise 15.2 is Theorem 9.1 of Mission VI with $B \le 1/\gamma$ and $R \le \rho$. Claim 15.1 is the book's computation with the foot of the perpendicular $v = x - (\langle w, x\rangle + b)w$ and a Pythagorean inequality for every other point of the hyperplane, packaged as an infimum distance. Lemma 15.2 is the rescaling argument of the book, together with the observation that both labels force $w_0 \ne 0$; Exercise 15.1 needs the positivity of the optimal margin on a separable sample. Corollary 15.7 is Corollaries 13.8 and 13.9 of Mission IX for the hinge loss, whose Lipschitz constant is $\|x\|$ only on the support of $D$, so the stability argument must be run with the almost-sure bound; the 0–1 clause is the pointwise inequality $\ell_{0-1} \le \ell_{hinge}$. Theorem 15.4 is the content of §26.3: Rademacher complexity of the class of norm-bounded halfspaces, the contraction lemma for the ramp loss, the observation that the Hard-SVM output has zero ramp loss on the sample and norm at most $1/\gamma$, and a concentration step, all of which will be items of the Rademacher mission. Theorem 15.8 is the KKT theorem for a strictly convex quadratic with affine constraints (Slater's condition holds), and Lemma 15.9 is the general Fritz John theorem for differentiable data, whose proof goes through a separation or penalty argument; neither is in Mathlib.

Formalization scope

Hard-SVM and Soft-SVM are relations and learners, not programs; the margin is a real infimum over the sample; the ramp loss is defined but its bounds belong to Chapter 26. Theorem 15.4 is stated for any learner that returns the Hard-SVM solution whenever the sample is feasible, which is almost surely the case under the margin assumption, and bounds the failure event in outer measure. Corollary 15.7 carries the measurability conventions of Mission IX. The Fritz John lemma is stated correctly rather than as printed. The duality of §15.4, the SGD implementation of §15.5 (whose guarantee needs the trajectory bound of §14.5.3 rather than Theorem 14.11 as stated in Mission X), Exercises 15.3 and 15.4, and Remark 15.2 are not stated.

Trivializing readings are excluded: both labels must be present for the normalized Hard-SVM output, the margin assumption and the support condition are almost sure with respect to $D$, and the risks are genuine integrals. Welcome contributions: the uniqueness of the Hard-SVM minimizer, the KKT conditions for affine constraints, and the pointwise comparison of the 0–1, ramp and hinge losses.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 15. doi:10.1017/CBO9781107298019
• C. Cortes, V. Vapnik, Support-vector networks, Machine Learning 20(3), 1995. doi:10.1007/BF00994018
• B. E. Boser, I. M. Guyon, V. N. Vapnik, A training algorithm for optimal margin classifiers, Proceedings of COLT, 1992. doi:10.1145/130385.130401
• F. John, Extremum problems with inequalities as subsidiary conditions, in Studies and Essays Presented to R. Courant, 1948.
• N. Cristianini, J. Shawe-Taylor, An Introduction to Support Vector Machines, Cambridge University Press, 2000. doi:10.1017/CBO9780511801389

Motivation

Chapter 13 showed that convex-Lipschitz-bounded and convex-smooth-bounded problems are learnable by regularized loss minimization; Chapter 14 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) shows how to learn them with the simplest possible algorithm. Gradient descent moves against the gradient with a fixed step size and outputs the average of its iterates; its analysis (Lemma 14.1) is a single telescoping identity that bounds $\sum_t \langle w^{(t)} - w^\star, v_t\rangle$ for any sequence of directions $v_t$, and this generality is the whole point. It gives the rate $B\rho/\sqrt T$ for convex Lipschitz functions (Corollary 14.2), extends to nondifferentiable functions through subgradients (Definition 14.4, Lemmas 14.3 and 14.7), and, because it never used that the directions were gradients, extends to stochastic gradient descent, in which each direction is random with a subgradient as its conditional expectation (Theorem 14.8). Applied to the risk $L_D(w)$ with a fresh example at each step, SGD is a learning algorithm whose sample complexity is the iteration count: $B^2\rho^2/\epsilon^2$ examples for convex-Lipschitz-bounded problems (Corollary 14.12) and $12B^2\beta/\epsilon^2$ for convex-smooth-bounded ones (Theorem 14.13, Corollary 14.14). A projected, decreasing-step variant for strongly convex objectives has rate $(\rho^2/(2\lambda T))(1 + \log T)$ (Theorem 14.11).

Setting

Hypotheses are vectors in $\mathbb{R}^d$; convex, Lipschitz and smooth losses, convex-Lipschitz-bounded and convex-smooth-bounded problems, and strong convexity are those of Mission IX. A vector $v$ is a subgradient of $f$ at $w$ if $f(u) \ge f(w) + \langle u - w, v\rangle$ for all $u$. The iterates of an update rule $w^{(1)} = 0$, $w^{(t+1)} = w^{(t)} - \eta v_t$ are indexed from $0$, and the output after $T$ steps is $\bar w = \frac1T\sum_{t < T} w^{(t)}$. The randomness of SGD is modelled as the chapter uses it in §14.5: a sample $z_0, \dots, z_{T-1}$ drawn i.i.d. from $D$ and an oracle $g$ with $v_t = g(w^{(t)}, z_t)$, where $g$ is a stochastic subgradient oracle for $f$ if $\mathbb{E}_{z \sim D}\, g(w, z) \in \partial f(w)$ for every $w$. This is the book's condition $\mathbb{E}[v_t \mid w^{(t)}] \in \partial f(w^{(t)})$ in the case where the direction depends on the past only through $w^{(t)}$ and on fresh randomness, which is what every application in the book does; the expectation $\mathbb{E}[f(\bar w)]$ is then an integral over $D^T$. For learning, $g(w, z)$ is a subgradient of $\ell(\cdot, z)$ at $w$, so that $\mathbb{E}_z g(w,z)$ is a subgradient of $L_D$ at $w$ (14.13). The projection of $w$ onto a convex set $H$ is a nearest point of $H$, and the strongly convex variant projects after each step with step size $1/(\lambda t)$.

Formalization targets

Goal: Theorem 14.8

For a convex $f$, $B, \rho > 0$, a measurable oracle $g$ with $\mathbb{E}_z g(w, z) \in \partial f(w)$ and $\|g(w, z)\| \le \rho$, any $w^\star$ with $\|w^\star\| \le B$, $T \ge 1$ and $\eta = B/(\rho\sqrt T)$: $\mathbb{E}[f(\bar w)] - f(w^\star) \le B\rho/\sqrt T$; and for every $\epsilon > 0$, $T \ge B^2\rho^2/\epsilon^2$ gives $\mathbb{E}[f(\bar w)] - f(w^\star) \le \epsilon$.

Milestones

Lemma 14.1. For any directions, $\sum_{t<T}\langle w^{(t)} - w^\star, v_t\rangle \le \|w^\star\|^2/(2\eta) + (\eta/2)\sum_{t<T}\|v_t\|^2$; with $\|v_t\| \le \rho$, $\|w^\star\| \le B$ and $\eta = B/(\rho\sqrt T)$ the average is at most $B\rho/\sqrt T$.

Corollary 14.2. Subgradient descent on a convex $\rho$-Lipschitz $f$ with $\eta = B/(\rho\sqrt T)$ has $f(\bar w) - f(w^\star) \le B\rho/\sqrt T$ for every $\|w^\star\| \le B$, and $T \ge B^2\rho^2/\epsilon^2$ gives $\epsilon$.

Lemma 14.7. A convex $f$ on $\mathbb{R}^d$ is $\rho$-Lipschitz iff all its subgradients have norm at most $\rho$.

Lemma 14.9. For the projection $v$ of $w$ onto a convex $H$ and $u \in H$, $\|w - u\|^2 \ge \|v - u\|^2$.

Theorem 14.11. For $\lambda$-strongly convex $f$, a closed convex $H$, an oracle with $\mathbb{E}_z\|g(w,z)\|^2 \le \rho^2$ and any $w^\star \in H$, the projected variant with $\eta_t = 1/(\lambda t)$ has $\mathbb{E}[f(\bar w)] - f(w^\star) \le (\rho^2/(2\lambda T))(1 + \log T)$.

Corollary 14.12. SGD on the risk of a convex-Lipschitz-bounded problem with $T \ge B^2\rho^2/\epsilon^2$ examples has $\mathbb{E}[L_D(\bar w)] \le L_D(w) + \epsilon$ for every $w \in H$.

Theorem 14.13. For convex, $\beta$-smooth, nonnegative losses and $\eta\beta < 1$, SGD with gradient directions has $\mathbb{E}[L_D(\bar w)] \le \frac{1}{1-\eta\beta}(L_D(w^\star) + \|w^\star\|^2/(2\eta T))$.

Corollary 14.14. For a convex-smooth-bounded problem with $\ell(0,z) \le 1$ and any $\epsilon > 0$, SGD with $\eta = 1/(\beta(1 + 3/\epsilon))$ and $T \ge 12B^2\beta/\epsilon^2$ has $\mathbb{E}[L_D(\bar w)] \le L_D(w) + \epsilon$ for every $w \in H$.

Further items: Lemma 14.3, Claims 14.5, 14.6 and 14.10, and the hinge-loss subgradient of Example 14.2.

Significance

SGD is the algorithm behind most of modern machine learning, and Theorem 14.8 is its basic guarantee: dimension-free, independent of the form of $f$ beyond convexity, and with a sample complexity matching the regularization bound of Chapter 13 up to a constant. Lemma 14.1 isolates the deterministic identity that makes both gradient descent and its stochastic version work, and Lemma 14.7 is the bridge between the Lipschitz assumption of Chapter 12 and the bounded directions the analysis needs. The learning corollaries make the point that runs through Part II of the book: for convex problems, optimization and learning are the same activity, and one pass over the data suffices.

Nothing here is machine-checked. The chapter's statements are essentially correct, and the formalization records the reading choices rather than corrections: the i.i.d.-oracle model of the randomness, the subgradient form of gradient descent, the bound at every point of the ball rather than at a minimizer, and, in Corollary 14.14, the assumptions $\epsilon \le 1$ and $0 \in H$ under which the derivation from Theorem 14.13 goes through.

Difficulty

Lemma 14.1 is a completed square and a telescoping sum and is the intended entry point; the $B\rho/\sqrt T$ clause is the substitution of $\eta$. Corollary 14.2 is Lemma 14.1 with Jensen's inequality for the average and the subgradient inequality at each iterate, plus Lemma 14.7 to bound the directions. The subgradient facts need convex analysis: Lemma 14.3 in the direction "convex implies subgradients exist" is the supporting hyperplane theorem on $\mathbb{R}^d$, which Mathlib does not offer directly; Claim 14.5 uses the first-order characterization of convexity for differentiable functions; Lemma 14.7's "Lipschitz implies bounded subgradients" is the book's one-line argument along $u = w + \epsilon v/\|v\|$. Theorem 14.8 is Lemma 14.1 plus the conditioning argument of the book, which in the i.i.d.-oracle model is Fubini on the product $D^T$: the iterate $w^{(t)}$ is a measurable function of $z_0, \dots, z_{t-1}$, and integrating $\langle w^{(t)} - w^\star, g(w^{(t)}, z_t)\rangle$ over $z_t$ first gives $\langle w^{(t)} - w^\star, \mathbb{E}_z g(w^{(t)}, z)\rangle \ge f(w^{(t)}) - f(w^\star)$. Theorem 14.11 adds the projection lemma, the strong-convexity inequality of Claim 14.10, the telescoping of $\frac{\lambda t}{2}(a_t - a_{t+1}) - \frac\lambda2 a_t$ and the harmonic sum $\sum_{t \le T} 1/t \le 1 + \log T$; the second-moment hypothesis makes $\mathbb{E}\|w^{(t)} - w^\star\|^2$ finite inductively. Corollary 14.12 is Theorem 14.8 for $f = L_D$ with the oracle of (14.13), which requires exchanging a subgradient inequality with the integral over $z$. Theorem 14.13 replaces the Lipschitz bound by self-boundedness, $\|\nabla\ell\|^2 \le 2\beta\ell$, and rearranges; Corollary 14.14 is its arithmetic under the added assumptions. In all expectation statements the measurability of the iterates in the sample, from the measurability of the oracle, is a routine but necessary lemma.

Formalization scope

Iterates are defined by structural recursion, so no argmin is chosen; the sample-driven SGD stops after $T$ updates; the projection onto $H$ is a chosen nearest point, unique for closed convex $H$. Bounds are stated for every $w^\star$ in the ball (or in $H$) rather than for a minimizer, which is what the proofs give and is stronger. The oracle bound $\|g(w,z)\| \le \rho$ is required surely (the book: with probability $1$); the almost-sure version is a routine extension. The second-moment hypothesis of Theorem 14.11 is a lower Lebesgue integral, so that a non-integrable oracle cannot satisfy it vacuously. The learning corollaries assume a measurable loss, nonnegative and bounded at the origin, so that the risks are genuine integrals, and a measurable selector of subgradients. Variable step sizes (§14.4.2), other averaging schemes (§14.4.3), SGD for regularized loss minimization (§14.5.3) and the exercises are not stated.

Trivializing readings are excluded: the expectations are over the product law of the examples with measurable integrands, the subgradient conditions are pointwise inequalities, and the iteration counts are the book's. Welcome contributions: Lemma 14.1 as a reusable telescoping lemma, the measurability of the SGD iterates, and the Fubini step that turns an oracle condition into the inequality (14.10).

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 14. doi:10.1017/CBO9781107298019
• H. Robbins, S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22(3), 1951. doi:10.1214/aoms/1177729586
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, Proceedings of ICML, 2003.
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19(4), 2009. doi:10.1137/070704277
• S. Shalev-Shwartz, Online learning and online convex optimization, Foundations and Trends in Machine Learning 4(2), 2012. doi:10.1561/2200000018