Convex Optimization

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$:

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$:

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

Chapter XI boosted a weak learner into a strong one for a single offline fit to a fixed sample. Chapter 12 asks the analogous question online: when the pool of experts is too large to run Hedge over directly (the contextual-learning setting, where "experts" are policies mapping contexts to actions and their number is exponential), can black-box access to a cheap approximate — "weak" — online learner be boosted into an algorithm with vanishing regret against the whole hypothesis class, without ever touching it directly? Chapter 12 answers yes, by cascading $N$ weak learners through a Frank–Wolfe-style online construction whose running time is independent of the hypothesis class's size.

Setting

A $\gamma$-weak OCO learner (WOCL, Definition 12.1) for hypothesis class $H$ guarantees, against any linear loss sequence with bounded range, $\sum_t f_t(W(a_t)) \le \gamma\min_{h\in H}\sum_tf_t(h(a_t)) + \mathrm{Regret}_T(W)$ — competitive with only a $\gamma$-fraction of the best fixed hypothesis's performance, plus a sublinear additive term. Because a $\gamma$-multiple guarantee is not shift-invariant, this is stated (Eq. 12.2) after normalizing losses so $f_t(\bar x) = 0$ at the decision set's center of mass.

The weak learner's predictions must be scaled by $1/\gamma$ to be useful, which pushes them outside the decision set $K$ — so Algorithm 36 needs a way to evaluate a proxy loss at points outside $K$ and project back without paying much. Section 12.3's extension operator $X_{K,\kappa,\delta}[f] = S_\delta[f + \kappa\cdot\mathrm{Dist}(\cdot,K)]$ (a smoothed, distance-penalized version of $f$) solves this: Lemma 12.3 shows it agrees with $f$ on $K$ up to $\delta G$, and that projecting onto $K$ costs at most another $\delta G$.

Algorithm 36 cascades $N$ copies of a $\gamma$-WOCL: starting from $x^0_t=0$, each stage $i=1,\dots,N$ takes a $(1-\eta_i,\eta_i)$-weighted step toward the $i$-th weak learner's scaled prediction, and each weak learner is fed the gradient of the extended loss at the previous stage's iterate as its own linear loss — a genuinely projection-free, Frank–Wolfe-style construction (as in Chapter VII), applied here to a cascade of learners rather than a single gradient-descent sequence.

Formalization targets

Lemma 12.3 (extension operator properties, milestone)

$|\hat f(x)-f(x)| \le \delta G$ for $x\in K$; $\hat f(\Pi_K(x)) \le \hat f(x) + \delta G$ for $\kappa=G$.

Lemma 12.5 (smoothed-loss regret comparison, milestone)

For $\hat f_t$ $\beta$-smooth and $\hat G$-Lipschitz, $\sum_t \hat f_t(x^N_t) - \sum_t\hat f_t(x^\star_t) \le \frac{2\beta D^2T}{\gamma^2N} + \frac{\hat GD}\gamma\mathrm{Regret}_T(W)$.

Theorem 12.4 — the mission's goal ("Main")

With $\delta=\sqrt{D^2/(\gamma N)}$, $\eta_i=\min\{2/i,1\}$, Algorithm 36's predictions satisfy

Significance

Theorem 12.4's comparator is the convex hull of $H$, not the best single hypothesis — strictly stronger, and (as the book notes) still a meaningful guarantee even at $\gamma=1$ (a weak learner that already matches $H$'s best hypothesis), since the boosting algorithm's payoff is purely the upgrade from $H$ to $CH(H)$. Combined with §12.1.1's binary-classification instantiation and the $O(\sqrt{T\log N})$-vs-$O(T\cdot\mathrm{poly}(\log N))$-style efficiency argument, this is the chapter's answer to whether contextual-learning-scale expert classes (exponential in context count) can be handled with per-round cost independent of $|H|$ — a genuinely new computational regime relative to Hedge's $O(\log N)$-dependence. No prior art was found on the platform for online boosting or the extension operator (planning search: q=online+boosting, q=extension+operator — 0 hits); this mission drafts all three results fresh, building internally on a Frank–Wolfe-style construction restated locally (Chunk 07 is not yet published).

Difficulty

Lemma 12.3's proof combines the smoothing operator's own approximation guarantee (part 1, "since $\mathrm{Dist}(x,K)=0$ for $x\in K$, this follows immediately from Lemma 2.8") with a Cauchy–Schwarz argument balancing the gradient-norm bound $G$ against the penalty coefficient $\kappa$ exactly at $\kappa=G$ (part 2) — a delicate one-parameter tuning, not a generic estimate. Lemma 12.5's proof (not fully excerpted here, continuing past PDF p. 223 with an inductive argument on $\Delta_i = \sum_t(\hat f_t(x^i_t)-\hat f_t(x^\star_t))$ across the $N$ cascade stages) is structurally the Chapter VII Theorem 7.1/Lemma 7.4 argument applied once per stage, compounding the $\gamma$-WOCL guarantee's slack across all $N$ stages simultaneously — a genuinely two-dimensional induction (over both rounds $t$ and stages $i$) that the offline or single-stage online analyses do not need. Theorem 12.4's own proof (PDF p. 224 onward, not fully excerpted) combines both lemmas with the specific parameter substitutions $\beta=dG/\delta$, $\hat G = G$, and $\delta=\sqrt{D^2/(\gamma N)}$ to reach the stated closed-form bound.

Formalization scope

Extension/SmoothedFunction redeclare Chapter II's smoothing operator (matching BanditConvex.SmoothedFunction, Chunk 06, in content — neither is yet published) rather than importing it, per Addendum 2 rule 5. IsGammaWOCL is drafted at the shifted-form Eq. (12.2) the rest of the chapter actually works with (not Definition 12.1's own unshifted form with the center-of-mass term $\bar x$), matching the book's own explicit simplification. IsOnlineBoostingRun mechanizes Algorithm 36's full five-line cascade (stage-by-stage iterate, weak-learner scaling, final projection, and the per-stage linear-loss construction from the extended loss's gradient) — the fullest mechanization in this mission's items, since Theorem 12.4's own hypotheses (hWOCL, one γ-WOCL guarantee per stage) need the run's internal structure to connect xplay to the weak learners' regret guarantees at all. Lemma 12.5 is drafted at a more abstract level (x^N, x^\star, Regret_T(W) as direct inputs, matching how the book's own proof of that lemma proceeds before Theorem 12.4's own parameter substitution), consistent with the "no more mechanization than the statement needs" principle used throughout this series (e.g. Chunk 10's Lemma 7.4-style scoping). CH(H) is Mathlib's own convexHull ℝ H, applied to H viewed as a subset of the function space — a faithful match to the book's {∑_{h∈H}p_hh \mid p\in\Delta_H} that also correctly handles infinite H, which the book's own sum notation does not literally cover.

Not formalized: §12.1's motivating discussion and its binary-classification/personalized-article examples (illustrative, not numbered theorems); the running-time-independent-of-|H| claim (prose, not part of Theorem 12.4's own mathematical content, per BRIEF.md); Remarks 1-2 following Theorem 12.4 (commentary, no further claim).

Selected references

• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 12.
• A. Beygelzimer, S. Kale, H. Luo, "Optimal and adaptive algorithms for online boosting," ICML 2015.

Motivation

Every algorithm in Chapters I–VIII minimizes regret, an online, adversarial performance measure with no reference to a data-generating distribution. Chapter 9 asks what regret minimization buys in the classical statistical learning setting, where examples are drawn i.i.d. from a fixed distribution and the goal is a hypothesis that generalizes well to unseen data. The chapter's answer is a black-box reduction: run any OCO algorithm on the sequence of losses induced by i.i.d. training examples, average its iterates, and the sublinear-regret guarantee converts directly into a PAC generalization bound — with no algorithm-specific analysis required.

Setting

A hypothesis $h$ predicts labels from examples $x \in X$; its generalization error against a distribution $D$ over labeled pairs $(x,y)$ is $\mathrm{error}(h) = \mathbb E_{(x,y)\sim D}[\ell(h(x),y)]$ for a loss function $\ell$. Section 9.1's Theorem 9.1 (No Free Lunch) shows this goal is hopeless without restricting to a hypothesis class $H$: for any learning algorithm and any sample size $m$, there is a domain, a zero-error concept, and a distribution against which the algorithm's learned hypothesis is wrong at least $1/10$ of the time with probability at least $1/10$. Definitions 9.2–9.3 (PAC and agnostic PAC learnability) and Theorem 9.4 (finite classes are agnostically PAC learnable) set up the target the chapter's reduction achieves for a much broader class of hypothesis sets.

Section 9.2's reduction (Algorithm 29) takes any OCO algorithm $A$ and a convex hypothesis class $H \subseteq \mathbb R^d$: draw $T$ i.i.d. labeled examples, feed $A$ the loss function $f_t(h) = \ell(h(x_t), y_t)$ at each round, and output the running average $\bar h = \frac1T\sum_{t=1}^T h_t$ of $A$'s iterates.

Formalization targets

Theorem 9.1 (No Free Lunch, milestone)

For any domain $X$ with $|X| = 2m > 4$ and any algorithm $A : (\text{sample of size } m) \to (X \to \mathrm{Bool})$, there is a concept $C$ and a distribution $D$ with $\mathrm{error}(C) = 0$ and $\Pr_{S\sim D^m}[\mathrm{error}(A(S)) \ge 1/10] \ge 1/10$.

Theorem 9.5 — the mission's goal

For any $\delta > 0$, with probability at least $1-\delta$,

Significance

Theorem 9.5 is a genuine reduction theorem, in the strongest sense the book uses that phrase in this manuscript: it needs no property of $A$ beyond a regret bound, so every sublinear-regret algorithm in Chapters III–VIII (online gradient descent, RFTL, the bandit and projection-free algorithms) is, via this one theorem, automatically also an agnostic PAC learning algorithm for its hypothesis class — with an explicit, finite-sample generalization bound, not merely an asymptotic guarantee. This is also the book's only chapter connecting OCO to classical statistical learning theory, making Theorem 9.5 the bridge result the rest of the manuscript's machinery feeds into. No prior art was found on the platform for PAC learning, no-free-lunch, or generalization bounds in this sense (planning search: q=PAC, q=no+free+lunch, q=generalization — the one "no free lunch" hit found, PRNGCompression.prng_no_free_lunch, is an unrelated Kolmogorov-complexity result, not a substitute); this mission drafts both results fresh.

Difficulty

Theorem 9.1's proof (the probabilistic method) computes an expectation over a uniformly random concept $C$ and a uniformly random sample $S$ simultaneously, shows this joint expectation of the learned hypothesis's error is at least $1/4$, and only then extracts (i) the existence of a single bad concept via linearity of expectation, and (ii) a probability bound via Markov's inequality on the error as a random variable over samples for that fixed concept — a genuinely two-stage probabilistic argument, not a direct combinatorial construction. Theorem 9.5's proof (not included in the excerpted milestone pages, continuing past PDF p. 180 into §9.2.1's Azuma's inequality machinery) builds a martingale from the sequence of per-round loss deviations and applies a concentration inequality to convert the algorithm's regret bound (a statement about the sum of realized losses) into a high-probability statement about $\bar h$'s expected loss under $D$ — the gap between "regret is small" and "generalization error is small" is exactly what the martingale/concentration argument closes.

Formalization scope

GeneralizationError/GeneralizationErrorZeroOne give the two loss regimes the chapter uses: a general parametrized real-valued hypothesis (matching the linear-hypothesis convention $h_w(x) = w^\top x$ of §9.1.3, generalized via an explicit pred evaluation map since the book's own notation "$h(x)$" for $h \in H \subseteq \mathbb R^d$ implicitly identifies a parameter vector with its induced predictor) and the zero-one loss for Bool-labeled concepts (Theorem 9.1's own setting). IsAgnosticReductionRun formalizes Algorithm 29's construction directly, including its round-0 convention (h_1 ← A(∅), matching the series' standing convention for an empty history) and the i.i.d. sampling assumption made explicit via ProbabilityTheory.iIndepFun and identical marginal law D. Theorem 9.5's own regret hypothesis (hA) states "an OCO algorithm whose regret is guaranteed to be bounded by RegretT(A)" as a genuine property of A — holding for every cost sequence and horizon — matching the book's phrasing exactly, not a one-off fact about the single realized (random) cost sequence this particular run produces. The loss ℓ is assumed bounded in [0,1], the chapter's implicit standing assumption (matching the zero-one loss and bounded hinge-loss examples of §9.1.3) needed for the concentration argument behind the √(8log(2/δ)/T) term; see MODERATION_NOTES.md.

Not formalized: Definitions 9.2–9.3 (PAC/agnostic-PAC learnability) and Theorem 9.4 (finite-class PAC learnability), per BRIEF.md's explicit guidance that Theorem 9.4's proof is not self-contained on these pages but spread across the whole chapter, culminating in Theorem 9.5 itself — treating it as background context rather than a separate formalization target avoids either reconstructing that proof or drafting a numbered result whose "proof" would just be a forward reference to this mission's own goal. Theorem 9.5's optional corollary form (the sample complexity bound T = O((1/ε²)log(1/δ) + T_ε(A))) is likewise not drafted, per BRIEF.md's "otherwise keep the milestone to the displayed inequality." §9.2.1's Azuma's inequality survey (background probability theory, available in Mathlib's Probability/Martingale/) is not itself a formalization target.

Selected references

• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 9.
• 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.

Motivation

Every algorithm through Chapter VI updates its iterate by a Euclidean projection onto the decision set $K$. For many decision sets that arise in practice — bounded-nuclear-norm matrices (matrix completion / recommendation systems), the flow polytope (network routing), the Birkhoff–von Neumann polytope (ranking/permutations), matroid polytopes — a projection requires an expensive operation (an SVD, a quadratic program) while a linear minimization over the same set is comparatively cheap (an eigenvector computation via the power method, a shortest-path or minimum-weight-matching computation, a greedy matroid algorithm). Chapter 7 develops an OCO algorithm that replaces every projection with a call to a linear-minimization oracle, at the cost of a worse regret rate.

Setting

The conditional gradient (CG) / Frank–Wolfe method (Algorithm 25) minimizes a $\beta$-smooth function $f$ over a convex set $K$ (diameter $D$) without ever projecting: at each round it calls the oracle $v_t = \arg\min_{x\in K}\langle x, \nabla f(x_t)\rangle$ and steps $x_{t+1} = x_t + \eta_t(v_t - x_t)$, staying inside $K$ automatically since it is a convex combination of two points of $K$. Theorem 7.1 gives its convergence rate; §7.3.1's matrix completion example and §7.4's routing/ranking/matroid examples motivate why the oracle call is often much cheaper than a projection.

The online conditional gradient (OCG) algorithm (Algorithm 27) lifts this to the OCO setting. Applying CG naively to each $f_t$ separately fails (the method only sees gradient direction, and a single round's direction is not enough information); instead, the algorithm builds the aggregate regularized function $F_t(x) = \eta\sum_{\tau=1}^{t-1}\langle\nabla_\tau, x\rangle + \|x-x_1\|^2$ from all past gradients, calls the linear oracle on $\nabla F_t(x_t)$, and takes a $(1-\sigma_t)/\sigma_t$-weighted step toward the oracle's answer.

Formalization targets

Theorem 7.1 (offline CG convergence, milestone)

Lemma 7.4 (per-round iterate bound, milestone)

Theorem 7.3 — the mission's goal

Online conditional gradient (Algorithm 27) with $\eta = D/(2GT^{3/4})$, $\sigma_t = \min\{1, 2/\sqrt t\}$ attains

Significance

This is the chapter's central trade: Algorithm 27's $O(T^{3/4})$ regret is worse than Chapter III's full-information $O(\sqrt T)$ rate and Chapter V's RFTL rate, but its per-round cost is a single linear-minimization oracle call, not a projection — exactly the trade that makes it the practical choice for the recommendation-system, routing, and ranking applications the chapter develops in detail. Theorem 7.1's offline rate is independently significant as the field's standard Frank–Wolfe convergence guarantee, reused as the analytical engine (via Eq. (7.2)) for both Lemma 7.4's online bound and, historically, for a large family of projection-free methods outside OCO entirely. No prior art was found on the platform for Frank–Wolfe, conditional gradient, or projection-free methods (q=Frank-Wolfe returned 0 hits during planning); this mission drafts the standard textbook account fresh.

Difficulty

Theorem 7.1's proof is a one-step smoothness-plus-convexity inequality (Eq. (7.2)) combined with an induction lemma (Lemma 7.2, not separately drafted — it is a purely algebraic recursion h_{t+1} ≤ h_t(1-η_t) + η_t²c ⟹ h_t ≤ 4c/t, reused verbatim by Lemma 7.4's own induction and not independently central to the chapter's content). Lemma 7.4's proof is the chapter's most delicate step: it applies Theorem 7.1's offline analysis technique to the online aggregate function $F_t$ — not to any single $f_t$, and not even to a fixed function across rounds, since $F_t$ itself changes every round as more gradients accumulate — then combines it with a second inequality (comparing $F_t(x^\star_t)$ to $F_{t+1}(x^\star_{t+1})$ via strong convexity and Cauchy–Schwarz) and a careful algebraic balancing of the $\eta$, $G$, $\sigma_t$ parameters (Eq. (7.6)) to close the induction. Theorem 7.3's own proof is a second reduction: it relates the algorithm's regret against the true cost sequence $f_t$ to Lemma 7.4's bound on $F_t$, via an intermediate comparison to $x^\star_t$ (playing the role of Chapter V's RFTL iterates applied to a shifted cost sequence $\tilde f_t$).

Formalization scope

IsLinearMinimizer makes the "projection-free" linear-oracle call (Eq. (7.4)) an explicit, first-class object, reused by both Algorithm 25 and Algorithm 27's definitions, rather than silently replaced by a projection anywhere. SmoothOn is redeclared under this chapter's own sub-namespace (not imported from Chapter II, which is not yet a published series definition); see MODERATION_NOTES.md. AggregateFunction/AggregateGradient give $F_t$ and its closed-form gradient explicitly, matching Algorithm 27 line 4's formula exactly (the book computes $\nabla F_t$ directly rather than leaving it abstract, so this mission does too). This chunk indexes rounds from 1 throughout (not the 0-indexed Finset.range shift used elsewhere in the series), since Algorithm 27's own line 4 sums $\tau=1$ to $t-1$ and every theorem in this chapter states a per-round or Finset.Icc 1 T-summed bound directly in the book's own round numbers — a deliberate, chunk-local convention choice, not an inconsistency with earlier chapters' definitions (this chunk does not import them). Lemma 7.4 keeps Theorem 7.3's specific parameters and a $G$-Lipschitz hypothesis as explicit premises, since the book's own proof of the lemma uses them, rather than presenting it as a fully parameter-free general fact.

Not formalized: Lemma 7.2 (a routine algebraic recursion, not independently central, and reused identically inside Lemma 7.4's own proof rather than cited as a numbered result on its own); Algorithm 26 and §7.3.1's matrix-completion specialization, §7.4's routing/ranking/matroid examples, and Corollary-level results (illustrative applications, not further formalizable theorems); §7.1's linear-algebra review (singular values, nuclear norm — background, not a formalization target for this mission).

Selected references

• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 7.
• M. Frank, P. Wolfe, "An algorithm for quadratic programming," Naval Research Logistics Quarterly 3(1-2), 1956, 95-110.
• E. Hazan, S. Kale, "Projection-free online learning," ICML 2012 (the chapter's Algorithm 27).

Motivation

Two-player zero-sum games and linear programming are, on their surface, unrelated pieces of 20th-century mathematics: von Neumann's minimax theorem for games (1928) was proved with tools from topology, and linear programming duality (Dantzig, 1940s) with convexity and geometry. Yet the two are formally equivalent — Dantzig recounts von Neumann conjecturing the equivalence outright, on first hearing a description of linear programming, because he had "just recently completed a book with Oscar Morgenstern on the theory of games" [Albers, Alexanderson, and Reid, More Mathematical People, 1990]. Freund and Schapire (1999) later showed that both concepts reduce, in one uniform way, to online regret minimization: a decades-old topological existence proof and a decades-old LP-duality argument both become corollaries of a single fact about no-regret learning. This mission formalizes the algorithmic content of that reduction — Hazan's Lemma 8.4, which is not merely an existence statement but a concrete, efficient algorithm with an explicit convergence rate.

Setting

A two-player zero-sum game in normal form is a real matrix $A \in \mathbb{R}^{n \times m}$ (Hazan restricts entries to $[-1,1]$ for interpretability as losses/rewards, a convention this mission's theorems drop as inessential — the argument is invariant to scaling and shifting). The row player picks a mixed strategy $x$ in the probability simplex $\Delta_n = \{x \in \mathbb{R}^n : x_i \ge 0, \sum_i x_i = 1\}$; the column player picks $y \in \Delta_m$. The row player's expected loss, and simultaneously the column player's expected reward, is the bilinear form $x^{\mathsf T} A y$.

The row player's guaranteed loss is $\lambda_R = \min_{x \in \Delta_n} \max_{y \in \Delta_m} x^{\mathsf T} A y$: the smallest loss she can secure no matter what the column player does. Symmetrically, the column player's guaranteed reward is $\lambda_C = \max_{y \in \Delta_m} \min_{x \in \Delta_n} x^{\mathsf T} A y$. Always $\lambda_R \ge \lambda_C$ ("weak duality" — an elementary max-min/min-max inequality, Direction 1 of Section 8.3). Von Neumann's minimax theorem (Theorem 8.3) is the nontrivial converse: $\lambda_R = \lambda_C$, a common value $\lambda^\star$ called the value of the game, whose optimal strategies form a Nash equilibrium — already on the platform as AGT.zero_sum_minimax.

Algorithm 28 ("Simple LP", p. 147) computes an approximate equilibrium constructively. The row player runs a multiplicative-weights / Exponentiated Gradient update against the sequence of best-response losses the column player generates in a repeated $T$-round play of the game: starting from the uniform strategy $x_1 = (1/n, \dots, 1/n)$, at each round $t$ the column player best-responds with $y_t \in \arg\max_{y \in \Delta_m} x_t^{\mathsf T} A y$, and the row player updates $x_{t+1}(i) \propto x_t(i)\, e^{-\eta (A y_t)_i}$. The algorithm returns the time-averaged strategy $\bar{x} = \frac{1}{T}\sum_{t=1}^T x_t$.

Formalization targets

Goal — Lemma 8.4

for the vector $\bar{x}$ returned by Algorithm 28 after $T$ rounds with learning rate $\eta = \sqrt{2 \log n / T}$. The book calls $\bar{x}$ a "$\sqrt{2 \log n}/\sqrt{T}$-approximate solution" to the zero-sum game — and, via Section 8.2.1's equivalence, to the linear program the game encodes — in exactly this sense. The goal is stated against $\lambda_R$, the quantity the algorithm's own analysis produces; Theorem 8.3 identifies it with $\lambda_C$ and with the book's $\lambda^\star$, so nothing about the bound is lost by this choice of rendering.

Supporting milestone — Eq. (8.1)

the external-regret bound the row player's multiplicative-weights update achieves against the adaptively-chosen linear loss sequence $f_t(\cdot) = (\cdot)^{\mathsf T} A y_t$ — the single analytical fact the goal's proof needs.

Significance

The result itself. Lemma 8.4 gives a genuinely efficient algorithm: $O(\log n / \varepsilon^2)$ rounds of a trivial multiplicative update to reach an $\varepsilon$-approximate value and equilibrium of an $n \times m$ zero-sum game, and — through the equivalence with LP duality — an approximation algorithm for a broad class of linear programs, predating and prefiguring the multiplicative-weights-based approximation schemes surveyed by Arora, Hazan, and Kale (2012). It is also the constructive engine behind Theorem 8.3: unlike the classical topological proof of the minimax theorem, this one produces the equilibrium, not just its existence.

Formalizing it. The equilibrium-existence half of this story, Theorem 8.3, is already a published, proved-format Prove2Me theorem (AGT.zero_sum_minimax, from the Algorithmic Game Theory series) and is reused here as a reference item rather than redrafted. What that theorem does not capture — and what makes this mission non-trivial rather than a restatement — is the quantitative, algorithmic content: that one specific, simple, Hedge-type update, run for a specific number of rounds, provably gets within a specific, explicit distance of the value, using only the existence of some sublinear-regret online algorithm as a black box.

Difficulty

The tempting shortcut is to formalize only "no-regret learning dynamics converge to an equilibrium" as a qualitative statement, discharging it by citing AGT.zero_sum_minimax (equilibria exist) plus a generic regret bound. That collapses Lemma 8.4 into a restatement of Theorem 8.3 and drops exactly what is new here: the explicit rate $\sqrt{2\log n}/\sqrt{T}$, tied to one concrete update rule (Algorithm 28) rather than an arbitrary sublinear-regret black box. The real content is in chaining three quantitative facts — Eq. (8.1)'s specific regret bound for the multiplicative-weights update, the column player's best-response equality (Eq. (8.2)), and the definitional unfolding of $\lambda_R$ — with none of the slack that a purely qualitative "an algorithm with sublinear regret exists" argument would tolerate.

Formalization scope

Matrices are Matrix (Fin n) (Fin m) ℝ with n, m ≥ 1 (empty strategy sets are excluded throughout, matching this mission's reference item AGT.zero_sum_minimax); mixed strategies use Mathlib's stdSimplex ℝ (Fin n). lambdaR/lambdaC are rendered with iInf/iSup over simplex membership, the same convention Introduction to Online Convex Optimization III fixed for RegretT earlier in this series. Algorithm 28's run is packaged as a Prop-valued structure (IsSimpleLPRun) rather than a computable function, in the style of this series' other algorithm-run definitions (IsHedgeRun, IsOnlineGradientDescent): initial uniform strategy, a best-response condition on the column player at every round, and the multiplicative-weights recursion on the row player, with the learning rate η left free and fixed to √(2 log n / T) only at the point the theorems need the book's specific constant.

The trivializing risk here is stating only that some sublinear-regret algorithm secures the bound (already implied, vacuously, by AGT.zero_sum_minimax plus any regret bound); this mission rules that out by fixing the exact update rule of Algorithm 28 in IsSimpleLPRun and proving the bound for that rule specifically, with the book's exact constant √(2 log n)/√T, not an unspecified O(·).

Chapter 5's Corollary 5.7 (the general RFTL/Exponentiated-Gradient regret bound) belongs to a different mission of this series and is not imported; eg_regret_bound restates, locally and self-containedly, exactly the instance of it this chapter's proof needs. A later mission for Chapter 5, once published, could supersede this local restatement by specializing its general bound — a natural contribution for a solver with that mission's Lean available.

Selected references

• J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen, 1928.
• Y. Freund and R. E. Schapire, "Adaptive Game Playing Using Multiplicative Weights", Games and Economic Behavior, 1999. https://doi.org/10.1006/game.1999.0738
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., 2022. arXiv:1909.05207v3
• N. Nisan, T. Roughgarden, E. Tardos, and V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007. https://doi.org/10.1017/CBO9780511800481
• S. Arora, E. Hazan, and S. Kale, "The Multiplicative Weights Update Method: a Meta-Algorithm and Applications", Theory of Computing, 2012. https://doi.org/10.4086/toc.2012.v008a006

Motivation

Online convex optimization (OCO) models a repeated decision process: at each round a learner picks a point in a convex set, an adversary (or the world) reveals a convex cost function, the learner pays that cost at its own point, and the process repeats. No statistical assumption on the sequence of costs is made. This model, introduced by Zinkevich [Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003], underlies most of modern online learning: portfolio selection, online routing, and — through its special case of stochastic optimization — the training of essentially every large machine-learning model in current use, since stochastic gradient descent (the subject of §3.4 of this chapter) is exactly an application of the regret bounds proved here.

The algorithm this chapter introduces, online gradient descent (OGD), is the field's default answer: take a gradient step against the most recently observed cost, project back onto the feasible set. It predates OCO itself as a heuristic, but Zinkevich's contribution — and this chapter's — is the regret analysis: a guarantee that holds against every sequence of costs, adversarially chosen, with an explicit, small constant. Precursors for less general settings appear in Kivinen and Warmuth [1997]; logarithmic-regret algorithms for OCO, the subject of §3.3 here, are due to Hazan, Agarwal and Kale [2007].

The online convex optimization protocol

Fix a convex set $K$ in a real inner product space, playing the role of the decision (or "action") space, and a sequence of cost functions $f_1, f_2, \dots : K \to \mathbb{R}$, each convex. At round $t$, the learner (not knowing $f_t$) plays a point $x_t \in K$, then observes $f_t$ and pays $f_t(x_t)$. Regret after $T$ rounds compares the learner's cumulative cost to that of the single best fixed decision made with hindsight of the whole sequence:

A learner with regret $o(T)$ is, on average, eventually as good as the best fixed point in $K$, even though it never knew the cost sequence in advance.

Two chapter-wide parameters bound how hard an instance can be: $D$, the diameter of $K$ ($\operatorname{dist}(x,y) \le D$ for all $x, y \in K$), and $G$, a common bound on the gradient norm of every $f_t$ over $K$ ($\|\nabla f_t(x)\| \le G$ for all $x \in K$), which implies but is strictly stronger than $G$-Lipschitzness on $K$. Online gradient descent (Algorithm 8) plays $x_1 \in K$ arbitrarily, then at every round sets $y_{t+1} = x_t - \eta_t \nabla f_t(x_t)$ and projects, $x_{t+1} = \Pi_K(y_{t+1})$, for a sequence of step sizes $\eta_t$ chosen in advance.

Formalization targets

Goal: Theorem 3.1 (online gradient descent regret)

using step sizes $\eta_t = D / (G\sqrt{t})$. This is the chapter's — and arguably the book's — central result: the simplest algorithm for the fully general OCO protocol already attains $O(\sqrt{T})$ regret, with an explicit small constant, against convex Lipschitz costs with no further structure.

Milestone: Theorem 3.2 (matching lower bound)

Any algorithm for OCO incurs $\Omega(DG\sqrt{T})$ regret in the worst case: no algorithm, however clever, can improve asymptotically on Theorem 3.1's rate. This is the weaker, worst-case-existence half of the theorem (see Formalization scope).

Milestone: Theorem 3.3 (logarithmic regret under strong convexity)

If every $f_t$ is additionally $\alpha$-strongly convex, the same algorithm — with only the step sizes changed to $\eta_t = 1/(\alpha t)$ — achieves

Strong convexity is a strictly stronger hypothesis than convexity, so this target does not subsume the goal; it sits alongside it as the chapter's second, sharper regime.

Significance

Theorem 3.1 is the reference point against which every later algorithm and every later chapter's improvement (Online Newton Step, RFTL, adaptive-regret methods) is measured: any new algorithm for OCO is judged first by whether it matches this $O(\sqrt{T})$ rate, then by what extra structure lets it do better. Theorem 3.2 closes the question for the general convex-Lipschitz class: $O(\sqrt{T})$ is not an artifact of a loose analysis, it is information-theoretically necessary. Theorem 3.3 identifies the one extra hypothesis (strong convexity) that buys an exponential improvement in the horizon dependence, from $\sqrt{T}$ to $\log T$, without any other change to the algorithm — the same phenomenon that in the book's Chapter 2 separated well-conditioned from general convex offline optimization, now transplanted to the online, adversarial setting.

None of these three statements has a machine-checked proof on the platform prior to this mission (see Formalization scope below for what was checked). Formalizing them establishes the regret protocol and the OGD algorithm as reusable definitions for the rest of this thirteen-chapter series, several chapters of which (Online Newton Step, RFTL, bandit convex optimization) build directly on Algorithm 8 or its regret guarantee.

Difficulty

The regret bound's proof (Theorem 3.1) is short but not naive: bounding $\nabla_t^\top(x_t - x^\star)$ by convexity alone gives no telescoping structure, so the argument instead bounds it using the projection step — the Pythagorean inequality $\|\Pi_K(z) - x^\star\| \le \|z - x^\star\|$ for $x^\star \in K$ — applied to the specific point $z = x_t - \eta_t \nabla_t$. This turns the per-round convexity bound into a telescoping sum in $\|x_t - x^\star\|^2$, and only the resulting sum, evaluated with the specific step-size schedule $\eta_t = D/(G\sqrt{t})$, produces the $\sqrt{T}$ rate; a constant or linearly growing step size does not. The same projection argument is reused for Theorem 3.3, where the strong-convexity inequality is engineered to make the $\|x^\star - x_t\|^2$ terms cancel exactly against the projection telescoping, leaving a harmonic sum. Theorem 3.2's difficulty is of a different kind: it is a lower bound over every algorithm, proved by exhibiting a randomized hard instance (the hypercube with $2^n$ sign-vector linear costs) on which no algorithm can do better than random guessing in expectation.

Formalization scope

$K$ is formalized as a subset of an arbitrary real, complete inner product space (not fixed to $\mathbb{R}^n$), since the chapter's argument uses only Hilbert-space structure. Rounds are 0-indexed (Finset.range T) rather than the book's 1-indexed rounds, so a step size stated here at round $t$ is the book's step size at round $t+1$. D and G are carried as shared section hypotheses (the chapter-wide diameter and gradient-norm bounds), not re-derived or re-stated per theorem; G is formalized exactly as the book defines it (p. 20: a bound on $\|\nabla f_t(x)\|$ over $K$, via Mathlib's HasGradientAt), not as the weaker two-point Lipschitz condition it implies — an earlier draft used the weaker Lipschitz hypothesis and was corrected during moderation, since it made the drafted theorems strictly stronger than the book's own (true by an added argument the book does not give, but not faithful to the stated proof). The projection step is formalized relationally (IsMetricProjection, an arbitrary closest point) rather than as a canonical function, since a general convex set need not come with one built into Mathlib.

For Theorem 3.2, this mission formalizes the theorem's main sentence — the worst-case existence claim — quantifying over "any algorithm" as a non-anticipating map from the full cost sequence to the play sequence, with the hard cost sequence existentially quantified after the algorithm and the horizon: for every algorithm and every horizon there is a cost sequence forcing $\Omega(DG\sqrt{T})$ regret against it. (An earlier draft quantified the cost sequence first — one fixed sequence defeating every algorithm — which is false: a constant algorithm playing a minimizer of that one sequence has zero regret against it; this was corrected during moderation.) It does not formalize the theorem's parenthetical strengthening, that the same $\Omega(DG\sqrt{T})$ bound holds even when costs are drawn from a fixed stationary distribution; that claim is about expected regret of a deterministic algorithm against a random cost sequence, and would need a probability-space formalization of the OCO protocol that this mission's definitions do not build. A formalization limited to the deterministic worst case does not trivialize the theorem: it is exactly the inequality "$O(\sqrt{T})$ cannot be improved," stated without the randomization machinery of its proof.

Theorem 3.4 (the stochastic gradient descent corollary, via a noisy gradient oracle with bounded second moment) is not included: it needs an expectation over a random oracle applied at a random, round-dependent point, which is a substantially heavier probabilistic object than the deterministic protocol built here, and is left for a future mission or an extension of this one.

Selected references

• Zinkevich, M. Online Convex Programming and Generalized Infinitesimal Gradient Ascent. ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf
• Kivinen, J. and Warmuth, M. K. Exponentiated Gradient Versus Gradient Descent for Linear Predictors. Information and Computation, 1997. https://doi.org/10.1006/inco.1996.2612
• Hazan, E., Agarwal, A. and Kale, S. Logarithmic Regret Algorithms for Online Convex Optimization. Machine Learning 69, 2007. https://doi.org/10.1007/s10994-007-5016-8
• Hazan, E. Introduction to Online Convex Optimization, 2nd ed. arXiv:1909.05207v3, Chapter 3. https://arxiv.org/abs/1909.05207

Motivation

Consider a decision maker who must choose, at each of $T$ rounds, between two actions on the advice of $N$ "experts," none of which is known in advance to be reliable. This is the prediction-from-expert-advice problem, introduced by Littlestone and Warmuth [Littlestone & Warmuth, The Weighted Majority Algorithm, FOCS 1989/Inf. Comput. 1994] and generalized to real-valued losses by Freund and Schapire's Hedge algorithm [Freund & Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, JCSS 1997]. It is one of the two founding problems of online learning (the other being universal portfolio selection, also introduced in this book's first chapter) and the historical origin of the multiplicative-weights update method, later recognized as a single algorithmic idea underlying results across game theory, optimization, and computational complexity [Arora, Hazan & Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 2012]. This mission formalizes the chapter's three central guarantees: a matching deterministic lower bound, the Weighted Majority mistake bound, and Hedge's loss bound — the earliest instance, in the book's own development, of the "online convex optimization" phenomenon that its later chapters generalize to arbitrary convex losses.

Setting

At each round $t = 1, \dots, T$, a decision maker chooses one of two actions, $A$ or $B$. After the choice, the true outcome for that round is revealed, and any action that disagrees with it is charged a mistake. $N$ experts also each commit to a prediction every round, and the decision maker may consult their record.

The Weighted Majority (WM) algorithm maintains a weight $W_t(i)$ for each expert $i$, initialized to $W_1(i) = 1$. It predicts whichever action currently carries at least half the total weight, and after seeing the outcome, multiplies the weight of every expert who erred by $(1-\varepsilon)$ for a fixed parameter $\varepsilon \in (0, 1/2)$, leaving correct experts' weights unchanged. $M_T$ denotes the algorithm's own mistake count through round $T$, and $M_T(i)$ expert $i$'s.

The Randomized Weighted Majority (RWM) algorithm uses the same weights, but instead of following the majority it samples an expert with probability proportional to its weight, $p_t(i) = W_t(i) / \sum_j W_t(j)$, and follows that expert's prediction; $\mathbb E[M_T]$ is its expected mistake count.

Hedge generalizes further, from binary mistakes to arbitrary non-negative real-valued losses $\ell_t(i) \ge 0$ suffered by expert $i$ at round $t$. It samples expert $i_t$ with probability $x_t(i) = W_t(i)/\sum_j W_t(j)$ from weights updated multiplicatively in the loss, $W_{t+1}(i) = W_t(i) \, e^{-\varepsilon \ell_t(i)}$. Writing losses and the mixed strategy as vectors, the algorithm's expected loss at round $t$ is $x_t^\top \ell_t$.

Formalization targets

Goal — Theorem 1.5 (Hedge's loss bound)

where $\ell_t^2(i) := \ell_t(i)^2$. This is the chapter's most general result and the one the book reuses later on; it leaves $\varepsilon$ free (no asymptotic tuning), so it survives whatever later chapters do with $\varepsilon$.

Milestones

• Theorem 1.1 (deterministic lower bound). With $L \le T/2$ the best expert's mistake count, no deterministic algorithm can guarantee fewer than $2L$ mistakes on every instance.
• Lemma 1.3 (Weighted Majority): $M_T \le 2(1+\varepsilon) M_T(i) + 2\log N/\varepsilon$ for every expert $i$.
• Lemma 1.4 (Randomized Weighted Majority): $\mathbb E[M_T] \le (1+\varepsilon) M_T(i) + \log N /\varepsilon$ for every expert $i$.

Significance

Theorem 1.1 shows the mistake-bound question has no trivial answer: even against only two maximally simple experts, any deterministic strategy is beaten by a factor of $2$ by an adversary who knows its code. Lemmas 1.3 and 1.4 show this factor is essentially removable — first by relaxing "guarantee" to "guarantee in expectation" (RWM halves the deterministic penalty from $2(1+\varepsilon)$ to $(1+\varepsilon)$), then Theorem 1.5 removes the binary-mistake restriction altogether, replacing it with an explicit second-moment correction term $\varepsilon \sum_t x_t^\top \ell_t^2$ that vanishes as losses shrink. Together they trace the chapter's own narrative arc from "no algorithm beats $2L$" to "an explicit, parameter-free family of algorithms gets within $(1+\varepsilon)$ of the best expert for any $\varepsilon$." All four results are proved by the book via the same device — a potential function $\Phi_t = \sum_i W_t(i)$ — one of the first instances of the potential-function method that recurs throughout the rest of the book (e.g. Online Gradient Descent's regret proof) and throughout online learning generally. None of these four statements, in this exact form, has a formalized proof on Prove2Me or (to the extent searchable) elsewhere: the platform's closest existing result, BanditAlgorithm.ftrl_simplex_exp_weights_regret (see Formalization scope below), proves an asymptotically similar bound by an entirely different route and under a different loss model.

Difficulty

The natural first attempt at any of these bounds is to track $M_T$ (or $\mathbb E[M_T]$, or $\sum_t x_t^\top \ell_t$) directly and induct on $T$; this fails because the quantity itself has no useful recursive structure — knowing the algorithm's mistake count through round $t$ says nothing about round $t+1$'s outcome, which the adversary chooses to inflict maximum damage. The proofs instead introduce an auxiliary potential $\Phi_t = \sum_i W_t(i)$ that is not the quantity being bounded, track it in two directions — an upper bound in terms of the algorithm's own performance (using $1+x \le e^x$, or, for Hedge, $e^{-x} \le 1-x+x^2$ for $x \ge 0$) and a lower bound via the single best expert's weight, $W_T(i^\star) \le \Phi_T$ — and only convert back to the mistake/loss bound at the very end via one logarithm. Getting the direction of every inequality right (each of the four proofs chains four or five inequalities, each valid only in the stated parameter range) is the entire difficulty; there is no shortcut that avoids introducing $\Phi_t$.

Formalization scope

Each algorithm is represented as a Prop-valued run predicate parametrizing over the weight sequence, the input (expert predictions/losses and true outcomes), and the algorithm's own output (predictions or mixed strategy), rather than as an executable program: IsHedgeRun fixes W 0 i = 1, the update W (t+1) i = W t i * exp(-ε * ℓ t i), and x t i = W t i / ∑ j, W t j; IsWeightedMajorityRun additionally fixes the majority-vote prediction rule explicitly (per the triage rubric, the algorithm is part of the audited statement here, not a black box the proof is free to instantiate). Randomization in RWM and Hedge is captured exactly as the book itself does — as a deterministic expectation, i.e. the inner product of the probability vector with the {0,1}-mistake or loss vector — rather than as a measure-theoretic random variable; the book's own Section 1.3.3 makes this identification explicit ("denote in vector notation the expected loss of the algorithm by $\mathbb E[\ell_t(i_t)] = x_t^\top \ell_t$"), so no probability space is introduced. Theorem 1.1's "deterministic algorithm" is a causal map from an outcome history to a prediction (prediction at round $t$ depends only on outcomes before $t$), instantiated at the book's own two-expert construction (one expert always predicts $A$, the other always $B$) rather than a fully general $N$-expert adversary argument — a strictly weaker instance of the general claim, but the exact one the book's proof establishes, so no scope is lost relative to what is proved. $\varepsilon$ is kept as an explicit free parameter throughout, per the book's own presentation (no substitution of the corollary's optimized $\varepsilon^\star = \sqrt{\log N / M_T(i^\star)}$ into the milestone statements).

A trivializing formalization to rule out: fixing $N = 1$ (a single expert) would make Lemmas 1.3–1.5 hold vacuously with $M_T = M_T(i)$ regardless of the potential-function argument; every formal statement here quantifies over an unconstrained $N : \mathbb N$ with $N > 0$, not a hard-coded small case.

The mission needs no Mathlib infrastructure beyond finite sums, Real.log, and Real.exp; the book's own OCO protocol and regret definition (§1.1) are not needed, since this chapter's proofs work directly with mistake/loss counts (per the chunk brief). BanditAlgorithm.ftrl_simplex_exp_weights_regret (Bandit Algorithms XII, Prop. 28.7, arXiv:2003.05963 §28) proves $R_n \le \sqrt{2n\log d}$ for exponential weights on the simplex against $[0,1]$-valued losses, via an FTRL/mirror-descent instantiation — the same asymptotic phenomenon as Theorem 1.5, but a different proof technique, a different (bounded, not merely non-negative) loss assumption, and stated for simplex-comparator regret rather than the per-expert loss comparator here; it is listed as a reference/comparison point, not reused.

Selected references

• N. Littlestone, M. Warmuth, The Weighted Majority Algorithm, FOCS 1989 / Information and Computation 108(2), 1994. https://doi.org/10.1006/inco.1994.1009
• Y. Freund, R. Schapire, A Decision-Theoretic Generalization of On-Line Learning and an Application to Boosting, Journal of Computer and System Sciences 55(1), 1997. https://doi.org/10.1006/jcss.1997.1504
• S. Arora, E. Hazan, S. Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 8(1), 2012. https://doi.org/10.4086/toc.2012.v008a006
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter
  1. https://arxiv.org/abs/1909.05207

The classical convergence theory of smooth convex minimization. For a function that is $m$-strongly convex and $M$-smooth ($mI \preceq \nabla^2 f(x) \preceq MI$), gradient descent converges linearly, while Newton's method exhibits its famous two phases: a damped phase in which every backtracking step decreases the objective by a fixed amount $\gamma$, and a quadratically convergent phase in which the scaled gradient norm squares at each step, $\tfrac{L}{2m^2}\lVert \nabla f(x^{+})\rVert_2 \le \bigl(\tfrac{L}{2m^2}\lVert \nabla f(x)\rVert_2\bigr)^2$. Together they give the iteration count of B&V (9.36),

with $L$ the Lipschitz constant of the Hessian and $\alpha,\beta$ the backtracking parameters. This mission formalizes Chapters 9–10 of Boyd & Vandenberghe with every constant exactly as printed — a quantitative theory entirely absent from Mathlib.

The Karush–Kuhn–Tucker conditions are the central result of convex optimization: for a convex differentiable problem satisfying Slater's condition, a point is optimal exactly when primal feasibility, dual feasibility, complementary slackness and Lagrangian stationarity hold. This mission formalizes Chapters 4–5 of Boyd & Vandenberghe end to end — the first-order optimality criterion, concavity of the Lagrange dual, weak duality, Slater's strong-duality theorem with dual attainment (via the separating-hyperplane argument of §5.3.2), the saddle-point characterization, sensitivity bounds and Pareto scalarization — culminating in the full KKT characterization.

Motivation

Robust control repeatedly meets linear matrix inequalities that must hold for every value of an unknown, norm-bounded matrix. A typical instance is

where $F$ collects model uncertainty or noise. Such a condition quantifies over infinitely many matrices and cannot be checked directly. Petersen's lemma (Petersen and Hollot, Automatica 1986; Petersen, Systems & Control Letters 1987) replaces it by a single inequality in one scalar multiplier $\lambda>0$. The lemma is a standard tool in the design of quadratically stabilizing controllers for uncertain systems, and it was recently used for controller design from noisy data (Bisoffi, De Persis and Tesi, arXiv:2109.12175).

H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman (arXiv:2203.12959v3, 2023; SIAM J. Control Optim.) develop a theory of quadratic matrix inequalities (QMIs) and prove matrix versions of the S-lemma. In §4.5.3 they show that both the strict and the non-strict Petersen lemma follow from their matrix S-lemmas (Theorems 4.10 and 4.7) by a suitable choice of the two quadratic forms. This mission formalizes that derivation.

Timeline. Petersen and Hollot (1986) and Petersen (1987) state the lemma for stabilization of uncertain linear systems. Bisoffi, De Persis and Tesi (arXiv 2021) use strict and non-strict versions for data-driven stabilization. van Waarde, Camlibel, Eising and Trentelman (2023, Proposition 4.16) recover both versions from matrix S-lemmas.

Setting

All matrices are real. For a symmetric matrix $A$, $A \geqslant 0$ ($A>0$) means positive semidefinite (definite), and $A \leqslant B$ means $B-A\geqslant0$; the notation includes symmetry. $A^\dagger$ is the Moore–Penrose pseudo-inverse and $\bar F^{1/2}$ the positive semidefinite square root of $\bar F\geqslant0$.

Quadratic matrix inequalities. A symmetric $\Pi \in \mathbb S^{q+r}$ is partitioned into blocks $\Pi_{11}$ ($q\times q$), $\Pi_{12}$, $\Pi_{21}$, $\Pi_{22}$ ($r\times r$). Its solution sets are

and $\mathcal Z_r^+(\Pi)$ is defined in the same way with $>0$. The generalized Schur complement is $\Pi\,|\,\Pi_{22}=\Pi_{11}-\Pi_{12}\Pi_{22}^\dagger\Pi_{21}$, and the class $\boldsymbol\Pi_{q,r}$ consists of the $\Pi$ with $\Pi_{22}\leqslant0$, $\Pi\,|\,\Pi_{22}\geqslant0$ and $\ker\Pi_{22}\subseteq\ker\Pi_{12}$.

Petersen's data. Fix $C\in\mathbb R^{n\times n}$ symmetric, $E\in\mathbb R^{n\times p}$, $\bar F\in\mathbb R^{q\times q}$ with $\bar F\geqslant0$, and $G\in\mathbb R^{q\times n}$. The uncertainty set is $\mathcal F=\{F\in\mathbb R^{p\times q}: F^\top F\leqslant\bar F\}$. Display (4.17) defines

In this proposition the letters $q,r$ of the QMI section become $n,p$, so $\mathcal Z_p(N)\subseteq\mathbb R^{p\times n}$.

Formalization targets

Goal: Proposition 4.16 (Petersen's lemma)

(a) The robust strict inequality holds if and only if a single multiplier exists:

(b) If $E\neq0$, $\bar F>0$ and $G\neq0$, the same equivalence holds with $\leqslant 0$ in place of $<0$ on both sides.

Milestones

1. Lemma A.1 (p. 26): $A^\top A\leqslant B^\top B$ if and only if $A=SB$ for some contraction $S$ ($S^\top S\leqslant I$); the strict version under full column rank of $B$; and $S=AB^\dagger$ is such a factor.
2. Set identity (p. 17): $\{FG: F\in\mathcal F\}=\{S\bar F^{1/2}G: S^\top S\leqslant I\}=\{H: H^\top H\leqslant G^\top\bar FG\}$.
3. Reformulation (4.17) (p. 17): the strict robust inequality is $\mathcal Z_p(N)\subseteq\mathcal Z_p^+(M)$, the non-strict one is $\mathcal Z_p(N)\subseteq\mathcal Z_p(M)$, and $N\in\boldsymbol\Pi_{n,p}$ with $N_{22}<0$.
4. Theorem 4.10 (strict matrix S-lemma, p. 13): for $N\in\boldsymbol\Pi_{q,r}$ with $N_{22}<0$, $\mathcal Z_r(N)\subseteq\mathcal Z_r^+(M)$ iff $M-\alpha N>0$ for some $\alpha\geqslant0$.
5. Theorem 4.7 (matrix S-lemma, p. 12): for $N\in\boldsymbol\Pi_{q,r}$ with a positive eigenvalue, $\mathcal Z_r(N)\subseteq\mathcal Z_r(M)$ iff $M-\alpha N\geqslant0$ for some $\alpha\geqslant0$.
6. Schur-complement step (p. 17): for $\alpha>0$, $M-\alpha N>0$ iff $-C-\alpha G^\top\bar FG-\alpha^{-1}EE^\top>0$, together with the non-strict analogue.
7. Slater condition (p. 17): $\bar F>0$ and $G\neq0$ imply that $N$ has a positive eigenvalue.

Significance

The result itself. Petersen's lemma converts a semi-infinite family of matrix inequalities into one inequality that is jointly an LMI after a Schur complement. In controller synthesis this makes robust quadratic stabilization against norm-bounded uncertainty a convex feasibility problem. The derivation in this paper places the lemma inside a general theory: Petersen's lemma becomes the special case of the matrix S-lemmas for the pair $(M,N)$ of (4.17), and the hypotheses $E\neq0$, $\bar F>0$, $G\neq0$ of the non-strict version become exactly the Slater condition of Theorem 4.7.

Formalizing it. All results here are proved in the paper. None of them, and no matrix S-lemma, has a machine-checked proof on this platform. The mission produces formal statements and proofs of Petersen's lemma in both forms, of the contraction factorization Lemma A.1, and of the strict and non-strict matrix S-lemmas, which are reused by the data-driven stabilization results of the same paper (Theorems 5.1 and 5.3).

Difficulty

The "if" directions are routine: a multiplier certificate yields the robust inequality by completing a square. The difficulty is the converse, which needs a lossless S-lemma for matrix-valued quadratic forms. The scalar S-lemma rests on the convexity of the joint range of two quadratic forms (Dines' theorem). It does not apply directly to matrix inequalities, and the reduction of Section 4.2 from the matrix case to the vector case is the main obstacle. A second, smaller obstacle is the non-strict case: an equivalence with $\leqslant 0$ is false without a Slater-type condition, and the formal statement has to carry $E\neq0$, $\bar F>0$ and $G\neq0$ exactly where the paper does. Petersen's lemma does not follow from a pointwise choice of $F$. The quantifier over $\mathcal F$ must first become a QMI in $H=FG$, which is what Lemma A.1 provides.

Formalization scope

Matrices are Mathlib Matrix over ℝ. In the goal the sizes are Fin n, Fin p, Fin q. In the S-lemmas the two block index types are arbitrary finite types, and a partitioned matrix is a matrix over the sum type. $X<0$ is (−X).PosDef and $X\leqslant0$ is (−X).PosSemidef; both include symmetry, as the paper's notation does. $F^\top F\leqslant\bar F$ is (F̄ − FᵀF).PosSemidef. The multiplier $\lambda$ is required positive, so $\lambda^{-1}$ is the true inverse. The pseudo-inverse is the unique matrix satisfying the four Penrose conditions, selected by Hilbert's ε, and the square root is Mathlib's CFC.sqrt under the scoped matrix order. "At least one positive eigenvalue" refers to the eigenvalues of the symmetric matrix $N$. "Full column rank" is B.rank = q.

Two choices differ from a literal transcription, and both are disclosed in the items. The strict "Moreover" of Lemma A.1 carries no rank hypothesis, because $A^\top A<B^\top B$ already forces full column rank. The Schur step includes its non-strict analogue, which the paper uses implicitly ("the proof of statement (b) is analogous").

A trivializing formalization is excluded. The quantifier in the goal ranges over every $F\in\mathbb R^{p\times q}$ with $F^\top F\leqslant\bar F$, not over a fixed $F$ or over $H$. Part (b)'s extra hypotheses are not added to part (a), and the sanity instance $n=p=q=1$, $C=-3$, $E=G=\bar F=1$ satisfies every hypothesis and both multiplier conditions at $\lambda=1$.

A complete development needs: Loewner-order calculus and Schur complements for block matrices; Moore–Penrose pseudo-inverse identities; positive semidefinite square roots; the scalar S-lemma (Dines' theorem); and the reduction from matrix to vector QMIs. The S-lemmas and Lemma A.1 are reusable well beyond this mission. Proofs of any milestone, and of the auxiliary results of §4.1–4.2 (Lemmas 4.1–4.5, Theorem 4.6) as supporting theorems, are welcome.

Selected references

• H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman, Quadratic matrix inequalities with applications to data-based control, SIAM J. Control Optim., 2023; preprint arXiv:2203.12959v3. https://arxiv.org/abs/2203.12959v3
• I. R. Petersen, A stabilization algorithm for a class of uncertain linear systems, Systems & Control Letters 8 (1987) 351–357 (reference [35] of the paper).
• I. R. Petersen and C. V. Hollot, A Riccati equation approach to the stabilization of uncertain linear systems, Automatica 22 (1986) 397–411 (reference [36] of the paper).
• A. Bisoffi, C. De Persis and P. Tesi, Data-driven control via Petersen's lemma, preprint, 2021. https://arxiv.org/abs/2109.12175
• H. J. van Waarde, M. K. Camlibel and M. Mesbahi, From noisy data to feedback controllers: nonconservative design via a matrix S-lemma, IEEE Trans. Automat. Control 67 (2022) 162–175 (reference [54] of the paper).

Motivation

Quadratically constrained quadratic programs (QCQPs) minimize a quadratic function subject to quadratic inequality and equality constraints. They model trust-region subproblems, robust least squares, max-cut and many problems in signal processing and control. They are NP-hard in general, so practice relies on convex relaxations, and the standard one is the Shor semidefinite (SDP) relaxation. The SDP relaxation lifts $N$ variables to an $(N+1)\times(N+1)$ positive semidefinite matrix, which is expensive for large $N$.

For an important subclass, the simultaneously diagonalizable QCQPs (SD-QCQPs), a much cheaper relaxation is available: after a change of variables all quadratic forms are diagonal, and the products $x_j^2$ can be relaxed by $N$ new variables $y_j \ge x_j^2$. This is a second-order cone (SOCP) relaxation, studied by Ben-Tal and den Hertog (2014) and Locatelli (2016) for the trust-region problem with additional constraints and related problems. Whether one may use the SOCP relaxation in place of the SDP relaxation without losing anything, for the optimal value and for the convex-hull description, is the question settled here.