Machine Learning

Motivation

Every convex optimization algorithm in machine learning — from projected gradient descent to support vector machines to the mirror-descent methods of later chapters of this book — is justified by a small set of optimality certificates: a checkable condition on a candidate solution that guarantees it actually solves the problem, without searching the whole feasible set. The most widely used such certificate is the Karush–Kuhn–Tucker (KKT) system: a set of gradient and complementary-slackness equations that a solution of a convex program with differentiable data must satisfy, and that (under a mild constraint qualification) is also sufficient. It is the tool a practitioner reaches for to check optimality of a numerical solver's output, and the tool a theorist reaches for to derive an algorithm (dual ascent, augmented Lagrangian, interior point methods) in the first place. Every convex machine learning model introduced in Chapter 1 of this book — regularized least squares, support vector machines, logistic regression with constraints — is an instance of the general convex program these milestones analyze.

The result traces back to Kuhn and Tucker's 1951 paper Nonlinear Programming, with Karush's 1939 unpublished thesis establishing the same conditions independently and earlier; Slater's 1950 unpublished note is the source of the constraint qualification that bears his name and that makes the necessity direction possible. Lan's Chapter 2 gives a compact, modern, purely finite-dimensional derivation of the whole chain — separation, duality, saddle points, KKT — from first principles, self-contained in about twenty pages, aimed squarely at the convex programs that appear in machine learning.

Setting

Fix $n, m, p \in \mathbb{N}$ and work in $\mathbb{R}^n$ with its standard inner product $\langle \cdot,\cdot\rangle$. A convex program (2.3.16) is

where $X \subseteq \mathbb{R}^n$ is a nonempty closed convex set, $f, g_1,\dots,g_m : X \to \mathbb{R}$ are convex, and $h_1,\dots,h_p$ are affine. A point $x \in X$ is feasible if it satisfies every $g_i(x)\le 0$ and $h_j(x)=0$; $x^*$ is optimal if it is feasible and $f(x^*)\le f(x)$ for every feasible $x$.

The normal cone of $X$ at $x$ is $N_X(x) := \{w \in \mathbb{R}^n : \langle w, y-x\rangle \le 0 \ \forall y \in X\}$ — the set of directions that make an obtuse angle with every direction into $X$ from $x$; it is $\{0\}$ when $X = \mathbb{R}^n$, recovering unconstrained first-order optimality. The Lagrangian is $L(x,\lambda,y) := f(x) + \sum_i \lambda_i g_i(x) + \sum_j y_j h_j(x)$ for multipliers $\lambda \ge 0$, $y \in \mathbb{R}^p$; the Lagrange dual value is $\varphi(\lambda,y) := \min_{x\in X} L(x,\lambda,y)$, and the Lagrange dual problem is $\varphi^* := \max_{\lambda\ge 0,\,y}\varphi(\lambda,y)$. Weak duality, $\varphi^*\le f^*$, holds unconditionally by construction. Slater's condition asks for $\bar x \in \operatorname{int} X$ with $g(\bar x) < 0$, $h(\bar x)=0$; the restricted Slater condition weakens the interior requirement to the relative interior $\operatorname{rint} X$ while keeping strict inequality for every (here: every) nonlinear constraint.

Formalization targets

Goal — Theorem 2.8(b), KKT necessity

Companion — Theorem 2.8(a), KKT sufficiency

Supporting milestones, in attack order

• Theorem 2.1 (separation): a point outside a closed convex set is strictly separated from it by a hyperplane.
• Proposition 2.9 (Convex Theorem on Alternative): insolvability of a strict-inequality system, plus a Slater point, forces solvability of a dual multiplier system.
• Theorem 2.6 (strong duality): under Slater's condition, $\varphi^* = f^*$ and the dual is solvable.
• Theorem 2.7(a)/(b) (saddle points): $x^*$ is optimal iff it extends to a saddle point of $L$ (the "only if" needs Slater's condition; the "if" needs nothing beyond the saddle inequalities).

Each of these five is stated the way the book states it — no constant is hard-coded, no O(·) is involved, and every hypothesis (closedness, convexity, Slater/restricted-Slater) is exactly the one the corresponding proof uses.

Significance

The KKT system is the interface between convex optimization theory and every algorithm that exploits it: primal-dual methods track approximate KKT residuals as a stopping criterion, and the derivation of the Lagrange dual (used throughout the book's later treatment of composite and constrained problems) rests on strong duality, milestone strong_duality here. The saddle-point characterization (saddle_point_sufficient/saddle_point_necessary) is the standard route to designing an algorithm: a method that provably drives a pair $(x_k,\lambda_k)$ to a saddle point of $L$ is provably convergent to an optimal $x^*$, without ever needing to verify optimality directly against the primal problem.

None of the six substantive results here has a machine-checked proof on Prove2Me. The platform holds a genuinely weaker unconstrained-in-$K$ condition (OnlineConvexOpt.ConvexBasics. kkt_optimality, Hazan's Theorem 2.2: $\langle\nabla f(x^*), y-x^*\rangle \ge 0$ for $y \in K$, with no inequality/equality constraints or multipliers at all) and a structurally different, strictly more general cone-based Lagrange-duality development (VectorSpaceOpt.lagrange_duality and VectorSpaceOpt.lagrangian_saddle_sufficient_pointed, from Luenberger, which bundle all constraints into a single map into a convex cone in a general normed space, rather than Lan's explicit $\mathbb{R}^m$ inequality / $\mathbb{R}^p$ equality split). Formalizing this mission produces the finite-dimensional convex-program version of KKT in exactly the shape it is used and taught: separate multiplier vectors for inequality and equality constraints, an explicit normal cone rather than a cone-map abstraction, and both directions of the necessity/sufficiency split.

Difficulty

The separation theorem (Theorem 2.1) itself is routine once the projection onto a closed convex set is available. The real difficulty is entirely in the direction of the Convex Theorem on Alternative that Proposition 2.9 states: the naive idea — "insolvability of (I) should give a separating hyperplane between $\{x : f(x)<c\}$ and $\{x: g(x)\le 0\}$ directly" — fails, because these are sets in $\mathbb{R}^n$ and separating them there does not produce a sign-definite multiplier vector. Lan's proof instead lifts to $\mathbb{R}^{m+1}$ and separates the epigraph-like set $T = \{u : \exists x\in X,\ f(x)\le u_0, g(x)\le u_{1:m}\}$ from the open orthant-like set $S = \{u: u_0<c, u_{1:m}\le 0\}$; only in this lifted space does the separating normal's sign constraint (forced by $S$'s unboundedness in the positive directions) translate into $\lambda \ge 0$. Getting the sign of the $0$-th coordinate strictly positive — needed to normalize and divide — is itself a small separate argument using the Slater subsystem's solution. The KKT necessity direction (the goal) then chains three of these already-nontrivial results (separation → CTA → strong duality → saddle necessity) before translating the saddle-point condition on $L$ into the gradient/normal-cone form via differentiability of $f, g$ at $x^*$.

Formalization scope

All milestones are stated over EuclideanSpace ℝ (Fin n) with Convex/ConvexOn from Mathlib. Affine equality constraints $h_j$ are represented by explicit witnesses $w_j \in \mathbb{R}^n, b_j \in \mathbb{R}$ with $h_j(x) = \langle w_j, x\rangle + b_j$, so that $\nabla h_j = w_j$ is available without a separate affine-differentiability lemma. The normal cone $N_X^*(x)$ is Lan's own primal-space object (normalCone); the restricted Slater condition uses Mathlib's intrinsicInterior ℝ X for $\operatorname{rint} X$, distinct from the plain interior X used by the un-restricted Slater condition of Theorems 2.6/2.7(b). Primal optimal values and Lagrange dual values are stated via IsGLB/pointwise-inequality forms rather than raw sInf, so that no hypothesis is silently made true by an empty or unbounded set defaulting sInf to a junk value — in every milestone here the relevant set is guaranteed nonempty by the Slater-point hypothesis already present.

A trivializing formalization this mission rules out: stating kkt_necessary/kkt_sufficient with $X = \mathbb{R}^n$ (no set constraint) and empty $g, h$ (no functional constraints) would collapse the normal-cone condition to $\nabla f(x^*) = 0$ and make the whole KKT apparatus vacuous of any duality content; the milestones here keep $X$, $g$ and $h$ as genuine free parameters (the theorems are stated for arbitrary m, p : ℕ, including but not restricted to the degenerate case) so that the constrained content of Lan's theorem is what gets proved.

Reusable beyond this mission: normalCone and lagrangian are generic enough that any later chapter of this book needing Lagrangian duality or normal-cone stationarity (none of the current first-wave chapters 03/06 needs them directly) could import them once published rather than redeclaring. Contributions most welcome on the two hardest milestones, cta_solvable_of_insolvable and kkt_necessary, since they carry the mission's real difficulty; separation_point_closed can likely be discharged quickly via Mathlib's geometric_hahn_banach_point_closed.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 2. https://doi.org/10.1007/978-3-030-39568-1
• H. W. Kuhn and A. W. Tucker, "Nonlinear Programming," Proceedings of the Second Berkeley Symposium on Mathematical Statistics and Probability, 1951, pp. 481–492.
• W. Karush, "Minima of Functions of Several Variables with Inequalities as Side Constraints," M.Sc. thesis, University of Chicago, 1939.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (standard modern reference for the separation theorem and Lagrangian duality used throughout).

Motivation

Every statistical guarantee for a learning algorithm ultimately rests on a concentration inequality: a bound on how far an empirical average can stray from its expectation. For real-valued averages, Bernstein's inequality (1924, refined through the 20th century) is the classical tool — sharper than Hoeffding's inequality whenever the summands' variance is small compared to their range. Modern learning theory, however, frequently needs to control averages of objects that are not real numbers but elements of a Hilbert space: feature vectors $\Phi(x_i)y_i$, gradients of a loss, or the values a kernel machine's empirical risk functional takes. Steinwart & Christmann, Support Vector Machines (Springer 2008, Information Science and Statistics), Chapter 6, develop exactly the vector-valued extension needed for the book's own SVM consistency proofs: Theorem 6.14, Bernstein's inequality for independent random variables taking values in a separable Hilbert space, and its corollaries.

Setting

Fix a probability space $(\Omega,\mathcal A,P)$ and a separable real Hilbert space $H$. Random variables $\xi_1,\dots,\xi_n : \Omega \to H$ are independent if the family is mutually independent (not merely pairwise), and $\xi_i$ has essential supremum bound $B$, $\|\xi_i\|_\infty \le B$, if $\|\xi_i(\omega)\|_H \le B$ for $P$-almost every $\omega$. Writing $\mathbb E$ for $\mathbb E_P$, the quantities of interest are the mean $\mathbb E\,\xi_i \in H$ (a Bochner integral) and the variance bound $\sigma^2$, an upper bound on $\mathbb E\,\|\xi_i\|_H^2$.

The classical scalar case (Theorem 6.12, itself a refinement of Hoeffding's inequality, Theorem 6.10) bounds $P\big(\frac1n\sum_i \xi_i \ge \varepsilon\big)$ for real-valued, mean-zero, range- and variance-bounded $\xi_i$. The tool behind both the scalar and the vector-valued case is a general exponential-moment inequality (Theorem 6.13) valid for independent, integrable random variables taking values in any separable Banach space $E$:

Formalization targets

Goal: Theorem 6.14 (Bernstein's inequality in Hilbert spaces)

for independent, mean-zero $\xi_1,\dots,\xi_n : \Omega \to H$ with $\|\xi_i\|_\infty \le B$ and $\mathbb E\|\xi_i\|_H^2 \le \sigma^2$. This is the weakest stable form of the claim: it is stated for a general separable Hilbert space (not a fixed finite dimension), with the tail written as a sum of three explicit terms rather than folded into an unspecified constant, so it survives specialization to any concrete $H$ without modification.

Supporting facts

Theorem 6.13 (above) is the direct tool Theorem 6.14's own proof invokes ("we will prove the assertion by applying Theorem 6.13"); Theorem 6.12 is the scalar analogue Theorem 6.14 generalizes, included to make the generalization's exact form (three terms, not two) checkable against its source; Corollary 6.15, Hoeffding's inequality in Hilbert spaces, is the immediate mean-free-of-a-variance-bound consequence of Theorem 6.14 obtained by centering, reused directly in the book's own oracle-inequality proof (§6.4).

Significance

Theorem 6.14 is the concentration inequality behind the book's later empirical-process arguments for SVMs: whenever an SVM's analysis needs to bound the deviation of an empirical average of Hilbert-space-valued quantities (feature-map evaluations, loss gradients) from its mean, this is the tool invoked, via Corollary 6.15 in the book's own oracle-inequality derivation. Its distinct contribution over simply applying the scalar Theorem 6.12 coordinate-by-coordinate (which is not available without a fixed, finite orthonormal basis, and even then would produce dimension- dependent bounds) is that the bound here is entirely dimension-free: it depends on $H$ only through the variance bound $\sigma^2$ and the range bound $B$, not through $\dim H$.

The scalar Bernstein inequality is classical (Bernstein 1924, refined by Bennett 1962 and others to the sharper multiplicative form used here); its Banach- and Hilbert-space generalizations (via the martingale-difference / Yurinskii-type argument Theorem 6.13's proof uses) are standard in the empirical-process-theory literature by the time of this book (see, e.g., Pinelis 1994 for closely related Banach-space martingale inequalities). No machine-checked Lean proof of the Hilbert-space form is known to exist on the platform at the time of writing (the platform's own HighDimProb.Concentration.bernstein_unweighted, from the Vershynin series, is a different, sub-exponential-norm scalar statement — see Formalization scope); this mission asks for the book's own bounded-summand, explicit-constant Hilbert-space form.

Difficulty

The natural first attempt generalizes the scalar proof's Markov-inequality argument directly: bound $\mathbb E\,e^{t\|\sum_i\xi_i\|}$ using independence. This breaks immediately because $\|\cdot\|_H$ is not linear, so $e^{t\|\sum_i \xi_i\|}$ does not factor over $i$ the way $e^{t\sum_i \xi_i}$ does in the scalar case — there is no vector-valued analogue of the moment generating function that tensorizes under independence directly. Theorem 6.13's proof resolves this with a martingale-difference decomposition (writing the deviation as a telescoping sum of conditional-expectation differences $X_k$ across the filtration generated by $\xi_1,\dots,\xi_k$) rather than a direct product-of-moment-generating-functions argument, at the cost of needing $E$ separable (for the conditional expectations and the resulting sums to be well-defined and measurable). Deriving Theorem 6.14 from Theorem 6.13 then requires controlling the two extra terms Theorem 6.13 introduces (the mean-norm term and the per-summand correction) using only the Hilbert-space-specific facts $\mathbb E\langle\xi_i,\xi_j\rangle=0$ for $i\ne j$ (from independence and mean-zero) and the scalar bound on $\mathbb E\|\xi_i\|^2$ — which is exactly where the tail's extra $\sqrt{\sigma^2/n}$ term originates, and is not obtainable by naively reusing the scalar Theorem 6.12's two-term optimization over $t$ unchanged.

Formalization scope

$H$ (and, for Theorem 6.13, $E$) is an arbitrary separable real (Hilbert, resp. Banach) space — not fixed to a Euclidean space of any dimension — matching the book's own generality, which is essential since the theorem's dimension-independence is part of its content. $\|\xi_i\|_\infty \le B$ is formalized as the almost-sure bound ∀ᵐ ω ∂P, ‖ξ i ω‖ ≤ B, matching the book's $L^\infty(P)$ convention rather than requiring the bound to hold for literally every $\omega$. Independence is the mutual independence of the whole family (Mathlib's iIndepFun), matching Theorem 6.13's proof, which uses independence of $\xi_k$ from $\sum_{i\ne k}\xi_i$ for every $k$ simultaneously, not merely pairwise independence.

A trivializing formalization would state the conclusion in terms of the scalar random variable $\|\xi_i\|_H$ rather than the vector-valued average's norm $\big\|\frac1n\sum_i \xi_i\big\|_H$ — this would collapse the theorem to an easier scalar statement about a nonnegative random variable and lose the whole point of the vector-valued generalization; it is ruled out here by writing the norm of the sum (not a sum of norms) inside the probability. Likewise, dropping the $\sqrt{\sigma^2/n}$ middle term of the tail bound (present here, absent from the scalar Theorem 6.12) would silently understate the genuine dimension-independent cost of vector-valued concentration; all three terms are kept.

Theorem 6.13's general Banach-space statement, and the scalar Theorem 6.12, are reusable beyond this mission (Theorem 6.13 is the tool any future Banach-space-valued concentration mission in this series would reach for first). The platform's existing HighDimProb.Concentration. bernstein_unweighted/hoeffding_rademacher (Vershynin series) are not reused as kind: reference items here: they use a sub-Gaussian/sub-exponential-Orlicz-norm parameterization and a universal (unspecified) constant, a genuinely different hypothesis structure from this chapter's explicit $L^\infty$-bounded, exact-constant form — reusing them would misrepresent this chapter's own, sharper statement. Completing the four sorrys (Theorems 6.12-6.14, Corollary 6.15) is welcome; the martingale-difference argument behind Theorem 6.13 is the natural starting point, since the other three all reduce to it directly.

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 6, §6.2, pp. 210-217).
• S. Bernstein, "On a modification of Chebyshev's inequality and of the error formula of Laplace," Ann. Sci. Inst. Sav. Ukraine, Sect. Math. 1(4), 1924 (original scalar inequality).
• G. Bennett, "Probability inequalities for the sum of independent random variables," Journal of the American Statistical Association 57(297), 1962, pp. 33-45. https://doi.org/10.1080/01621459.1962.10482149
• I. Pinelis, "Optimum bounds for the distributions of martingales in Banach spaces," Annals of Probability 22(4), 1994, pp. 1679-1706. https://doi.org/10.1214/aop/1176988477

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)

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

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.

Motivation

Online convex optimization (OCO) asks a learner to repeatedly pick a point in a convex set $K$, pay a cost that an adversary reveals only after the choice is made, and be judged against the best fixed point in hindsight. Chapter III of this series formalized the simplest general-purpose answer, online gradient descent (OGD): take a gradient step, project back onto $K$. OGD's analysis, however, is tied to the Euclidean geometry of the projection step — it treats every coordinate of $K$ alike, and its regret bound degrades badly when $K$'s natural geometry is not Euclidean (the probability simplex under the $\ell_1$ norm is the standard example, where a Euclidean-projection algorithm's regret scales with $\sqrt{n}$ in the dimension $n$, while an algorithm that exploits the simplex's own geometry attains regret scaling only with $\sqrt{\log n}$).

Regularized Follow the Leader (RFTL) is the meta-algorithm this chapter introduces to fix this: rather than fixing a specific geometry, RFTL is parameterized by an arbitrary regularization function $R$, and its regret bound depends on $R$ only through two scalar quantities the mission makes explicit — the range of $R$ over $K$, and a $R$-dependent "local norm" of the gradients. Choosing $R$ to match $K$'s geometry (entropy regularization on the simplex, for instance) recovers the sharp bounds that plain OGD cannot. RFTL and its close relative Online Mirror Descent (OMD), also introduced here, are the ancestors of essentially every regularization-based online learning algorithm in use today, including the multiplicative-weights/Hedge algorithm of Chapter I as a special case (entropy regularization on the simplex) and the exponentiated-gradient algorithm this book's own Chapter VIII reuses (Corollary 5.7, a further specialization of Theorem 5.2 this mission's Theorem 5.2 underlies). The naive "Follow the Leader" strategy this chapter opens by refuting — always play the empirically best point so far — is a natural first idea and provably fails: the book gives an explicit two-point cost sequence on which it incurs regret linear in the horizon. Regularization is the fix, and quantifying exactly how much it costs and buys is this chapter's content.

Setting

Fix a convex, nonempty decision set $K$ in a real inner product space $E$ and a sequence of convex cost functions $f_1, f_2, \dots : K \to \mathbb{R}$. As in Chapter III, regret after $T$ rounds is

A regularization function $R : K \to \mathbb{R}$ is a strongly convex, smooth, twice differentiable function with a positive-definite Hessian on the interior of $K$. Its Bregman divergence measures the gap between $R$ and its own first-order Taylor approximation:

By the mean value theorem, $B_R(x\|y) = \tfrac12\|x-y\|_z^2$ for some point $z$ on the segment $[x,y]$, where $\|\cdot\|_z$ is the norm induced by the Hessian $\nabla^2 R(z)$; its dual norm, denoted $\|\cdot\|_z^*$, is the local norm at $z$. Writing $\|\cdot\|_t$ for the local norm between consecutive iterates $x_t, x_{t+1}$, the $R$-diameter of $K$ is $D_R^2 = \max_{x,y\in K}(R(x)-R(y))$.

The RFTL algorithm (Algorithm 13), with step size $\eta > 0$, plays $x_1 = \arg\min_{x\in K} R(x)$, then at every round updates

The agile Online Mirror Descent algorithm (Algorithm 14, agile version) instead maintains a dual point $y_t$ with $\nabla R(y_1) = 0$, updates it by $\nabla R(y_{t+1}) = \nabla R(x_t) - \eta \nabla_t$, and projects via the Bregman divergence, $x_{t+1} = \arg\min_{x\in K} B_R(x\|y_{t+1})$ (with $x_1$ defined the same way from $y_1$). RFTL and the lazy variant of OMD coincide for linear costs (Lemma 5.5, not formalized here — it is not used by either target); the agile variant's analysis is genuinely different and is the mission's second target.

Formalization targets

Target (Theorem 5.2 — RFTL's regret bound)

This is the mission's goal: RFTL, run with any admissible regularizer, attains a regret bound governed only by the cumulative squared local norm of the gradients and $R$'s range over $K$. The bound is proved via two milestones: Lemma 5.3 (regret controlled by the total "prediction drift" $\sum_t \nabla_t^\top(x_t - x_{t+1})$ plus $D_R^2/\eta$), which in turn rests on Lemma 5.4 (a "follow-the-leader beats be-the-leader" comparison inequality, proved by induction on the horizon).

Further target (Theorem 5.6 — agile OMD's regret bound)

A structurally similar bound for the agile variant, included as its own goal-level item since — as the book states explicitly — its proof technique is unrelated to RFTL's, not a corollary of it.

Both targets are the book's own tightest, non-asymptotic statements: neither is weakened to an $O(\cdot)$ form, and the book's own further (unnumbered) corollary specializing Theorem 5.2 to a uniform local-norm bound $\|\nabla_t\|_t^* \le G_R$ is left out, matching this series' convention of formalizing only the numbered results.

Significance

The results themselves. Theorem 5.2 is the general regret theorem behind every regularization scheme in online learning: instantiating $R$ recovers the projected-gradient bound of Chapter III (Euclidean $R$), the multiplicative-weights bound of Chapter I (entropy $R$ on the simplex), and — through the exponentiated-gradient specialization (Corollary 5.7, not itself a target here) — the row-player regret bound this book's own Chapter VIII cites as "Eq. (8.1)" in its reduction of zero-sum games to regret minimization. Theorem 5.6 gives the same guarantee for an algorithm (agile OMD) that, unlike RFTL, maintains a feasible point at every round, which the book notes is preferable in the adaptive-regret setting of Chapter X.

Formalizing it. Both theorems have complete, elementary proofs in the source (no gaps, no "with high probability", no hidden regularity conditions); the mission's work is converting the analytic argument — the Bregman-divergence identity, the generalized Cauchy-Schwarz inequality bounding the drift term by the local norm, and the two induction arguments underlying Lemma 5.4 — into machine-checked statements. No formalization of RFTL, OMD, or the local-norm machinery exists on the platform (checked below); the closest Formalpedia entries state a related but distinctly narrower result.

Difficulty

The central obstacle is that the regularizer $R$ is a hypothesis, not a fixed function: the theorem must hold for every admissible $R$ simultaneously, so nothing about $R$ beyond its stated properties (strong convexity, smoothness, twice differentiability) may be used. A newcomer's first instinct — bound the local norm $\|\nabla_t\|_t^*$ by a fixed multiple of the Euclidean dual norm $\|\nabla_t\|_2$ — fails in general and is exactly the bound RFTL is designed to avoid needing; the whole point of the local-norm formulation is that it can be tight for regularizers (like entropy) whose Hessian is very far from a multiple of the identity. A second obstacle is Lemma 5.4's induction, which compares $x_{t+1}$ (a minimizer over $t+1$ terms) against $u$ using the minimality of $x_{t+1}$ at exactly the right instantiation — an argument that looks almost circular until the induction hypothesis is applied at $u = x_{t+2}$, not at the theorem's free variable.

Formalization scope

$K$ ranges over an arbitrary real, complete inner product space (a real Hilbert space), matching Chapters III and IV, not a fixed $\mathbb{R}^n$. The RFTL and agile-OMD update rules are represented relationally (IsArgMinOn), since Mathlib has no canonical argmin operator for a general convex set — mirroring IsMetricProjection's precedent from Chapter III. The Hessian at the mean-value-theorem's intermediate point is represented via the second Fréchet derivative of $R$'s gradient map (HasFDerivAt), since Mathlib has no dedicated Hessian type; the local dual norm is then any value satisfying the resulting existential characterization (IsLocalDualNormSq), stated once and shared by both targets. A boundedness hypothesis on $R$ over $K$ is added to Lemma 5.3's statement to keep the $R$-diameter $D_R^2$ from collapsing to Mathlib's junk value for an unbounded supremum — a condition every regularizer the book actually uses (strongly convex and smooth over a bounded $K$) already satisfies, so it narrows nothing.

Trivializing formalization ruled out. A regret bound stated for an "algorithm" defined loosely enough to include the after-the-fact optimal choice would be vacuous; IsRFTLRun and IsOMDAgileRun instead pin down the exact history-dependent update rule of Algorithms 13 and 14 (the current gradient sequence, the current regularizer, and nothing else) as a hypothesis, so a proof must genuinely use the specific update. Theorem 5.2 and Theorem 5.6 are kept as two separate items rather than one theorem parameterized by an algorithm choice, since — per the chapter's own remark that their analyses are unrelated — a merged statement would either need to branch internally on the algorithm or silently identify two genuinely different update rules.

Reuse and prior art. OnlineConvexOpt.FirstOrder.RegretT (Chapter III, published) is imported and reused verbatim, keeping the regret functional identical across the whole book. Definitions specific to Chapter IV (OnlineConvexOpt.SecondOrder, not yet published) are not imported per this series' convention that a draft cannot import another draft; quadForm is redeclared locally instead. On the platform, BanditAlgorithm.ftrl_regret_bound, BanditAlgorithm.mirror_descent_regret_bound, and BanditAlgorithm.ftrl_simplex_exp_weights_regret (the Bandit Algorithms series, Chapter XII) state regret bounds for FTRL and Mirror Descent in the linear-cost, bandit-idiom setting (a fixed linear loss $\langle a, y_t\rangle$ at each round, regret compared via a Bregman-divergence potential at fixed points). Hazan's Theorem 5.2 and 5.6 are for general convex $f_t$ and use the book's own local-norm object, which has no counterpart in those statements; they are read in full and are not faithful substitutes (different hypothesis class), so this mission drafts its own, independent items rather than reusing them.

Selected references

• Hazan, Introduction to Online Convex Optimization, 2nd ed., Chapter 5. arXiv:1909.05207v3
• Shalev-Shwartz, Online Learning and Online Convex Optimization, Foundations and Trends in Machine Learning, 2012 (surveys RFTL/Mirror Descent under the name "Online Mirror Descent"). https://doi.org/10.1561/2200000018
• Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003 (the Euclidean special case this chapter generalizes). https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf

Motivation

Online decision-making problems — multi-armed bandits, contextual bandits, structured bandits, and episodic reinforcement learning — look superficially different but share a common shape: a learner repeatedly acts, observes feedback, and is scored by regret against the best action in hindsight. Foster, Kakade, Qian and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making (Foster & Rakhlin, arXiv:2312.16730v1) develops a unifying account of this shape and asks a sharper question than "does this specific algorithm work?": for a given class of possible environments, what is the best regret any algorithm can achieve? The Decision-Estimation Coefficient (DEC), introduced by Foster, Kakade, Qian and Rakhlin (2021, "The Statistical Complexity of Interactive Decision Making") and refined by Foster, Golowich, Qian, Rakhlin and Sekhari (2023), was proposed as the answer: a single real-valued complexity measure of a model class that simultaneously (i) drives a generic optimal-up-to-constants algorithm (Estimation-to-Decisions, E2D), and (ii) lower-bounds the regret of every algorithm. Item (ii) is what turns the DEC from "a complexity measure that happens to work for the algorithms we know" into a genuine characterization of statistical difficulty, in the same sense that minimax rates characterize the difficulty of estimation problems in classical statistics. This mission formalizes that lower bound.

Setting

Chapter 6 of the book (pp. 93–128) introduces Decision Making with Structured Observations (DMSO), a protocol general enough to subsume the contextual-bandit, structured-bandit and episodic tabular-RL protocols of earlier chapters. Over $T$ rounds, the learner selects a decision $\pi_t$ from a decision space $\Pi$; nature draws a reward-observation pair $(r_t, o_t)$ from a fixed, unknown model $M^\star(\cdot \mid \pi_t)$, where a model $M$ maps each decision to a distribution over a reward space $R$ and an observation space $O$. The learner has access to a model class $\mathcal{M}$ containing $M^\star$ (realizability). For $M \in \mathcal{M}$, write $f^M(\pi) := \mathbb{E}_{M,\pi}[r]$ for the mean reward function and $\pi_M := \arg\max_\pi f^M(\pi)$ for the optimal decision; regret is $\mathrm{Reg} := \sum_{t=1}^T f^{M^\star}(\pi_{M^\star}) - \mathbb{E}_{\pi_t \sim p_t}[f^{M^\star}(\pi_t)]$, exactly as in the bandit chapters, now for the general model class.

Because observations, not just mean rewards, now carry information, the DEC needs a way to measure distance between the full conditional distributions $M(\pi)$ and $\hat M(\pi)$, not just between scalars $f^M(\pi)$ and $f^{\hat M}(\pi)$. The chapter uses the squared Hellinger distance $D_H^2$, one of a family of Csiszár $f$-divergences that also includes total variation ($D_{TV}$) and Kullback-Leibler ($D_{KL}$) divergence. For a reference model $\hat M$ and scale $\gamma > 0$, the general Decision-Estimation Coefficient is the min-max game value

and $\mathrm{dec}_\gamma(\mathcal{M}) := \sup_{\hat M \in \mathrm{co}(\mathcal{M})} \mathrm{dec}_\gamma(\mathcal{M}, \hat M)$. This mission's Lean development (FoundationsRL.GeneralDM) formalizes discrete versions of $D_{TV}$, $D_H^2$, $D_{KL}$ for a finite outcome type, the DMSO regret, and this DEC.

Formalization targets

The goal is Proposition 28 (DEC Lower Bound), p. 105:

Here $\mathrm{dec}^c_\varepsilon$ is the constrained DEC (§6.5.1), a variant of the offset DEC above that hard-constrains the information gain rather than subtracting it — a technical refinement needed to make the lower-bound direction go through — and the "localization condition" $\mathrm{dec}^c_{\varepsilon_T}(\mathcal{M}) \ge 10\varepsilon_T$ is a genuine hypothesis of the proposition, not a footnote. Unlike almost every other target in this series of missions, the statement quantifies over every algorithm rather than naming one: it is a genuine impossibility result. Two supporting divergence facts are included as milestones because the DEC's information-theoretic argument rests on them: Lemma 19 ($D_{TV}^2 \le D_H^2 \le D_{KL}$) and Lemma 20 (a bounded-likelihood-ratio refinement bounding $D_{KL}$ in terms of $D_H^2$). The chapter's own matching upper bound, Proposition 26 (the E2D regret bound for the general DMSO protocol, the direct analogue of Chapter 4's Proposition 13), is included as a milestone to give the reader the matching pair the chapter presents together. Finally, Corollary 1 restates the lower bound in terms of the localized offset DEC (combining Proposition 28 with Proposition 27), included as a milestone showing the lower bound's reach beyond the constrained DEC alone.

Significance

Proposition 28 is what makes the DEC a genuine characterization of the statistical complexity of interactive decision making, rather than merely a sufficient condition for a particular algorithm family to succeed. Combined with the (uncited, technically deeper) matching upper bound for the constrained DEC — Proposition 29, stated but not proved in the book — it shows that for any finite model class, the constrained DEC is necessary and sufficient for low regret up to a $\sqrt{\log|\mathcal{M}|}$ factor in the localization radius: no complexity measure that is substantially different from the DEC can characterize the same problems. This is the general decision-making analogue of how minimax rates pin down statistical estimation, now for interactive protocols with adaptive feedback.

Formalizing the lower bound is new work: no result of this shape exists on the Prove2Me platform (searches for "decision-estimation", "general divergence", "constrained DEC" and "Hellinger" — the last of which surfaces two related-but-distinct affinity/Le Cam bounds from a different mission on bandit lower bounds — return no faithful prior art; see MODERATION_NOTES.md). The formal statement is the boxed proposition; the book gives a self-contained but simplified proof (two named simplifying assumptions, §6.5.3) and cites Foster, Golowich, Qian, Rakhlin & Sekhari (2023) for the unrestricted argument. This mission's Lean items are draft statements (:= by sorry), not proofs; formalizing the proof itself — a two-point adaptive testing argument using the chain rule for KL divergence and a change-of-measure step — is the open contribution this mission proposes.

Difficulty

The obvious first attempt is to try to prove the lower bound by exhibiting one fixed pair of hard models $M, \hat M$, as in classical two-point minimax lower bounds (Le Cam's method, Fano's inequality). This fails here because the decision-making protocol is interactive and adaptive: the algorithm's queries depend on what it has observed, so a model pair chosen obliviously (before seeing the algorithm) cannot in general be made indistinguishable to every algorithm — an adaptive algorithm can be constructed that distinguishes any two fixed models quickly by querying where they differ. The book's proof instead selects the "hard" alternative model $M$ as a function of the algorithm's own strategy (via the constrained DEC's arg max, Eq. (6.36)), so that the pair is hard specifically for the algorithm under consideration, then uses the chain rule for KL divergence plus the change-of-measure identity between the algorithm's induced distributions under $M$ and $\hat M$ to conclude that the algorithm's realized decisions must look similar under both models — hence it cannot get low regret on both simultaneously. Every step of this argument depends on the exact game structure of the constrained DEC, not just its numerical value; a formalization that leaves $\mathrm{dec}^c_\varepsilon$ as an unconstrained real parameter (rather than the actual $\inf$-$\sup$ game with its information-gain constraint) would make the lower bound's conclusion vacuous, since the hypothesis $\mathrm{dec}^c_{\varepsilon_T}(\mathcal{M}) \ge 10\varepsilon_T$ would no longer track any actual property of $\mathcal{M}$.

Formalization scope

The decision space $\Pi$ and the outcome (reward, observation) alphabet $Y$ are both taken as finite types (Fintype); a model $m : \Pi \to Y \to \mathbb{R}$ is a conditional probability vector, and a reward-extraction map $\mathrm{rew} : Y \to \mathbb{R}$ recovers the mean reward $f^m(\pi) = \sum_y m(\pi)(y)\cdot\mathrm{rew}(y)$. hellingerSq, totalVariationDiscrete, klDivDiscrete specialize the book's general dominating-measure divergence formula (Eq. (6.5)) to the counting measure on this finite type; klDivDiscrete returns an ENNReal so its $+\infty$ case (when $P$ is not absolutely continuous w.r.t. $Q$) is represented honestly. The DEC, the constrained DEC and the localized subclass are literal sInf-of-sSup/sSup-of-sSup transcriptions of the book's min-max games — the same convention this series uses for the Chapter-4 DEC — not opaque free real numbers, which rules out the trivializing formalization named above.

Three deviations from this series' usual convention of pinning every constant to the value the book's own proof derives are deliberate and disclosed. First, the numerical constant $c$ in $\varepsilon_T := c/\sqrt{T}$ is explicitly called "not important" by the authors themselves (footnote a, p. 105); it is existentially quantified (∃ c > 0) rather than pinned to a numeral. Second — added at moderation, round 2, 2026-09-19, after the constant was found to be pinned incorrectly — the lower bound's own multiplicative constant is also existentially quantified (∃ c' > 0) rather than pinned to 1/20. The book's printed proof (§6.5.3, pp. 107–110) derives 1/20 (p. 110, not p. 109 as an earlier draft of this mission stated) only under two named simplifying assumptions the theorem's hypotheses do not carry (p. 107, "Simplifications": a class-wide bounded-curvature hypothesis, Eq. (6.34); and a bound on the unaugmented $\sup_{\hat M\in\mathcal M}\mathrm{decc}_\varepsilon(M,\hat M)$ rather than the officially-defined, augmented $\mathrm{decc}_\varepsilon(M) = \sup_{\hat M\in\mathrm{co}(\mathcal M)} \mathrm{decc}_\varepsilon(M\cup\{\hat M\},\hat M)$ this mission's decC implements). Since augmenting either supremum's domain can only raise its value, the printed proof's bound on the narrower, unaugmented quantity does not license a pinned 1/20 against the fully general decC this theorem states; the book itself attributes the proof of the general statement to an external reference (Foster, Golowich, Qian, Rakhlin & Sekhari 2023) not in this document. The existential c' matches the book's own unpinned $\gtrsim$ for Proposition 28 as printed on pp. 105–106. Third, "any algorithm" and $\mathbb{E}[\mathrm{Reg}(T)]$ are formalized, as throughout this series, without a full stochastic-process/history model: regret is a deterministic quantity evaluated at a fixed realized decision-distribution sequence $p : \mathrm{Fin}\,T \to \Pi \to \mathbb{R}$, rather than an expectation over an adaptive, history-dependent algorithm's own randomness. Formalizing the fully adaptive, measure-theoretic version of "any algorithm" — with an explicit filtration and expectation over the induced process law $P_M$ — is future work a solver could add; the current statement is faithful to the book's deterministic-per-realization content but not to its full generality over randomized, history-dependent strategies. The DMSO protocol (Def_FoundationsRL_GeneralDM_Protocol) and the DEC (Def_FoundationsRL_GeneralDM_DEC) are restated locally rather than imported from Chapter 4's mission (FoundationsRL.Structured), since draft items cannot import another chunk's drafts; contributions extending either mission to reuse the other's substrate once both are published are welcome.

Selected references

• Foster, D. J., Kakade, S. M., Qian, J., & Rakhlin, A. (2023). Foundations of Reinforcement Learning and Interactive Decision Making. arXiv:2312.16730.
• Foster, D. J., Kakade, S. M., Qian, J., & Rakhlin, A. (2021). The Statistical Complexity of Interactive Decision Making. arXiv:2112.13487.
• Foster, D. J., Golowich, N., Qian, J., Rakhlin, A., & Sekhari, A. (2023). A Unified Model and Dimension for Interactive Estimation. arXiv:2306.06184.
• Polyanskiy, Y., & Wu, Y. Information Theory: From Coding to Learning. Cambridge University Press (draft edition cited by the book as [68]).

Motivation

Many hard combinatorial optimization problems — finding the maximum cut of a graph, deciding the ground state of an Ising spin system, bounding the correlation of a physical system — can be written as maximizing a bilinear form over sign vectors $x_i \in \{-1, 1\}$. Exhaustive search over $2^n$ sign patterns is intractable, so practitioners relax the problem: replace each sign $x_i$ by a unit vector $X_i$ in a higher-dimensional space and optimize the resulting inner products instead. This relaxation, a semidefinite program, is convex and solvable in polynomial time. The question is how much is lost in the relaxation — whether its optimal value can be far from the true, combinatorial optimum.

Grothendieck's inequality, proved by Alexander Grothendieck in 1953 in the context of Banach space theory (Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79), answers this for a broad class of such relaxations: replacing signs by unit vectors in an arbitrary Hilbert space changes the optimal value by at most an absolute, dimension-free constant factor. The inequality has since become a standard tool across combinatorial optimization, Banach space geometry, and (via the Goemans-Williamson algorithm for maximum cut, Section 3.6 of the source) approximation algorithms; see U. Haagerup, The Grothendieck inequality for bilinear forms on $C^*$-algebras, Adv. Math. 56 (1985) for the tightest known constant, and Alon–Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), for the algorithmic connection this mission's Theorem 3.5.6 sets up.

Setting

Fix positive integers $m, n$. Consider a real $m \times n$ matrix $A = (a_{ij})$. Say $A$ is normalized if for every choice of numbers $x_1, \dots, x_m, y_1, \dots, y_n \in \{-1, 1\}$,

This says $A$, viewed as a bilinear form on $\{-1,1\}^m \times \{-1,1\}^n$, has sup-norm at most $1$. Now let $H$ be any real Hilbert space — a real vector space equipped with an inner product $\langle \cdot, \cdot \rangle$ complete in the induced norm — and consider vectors $u_1, \dots, u_m \in H$ and $v_1, \dots, v_n \in H$, each of unit norm $\|u_i\| = \|v_j\| = 1$. Replacing the scalar product $x_i y_j$ by the inner product $\langle u_i, v_j \rangle$ in the same bilinear form gives $\sum_{i,j} a_{ij} \langle u_i, v_j \rangle$, a real number depending on the choice of $H$ and of the unit vectors. The question is how large this can be, uniformly over every such choice.

Formalization targets

Grothendieck's inequality (Theorem 3.5.1)

for every real Hilbert space $H$ and unit vectors $u_i, v_j \in H$, where $K$ is a constant depending on neither $A$, its dimensions, nor $H$. This mission's goal formalizes the book's own first-pass bound $K \le 288$ (Section 3.5), proved by a Gaussian truncation argument; it does not fix a numeral for $K$, only that some absolute constant works, matching the shape of the true statement rather than a specific numeral that a sharper argument (the book's own Section 3.7 gives $K \le 1.783$) would immediately obsolete. See Formalization scope below for why this is the goal, not the sharper bound.

Significance

The result itself. Grothendieck's inequality is the single fact that makes semidefinite relaxation a provably good algorithmic strategy rather than a heuristic: whatever the true, hard-to-compute combinatorial optimum of a $\{-1,1\}$-valued bilinear optimization is, the tractable Hilbert-space relaxation cannot overshoot it by more than the constant $K$. Milestone Theorem 3.5.6 makes this concrete for positive-semidefinite matrices, showing the semidefinite relaxation SDP$(A)$ of the integer program INT$(A)$ satisfies INT$(A) \le$ SDP$(A) \le 2K \cdot$ INT$(A)$ — the guarantee underlying the Goemans-Williamson 0.878-approximation algorithm for maximum cut (Theorem 3.6.5 of the source, out of scope for this mission; see Formalization scope).

Formalizing it. The inequality and its two chapter milestones are proved but not previously formalized on this platform (checked by concept search for "Grothendieck", "semidefinite", "positive-semidefinite", and "max-cut" — no hits beyond the unrelated Grothendieck-Teichmüller group). What remains after this mission is the sharper $K \le 1.783$ argument of Section 3.7 (the "kernel trick"), a separate, heavier development building on positive-definite kernels, and full proofs of every milestone below (currently open sorry goals).

Difficulty

The statement of Grothendieck's inequality contains no randomness, yet every known elementary proof is probabilistic; this is itself a striking feature of the result. The obvious approach — bound $\sum_{i,j} a_{ij}\langle u_i,v_j\rangle$ directly by exploiting the normalization hypothesis on $A$ — fails because the normalization hypothesis only controls $A$ against sign vectors, and there is no way to project an arbitrary unit vector in a Hilbert space onto $\{-1,1\}$ without losing information. The book's proof instead represents each unit vector $u_i, v_j$ via a scalar Gaussian random variable $\langle g, u_i\rangle$ for a single Gaussian vector $g$, recovering the inner products in expectation (Exercise 3.3.5); but these Gaussian variables are unbounded, so the normalization hypothesis (which bounds $A$ against bounded $\pm 1$ inputs) cannot be applied to them directly. The core technical step is a truncation argument: splitting each Gaussian variable into a bounded part and a small-$L^2$-norm unbounded remainder, applying the hypothesis to the bounded parts, and bounding the remainder terms by treating them as elements of the Hilbert space $L^2$ and invoking the very inequality being proved (Theorem 3.5.1 itself, applied with $H = L^2$) as a self-referential bootstrap — this is why the proof fixes $K$ as the smallest valid constant before starting, rather than building it up from scratch.

Formalization scope

The goal and both milestones work with the real matrix and real inner product space directly; H is required to be a complete real inner product space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), matching the book's "any Hilbert space." No dimension bound on $H$ is imposed — the inequality's content is exactly that $K$ does not grow with $\dim H$.

This mission does not formalize the sharper $K \le 1.783$ bound of Section 3.7, nor Theorem 3.6.5 (the 0.878-approximation guarantee for maximum cut via randomized rounding): the latter's statement quantifies over "the result of a randomized rounding of the solution of the semidefinite program," which would drag a specific algorithm into the audited statement rather than keeping it a self-contained mathematical claim (the statement/proof-separation trap this series' triage rubric flags). Grothendieck's identity (Lemma 3.6.6), the key fact behind that rounding step, is included on its own as a milestone, stated with an explicit, named random sign variable rather than an opaque "rounding procedure."

A trivializing formalization would state the goal with $K$ allowed to depend on $A$, $m$, $n$, or $H$ — every such bound is easy (e.g. $K = \sum_{ij} |a_{ij}|$) and carries none of the theorem's content; the Lean statement rules this out by quantifying $K$ before every other object. $\mathrm{INT}(A)$ and $\mathrm{SDP}(A)$ (Theorem 3.5.6) are defined from scratch in this chunk's namespace, using Matrix.PosSemidef from Mathlib for the positive-semidefiniteness hypothesis (which bundles the real-symmetric condition); Mathlib has no ready-made SDP-value construction to reuse. The sub-gaussian (Orlicz $\psi_2$) norm used by Theorem 3.1.1 is reused, unchanged, from the 01-concentration mission in this series (HighDimProb.Concentration.SubgaussianNorm) rather than redefined.

Selected references

• A. Grothendieck, Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79.
• U. Haagerup, The Grothendieck inequality for bilinear forms on $C^*$-algebras, Adv. Math. 56 (1985), 93–116.
• N. Alon, A. Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), 787–803.
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42 (1995), 1115–1145.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 3, DOI 10.1017/9781108231596.

Motivation

Any dataset of $N$ points can be described exactly by embedding it in $\mathbb R^n$ for $n$ large enough — but a large $n$ is expensive: nearest-neighbor search, clustering, and streaming algorithms all scale with the ambient dimension, not with $N$. The question that opens this mission is whether the dimension can be cut down while leaving the data's geometry — the pairwise distances between points — essentially untouched.

Johnson and Lindenstrauss answered this in 1984, while studying extensions of Lipschitz maps into Hilbert space (W. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemp. Math. 26 (1984), 189–206): $N$ points in any Euclidean space, of any dimension $n$, can be mapped by a single linear map into a space of dimension only $O(\varepsilon^{-2}\log N)$, distorting every pairwise distance by at most a factor of $1\pm\varepsilon$. The map does not depend on the data beyond its cardinality — a single random object works simultaneously for the whole point set with high probability. This is now one of the standard tools of randomized dimension reduction, cited across nearest-neighbor search, streaming linear algebra, compressed sensing, and machine learning pipelines that need to shrink feature dimension before a downstream algorithm runs.

Setting

Fix a probability space $(\Omega,\mathcal F,\mathrm{Prob})$. A random orthogonal projection of rank $m$ in $\mathbb R^n$ is a map $P:\Omega\to(\mathbb R^n\to\mathbb R^n)$, continuous and linear for each $\omega$, such that almost surely $P_\omega$ is idempotent ($P_\omega\circ P_\omega = P_\omega$), self-adjoint, and has range of dimension $m$ — i.e. $P_\omega$ is the orthogonal projection onto some $m$-dimensional subspace $E_\omega\subset\mathbb R^n$. It is uniformly distributed in the Grassmannian $G_{n,m}$ (written $E\sim\mathrm{Unif}(G_{n,m})$) when its law is rotation invariant: for every orthogonal transformation $U$ of $\mathbb R^n$, the conjugated map $\omega\mapsto U\circ P_\omega\circ U^{-1}$ has the same law as $P$. Conjugating a projection by $U$ is exactly the projection onto the image of its range under $U$, so this says the law of the random subspace $E=\mathrm{range}(P)$ is invariant under the full orthogonal group — the operational definition Vershynin himself uses for a "uniformly distributed" random subspace, since no coordinate-free formula for such a subspace's law is given directly.

A companion notion drives the proof: a random vector $X$ is uniform on the Euclidean sphere of radius $r$, $X\sim\mathrm{Unif}(r\,S^{n-1})$, when it lies on that sphere almost surely and its law is likewise rotation invariant. And a real random variable $Y$ is sub-gaussian with sub-gaussian ($\psi_2$) norm $\|Y\|_{\psi_2} := \inf\{t>0:\mathbb E\exp(Y^2/t^2)\le 2\}$, the standard non-asymptotic measure of how light-tailed $Y$'s distribution is (a bounded or Gaussian random variable has finite $\psi_2$ norm; the tail probability $\mathbb P\{|Y|\ge s\}$ then decays at least as fast as $2\exp(-cs^2/\|Y\|_{\psi_2}^2)$).

Formalization targets

Goal (Theorem 5.3.1, Johnson-Lindenstrauss Lemma)

for every finite $X\subset\mathbb R^n$, every $\varepsilon>0$, and every random orthogonal projection $P$ of rank $m$ uniformly distributed in $G_{n,m}$. The universal quantifier over pairs $x,y\in X$ sits inside the single probability event — this is the union-bound content that makes the statement a genuine simultaneous guarantee for the whole point set, not a restatement of the single-vector lemma below for one fixed pair. Both constants are the book's own unnamed absolute constants, never depending on $n$, $m$, $N=|X|$, or $\varepsilon$; this is the weakest stable form of the claim (no numeral is hard-coded for $C$ or $c$), matching the book's own statement exactly.

Significance

The lemma gives a universal, data-oblivious dimension-reduction guarantee: the target dimension $m=O(\varepsilon^{-2}\log N)$ depends only on the number of points and the desired distortion, never on the ambient dimension $n$ or on the geometry of the specific point set. This is what makes it usable as a black-box preprocessing step ahead of an algorithm whose cost scales with $n$ — the projection is drawn once, without looking at the data, and works with high probability for every pairwise distance simultaneously. The bound is also known to be essentially optimal in $N$: Alon (Problems and results in extremal combinatorics, Discrete Math. 273 (2003)) showed a lower bound of $\Omega(\varepsilon^{-2}\log N/\log(1/\varepsilon))$ on the target dimension, so the $\log N$ dependence cannot be removed.

The theorem itself has been proved for decades and admits several proof strategies (this book's route through Lipschitz concentration on the sphere; the original volume/measure-concentration argument; later "sparse" or structured variants of the projection for faster computation). This mission formalizes the classical dense-Gaussian-projection proof route as Vershynin presents it, building the sphere-concentration engine (Theorem 5.1.4) and the single-vector projection lemma (Lemma 5.3.2) that the union-bound argument for the goal rests on. No machine-checked formal proof of this chain is known to exist on the platform prior to this mission (see Formalization scope below); what is contributed is the statement infrastructure — the goal and its two direct supporting lemmas, stated with explicit, unpinned absolute constants — for solvers to close.

Difficulty

The natural first idea — bound the distortion of a single fixed vector under a random projection, then take a union bound over the $\binom N2$ pairwise differences — is exactly the strategy Lemma 5.3.2 and the goal use, but it does not by itself explain why the single-vector concentration bound (Lemma 5.3.2(b)) holds with the stated sub-gaussian-type tail. That bound is not elementary: it reduces to a uniform concentration statement for an arbitrary Lipschitz function of a uniformly random point on a high-dimensional sphere (Theorem 5.1.4), since $\|Pz\|_2$, viewed as a function of a rotated copy of $z$, is a $1$-Lipschitz function on the sphere. Proving that every Lipschitz function concentrates — not just linear ones, for which sub-gaussianity was already established in Chapter 3 — needs a genuinely different tool: comparing the sub-level sets of an arbitrary Lipschitz function to spherical caps via an isoperimetric inequality on the sphere. This geometric input is what makes the concentration phenomenon behind Johnson-Lindenstrauss a dimension-free fact rather than a special property of coordinate projections.

Formalization scope

$X$ is a Finset of points in EuclideanSpace ℝ (Fin n), matching "a set of $N$ points"; $N$ is read off as X.card. The random subspace $E\in G_{n,m}$ is represented throughout by the orthogonal projection $P$ onto it (IsUniformProjection), following the book's own statements, which are phrased in terms of $P$ rather than $E$; the scaled map $Q=\sqrt{n/m}\,P$ of the goal is written Real.sqrt (n/m) • P ω applied to x - y, using linearity of $P_\omega$ to realize $Qx-Qy = Q(x-y)$. Both "uniform on the sphere" and "uniform in the Grassmannian" are defined operationally by rotation invariance of the underlying law, since Mathlib has no ready-made normalized surface measure on a general-radius Euclidean sphere or Haar-measure construction on the Grassmannian/orthogonal group to build a canonical uniform object from; rotation invariance uniquely determines the corresponding measure among those supported on the relevant set, so the operational and constructive definitions coincide extensionally. Every "absolute constant" in the book ($C$ in Theorem 5.3.1's sample-complexity hypothesis, $c$ in every failure-probability bound, and the sub-gaussian constant $C$ of Theorem 5.1.4) is existentially quantified ahead of the dimension, sample size, and every other object, and pinned to no numeral — a formalization that hard-coded a specific numeral for any of these would be invalidated by the next sharper constant in the literature and would not match what the book actually proves.

A trivializing formalization is one that states the conclusion for a single fixed pair $x,y$ rather than universally over all pairs inside one event; that would collapse the union-bound content that makes this a dimension-reduction statement for a whole point set (with $N$ points), rather than a restatement of the single-vector Lemma 5.3.2(b). This mission's goal statement is built to rule that out explicitly (see Formalization targets above).

Reusable infrastructure: subgaussianNorm (the Orlicz $\psi_2$ norm, restated per Vershynin Definition 2.5.6) and the rotation-invariance idiom for "uniformly distributed" random geometric objects are of independent interest to any later chapter needing sub-gaussian random vectors or random subspaces/projections (e.g. Chapters 4, 6, 7, 9, 11 of this same book series). Solvers' contributions are welcome on: the isoperimetric inequality on the sphere and its use to prove Theorem 5.1.4 (the mission's hardest open leaf); the coordinate-projection computation underlying Lemma 5.3.2(a); and the concentration-plus-union-bound argument closing the goal from the three supporting lemmas.

Selected references

• W. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemporary Mathematics 26 (1984), 189–206.
• N. Alon, Problems and results in extremal combinatorics, I, Discrete Mathematics 273 (2003), 31–53. https://doi.org/10.1016/S0012-365X(03)00227-9
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 5. https://doi.org/10.1017/9781108231596

How quickly does the empirical mean of independent random variables concentrate around the true mean? This question is the analytic engine of the entire theory of stochastic bandits: every optimistic algorithm (Explore-Then-Commit, UCB and its relatives) is calibrated by a tail bound on the sample mean. This mission formalizes the subgaussian framework of Chapter 5 of Lattimore–Szepesvári's Bandit Algorithms: a random variable $X$ is $\sigma$-subgaussian when $\mathbb{E}[e^{\lambda X}] \le e^{\lambda^2\sigma^2/2}$ for all $\lambda$, and the Cramér–Chernoff method converts this moment-generating-function control into the exponential tail $\mathbb{P}(X \ge \varepsilon) \le e^{-\varepsilon^2/(2\sigma^2)}$. The goal theorem is the Hoeffding-type bound: the sample mean of $n$ independent $\sigma$-subgaussian deviations exceeds the true mean by $\varepsilon$ with probability at most $\exp(-n\varepsilon^2/(2\sigma^2))$, together with its confidence form $\mathbb{P}\big(\hat\mu + \sqrt{2\sigma^2\log(1/\delta)/n} \le \mu\big) \le \delta$ — the exact bound every UCB index is built from. These few lines of analysis are cited by every regret bound in the series.

Robust fitting with uncertain measurements

Regression and classification fit a parameter vector to observed data. When measurements can vary within a prescribed set, a fit judged only at the nominal observations need not control its loss on the possible data. A worst-case loss constraint requires the loss bound to hold for every admissible matrix of measurements. Such a requirement can contain infinitely many inequalities even when the parameter vector has finitely many coordinates. Chapter 12 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization (2009) identifies structural assumptions under which this requirement has an exact finite convex representation.

This mission concerns the representation in Theorem 12.2.5. Its application is to robust fitting problems whose uncertainty support function separates into a feature-dependent factor and the infinity norm of a residual-space vector. The result applies to both symmetric losses, such as norms of regression residuals, and asymmetric losses formed from positive residual parts.

Data, residuals, and loss

Let $n,\ell,m$ be positive integers. The nominal data matrix $Z^n\in\mathbb R^{n\times m}$ has one column per measurement and one row per feature. For a parameter vector $\theta\in\mathbb R^n$, its residual vector is $r=(Z^n)^T\theta\in\mathbb R^m$. A fixed matrix $U\in\mathbb R^{n\times\ell}$ describes the structure of permitted perturbations, and a nonnegative scalar $\rho$ controls their size. The uncertain data matrices are

where $D\subset\mathbb R^{\ell\times m}$ is convex, compact, and contains zero. No independence of its columns is imposed.

The loss function $L:\mathbb R^m\to\mathbb R$ is finite and convex. Assumption L requires one of two forms: $L(r)=\pi(|r|)$ for every $r$, or $L(r)=\pi(r_+)$ for every $r$. Absolute value and positive part act coordinatewise. The function $\pi$ is convex and nondecreasing in every coordinate on the nonnegative orthant. The choice of form is global, rather than chosen separately at each residual.

Assumption A specifies the support of $D$ in every rank-one direction:

Here $\phi$ is finite, nonnegative, convex, and positively homogeneous, and $\psi$ is a norm. The goal uses $\psi(v)=\|v\|_\infty$. These are the standing objects and assumptions of Section 12.2, printed pages 311–319 of the source.

Formalization targets

For any real threshold $\tau$, the goal is the exact equivalence

if and only if there exists a real $\kappa$ satisfying

The goal also states convexity in $(\theta,\kappa)$ of the scalar functions on the left of these constraints. There are $2m$ shifted-loss inequalities and one amplitude inequality.

The numbered supporting targets preserve the source's identities. Equation 12.2.11 gives the Fenchel biconjugate representation of a finite convex loss. Equation 12.2.12 equates the worst-case realized loss with its conjugate expression involving the support of $D$. Equation 12.2.15 replaces that support by its factorization under Assumption A. Equation 12.2.18 equates the resulting worst-case loss with a maximum over the dual unit ball:

The maxima in these identities are required to be attained. The Fenchel representation itself uses the source's supremum notation.

What the representation provides

Theorem 12.2.5 replaces a constraint over a continuum of data matrices with finitely many evaluations of the original loss and the uncertainty gauge. It retains the dependence of uncertainty on the fitted parameter through $\phi(U^T\theta)$. Consequently, the representation describes exactly the robust feasible parameters, including zero uncertainty, rather than merely giving a sufficient condition. Evaluation efficiency remains relative to the supplied loss and gauge, as in the book's tractability discussion.

The mathematical result is established in the textbook. The contribution sought here is a machine-checked formalization of its statement and supporting identities. The general finite-dimensional Fenchel biconjugacy theorem already has a proved platform item and is reused as the first milestone; the other three identities and the capstone are open theorem statements in this draft.

Mathematical difficulty

The central issue is relating uncertainty in a matrix to uncertainty in the residual vector while preserving exactness. A uniform bound on individual matrix entries does not by itself express Assumption A. Conjugate functions also need extended values: replacing an infinite conjugate by a real default would change the optimization problem. Establishing equality of optimal values alone is insufficient for identities written with maxima; their attainment is part of the targets. The zero-amplitude case must agree with the nominal loss throughout.

Formalization scope

Vectors use finite-dimensional real Euclidean spaces and matrices have explicitly ordered feature and measurement indices. Coordinates use Fin m, so the first coordinate is indexed by zero. The infinity norm in the goal is taken on the plain coordinate function; it is not the Euclidean norm of the residual vector. The statements include both signs for every coordinate.

The published fenchelConjugate and fenchelBiconjugate definitions are reused. Conjugate objectives take values in EReal. Every claimed maximum is expressed using IsGreatest at a common finite real value, so existence, boundedness, equality, and attainment remain visible. The inner support supremum in Equation 12.2.12 is real-valued and ranges over a nonempty compact image. The dual unit ball in Equation 12.2.18 is represented directly by $\xi^Tv\le\psi(v)$ for all $v$.

All hypotheses about the loss, gauge, norm, and uncertainty set are explicit in each new theorem. None assumes the desired finite reformulation. Assumption L is retained despite the recorded observation that a weaker loss hypothesis suffices for the mathematical equivalence. There are no variant targets. A computational cost model and an optimization algorithm are outside this formalization; the explicit finite formulas and their convexity are the representation being formalized. Reusable work includes finite-dimensional conjugacy, compact support maximization, and dual-norm geometry.

Selected references

• A. Ben-Tal, L. El Ghaoui and A. Nemirovski, Robust Optimization, Princeton University Press, 2009. DOI: 10.1515/9781400831050. Section 12.2, printed pp. 311–319; Equations 12.2.11, 12.2.12, 12.2.15, 12.2.18 and Theorem 12.2.5.

Motivation

Graph neural networks and geometric learning on meshes rely on operators that combine the features of a node with those of its neighbours. The graph Laplacian is the oldest such operator: it is the discrete analogue of the Laplace–Beltrami operator of a surface, and its eigenvectors play the role of a Fourier basis on a graph. Early spectral graph networks (Bruna et al., 2013) learned filters directly in that eigenbasis. Such filters are expensive, since they need an eigendecomposition, and they do not transfer between graphs. Defferrard, Bresson and Vandergheynst (2016) replaced them with polynomial filters $\hat p(\Delta)X=\sum_{k=0}^r\alpha_k\Delta^kX$. These are computed with $r$ sparse matrix products, and their output at a node depends only on a bounded neighbourhood of that node.

This mission formalizes Section 4.6 of the book Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges by Bronstein, Bruna, Cohen and Veličković (arXiv:2104.13478v2). The section introduces the weighted Laplacian (24) and the spectral and polynomial filters built on it, and states that a polynomial filter of degree $r$ is localised in the $r$-hop neighbourhood. The section closes with the view of meshes as operators $Q$, which leads to remeshing invariance and to the result of Wang et al. (2019a) that remeshing-invariant functions depend only on the spectrum. The book numbers no theorems, lemmas or definitions, so every item of this mission is cited by section, equation number and printed page.

Setting

There are $n$ nodes $\{1,\dots,n\}$. A weight matrix $W=(w_{uv})\in\mathbb R^{n\times n}$ assigns a weight to each ordered pair of nodes. The neighbourhood of $u$ is $\mathcal N_u=\{v: w_{uv}\ne0\}$. Node features form a matrix $X\in\mathbb R^{n\times d}$ whose row $x_u$ is the $d$-dimensional feature vector of node $u$.

The degree of $u$ is $d_u=\sum_v w_{uv}$, and the degree matrix is $D=\operatorname{diag}(d_1,\dots,d_n)$. The Laplacian is

The graph is undirected when $W=W^\top$; then $\Delta$ is symmetric and has an orthonormal eigenbasis $\Phi=(\varphi_1,\dots,\varphi_n)$ with $\Delta=\Phi\Lambda\Phi^\top$ and $\Lambda=\operatorname{diag}(\lambda_1,\dots,\lambda_n)$. The Fourier coefficients of $X$ are $\hat X=\Phi^\top X$.

Given a degree $r$ and real coefficients $\alpha_0,\dots,\alpha_r$, the polynomial filter is

Hops are measured in a simple graph $G$ on the nodes that carries the weights: $w_{uv}\ne0$ with $u\ne v$ implies that $u$ and $v$ are adjacent. A node $v$ is within $r$ hops of $u$ if some walk in $G$ from $u$ to $v$ has length at most $r$.

A permutation $\sigma$ of the nodes acts by its permutation matrix $P$, with $(PX)_u=x_{\sigma^{-1}(u)}$ and $W\mapsto PWP^\top$. A function $f$ of $n\times n$ matrices $Q$ is remeshing invariant if $f(CQC^\top)=f(Q)$ for every orthogonal $C\in O(n)$. A matrix-valued $F$ is remeshing equivariant if $CF(Q)=F(CQC^\top)$.

Formalization targets

Goal: locality of polynomial filters (p. 65)

If $X$ and $X'$ agree at every node within $r$ hops of $u$, then

for every choice of $\alpha_0,\dots,\alpha_r$. This is the book's sentence "since the Laplacian is local, a polynomial filter of degree $r$ is localised in $r$-hop neighbourhood". The statement fixes no coefficients and no graph family.