Machine Learning

Motivation

Binary classification asks for a rule that predicts a label $y \in \{-1,1\}$ from an observation $x$. The natural loss for this task, the classification loss $L_{\mathrm{class}}$, is a step function: minimizing its empirical average over a class of functions $f$ is generally NP-hard, because the objective is non-convex and discontinuous in $f$. Every practical classification algorithm — logistic regression, boosting, and the support vector machine this book is about — sidesteps this by minimizing a convex surrogate loss instead, such as the hinge loss $L_{\mathrm{hinge}}(y,t) := \max\{0, 1-yt\}$, and hoping that a small surrogate risk implies a small classification risk.

Zhang (2004) and Bartlett, Jordan & McAuliffe (2006) put this hope on a rigorous footing: for a wide class of convex surrogates, controlling the excess surrogate risk controls the excess classification risk, with an explicit quantitative relationship. Steinwart & Christmann, Support Vector Machines (Springer 2008, Information Science and Statistics), Chapter 2, develop the special case of the hinge loss in closed form as Theorem 2.31 ("Zhang's inequality"), the sharpest and most self-contained instance of this calibration phenomenon: an exact equality for bounded functions, not merely an inequality.

Setting

Fix a measurable space $(X,\mathcal A)$ and a closed label set $Y \subset \mathbb R$; throughout this mission $Y := \{-1,1\}$. A loss function is a measurable map $L : X \times Y \times \mathbb R \to [0,\infty)$, read as the cost $L(x,y,f(x))$ of predicting $y$ by $f(x)$ when $x$ is observed. Given a distribution $P$ on $X \times Y$, the $L$-risk of a measurable $f : X \to \mathbb R$ is the average cost $R_{L,P}(f) := \int_{X\times Y} L(x,y,f(x))\,dP(x,y)$, and the Bayes risk $R^*_{L,P} := \inf_f R_{L,P}(f)$ is the smallest risk any measurable function can achieve.

The classification loss is $L_{\mathrm{class}}(y,t) := \mathbf 1_{(-\infty,0]}(y \cdot \operatorname{sgn} t)$ — it charges $1$ exactly when the sign of the prediction $t$ disagrees with the label $y$ — where $\operatorname{sgn}$ is the sign function with the book's convention $\operatorname{sgn}(0):=1$. The hinge loss is $L_{\mathrm{hinge}}(y,t) := \max\{0,1-yt\}$, a convex, piecewise-linear upper bound on $L_{\mathrm{class}}$ up to a factor of $2$. Writing $\eta(x) := P(y=1\mid x)$ for the conditional probability of the positive label given $x$, the Bayes classification function is $f^*_{L_{\mathrm{class}},P}(x) := \operatorname{sgn}(2\eta(x)-1)$: it predicts the majority label at $x$.

A loss $L$ can be clipped at $M>0$ if truncating every prediction to $[-M,M]$ never increases the loss: $L(x,y,\widehat t) \le L(x,y,t)$ for the clipped value $\widehat t$ of $t$. Both $L_{\mathrm{class}}$ and $L_{\mathrm{hinge}}$ can be clipped at $M=1$.

Formalization targets

Goal: Zhang's inequality (Theorem 2.31)

$$R_{L_{\mathrm{hinge}},P}(f) - R^*_{L_{\mathrm{hinge}},P} = \int_X |f(x) - f^*_{L_{\mathrm{class}},P}(x)| \cdot |2\eta(x)-1| \, dP_X(x) \qquad (f : X \to [-1,1])$$ $$R_{L_{\mathrm{class}},P}(f) - R^*_{L_{\mathrm{class}},P} \;\le\; R_{L_{\mathrm{hinge}},P}(f) - R^*_{L_{\mathrm{hinge}},P} \qquad (f : X \to \mathbb R)$$

The first target is an exact identity for bounded predictors: the excess hinge risk equals a weighted $L^1$ distance to the Bayes classifier. The second, weaker but unrestricted, statement is what makes the hinge loss a valid classification surrogate for arbitrary real-valued scores: no matter how large $|f|$ grows, the excess classification risk it incurs is bounded by its excess hinge risk. Because the second statement is the one actually used downstream (Chapter 6's oracle inequality composes it with a bound on the excess hinge risk to bound the excess classification risk), it is the weakest stable form of the calibration claim and the natural target to keep in mind when judging whether a variant formalization is still faithful.

Significance

Zhang's inequality is the single fact that licenses every consistency and rate-of-convergence result for SVM classification in the rest of the book (flagged explicitly on p. 38: "we will show in Section 3.4 that the other margin-based losses ... are also reasonable surrogates," and reused directly, e.g., in Chapter 6's oracle inequality via its restatement as Theorem 6.24 in Chapter 6 of this series). Its role is entirely mechanical but load-bearing: every SVM consistency proof reduces to bounding an excess surrogate risk, and Theorem 2.31 is what converts that bound back into a statement about the classification error anyone actually cares about.

The result itself has been known since Zhang (2004) and Bartlett–Jordan–McAuliffe (2006) in more general form (arbitrary convex margin losses, with an explicit "$\psi$-transform" relating excess risks); Theorem 2.31 is the closed-form hinge-loss instance, with the equality (not just an inequality) available because the hinge loss's clipped value is exactly linear in $\eta$. No machine-checked proof of either the general or the hinge-specific statement is known to exist in a public Lean/Mathlib development at the time of writing (see prior-art search below); this mission asks for a formalization of the hinge-specific case exactly as the book states it.

Difficulty

The natural first attempt is to expand both risk differences directly as integrals over $P$ and compare integrands. This works for the equality (bounded $f$), because the hinge loss is piecewise linear in $t$ and the calculation collapses to the algebraic identity $1+f(x)(1-2\eta(x)) = |f(x)-f^*_{L_{\mathrm{class}},P}(x)|\cdot|2\eta(x)-1|$ once $f^*$ is spelled out by cases on the sign of $2\eta(x)-1$. It fails for the inequality on unbounded $f$: neither risk difference has a closed algebraic form once $f$ is allowed to leave $[-1,1]$, and the excess classification risk itself is genuinely discontinuous in $f$. The book's proof resolves this by clipping $f$ first (Lemma 2.23: clipping a convex loss at a minimizer's interval only decreases its risk) and observing the excess classification risk is invariant under clipping — this reduces the general case to the bounded case, at the cost of needing Lemma 2.23 as a genuine prerequisite rather than a routine remark. The remaining pointwise step (Lemma 2.30) is a case-by-case real-variable inequality with no probabilistic content of its own, but gets the boundary case $\eta = 1/2$ (equivalently $2\eta-1=0$, where the book's sign convention $\operatorname{sgn}(0):=1$ is load-bearing) wrong if that convention is not tracked precisely.

Formalization scope

$X$ is an arbitrary measurable space; $Y$ is fixed to $\{-1,1\} \subset \mathbb R$ throughout. A loss is represented as a plain function Loss X := X → ℝ → ℝ → ℝ; nonnegativity and the restriction of the middle argument to $\{-1,1\}$ are supplied as explicit hypotheses at each use site rather than built into the type, since only some lemmas of the chapter need them (Lemma 2.23 needs neither). risk/bayesRisk are ordinary real-valued Bochner integrals/infima, not extended-real-valued as in the book; consequently every assertion that could otherwise degrade to a vacuous 0 - 0 from a non-integrable loss carries an explicit Integrable hypothesis on the relevant loss composed with $f$ — automatic in the book's own setting (bounded losses on a probability space) but not implied by the Lean types alone. $\eta(x) := P(y=1\mid x)$ is represented by its defining disintegration identity, $P(A\times\{1\}) = \int_{x\in A}\eta(x)\,dP_X(x)$ for every measurable $A \subseteq X$, rather than via a general regular-conditional-probability construction — a specific, checkable representation of "the conditional probability of $y=1$ given $x$" rather than a synonym for it.

A trivializing formalization would let $f^*_{L_{\mathrm{class}},P}$ or $\eta$ be an unconstrained hypothesis unconnected to $P$ and $L_{\mathrm{class}}$ (making the goal a tautology about whatever function is supplied); this is ruled out here by deriving $f^*_{L_{\mathrm{class}},P}$ from $\eta$ by the book's own formula $\operatorname{sgn}(2\eta-1)$ and constraining $\eta$ by the disintegration identity above, not taking either as a free unconstrained parameter.

Lemma 2.23, Lemma 2.30, L_class/L_hinge, risk/bayesRisk and CanBeClipped/clip are reusable beyond this mission: Lemma 2.23 and the risk/Bayes-risk vocabulary recur throughout the book (clippability is used again in Section 7.4 and, per this series' README, this chapter's Theorem 2.31 itself is restated inside Chapter 6's oracle inequality). Contributions completing the two milestone proofs and the goal's sorry are welcome; a from-scratch alternative proof avoiding Lemma 2.23 (e.g. by a direct case analysis on $f$ outside $[-1,1]$) would also be a valid solution to the goal, since the milestones are the book's own attack path, not a required lemma structure.

Selected references

• I. Steinwart & A. Christmann, Support Vector Machines, Springer, Information Science and Statistics, 2008. https://doi.org/10.1007/978-0-387-77242-4 (Chapter 2, pp. 21-47).
• T. Zhang, "Statistical behavior and consistency of classification methods based on convex risk minimization," Annals of Statistics 32(1), 2004, pp. 56-85. https://doi.org/10.1214/aos/1079120130
• P. L. Bartlett, M. I. Jordan & J. D. McAuliffe, "Convexity, classification, and risk bounds," Journal of the American Statistical Association 101(473), 2006, pp. 138-156. https://doi.org/10.1198/016214505000000907

Motivation

Chapter 2's finite-hypothesis-set learning bound is uninformative the moment $H$ is infinite — $\log|H|$ diverges — yet most hypothesis sets used in practice (linear separators, neural networks, decision trees) are infinite. Chapter 3 answers the question the previous chapter's own worked example (axis-aligned rectangles, Example 2.4) leaves open: is efficient learning from a finite sample still possible for an infinite hypothesis set, and can this be shown in general rather than case by case? The chapter's answer runs through two complementary notions of complexity — Rademacher complexity, a data-dependent measure of how well a function family correlates with random noise, and the VC-dimension, a purely combinatorial measure of the number of distinct labelings a hypothesis set can realize on a finite point set — connected by Massart's lemma and Sauer's lemma, and culminating in a generalization bound that replaces $\log|H|$ with the VC-dimension $d$.

Setting

For a family $G$ of functions $Z\to[0,1]$ and a sample $S=(z_1,\dots,z_m)$, the empirical Rademacher complexity $\hat R_S(G) = \mathbb E_\sigma[\sup_{g\in G}\frac1m\sum_i\sigma_i g(z_i)]$ (Definition 3.1) measures how well $G$ fits random sign noise $\sigma$ on $S$; the Rademacher complexity $R_m(G) = \mathbb E_{S\sim D^m}[\hat R_S(G)]$ (Definition 3.2) averages this over samples. Theorem 3.3 converts a Rademacher-complexity bound directly into a generalization bound via McDiarmid's inequality. For binary hypothesis sets $H\subseteq(X\to\{-1,+1\})$, the growth function $\Pi_H(m)$ (Definition 3.6) counts the maximum number of distinct dichotomies $H$ realizes on $m$ points, and the VC-dimension $\mathrm{VCdim}(H)$ (Definition 3.10) is the largest $m$ for which $\Pi_H(m)=2^m$ (i.e. $H$ shatters some set of $m$ points). Massart's lemma (Theorem 3.7) is the purely combinatorial tool bounding the expected maximum of a sum of signed vector components by $\sqrt{\log|A|}$, and Sauer's lemma (Theorem 3.17) bounds the growth function itself, by induction on $m+d$, whenever the VC-dimension is finite.

Formalization targets

Theorem 3.3 (Rademacher generalization bound, milestone). For $G:Z\to[0,1]$ and any $\delta>0$, with probability at least $1-\delta$ over an i.i.d. sample $S$ of size $m$, for all $g\in G$: $\mathbb E[g(z)] \le \frac1m\sum_i g(z_i) + 2R_m(G) + \sqrt{\log(1/\delta)/(2m)}$.

Theorem 3.7 (Massart's lemma, milestone). For a finite $A\subseteq\mathbb R^m$ with $r=\max_{x\in A}\|x\|_2$: $\mathbb E_\sigma[\frac1m\sup_{x\in A}\sum_i\sigma_i x_i] \le r\sqrt{2\log|A|/m}$.

Theorem 3.17 (Sauer's lemma, milestone). For $H$ with $\mathrm{VCdim}(H)=d$, for all $m\in\mathbb N$: $\Pi_H(m) \le \sum_{i=0}^d\binom{m}{i}$.

Corollary 3.19 — the mission's goal. For $H\subseteq(X\to\{-1,+1\})$ with $\mathrm{VCdim}(H)=d$ and any $\delta>0$, with probability at least $1-\delta$, for all $h\in H$:

$$R(h) \le \hat R_S(h) + \sqrt{\frac{2d\log(em/d)}{m}} + \sqrt{\frac{\log(1/\delta)}{2m}}.$$

Significance

Corollary 3.19 is the chapter's answer to the question chapter 2 leaves open: it is Theorem 2.13's direct infinite-hypothesis-set generalization, replacing $\log|H|$ (undefined for infinite $H$) with the VC-dimension $d$ (finite even for many infinite hypothesis sets, such as halfspaces in $\mathbb R^k$, which have VC-dimension $k+1$). It is also the template every later margin bound in the book specializes (Chapters 5, 9, 10's SVM, multi-class and ranking margin bounds all replace this bound's uniform $\log|H|$/VC-dimension term with a scale-sensitive complexity measure derived from the same Rademacher-complexity machinery), and Sauer's lemma is independently one of the most cited results in learning theory and extremal combinatorics. No prior art on the Prove2Me platform is faithful to any of this chapter's content: RademacherSymmetrization.radS_chernoff (Aether Catalog) proves a different, Massart-optimized Chernoff bound for the empirical Rademacher complexity of a finite class — a different object (empirical vs. population) with a different bound form from Theorem 3.3/3.5 — and sauerShelah_full proves only the trivial identity sauerShelahBound k k = 2^k, not Sauer's lemma itself. A further hit, sauer_shelah (Aether Catalog, Algebra/SauerShelah.lean), does state the Sauer-Shelah bound itself (F.card ≤ ∑_{i≤d} C(n,i) for a family F of subsets of Fin n shattering no set larger than d) — checked and not reused: it is a different idiom from Theorem 3.17 as this chunk needs it, a fixed finite ambient domain Fin n with F a Finset of its subsets directly, rather than the book's own growth function Π_H(m) (a supremum over point-tuples drawn from an arbitrary, possibly infinite X, Definition 3.6) that this chunk's other items and the goal (Corollary 3.19) are built on; reusing it would require either abandoning GrowthFunction/HasVCDim (needed faithfully by the goal itself) or a nontrivial reduction lemma this mission's budget does not include, so sauer_lemma is drafted fresh against this chunk's own GrowthFunction/HasVCDim. All ten items are drafted fresh.

Difficulty

Sauer's lemma's proof is a genuine two-parameter induction (on $m+d$) with a real combinatorial construction: restricting $H$ to a sample $S$ of size $m$, then splitting the restricted family into $G_1$ (its restriction to the first $m-1$ points) and $G_2$ (the concepts whose membership in $G$ changes with the addition of the $m$-th point), with $|G_1|+|G_2|=|G|$ and $\mathrm{VCdim}(G_2) \le \mathrm{VCdim}(G)-1$ — a genuinely combinatorial argument, not a statement that unfolds by simp; a weaker restatement using only the trivial bound $\Pi_H(m)\le 2^d$ would be true but is explicitly not what Theorem 3.17 states (BRIEF.md's named trivializing formalization for this chapter). Massart's lemma needs the expectation of a supremum over a finite set of $2^m$-many sign patterns kept as an honest average, not silently replaced by a looser union bound. Corollary 3.19's own $em/d$ term inside the logarithm needs the side condition $d\le m$ carried through explicitly — Corollary 3.18's own domain restricts to $m\ge d$, and the bound is false, not merely unproved, without it (at $m<d$, $em/d$ can be smaller than $1$, making the logarithm negative).

Formalization scope

GeneralizationError/EmpiricalError are restated locally in this chunk's RademacherVC namespace (byte-identical in content to chunk 02-pac's own copies), since a draft item cannot import another chunk's draft module; this duplication is expected and will collapse once 02-pac is moderated, uploaded and listed as reusable in missions/README.md's "Published definitions" table. EmpiricalRademacherComplexity/Massart's lemma model the Rademacher signs σ as ranging over the finite type Fin m → Bool rather than a measure-theoretic i.i.d. process, so the "expectation over σ" in both is the exact finite uniform average over its 2^m outcomes — faithful and simpler than a MeasureTheory construction, since σ's distribution really is uniform on a finite set of outcomes for every finite m. GrowthFunction takes a tuple of m points (Fin m → X) rather than a size-m subset of X, a harmless generalization (repeated points never increase the dichotomy count) documented in the item's own docstring. HasVCDim is a Prop parametrized by the candidate dimension rather than a total ℕ/ℕ∞-valued function, so it does not cover the book's VCdim(H)=+\infty case (Examples 3.15-3.16); every theorem using it takes HasVCDim H d as an explicit hypothesis, matching the book's own "let H... with VCdim(H)=d." Theorem 3.3 adds an explicit measurability hypothesis on G (hGm) beyond the book's own displayed statement, needed to keep the Bochner integral ∫ z, g z ∂D from silently evaluating to 0 for a non-measurable g — this is the book's own standing assumption (footnote 3, p. 30) made an explicit hypothesis rather than an implicit one. No numerical constant in any of the four theorems is altered from the book's own; Corollary 3.19's side condition d ≤ m is kept explicit, per BRIEF.md's pitfall note.

Not formalized: Lemma 3.4 and Theorem 3.5 (the binary-classification specialization of Theorem 3.3 via the zero-one-loss identity $\hat R_S(G)=\frac12\hat R_{S_X}(H)$), Corollary 3.8 and Corollary 3.9 (the intermediate Rademacher-to-growth-function and growth-function generalization bounds), and Corollary 3.18 (the VC-dimension bound on the growth function, $\Pi_H(m)\le(em/d)^d$ for $m\ge d$) — five intermediate results in the proof chain Theorem 3.3 → Theorem 3.5 → Corollary 3.8/3.9 → Sauer's lemma → Corollary 3.18 → Corollary 3.19 that are not independently drafted as milestones, per the budget guidance to keep a chunk to a goal plus its most load-bearing 3-8 milestones rather than every numbered result on the page; the three drafted milestones (Theorem 3.3, Massart's lemma, Sauer's lemma) are the chain's three genuinely distinct proof techniques (McDiarmid's inequality, a probabilistic-maximum bound, and a combinatorial induction), and the goal theorem's own statement is Corollary 3.19 exactly as displayed, not a restatement of any intermediate corollary. Radon's theorem (Theorem 3.13, background for the hyperplane VC-dimension example) and the worked VC-dimension examples (intervals, hyperplanes, rectangles, convex polygons, sine functions) are illustrations, not general results, and are not formalized — drafting only the example computations (e.g. VCdim(hyperplanes) = d+1) instead of the general finite-H machinery is exactly the trivializing formalization this mission avoids.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 3.
• V. Vapnik, A. Chervonenkis, "On the uniform convergence of relative frequencies of events to their probabilities," Theory of Probability and its Applications 16(2), 1971, 264-280.
• N. Sauer, "On the density of families of sets," Journal of Combinatorial Theory, Series A 13(1), 1972, 145-147.

Motivation

How many labeled examples does a learning algorithm need to see before its output generalizes well to unseen data? Chapter 2 of Foundations of Machine Learning answers this question for the simplest nontrivial setting — a finite hypothesis set — and in doing so introduces the book's central object, the Probably Approximately Correct (PAC) learning framework: a distribution-free, high-probability guarantee relating a learner's sample size to the accuracy and confidence of its output. Every later chapter's generalization bound (VC-based, Rademacher-based, margin-based) is a variant of the same "probability of a bad event is small" argument this chapter proves in its most elementary form, so getting the chapter's core definitions and its two bracketing theorems (consistent and inconsistent finite-$H$) right is the foundation the rest of the book's guarantees build on.

Setting

A learner sees a sample $S = (x_1,\dots,x_m)$ drawn i.i.d. from a fixed but unknown distribution $D$ on an instance space $X$, labeled by an unknown target concept $c$ drawn from a concept class $C$; a hypothesis $h$ from a fixed hypothesis set $H$ is judged by its generalization error $R(h) = \Pr_{x\sim D}[h(x)\ne c(x)]$ (Definition 2.1) against its empirical error $\hat R_S(h) = \frac1m\sum_i \mathbb 1_{h(x_i)\ne c(x_i)}$ (Definition 2.2) on the observed sample. A concept class is PAC-learnable (Definition 2.3) if some algorithm, given a polynomially-bounded number of samples, returns a hypothesis whose generalization error is at most $\epsilon$ with probability at least $1-\delta$, for every accuracy $\epsilon$ and confidence $\delta$ and every distribution $D$ — the "distribution-free" and "for all target concepts" character of the definition is what makes it a genuine worst-case learning guarantee rather than an average-case one tailored to a particular data-generating process.

Formalization targets

Theorem 2.5 (consistent case, milestone). If $H$ is finite and algorithm $A$ always returns a hypothesis consistent with the target concept on the training sample ($\hat R_S(h_S)=0$), then $\Pr_{S\sim D^m}[R(h_S)\le\epsilon]\ge1-\delta$ whenever $m \ge \frac1\epsilon(\log|H|+\log\frac1\delta)$.

Corollary 2.11 (single-hypothesis Hoeffding bound, milestone). For a fixed hypothesis $h:X\to\{0,1\}$ and any $\delta>0$, with probability at least $1-\delta$, $R(h) \le \hat R_S(h) + \sqrt{\log(2/\delta)/(2m)}$.

Theorem 2.13 (inconsistent case, goal). For a finite hypothesis set $H$ and any $\delta>0$, with probability at least $1-\delta$, simultaneously for every $h\in H$,

$$R(h) \le \hat R_S(h) + \sqrt{\frac{\log|H|+\log(2/\delta)}{2m}}.$$

Significance

Theorem 2.13 is the chapter's capstone because it removes Theorem 2.5's consistency requirement — the typical case in practice, where no hypothesis in $H$ perfectly fits the training data — while paying only an additive $\log|H|$ price inside the square root, via a union bound over $H$ applied to Corollary 2.11's per-hypothesis concentration bound. It is also the template every later generalization bound in the book refines: Chapter 3 replaces $\log|H|$ with the growth function / VC-dimension to handle infinite hypothesis sets, and Chapter 3's Rademacher-complexity bound is the direct machine-independent generalization of the same argument. No prior art on the Prove2Me platform is faithful to this chapter's PAC-learning content (GET /theorems?q=PAC-learnable returns no hits), so all six items are drafted fresh.

Difficulty

Theorem 2.13's own proof is a short combination of two ideas already present in the chapter (Corollary 2.11's Hoeffding bound plus a union bound over $|H|$ hypotheses), but each ingredient carries its own faithfulness burden. Corollary 2.11 needs the sample $S$ and the target hypothesis $h$ kept in the right relationship — $h$ fixed, $S$ random — for the bound to be Hoeffding's inequality and not a vacuous statement about a random hypothesis. Theorem 2.13 needs the $\forall h\in H$ quantifier placed inside the probability event (a single sample $S$ must work for every $h$ at once), not outside it (which would only assert each $h$'s bound holds with high probability for a sample chosen depending on $h$) — the difference between a uniform convergence bound and $|H|$ separate, weaker statements. Definition 2.3's "polynomial function $\mathrm{poly}(\cdot,\cdot,\cdot,\cdot)$" is a genuine formalization judgment call, addressed below.

Formalization scope

GeneralizationError/EmpiricalError are typed generally over $X, Y$ (matching Definition 2.1/2.2's own general statement, "$h : X\to Y$"), since Theorem 2.5 itself is stated for general $Y$, not just $Y=\mathrm{Bool}$; Corollary 2.11 and Theorem 2.13 specialize to $h : X\to\mathrm{Bool}$, matching their own explicit "$h:X\to\{0,1\}$" (Corollary 2.11) and the surrounding inconsistent-case section's restriction to binary classification. The i.i.d. sample $S\sim D^m$ is modeled as the identity random variable on the product-measure space $(\mathrm{Fin}\ m \to X,\ \mathrm{Measure.pi}(\lambda\_.\ D))$ in both Corollary 2.11 and Theorem 2.13, matching the book's own $S\sim D^m$ notation exactly. IsPACLearnable (Definition 2.3) makes "polynomial function" precise as a function bounded above by $K\cdot(a+b+n+s+1)^k$ for some constants $K>0$, $k\in\mathbb N$, uniform in its (nonnegative) arguments — the standard reading of "polynomial in its arguments" in the absence of a ready-made multivariate polynomial-growth predicate in Mathlib; dropping this constraint entirely (stating only "there is some threshold function") would silently weaken Definition 2.3 to a strictly easier notion of learnability, since virtually any finite or well-behaved concept class admits some (possibly super-polynomial) sample-complexity threshold — this is exactly the distinction Example 2.7 (the universal concept class) uses to demonstrate a class that is not PAC-learnable despite admitting a consistent hypothesis set. No numerical constant in Theorem 2.5, Corollary 2.11 or Theorem 2.13 is altered from the book's own; no upper bound on $\delta$ is added anywhere the book itself leaves it unrestricted (the theorems remain true, if vacuous, for $\delta>1$). Not formalized: the "efficiently PAC-learnable" running-time clause of Definition 2.3 (a second, independent polynomial-time condition on $A$ not needed by either milestone or the goal); Corollary 2.10 (the raw two-sided Hoeffding statement Corollary 2.11 is immediately derived from by solving for $\epsilon$, making it redundant with Corollary 2.11 as a formalization target); the axis-aligned-rectangles worked example (Example 2.4–2.9), which illustrates the framework rather than proving a new general result, and the trivializing formalization this chapter invites — reusing Mathlib's rectangle machinery to encode only the specific two-dimensional geometric argument rather than the general finite-$H$ theorems — is exactly what this mission avoids by drafting Theorems 2.5 and 2.13 in their general, hypothesis-set-agnostic form.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 2.
• W. Hoeffding, "Probability inequalities for sums of bounded random variables," Journal of the American Statistical Association 58(301), 1963, 13-30.

Motivation

Composite convex programs — objectives split into a smooth piece and a nonsmooth piece — are ubiquitous in data analysis: LASSO-type inverse problems, regularized empirical-risk minimization, and total-variation-type image reconstruction all minimize $f(x)+h(x)+\chi(x)$ over a convex set, where $f$ is smooth (a data-fidelity term, often expensive to differentiate — a large matrix-vector product, a PDE solve, a black-box simulation), $h$ is nonsmooth but structurally cheap (an $\ell_1$-type penalty, a simple subgradient), and $\chi$ enforces a "relatively simple" constraint absorbed into the proximal step. Classical accelerated proximal-gradient methods (Nesterov; Beck–Teboulle) solve such problems by computing $\nabla f$ and a subgradient $h'$ once per iteration, giving an optimal $O(1/\varepsilon^2)$ bound on evaluations of both. But in every example above, the two oracle calls have wildly different costs, and paying for $\nabla f$ as often as for $h'$ is wasteful. Ghadimi, Lan and Zhang (SIAM J. Optim., 2014, arXiv:1406.5613, "Generalized Uniformly Optimal Methods for Nonlinear Programming") posed the resulting question: given separate first-order access to $f$ and $h$, can the number of $\nabla f$-evaluations be reduced without inflating the (already-optimal) number of $h'$-evaluations? The gradient sliding (GS) algorithm formalized here, from Lan's textbook treatment (Chapter 8, building on Lan's own 2016 Mathematical Programming paper "Gradient sliding for composite optimization"), answers this in the affirmative: it "slides" past $\nabla f$-evaluations on most iterations while still achieving the optimal $O(1/\varepsilon^2)$ subgradient count for $h'$.

Setting

Fix a real inner-product space $E$ and a closed convex set $X\subseteq E$. The composite problem is

$$\Psi^* \equiv \min_{x\in X}\{\Psi(x) := f(x)+h(x)+\chi(x)\}, \qquad (8.1.1)$$

where $\chi$ is a "relatively simple" convex function (its own proximal step is assumed cheap), $f:X\to\mathbb R$ is convex with $L$-Lipschitz gradient,

$$f(x)\le f(y)+\langle\nabla f(y),x-y\rangle+\tfrac L2\|x-y\|^2, \qquad \forall x,y\in X, \quad (8.1.2)$$

and $h:X\to\mathbb R$ is convex and $M$-Lipschitz-like in the sense that for every subgradient $h'(y)\in\partial h(y)$,

$$h(x)\le h(y)+\langle h'(y),x-y\rangle+M\|x-y\|, \qquad \forall x,y\in X. \quad (8.1.3)$$

Let $V(a,b)$ be a Bregman-type prox-function built from a 1-strongly-convex distance-generating function $\nu$ (Sect. 3.2), so $V(a,b)\ge\tfrac12\|b-a\|^2$.

The gradient sliding (GS) algorithm (Algorithm 8.1) keeps an outer iterate $x_k$, model point $g_k(\cdot)\equiv l_f(x_k,\cdot):=f(x_k)+\langle\nabla f(x_k),\cdot-x_k\rangle$, and running average $\bar x_k$ ($\bar x_0=x_0$). Each outer step $k=1,\dots,N$ delegates to the prox-sliding (PS) procedure: given the affine model $g_k$, prox-center $x_{k-1}$, parameter $\beta_k$, and sliding length $T_k$, PS runs $T_k$ inner iterations

$$u_t = \arg\min_{u\in X}\{g(u)+l_h(u_{t-1},u)+\beta V(x,u)+\beta p_tV(u_{t-1},u)+\chi(u)\}, \qquad \tilde u_t = (1-\theta_t)\tilde u_{t-1}+\theta_tu_t, \quad (8.1.17)\text{--}(8.1.18)$$

where $l_h(y;u):=h(y)+\langle h'(y),u-y\rangle$ (8.1.14), without ever recomputing $\nabla f$ during these $T_k$ steps — the single affine model $g$ is reused throughout. This is the mechanism by which GS "slides" past most $\nabla f$-evaluations. PS returns $(x_k,\tilde x_k)$, and the outer loop updates $\bar x_k=(1-\gamma_k)\bar x_{k-1}+\gamma_k\tilde x_k$.

Formalization targets

Building block (Proposition 8.1)

$$\beta(1-P_t)^{-1}V(u_t,u)+[\Phi(\tilde u_t)-\Phi(u)] \le P_t(1-P_t)^{-1}\Big[\beta V(u_0,u)+ \frac{M^2}{2\beta}\sum_{i=1}^t(p_i^2P_{i-1})^{-1}\Big], \quad \forall u\in X, \, t\ge1,$$

where $\Phi(u):=g(u)+h(u)+\beta V(x,u)+\chi(u)$ and $\{p_t\},\{\theta_t\},\{P_t\}$ satisfy the recursion (8.1.20). This is the per-inner-iteration guarantee on how close $(u_t,\tilde u_t)$ comes to solving $\Phi$'s own minimization.

Intermediate (Theorem 8.1(a))

Assuming the PS schedule (8.1.20) and GS schedule conditions (8.1.25), (8.1.33) (the case where $X$ may be unbounded),

$$\Psi(\bar x_N)-\Psi(x^*) \le \frac{\Gamma_N\beta_1}{1-P_{T_1}}V(x_0,x^*) + \frac{M^2\Gamma_N}{2}\sum_{k=1}^N\sum_{i=1}^{T_k}\frac{\gamma_kP_{T_k}} {\Gamma_k\beta_k(1-P_{T_k})p_i^2P_{i-1}}, \qquad \forall N\ge1,$$

a general bound in terms of the abstract schedule, obtained by telescoping Proposition 8.1's guarantee (via Proposition 8.2's per-outer-step recursion, cited but not restated here) across outer iterations.

Goal (Corollary 8.1(a))

With the concrete schedule $p_t=t/2$, $\theta_t=2(t+1)/(t(t+3))$ (8.1.39), and, for a fixed horizon $N$ and free parameter $\tilde D>0$,

$$\beta_k=\frac{2L}{k}, \qquad \gamma_k=\frac2{k+1}, \qquad T_k=\Big\lceil\frac{M^2Nk^2}{\tilde DL^2}\Big\rceil, \quad (8.1.40)$$ $$\Psi(\bar x_N)-\Psi(x^*) \le \frac{2L}{N(N+1)}\big[3V(x_0,x^*)+2\tilde D\big], \qquad \forall N\ge1. \quad (8.1.41)$$

This is the explicit-constant complexity bound: it is the weakest statement stable under changing $L,M,N,\tilde D$, obtained purely algebraically from Theorem 8.1(a)'s general bound once the schedule is plugged in.

Significance

Corollary 8.1(a), together with the schedule of $T_k$, shows the total number of outer iterations — and hence $\nabla f$-evaluations — needed for an $\varepsilon$-solution is $O(L/ \varepsilon)$, matching the optimal rate for smooth-only minimization (no penalty for the nonsmooth term's presence), while the total number of inner iterations $\sum_kT_k$ — and hence $h'$-evaluations — remains $O(1/\varepsilon^2)$, the rate that is already known to be unimprovable for nonsmooth convex minimization. GS is thus the first method (per the section's own account) to decouple the two oracle costs at their respective optimal rates, rather than paying the worse of the two for both. This underlies later chapters' extensions (accelerated gradient sliding, decentralized optimization over networks) and is directly applicable whenever a composite objective's two components have asymmetric evaluation cost, as in the LASSO-type and regularized-loss examples above. Formalizing it contributes a machine-checked account of the telescoping/recursion argument across two nested loops (outer GS, inner PS) — a pattern distinct from the single-loop accelerated-gradient arguments already in this series (Chapters 3, 7) and not otherwise present in the corpus (q=gradient sliding, q=prox sliding, q=composite optimization all return zero hits as of 2026-09-18).

Difficulty

The obvious first idea — treat the PS procedure's inexact inner solve as adding an error term to a standard accelerated-gradient argument and bound that error by the number of inner steps — fails because a naive termination criterion (the function-value optimality gap of the PS subproblem) does not yield the accelerated rate; the book's own analysis (the paragraph preceding Proposition 8.1) states this explicitly. The working criterion instead combines the optimality gap and the distance to the optimal solution, weighted by the $P_t$-sequence — this is exactly the left-hand side of (8.1.21), not a simpler quantity, and it is this specific combination that telescopes cleanly across both the inner PS loop and, subsequently, the outer GS loop.

Formalization scope

E is NormedAddCommGroup E, InnerProductSpace ℝ E; X : Set E. The Bregman divergence V, model function g/lh, and constraint function chi are hypothesis-carrying objects (functions with the defining (in)equalities as hypotheses), matching this series' convention rather than fixing them to the Euclidean/entropic special case. ps_procedure_bound (Proposition 8.1) takes the three-point inequality that the argmin in (8.1.17) yields (a standard consequence of Lemma 3.5, cited but not re-derived) as an explicit hypothesis on the sequence u, rather than proving well-posedness of the argmin itself. gs_convergence_bound (Theorem 8.1(a)) similarly takes Proposition 8.2's per-outer-step recursion (8.1.26) as a hypothesis — its own proof composes Proposition 8.1 with model-function inequalities (8.1.27)-(8.1.31) that are outside this mission's selected scope — and formalizes only part (a) (unbounded X), not part (b) (compact X, reverse monotonicity), since only (a) is on the goal's dependency path. explicit_gs_rate (Corollary 8.1(a)) uses the closed forms $P_t=2/((t+1)(t+2))$ and $\Gamma_k=2/(k(k+1))$ that the specific schedule (8.1.39)-(8.1.40) produces (8.1.44, 8.1.46 — cited, not restated), rather than the general recursion, and takes Theorem 8.1(a)'s bound, specialized to this schedule, as a hypothesis: its own content is the purely algebraic simplification (8.1.45)-(8.1.48) into the closed-form bound (8.1.41), not a re-derivation of the general theorem. The source PDF's own printed $\beta_k=2L/(\nu k)$ (8.1.40) is a text-extraction artifact (no such $\nu$-indexed quantity appears anywhere in this section); the proof's own algebra ($\gamma_k\beta_k/(\Gamma_k(1-P_{T_k}))=2L/(1-P_{T_k})$, using $\Gamma_k=2/(k(k+1))$, $\gamma_k=2/(k+1)$) is consistent only with $\beta_k=2L/k$, which is what is formalized. A trivializing formalization would fix $h\equiv0$ or $\chi\equiv0$, collapsing the composite problem to plain smooth minimization and making the entire PS-procedure apparatus vacuous; this is ruled out by keeping $h$ and $\chi$ as free convex functions throughout with hMLip an active, non-degenerate hypothesis. Proposition 8.2 (the recursion gs_convergence_bound cites) and Theorem 8.1(b) (the compact-X case) are natural extensions a further contribution could add.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, 2020, Chapter 8. https://doi.org/10.1007/978-3-030-39568-1
• G. Lan, Gradient sliding for composite optimization, Mathematical Programming 159 (2016), 201–235. https://doi.org/10.1007/s10107-015-0955-5
• S. Ghadimi, G. Lan, H. Zhang, Generalized Uniformly Optimal Methods for Nonlinear Programming, Journal of Scientific Computing, 2019 (arXiv preprint 2015). arXiv:1406.5613

Motivation

Most machine learning training objectives — deep network losses, matrix factorization, regularized empirical risk with a nonconvex loss — are not convex, yet the great majority of convergence theory available before Ghadimi and Lan's 2013 work applied only to convex problems or gave no non-asymptotic rate at all. Ghadimi and Lan (2013) established the first non-asymptotic complexity bounds for stochastic first-order methods on smooth nonconvex problems, using the norm of a gradient mapping (rather than function-value suboptimality, which is meaningless without convexity) as the convergence measure, together with a randomized stopping rule that removes the need to know in advance which iterate will be best. This mission formalizes the constrained, composite generalization of that theory — Lan's own extension (2020) to problems with a nonsmooth term $h$ and a general Bregman geometry rather than the Euclidean norm — culminating in the stochastic complexity bound for the randomized stochastic mirror descent (RSMD) algorithm.

Setting

Fix a nonempty closed convex $X\subseteq\mathbb{R}^n$, a continuously differentiable (possibly nonconvex) $f:X\to\mathbb{R}$ with $L$-Lipschitz gradient, and a simple convex (possibly nonsmooth) $h:X\to\mathbb{R}$ (e.g. $h=\|\cdot\|_1$ or $h\equiv0$); write $\Psi:=f+h$, $\Psi^*:=\min_{x\in X}\Psi(x)$ (assumed finite). For a distance-generating function $\nu$ with modulus 1 and its prox-function $V(z,x):=\nu(x)-\nu(z)-\langle\nabla\nu(z),x-z\rangle$, the generalized projection at $x$ with gradient-like input $g$ and stepsize $\gamma>0$ is

$$x^+ := \arg\min_{u\in X}\Big\{\langle g,u\rangle + \tfrac1\gamma V(x,u) + h(u)\Big\}, \qquad P_X(x,g,\gamma) := \tfrac1\gamma(x-x^+),$$

which reduces to $\nabla f(x)$ itself when $X=\mathbb{R}^n$ and $h\equiv0$: $P_X$ is a generalized projected gradient (or gradient mapping) of $\Psi$ at $x$, and its norm going to zero is the right notion of "approximately stationary" for the composite, possibly-nonconvex problem $\min_{x\in X}\Psi(x)$.

The randomized stochastic mirror descent (RSMD) algorithm, given only a stochastic first-order oracle returning $G(x,\xi)$ with $\mathbb{E}[G(x,\xi)]=\nabla f(x)$ and $\mathbb{E}[\|G(x,\xi)- \nabla f(x)\|^2]\le\sigma^2$ (Assumption 13), forms a mini-batch average $G_k$ of $m_k$ oracle calls at each step $k$, updates $x_{k+1}$ via the generalized projection with $g=G_k$, and stops at a randomly chosen index $R$ (drawn from a prescribed pmf $P_R$, independently of the optimization process) rather than a deterministic final iterate.

Formalization targets

Goal — Theorem 6.6(a), RSMD complexity

$$\mathbb{E}\big[\|\tilde g_{X,R}\|^2\big] \le \frac{LD_\Psi^2 + \sigma^2\sum_{k=1}^N(\gamma_k/ m_k)}{\sum_{k=1}^N(\gamma_k-L\gamma_k^2)}, \qquad \tilde g_{X,k}:=P_X(x_k,G_k,\gamma_k),$$

for $0<\gamma_k\le1/L$ (strict for at least one $k$) and $P_R$ chosen as in (6.2.30), the expectation over both $R$ and the oracle randomness $\xi_{[N]}$.

Supporting milestones, in attack order

• Lemma 6.4: $\langle g,P_X(x,g,\gamma)\rangle \ge \|P_X(x,g,\gamma)\|^2 + \tfrac1\gamma[h(x^+) -h(x)]$ — the bound that lets a smoothness inequality on $f$ become a descent inequality on the whole composite $\Psi$.
• Lemma 6.6: the three-point characterization of $x^+$, the composite-problem analogue of Chapter 3's Lemma 3.4.
• Theorem 6.5 (deterministic ancestor): $\|g_{X,R}\|^2 \le LD_\Psi^2/\sum_{k=1}^N(\gamma_k- L\gamma_k^2/2)$ for the exact-gradient nonconvex MD algorithm.
• Corollary 6.4: the constant-stepsize instantiation $\|g_{X,R}\|^2\le2L^2D_\Psi^2/N$.

Every result states its constants exactly as the book derives them; no milestone or the goal hides a rate behind an unspecified $O(\cdot)$.

Significance

The goal theorem gives the complexity of the RSMD algorithm in terms of a squared generalized gradient-mapping norm — the correct convergence criterion for constrained, composite, possibly nonconvex stochastic optimization, since function-value suboptimality is not controllable without convexity and unconstrained gradient norms are meaningless once $X\ne\mathbb{R}^n$ or $h$ is nonsmooth. Choosing $m_k$ and $N$ appropriately (a corollary this mission does not formalize) turns this bound into the celebrated $O(\sigma^2/\varepsilon^2)$ total-oracle-call complexity for finding an $\varepsilon$-stationary point in expectation — the standard benchmark every later stochastic nonconvex method (variance-reduced SGD, SPIDER, and their composite/constrained variants) is compared against.

No result in this mission has a machine-checked proof on Prove2Me under this exact hypothesis set. The two closest platform results, both from lean-optrates (Shi), are genuinely different objects: ShiOptRates.gd_exact_rate is plain, unconstrained, deterministic gradient descent ($x_{k+1}=x_k-L^{-1}g(x_k)$, no set $X$, no composite $h$, no generalized projection), and ShiOptRates.Stochastic.sgd_rate is plain SGD under the same unconstrained, non-composite setup — its filtration/conditional-expectation formalization pattern (a Filtration ℕ, μ[·|ℱ k] for the unbiasedness and variance-bound hypotheses) is the same one this mission's goal theorem uses, confirming it as the platform's established idiom for this class of result, but the mathematical content (plain gradient step vs. generalized-projection/mirror-descent step, no $X$ or $h$) is different. Neither is reused; both are noted as the platform's nearest existing work.

Difficulty

The generalized projection $x^+$ replaces the Euclidean projection with an arbitrary Bregman-based prox-mapping and absorbs the nonsmooth term $h$ directly into the subproblem — a formalization that quietly assumes $h\equiv0$ or $X=\mathbb{R}^n$ would collapse every milestone here into the $\nabla f(x)$ special case and prove nothing about the constrained composite problem the chapter is actually about. The harder difficulty is in the goal theorem's own randomness: the book's proof does not use an unconditional (marginal) form of Assumption 13, because from step 2 onward $x_k$ is itself a random variable (a function of the history $\xi_{[k-1]}$), so the cross-term $\mathbb{E}[\langle\delta_k,g_{X,k}\rangle]$ the proof needs to vanish requires a conditional statement — "$\mathbb{E}[\langle\delta_k,g_{X,k}\rangle\mid\xi_{[k-1]}]=0$" is the book's own phrasing. A formalization using only marginal moment bounds would either be unprovable as stated or, worse, would misstate the theorem by using hypotheses too weak for the claimed conclusion.

Formalization scope

generalized_projection_gradient_bound, generalized_projection_characterization, nonconvex_md_bound and nonconvex_md_rate are stated over a real inner product space (Chapter 6's own generality — unlike Chapter 3, §6.2.3 explicitly restricts to "the norm associated with the inner product"), with every argmin-defined point ($x^+$, and the iterate sequence $x_k$) represented by its pointwise minimality property rather than an argmin term, consistent with this series' convention. The goal theorem, rsmd_complexity_bound, additionally introduces a probability space (Ω,P) and a Mathlib Filtration ℕ 𝒢, with x k/G k required 𝒢(k-1)-strongly-measurable and Assumption 13 stated via MeasureTheory.condExp (𝒢 (k-1)) (conditional mean 0, conditional second moment ≤ σ²/m_k) — the conditional form the book's own proof actually needs, not a weaker marginal substitute. The σ²/m_k bound is (6.2.40)'s conclusion for the m_k-sample batch average, taken as a hypothesis on the already-averaged G k directly rather than re-derived from m_k raw i.i.d. calls (that derivation is not itself a numbered result of the book). $R$'s independence from the process is stated via ProbabilityTheory.IndepFun; every integrability side condition the conclusion's Bochner integral needs to be non-vacuous is stated explicitly, guarding against the well-known trap of an uninhabited/non-integrable hypothesis silently defaulting condExp/the integral to 0 and making the theorem trivially true.

A trivializing formalization this mission rules out: taking $X=\mathbb{R}^n$ and $h\equiv0$ throughout would make every generalized projection collapse to the ordinary gradient, reducing this entire mission to a restatement of plain (stochastic) gradient descent — exactly the ShiOptRates results already on the platform — rather than the constrained composite theory the chapter develops; $X$, $h$ and $V$ are kept as genuine free parameters in every milestone and the goal.

Left out of scope, for time: Theorem 6.6(b) (the convex-case corollary on $\mathbb{E}[\Psi (x_R)-\Psi(x^*)]$, requiring the nondecreasing/nonincreasing stepsize side-conditions of (6.2.33)/(6.2.35)); the raw-sample derivation of (6.2.40); Lemma 6.3 (the stationarity consequence of a small gradient mapping, using $\partial h$ and the normal cone $N_X$); the 2-RSMD algorithm and its large-deviation improvement; and the gradient-free (RSMDF) variant.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, §6.2. https://doi.org/10.1007/978-3-030-39568-1
• S. Ghadimi and G. Lan, "Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming," SIAM Journal on Optimization, 23(4), 2013, pp. 2341–2368.
• S. Ghadimi, G. Lan and H. Zhang, "Mini-batch Stochastic Approximation Methods for Nonconvex Stochastic Composite Optimization," Mathematical Programming, 155(1–2), 2016, pp. 267–305 (the RSMD algorithm's original source).

Motivation

Gradient descent's convergence rate for a general smooth convex problem is $O(1/k)$ in the function-value gap; Nemirovski and Yudin (1983) proved that no first-order method can do better than $O(1/k^2)$ is achievable, and Nesterov (1983, 1988, 2004) constructed the first method attaining it — the accelerated (or "fast") gradient method. For thirty years this was the standard route to $O(1/k^2)$-rate solvers in convex optimization, and the technique underlies essentially every modern accelerated first-order method used at scale in machine learning (accelerated SGD, momentum methods, Nesterov-style extensions of Adam). The two building blocks this mission formalizes on the way there — subgradient descent (Polyak, 1960s) and mirror descent (Nemirovski & Yudin, 1983) — are themselves the default tools whenever the objective is nonsmooth or the constraint set's natural geometry is not Euclidean (e.g. the probability simplex, where mirror descent with the entropic distance-generating function beats projected subgradient descent by a $\sqrt{n/\ln n}$ factor).

Setting

Fix a nonempty closed convex set $X$ (in Lean: a normed real vector space $E$, X : Set E) and a convex $f : X \to \mathbb{R}$; write $f^* := \min_{x\in X} f(x)$ and $x^*$ for an arbitrary minimizer. The projected-subgradient update is $x_{t+1} := \arg\min_{x\in X}\gamma_t\langle g(x_t),x\rangle + \tfrac12\|x-x_t\|_2^2$ for a subgradient $g(x_t)\in\partial f(x_t)$ and stepsize $\gamma_t>0$. Its generalization, mirror descent, replaces the Euclidean proximal term with a Bregman divergence $V(x,z) := \nu(z) - \nu(x) - \langle\nabla\nu(x),z-x\rangle$ built from a 1-strongly-convex distance-generating function $\nu$ with respect to a general norm $\|\cdot\|$ (dual norm $\|\cdot\|_*$): $x_{t+1} := \arg\min_{x\in X}\gamma_t g_t(x) + V(x_t,x)$, where $g_t$ is now a continuous linear functional (a subgradient in the dual space, since the norm need not come from an inner product). Choosing $\nu(x)=\|x\|_2^2/2$ recovers $V(x,z) = \|z-x\|_2^2/2$ and the plain subgradient update as a special case.

The accelerated gradient method additionally assumes $f$ has $L$-Lipschitz gradient ($f(y)-f(x)-\langle f'(x),y-x\rangle \le \tfrac{L}{2}\|y-x\|^2$) and is $\mu$-generalized-strongly-convex w.r.t. $V$ ($f(x)+\langle f'(x),y-x\rangle+\mu V(x,y)\le f(y)$ for $\mu\ge0$), and tracks three coupled sequences from $(x_0,\bar x_0)\in X\times X$:

$$\tilde x_t = (1-q_t)\bar x_{t-1}+q_tx_{t-1},\quad x_t = \arg\min_{x\in X}\{\gamma_t[\langle f'(\tilde x_t),x\rangle+\mu V(\tilde x_t,x)]+V(x_{t-1},x)\},\quad \bar x_t = (1-\alpha_t)\bar x_{t-1}+\alpha_tx_t.$$

Formalization targets

Goal — Theorem 3.6, closed-form rate

With $q_t=\alpha_t=\tfrac{2}{t+1}$, $\gamma_t=\tfrac{t}{2L}$ and $\mu=0$:

$$f(\bar x_k) - f(x^*) \le \frac{4L}{k(k+1)}V(x_0,x^*).$$

Supporting milestones, in attack order

• Lemma 3.1 / Theorem 3.1 (Euclidean case): the three-point inequality for the plain projected-subgradient step, and the resulting $\sum_t \gamma_t[f(x_t)-f(x)] \le \tfrac12(\|x-x_s\|_2^2 + M^2\sum_t\gamma_t^2)$ bound under $M$-Lipschitz $f$.
• Lemma 3.4 / Theorem 3.5 (general-norm mirror descent): the same two results with the squared Euclidean distance replaced by $V$ and the Euclidean norm by a general dual pair $\|\cdot\|,\|\cdot\|_*$.
• Proposition 3.1: the one-step accelerated-method recursion $f(\bar x_t)-f(x)+\alpha_t(\mu+ 1/\gamma_t)V(x_t,x) \le (1-\alpha_t)[f(\bar x_{t-1})-f(x)]+(\alpha_t/\gamma_t)V(x_{t-1},x)$.
• Theorem 3.6, general form: Proposition 3.1's recursion telescoped across $t=1,\dots,k$ (with $\mu=0$) into a single two-term bound relating step $k$ to step $0$.

Every constant here is exactly the book's; no milestone hides an $O(\cdot)$ behind an unspecified absolute constant.

Significance

The chain culminates in an explicit, non-asymptotic $O(1/k^2)$ certificate for accelerated gradient descent — the theoretically optimal rate for smooth convex minimization by a first-order method (matching the Nemirovski–Yudin lower bound, not re-derived here). Formalizing it forces every implicit convention in a standard optimization-course derivation to become explicit: which of the three sequences $x_t,\tilde x_t,\bar x_t$ a given quantity refers to, exactly which inequality (3.3.7)-(3.3.9) each specific stepsize schedule needs to satisfy, and the precise index range over which the chapter's own stated hypotheses actually get used in its own proof (see Difficulty below).

None of these six results (or their strongly-convex counterpart, Theorem 3.7, left for future work — see Formalization scope) has a machine-checked proof on Prove2Me. The one theorem with the same name as this mission's subject, BanditAlgorithm.mirror_descent_regret_bound (Lattimore & Szepesvári, Theorem 28.4), is a different object: an online, adversarial regret bound against a changing sequence of loss vectors $y_t$, not an offline function-value gap for a single fixed $f$; not reused. Likewise OnlineConvexOpt.FirstOrder.online_gradient_descent_regret (Hazan) and OnlineConvexOpt.ConvexBasics.constrained_gd_well_conditioned_convergence are, respectively, an online-regret bound and a plain-gradient-descent (non-accelerated) linear-rate result — checked and confirmed not reusable per the mission brief.

Difficulty

The three-point inequalities (Lemmas 3.1/3.4) are routine consequences of a strongly-convex minimizer's optimality condition. The real difficulty is bookkeeping across three coupled sequences in the accelerated method: a formalization using only $x_t$ and $\bar x_t$ (dropping $\tilde x_t$, the point at which the gradient is actually evaluated) is not Lan's algorithm and proves either a false or a different bound — $\tilde x_t$ is what lets the method use a gradient computed at a point between $x_{t-1}$ and $\bar x_{t-1}$, which is exactly the extrapolation step that makes acceleration work.

A second, subtler difficulty is that Theorem 3.6's own stated hypothesis — "(3.3.15) for any $t=1,\dots,k$" — is not quite what its proof uses. Telescoping Proposition 3.1's per-step bound via (3.3.15) requires the previous step's constants $\gamma_{t-1},\alpha_{t-1}$; at $t=1$ these would be $\gamma_0,\alpha_0$, values the recursion (3.3.4)-(3.3.6) never defines (it only ever uses $q_t,\gamma_t,\alpha_t$ for $t\ge1$). The book's own proof, read closely, invokes (3.3.15) only for $t=2,\dots,k$, with $t=1$ handled directly by Proposition 3.1's conclusion connecting $\bar x_1,x_1$ to the given base data $\bar x_0,x_0$. Formalizing the literal hypothesis range would either be unstatable (no $\gamma_0,\alpha_0$ exist) or vacuous (adding unused ghost parameters); this mission states the range the proof actually needs.

Formalization scope

Chapter 3's own §3.1/§3.2 split (Euclidean vs. general norm) is preserved rather than collapsed: subgradient_iterate_three_point/subgradient_descent_bound are stated over a real inner product space with the vector subgradient $g(x_t)\in E$ and the Euclidean norm, exactly matching §3.1; mirror_iterate_three_point/mirror_descent_bound and the two accelerated-method milestones are stated over a general real normed space [NormedAddCommGroup E] [NormedSpace ℝ E], with subgradients as continuous linear functionals E →L[ℝ] ℝ (whose Mathlib operator norm is already the dual norm $\|\cdot\|_*$, needing no separate definition) and the Bregman divergence $V : E \to E \to \mathbb{R}$ left as a free two-point function — but, following a 2026-09-19 revision, no longer a totally free function. V is now required to satisfy the two facts (3.2.2)/(3.2.3)/(3.2.6) actually establish and every downstream proof (Lemma 3.4, Theorem 3.5, Proposition 3.1, Theorem 3.6) uses: nonnegativity ($V(x,z)\ge 0$ for $x,z\in X$) and the three-point/cosine identity $V(x,z) = V(x,y) + \langle\nabla V(x,\cdot)(y), z-y\rangle + V(y,z)$, the latter made explicit via an added parameter dV : E → E → (E →L[ℝ] ℝ) read as "the gradient of $V(x,\cdot)$ at $y$." Without these two hypotheses the five items that use an abstract V (mirror_iterate_three_point, mirror_descent_bound, accelerated_one_step_recursion, accelerated_gradient_recursion_bound, accelerated_gradient_rate) are false as stated — a constant V satisfies the bare pointwise-minimality hypotheses while violating the conclusion, as two worked counterexamples confirmed. This mission does not derive V/dV from an explicit distance-generating function $\nu$ (the heavier, fully book-literal route (3.2.1)-(3.2.2) would); it takes the two facts the proofs actually consume as hypotheses directly, which is lighter and sufficient. Satisfiability is witnessed by the Euclidean case already in §3.1: $\nu(x)=\|x\|^2/2$, $V(x,z)=\|z-x\|_2^2/2$, $dV\,x\,y = \langle y-x,\cdot\rangle$, exactly how subgradient_iterate_three_point/subgradient_descent_bound already handle the Euclidean special case. A trivializing formalization this mission rules out: specializing $V$ to the Euclidean squared distance in mirror_iterate_three_point/mirror_descent_bound would make those two milestones restatements of the §3.1 Euclidean results rather than genuine generalizations, exactly the pitfall the chapter brief flags.

Every argmin-defined iterate ($x_{t+1}$ in each of the three update rules) is represented by its defining pointwise-minimality property rather than by an IsMinOn/argmin term, so no existence or uniqueness lemma for the underlying minimization problem is needed anywhere in this mission — matching how the book's own proofs use these updates (via their first-order optimality condition, never via an explicit formula for the minimizer).

Left out of scope, for time: Theorem 3.7 (the strongly-convex, $\mu>0$ linear-rate companion to Theorem 3.6, sharing Proposition 3.1 as its own base lemma) and Corollary 3.5 (the composite-objective extension $f=\hat f+F$). Both are natural continuations reusing this mission's accelerated_one_step_recursion; a later mission or an amendment to this one could add them as additional milestones/goals without touching what is here.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 3. https://doi.org/10.1007/978-3-030-39568-1
• Y. Nesterov, "A method for solving the convex programming problem with convergence rate $O(1/k^2)$," Doklady AN SSSR, 269, 1983, pp. 543–547.
• Y. Nesterov, Introductory Lectures on Convex Optimization, Springer, 2004.
• A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983 (source of the mirror-descent method and the $O(1/k^2)$ lower bound for smooth convex optimization).

Motivation

Von Neumann's minimax theorem (Chapter VIII) settles two-player zero-sum games with scalar payoffs. In 1956, Blackwell asked the natural generalization: what can a player guarantee in a repeated game with vector-valued payoffs, where "winning" means driving the average payoff into a target set rather than above a target value? For decades the resulting theory — approachability — and the regret-minimization theory this book develops were believed to be different, with approachability seen as the stronger notion. Chapter 13 closes that gap: approachability and online convex optimization are shown to be algorithmically equivalent, each reducible to the other with no loss of efficiency, and along the way this equivalence yields a constructive, rate-quantified proof of Blackwell's own theorem.

Setting

A generalized vector game (Definition 13.2) is given by bounded convex closed decision sets $K_1,K_2$ and a vector payoff $u:K_1\times K_2\to\mathbb R^d$. A set $S$ is approachable (Definition 13.3) if some non-anticipating algorithm, playing in $K_1$ against any sequence $y_1,y_2,\dots\in K_2$, drives the average payoff's distance to $S$ to zero. Blackwell's theorem (13.4) characterizes exactly which $S$ are approachable via a purely geometric condition: every column-player strategy $y$ admits a row-player best response $x$ landing the payoff in $S$.

Section 13.2 constructs an explicit approachability algorithm from any OCO algorithm: given a best-response oracle realizing Blackwell's condition, Algorithm 37 runs the OCO algorithm on the proxy losses $f_t(w) = w^\top u_{t-1} - h_S(w)$ (the support function $h_S(w)=\max_{x\in S}\{w^\top x\}$ letting distance-to-$S$ be written, via Lemma 13.5's minimax duality, as a convex optimization problem over the unit ball), queries the oracle at the OCO algorithm's play $w_t$, and averages the resulting rewards.

Formalization targets

Theorem 13.7 (OCO-to-approachability rate, milestone)

$$\mathrm{Dist}(\bar u_T, S) \le \frac{\mathrm{Regret}_T(A)}{T}.$$

Theorem 13.4 — the mission's goal (sufficiency direction only)

$$\big(\forall y\in K_2,\ \exists x\in K_1,\ u(x,y)\in S\big) \implies S\ \text{is approachable}.$$

Significance

This chapter's headline claim — approachability and OCO are equivalent — is proved in two directions in the book (§13.2 and §13.3); this mission drafts the direction the book itself foregrounds as "the more interesting implication" and constructively proves: any sublinear-regret OCO algorithm converts directly into an explicit approachability algorithm with an explicit convergence rate, giving a self-contained, algorithmic proof of a 1956 game-theory theorem using 1990s–2000s online-learning machinery. Historically, this equivalence resolved a standing misconception (approachability believed strictly stronger) and reframes Blackwell's theorem as a special case of regret minimization rather than a separate theory requiring its own toolkit. No prior art was found on the platform for Blackwell approachability (planning search: q=Blackwell — the one hit, PRNGCompression.prng_no_free_lunch's cousin, an unrelated Rao-Blackwellization result, is not a substitute); this mission drafts both items fresh.

Difficulty

Theorem 13.4's statement is a clean geometric implication, but the book is explicit that its proof is entirely carried by Theorem 13.7 plus an unstated "explicit conclusion" left as an exercise (the passage from a finite-horizon rate bound to the asymptotic Dist → 0 claim, using any of the book's own sublinear-regret OCO algorithms as a witness). Theorem 13.7's own proof combines three nontrivial facts: Lemma 13.5's minimax-duality rewriting of $\mathrm{Dist}(\cdot, S)$ as a linear optimization over the unit ball (itself proved via Sion's minimax theorem, not excerpted here), the best-response oracle's defining inequality (13.2) applied pointwise at each round's $w_t$, and the OCO algorithm's own regret guarantee applied to the specific proxy-loss sequence $f_t$ built from the realized game trajectory — a genuine composition of three separate pieces of machinery from earlier in the book (Chapters III–VIII), not a routine substitution.

Formalization scope

IsApproachable is declared as its own definition (per BRIEF.md's explicit instruction, since Theorem 13.4 depends on it), with the non-anticipation clause made explicit (matching the series' IsOnlineAlgorithm convention from Chunk 03) even though the book's own Definition 13.3 states it only informally ("x_t ← A(y_1,\dots,y_{t-1})"). SupportFunction is h_S exactly as displayed, as a real supremum (a genuine maximum given the chapter's standing "closed, bounded" hypothesis on S). $\mathrm{Dist}(\cdot,S)$ throughout is Euclidean distance, rendered as Mathlib's Metric.infDist — confirmed the chapter uses no other distance notion (checked §13.1-13.3 directly, per the pitfall BRIEF.md flags). Theorem 13.7 transcribes Algorithm 37's $f_t(w)=w^\top u_{t-1}-h_S(w)$ construction faithfully, including its one-round offset (using the previous round's realized reward to build the current round's proxy loss, while the conclusion averages the current round's rewards) — exactly as the book's own pseudocode has it, not smoothed over.

Scope decision on Theorem 13.4's biconditional. The book states Theorem 13.4 as an ↔ but proves, and explicitly flags as proved, only the sufficiency direction (←): "The necessity of this condition is left as an exercise... Our reductions henceforth give an explicit proof of Blackwell's theorem [meaning: of the sufficiency direction]." Per CAPTAIN_BRIEF.md rule 6 and BRIEF.md's explicit instruction, this mission drafts only that direction, named as such in the goal item's own docstring; see STATUS.md.

Not formalized (out of scope for this mission, given the remaining budget and the explicit "exercise" status of several results on these pages): the necessity direction of Theorem 13.4; Lemma 13.5 (minimax duality for Dist, itself relying on Sion's theorem, not separately formalized here); Lemma 13.6 (the equivalent best-response-oracle condition); §13.3's entire approachability-to-OCO direction (Theorem 13.9, Lemma 13.8, the cone/polar-cone machinery of §13.3.1) and §13.3.3 (existence of a best-response oracle for the constructed set); the "explicit conclusion" of Blackwell's theorem from Theorem 13.7, left as an exercise by the book itself.

Selected references

• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 13.
• D. Blackwell, "An analog of the minimax theorem for vector payoffs," Pacific Journal of Mathematics 6(1), 1956, 1-8.
• N. Abernethy, P. Bartlett, E. Hazan, "Blackwell approachability and no-regret learning are equivalent," COLT 2011.