Convex Optimization

Motivation

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

Setting

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

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

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

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

Formalization targets

Goal — Theorem 6.6(a), RSMD complexity

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

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

Supporting milestones, in attack order

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

Setting

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

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

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

Formalization targets

Goal — Theorem 3.6, closed-form rate

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

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

Supporting milestones, in attack order

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

Setting

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

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

Formalization targets

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

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

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

$$\sum_t f_t(x_t) - \min_{h^\star\in CH(H)}\sum_t f_t(h^\star(a_t)) \le \frac{5dGDT}{\gamma\sqrt N} + \frac{2GD}\gamma\mathrm{Regret}_T(W).$$

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–V observes the full cost function $f_t$ after playing $x_t$. Many applications only reveal the scalar cost $f_t(x_t)$ incurred — routing a network and observing total latency, or placing an ad and observing the click-through revenue, without ever seeing the cost of a path or bid not taken. This is the bandit feedback model, and Chapter 6 asks whether sublinear regret survives it. The chapter's answer is a general two-part reduction — turn a first-order full-information algorithm into a bandit algorithm by feeding it an unbiased gradient estimator built from a single scalar observation — instantiated concretely on online gradient descent to produce the first historical bandit convex optimization algorithm, the FKM algorithm (Flaxman–Kalai–McMahan).

Setting

Let $K \subseteq \mathbb R^n$ be the decision set, containing the unit ball centered at $0$, with diameter at most $D$. At each round $t = 1,\dots,T$ the player picks $y_t \in K$, an adversary has fixed a cost function $f_t$ (Lipschitz constant $G$, bounded by $1$ in absolute value on $K$), and the player observes only the scalar $f_t(y_t)$ — never $f_t$ itself or its gradient. Regret is $\sum_{t=1}^T f_t(y_t) - \min_{x\in K}\sum_{t=1}^T f_t(x)$, exactly as in the full-information setting, but now the algorithm's plays are themselves random (they depend on the sampled gradient estimates), so the guarantee is on expected regret.

The chapter's construction has two independent parts. Part 1 (Lemma 6.5) is a black-box reduction: given any first order full-information algorithm $A$ (Definition 6.4 — one that depends on each cost function only through its gradient at the played point) with a full-information regret bound $B_A(\nabla f_1(x_1),\dots,\nabla f_T(x_T))$, feeding $A$ an unbiased estimator $g_t$ of $\nabla f_t(x_t)$ in place of the true gradient preserves the regret bound in expectation, up to $B_A$ evaluated at the estimators instead of the true gradients. Part 2 (Lemma 6.7) supplies such an estimator using only one scalar observation per round: sample $u$ uniformly from the unit sphere, play $y = x + \delta u$ for a small radius $\delta$, and $g = \frac{n}{\delta} f(y)u$ is (for linear $f$) an unbiased estimator of $\nabla f(x)$ — more precisely, an unbiased estimator of the gradient of $f$'s $\delta$-smoothed version $\hat f_\delta(x) = \mathbb E_{v\in B}[f(x+\delta v)]$, by a Stokes'-theorem identity relating a ball integral to a sphere integral.

Formalization targets

Lemma 6.5 (the reduction, milestone)

$$\mathbb E\Big[\sum_{t=1}^T f_t(x_t)\Big] - \sum_{t=1}^T f_t(u) \le \mathbb E[B_A(g_1,\dots,g_T)]$$

for any fixed $u \in K$, any first order algorithm $A$ with full-information bound $B_A$, and any sequence of estimators $g_t$ with $\mathbb E[g_t \mid \text{history through round } t] = \nabla f_t(x_t)$.

Lemma 6.7 (the spherical estimator identity, milestone)

$$\mathbb E_{u\in S}[f(x+\delta u)\,u] = \frac{\delta}{n}\nabla \hat f_\delta(x).$$

Theorem 6.9 — the mission's goal

The FKM algorithm (Algorithm 23: play $y_t = x_t + \delta u_t$, form $g_t = \frac n\delta f_t(y_t)u_t$, update $x_{t+1} = \Pi_{K_\delta}[x_t - \eta g_t]$ on the shrunk set $K_\delta = \{z \mid (1-\delta)^{-1}z \in K\}$) with $\eta = D/(nT^{3/4})$, $\delta = 1/T^{1/4}$ guarantees

$$\sum_{t=1}^T \mathbb E[f_t(y_t)] - \min_{x\in K}\sum_{t=1}^T f_t(x) \le 9nDGT^{3/4} = O(T^{3/4}).$$

Significance

Theorem 6.9's $O(T^{3/4})$ rate is strictly worse than the $O(\sqrt T)$ rate of full-information online gradient descent (Chapter III) — this gap, not a shared rate, is the chapter's real content: bandit feedback provably costs regret, and the FKM algorithm is the historically first algorithm to pin down how much, via the clean two-part reduction that later chapters' improved bandit algorithms (§6.5's self-concordant-barrier method, not formalized here) all refine. Lemma 6.5 is independently reusable: it is a template, quantified over an arbitrary first-order algorithm $A$ and an arbitrary unbiased-estimator family, not tied to the sphere-sampling construction that instantiates it for Theorem 6.9. No prior art was found on the platform for bandit convex optimization, gradient-free methods, or Frank–Wolfe-style estimators; this mission's three items formalize the standard textbook account fresh.

Difficulty

Lemma 6.5's proof is a martingale-style argument: it introduces auxiliary deterministic functions $h_t(x) = f_t(x) + \xi_t^\top x$ (where $\xi_t = g_t - \nabla f_t(x_t)$) whose gradient at $x_t$ is exactly $g_t$, applies $A$'s full-information bound to the $h_t$'s (a genuinely random cost sequence, since $\xi_t$ is random), and then takes expectations, using unbiasedness ($\mathbb E[\xi_t \mid \text{history}] = 0$) to show $\mathbb E[h_t(x_t)] = \mathbb E[f_t(x_t)]$ and $\mathbb E[h_t(u)] = f_t(u)$ for the fixed comparator $u$. This requires a genuine filtration and conditional expectation, not merely an unconditional expectation, since $x_t$ and $g_t$ are themselves random and adapted to different points in the history. Lemma 6.7's proof invokes Stokes' theorem to relate $\nabla \int_{B_\delta} f(x+v)\,dv$ to $\int_{S_\delta} f(x+u)\frac{u}{\|u\|}\,du$, then uses the volume ratio $\mathrm{vol}_n(B_\delta)/\mathrm{vol}_{n-1}(S_\delta) = \delta/n$ — a calculus fact about Euclidean balls and spheres, not itself re-derived in this mission's Lean (the identity is drafted as the statement Lemma 6.7 asserts, to be proved from Mathlib's own ball/sphere volume and divergence-theorem lemmas).

Formalization scope

IsFirstOrderOnlineAlgorithm formalizes only the substitution property of Definition 6.4 (the book's second bullet); the first bullet, a closure condition on the admissible family of loss functions, is a precondition on $A$'s domain rather than a checkable mathematical property and is not formalized — see MODERATION_NOTES.md. SmoothedFunction (Eq. (6.4)) and IsUniformOnUnitSphere are declared once and shared by both milestones and the goal, rather than re-derived inline. Lemma 6.5's history is modeled by an explicit filtration 𝓕 (with x t adapted to 𝓕 t and g t to 𝓕 (t+1)), since Lean's conditional expectation needs a concrete σ-algebra to condition on; the book's informal "history $x_1,f_1,\dots,x_t,f_t$" is exactly this filtration once the (deterministic) $f_\tau$'s are set aside as carrying no randomness. Kδ, the shrunk decision set Algorithm 23 actually projects onto, is kept a separate object from K throughout (a pitfall the chapter brief flags explicitly), and $\min_{x\in K}$ in Theorem 6.9 is rendered as an infimum, checked non-vacuous since $K$ is nonempty and the objective is bounded below on $K$ by the chapter's own $|f_t|\le 1$ assumption.

Not formalized: §6.5's self-concordant-barrier bandit linear optimization algorithm (starred, out of the recommended goal's scope) and Corollary 6.8's ellipsoidal-sampling generalization (a routine corollary of Lemma 6.7 the book itself derives, not independently central).

Selected references

• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 6.
• A. Flaxman, A. Kalai, H.B. McMahan, "Online convex optimization in the bandit setting: gradient descent without a gradient," SODA 2005.

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

$$\mathrm{Regret}_T = \sum_{t=1}^{T} f_t(x_t) - \min_{x^\star \in K} \sum_{t=1}^{T} f_t(x^\star).$$

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:

$$B_R(x \| y) = R(x) - R(y) - \nabla R(y)^\top(x - y).$$

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

$$x_{t+1} = \arg\min_{x \in K}\Big\{\eta \sum_{s=1}^{t} \nabla_s^\top x + R(x)\Big\}, \qquad \nabla_t := \nabla f_t(x_t).$$

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)

$$\mathrm{Regret}_T \;\le\; 2\eta \sum_{t=1}^{T} \|\nabla_t\|_t^{*2} \;+\; \frac{R(u) - R(x_1)}{\eta}, \qquad \text{for every } u \in K.$$

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)

$$\mathrm{Regret}_T \;\le\; \frac{\eta}{4} \sum_{t=1}^{T} \|\nabla_t\|_t^{*2} \;+\; \frac{R(u) - R(x_1)}{2\eta}, \qquad \text{for every } u \in K.$$

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 convex optimization measures a decision maker against the best fixed decision in hindsight, and the standard guarantee — achieved, for instance, by online gradient descent — is regret growing like $O(\sqrt T)$ over $T$ rounds. This rate is unimprovable for general convex losses: an adversary can always force $\Omega(\sqrt T)$ regret against any algorithm. But many losses that arise in practice are not merely convex — they carry extra curvature that a first-order method cannot exploit. The paradigm case is online portfolio selection: a trader repeatedly rebalances wealth across $n$ assets, observes the market's return vector, and is scored by the logarithm of her wealth growth. Thomas Cover's 1991 universal portfolio theory showed that a decision maker with vanishing average regret against this log-wealth objective grows her wealth, asymptotically, at the same rate as the best fixed (constantly rebalanced) portfolio in hindsight — without any statistical assumption on how the market behaves, in sharp contrast to the Geometric Brownian Motion model of mainstream finance (Cover, Universal Portfolios, Mathematical Finance 1991). Cover's own algorithm, and the class of losses his analysis needs, turned out to generalize far beyond portfolio selection: the same curvature condition governs online square-loss regression (Azoury–Warmuth 2001) and other exp-concave learning problems. This chapter isolates that condition — exp-concavity — and shows it buys a logarithmic-in-$T$ regret bound via a second-order algorithm, online Newton step, introduced by Hazan, Agarwal and Kale (Logarithmic Regret Algorithms for Online Convex Optimization, Machine Learning 2007), building on the polynomial-time randomization of Cover's algorithm due to Kalai and Vempala (Efficient Algorithms for Universal Portfolios, Journal of Machine Learning Research 2003) and on the multiplicative-weights algorithm EWOO, which Hazan, Kalai, Kale and Agarwal extended to general exp-concave losses (2006).

Setting

Fix a real inner-product space $E$ (in the goal theorem, $E = \mathbb{R}^n$) and a convex, bounded decision set $K \subseteq E$. As in Chapters I and III, an online convex optimization protocol runs for $T$ rounds: at round $t$ the player picks $x_t \in K$, an adversary reveals a convex cost $f_t : E \to \mathbb{R}$, the player incurs $f_t(x_t)$, and regret is

$$\mathrm{Regret}_T = \sum_{t=1}^T f_t(x_t) - \min_{x^\star \in K} \sum_{t=1}^T f_t(x^\star),$$

exactly Eq. (1.2) of Chapter I (OnlineConvexOpt.FirstOrder.RegretT, reused unchanged here). The costs are assumed $G$-gradient-bounded ($\|\nabla f_t(x)\| \le G$ on $K$) and $K$ has diameter $D$ ($\mathrm{dist}(x,y) \le D$ for $x,y \in K$), the same standing hypotheses as Chapters II–III.

A convex $f : E \to \mathbb{R}$ is $\alpha$-exp-concave over $K$ (Definition 4.1) if $g(x) = e^{-\alpha f(x)}$ is concave on $K$. This is strictly weaker than $\alpha$-strong convexity (Chapter III), yet Lemma 4.2 shows it is exactly a directional strong-convexity condition: a twice-differentiable $f$ is $\alpha$-exp-concave at $x$ iff its Hessian dominates $\alpha \nabla f(x)\nabla f(x)^\top$ — strong curvature only along the gradient direction, not in every direction, which is what lets loss functions like $-\log(r^\top x)$ (rank-one Hessian, far from strongly convex) qualify. Lemma 4.3 turns this into the quadratic lower bound the whole chapter runs on: for $\gamma \le \tfrac12\min\{1/(GD), \alpha\}$ and $x, y \in K$,

$$f(x) \ge f(y) + \nabla f(y)^\top (x - y) + \tfrac{\gamma}{2}\bigl(\nabla f(y)^\top (x-y)\bigr)^2 .$$

Two algorithms are formalized. The Exponentially Weighted Online Optimizer (Algorithm 11, EWOO) plays the $w_t$-weighted centroid of $K$, $x_t = \bigl(\int_K w_t\bigr)^{-1}\int_K x\, w_t(x)\,dx$ with $w_t(x) = e^{-\alpha\sum_{\tau<t} f_\tau(x)}$; it needs no Lipschitz or diameter bound but is only quasi-polynomial-time in general. Online Newton step (Algorithm 12, ONS) instead maintains a running second-moment matrix $A_t = A_{t-1} + \nabla_t\nabla_t^\top$ ($A_0 = \varepsilon I$) and moves by $y_{t+1} = x_t - \gamma^{-1}A_t^{-1}\nabla_t$, projecting back onto $K$ in the norm $\|\cdot\|_{A_t}$ induced by $A_t$ rather than the Euclidean norm. The formalization represents $A_t$ not as a matrix but as an operator $E \to_L E$, with $A_t = A_{t-1} + \nabla_t\nabla_t^\top$ rendered as Mathlib's rank-one operator InnerProductSpace.rankOne ℝ ∇_t ∇_t, $A_t^{-1}$ as ContinuousLinearMap.inverse, and the generalized projection as minimizing $\langle y - x, A_t(y-x)\rangle$ over $K$ (quadForm/IsGeneralizedProjection in Def_..._OnlineNewtonStep).

Formalization targets

Goal — Theorem 4.5

$$\mathrm{Regret}_T(\mathrm{ONS}) \le 2\Bigl(\tfrac1\alpha + GD\Bigr)\, n \log T , \qquad \gamma = \tfrac12\min\{\tfrac{1}{GD}, \alpha\},\ \ \varepsilon = \tfrac{1}{\gamma^2 D^2}, \ \ T \ge 4 .$$

This is the chapter's capstone: logarithmic regret in $T$, at the price of a factor of the ambient dimension $n$ — a genuine trade-off against the dimension-free $O(\sqrt T)$ of Chapter III, stated as such rather than hidden inside an $O(\cdot)$.

Comparator — Theorem 4.4

$$\mathrm{Regret}_T(\mathrm{EWOO}) \le \tfrac{n}{\alpha}\log T + \tfrac{2}{\alpha}.$$

Also logarithmic and, unlike Theorem 4.5, independent of $G$ and $D$ — the price is EWOO's running time, not its regret, so this is not a weaker version of the same target but an incomparable algorithm formalized for contrast.

Significance

Exp-concavity is the precise dividing line between $\Theta(\sqrt T)$-regret losses and losses that admit $O(\log T)$ regret via a tractable algorithm — narrower than convexity, broader than strong convexity, and satisfied by the log-loss of universal portfolio selection, the square loss of online regression, and (Chapter IX onward) losses arising from PAC learning reductions. The dimension dependence in Theorem 4.5 is not an artifact of a loose proof: it is inherent to the second-moment-matrix approach and is the reason later work (self-concordant barriers, sketching) is needed to remove it in special cases. Both regret bounds have long been proved on paper; formalizing them contributes machine-checked statements of the exp-concavity characterization, the quadratic lower bound it yields, and both algorithms' regret guarantees — none of which currently exist on the platform in any form (a search for "exp-concave", "online Newton step", "second-order online" and "universal portfolio" returned no hits).

Difficulty

The natural first idea for bounding $\mathrm{Regret}_T(\mathrm{ONS})$ is to bound each round's progress the way online gradient descent's analysis does: a generalized-Pythagorean argument (Lemma 4.6) reduces the regret to $\bigl(\tfrac1\alpha + GD\bigr)\bigl(\sum_t \nabla_t^\top A_t^{-1}\nabla_t + 1\bigr)$ — this much follows the OGD template with the Euclidean norm replaced by the $A_t$-norm. The obstruction is bounding $\sum_t \nabla_t^\top A_t^{-1}\nabla_t$ itself: term-by-term it need not be summable, since $\nabla_t^\top A_t^{-1}\nabla_t$ does not shrink with $t$ on its own. The book's proof instead recognizes $\nabla_t^\top A_t^{-1}\nabla_t = A_t^{-1}\bullet(A_t - A_{t-1})$ as a discrete log-determinant increment and telescopes it against $\log|A_T|/|A_0|$, using a matrix generalization of the scalar inequality $a^{-1}(a-b) \le \log(a/b)$. This determinant argument (the book's Lemma 4.7) is not itself formalized as a milestone here — see Formalization scope — so a solver of Theorem 4.5 must reconstruct or restate it.

Formalization scope

$K$, $D$, $G$ and $\alpha$ are the chapter's standing hypotheses, stated explicitly on every theorem rather than left as ambient unused variables, exactly as in Chapters II–III; $\gamma$ and $\varepsilon$ are pinned to the theorem's own formulas via explicit hypotheses (hγ, hε) rather than left as free existentials — Rule 7 of the captain brief. The running matrix $A_t$ is formalized as a continuous linear operator on $E$, not as a Matrix (Fin n) (Fin n) ℝ: the rank-one update uses InnerProductSpace.rankOne, and $A_t^{-1}$ uses ContinuousLinearMap.inverse, which is total (it returns the zero map when $A_t$ is not invertible, a convention that never bites here since every $A_t$ is positive definite by construction — $A_0 = \varepsilon I \succ 0$ and each update only adds a positive semidefinite rank-one term, so .inverse always agrees with the genuine inverse). IsOnlineNewtonStep and IsGeneralizedProjection are dimension-free, stated for a general real inner-product space; only the goal theorem and Theorem 4.4 fix $E = \mathbb{R}^n$, since only their bounds mention the dimension $n$ explicitly. RegretT is imported unchanged from OnlineConvexOpt.FirstOrder.Protocol (kind: reference), keeping the regret notation identical across the whole book series. A trivializing formalization is ruled out by requiring $0 < \alpha$, $0 < G$, $0 < D$ and $K$ nonempty throughout: dropping any of these would let $\gamma$, $\varepsilon$, or the bound itself degenerate (e.g. $\gamma \le 0$ would make the projection's norm ill-behaved), producing a statement that is vacuously true rather than the book's actual claim. Lemma 4.7 (the log-determinant inequality) and the exercises are not formalized: the former is a general fact about positive definite operators disconnected from the OCO-specific definitions this mission introduces, and the latter are pedagogical, not numbered results the chapter's own proofs depend on. Reusable beyond this mission: the exp-concavity definitions (IsExpConcaveOn, IsExpConcaveAt) for any later chapter's exp-concave losses (the series plan flags Chapters V and X), and the generalized-projection machinery for any future second-order OCO algorithm.

Selected references

• T. M. Cover, Universal Portfolios, Mathematical Finance 1(1), 1991. https://doi.org/10.1111/j.1467-9965.1991.tb00002.x
• E. Hazan, A. Agarwal, S. Kale, Logarithmic Regret Algorithms for Online Convex Optimization, Machine Learning 69(2–3), 2007. https://doi.org/10.1007/s10994-007-5016-8
• A. Kalai, S. Vempala, Efficient Algorithms for Universal Portfolios, Journal of Machine Learning Research 3, 2003. https://www.jmlr.org/papers/v3/kalai02a.html
• K. Azoury, M. Warmuth, Relative Loss Bounds for On-Line Density Estimation with the Exponential Family of Distributions, Machine Learning 43, 2001. https://doi.org/10.1023/A:1010896012157
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 4. https://arxiv.org/abs/1909.05207

Motivation

A "rule of thumb" classifier — a single pixel's brightness distinguishing handwritten "0" from "1" — is trivial to produce and barely better than a coin flip. A rule that gets every example right is, in general, far harder. Boosting asks whether many weak, easy-to-produce rules can be combined into one strong, hard-to-produce rule, and Chapter 11 answers it via a black-box reduction: any online convex optimization algorithm with sublinear regret, paired with access to a weak learner, yields a boosting algorithm — the same OCO-to-learning-theory template Chapter IX used for generalization, now applied to training-set fitting.

Setting

A concept class $H$ is $\gamma$-weakly-learnable (Definition 11.1) if some algorithm, given enough labeled samples, returns a hypothesis with error at most $\frac12-\gamma$ with high probability — better than random guessing by a fixed margin $\gamma$, far short of the arbitrarily-small error strong (PAC) learning demands. Section 11.2.1 fixes a simplified setting: binary zero-one loss, a realizable concept class (some $h^\star \in H$ has zero error), and a weak-learning oracle $W(p,\delta')$ returning, on distribution $p$ over a fixed sample $S$ of size $m$, a hypothesis with $\Pr[\mathrm{error}_p(W(p,\delta')) \ge \frac12-\gamma] \le \delta'$.

Algorithm 34 runs an OCO algorithm $A_{\mathrm{OCO}}$ over the $m$-dimensional simplex $\Delta_m$ (distributions over the sample): at each round it calls the weak learner on the current distribution $p_t$, builds the $\{0,1\}$-valued cost vector $r_t$ recording which examples $h_t$ got right, updates $p_{t+1} \leftarrow A_{\mathrm{OCO}}(f_1,\dots,f_t)$ for the linear cost $f_t(p) = r_t^\top p$, and finally outputs the majority vote $\bar h(x) = \mathrm{sign}(\sum_{t=1}^T h_t(x))$.

Formalization targets

Theorem 11.2 — the mission's sole target (goal)

For $T$ chosen so $\frac1T\mathrm{Regret}_T(A_{\mathrm{OCO}}) \le \frac\gamma2$, Algorithm 34 returns $\bar h$ with $\Pr[\mathrm{error}_S(\bar h) = 0] \ge 1-\delta$: with high probability, $\bar h$ classifies the entire training sample $S$ perfectly.

Significance

This is one of the cleanest reduction theorems in the book: it needs no property of the weak learner beyond its $\gamma$-margin guarantee, and no property of the OCO algorithm beyond a regret bound — any of Chapters III–X's algorithms (multiplicative weights, OGD, RFTL, ONS...) plugs in directly, and §11.2.3 specializes the reduction with multiplicative weights to recover a close relative of AdaBoost, one of machine learning's most influential algorithms. The proof technique — a contradiction argument on the existence of a "hard" residual distribution $p^\star$ uniform over the misclassified examples — is itself instructive and structurally different from Chapter IX's martingale/concentration argument, despite both chapters being "OCO implies a learning-theoretic guarantee" reductions. No prior art was found on the platform for boosting or AdaBoost (planning search: q=boosting, q=AdaBoost — 0 hits); this mission drafts the theorem fresh.

Difficulty

The proof's key step packages the algorithm's regret guarantee (a worst-case statement, true for every cost sequence including an adversarially-constructed one) into a proof by contradiction: assuming some nonempty set of misclassified examples $S_\phi$ survives, the uniform distribution $p^\star$ over $S_\phi$ is shown to make every $h_t$ perform at best exactly at the $\frac12$ threshold on average (since $\bar h$'s sign disagrees with the true label on every point of $S_\phi$, at most half of the $T$ rounds' hypotheses can have agreed there), while the weak-learner guarantee (via a union bound over all $T$ rounds) forces the actual played distributions $p_t$ to see $\ge\frac12+\gamma$ average performance — and the algorithm's low regret against $p^\star$ specifically then closes the gap into an outright contradiction ($\frac12+\gamma \le \frac12 + \frac\gamma2$, impossible for $\gamma>0$). This chain — union bound over rounds, regret bound against one specific (adversarially-identified) comparator, and an averaging argument over the residual set — is more intricate than its short proof suggests.

Formalization scope

EmpiricalErrorWeighted/EmpiricalError give the (weighted and uniform) training-error quantities exactly as the book states them, with real-valued (±1) labels and predictions — the convention this chapter's sign-based majority vote needs, distinct from Chapter IX's Bool-valued zero-one loss (a deliberate, chunk-local choice, not a conflict, since the two chapters use different label conventions for different reasons — see MODERATION_NOTES.md). IsBoostingRun formalizes Algorithm 34's five lines, with the weak learner's round-t call modeled as a random hypothesis h_t : Ω → X → ℝ (since a weak-learning call is itself probabilistic) rather than a deterministic function, matching the book's own probabilistic per-call guarantee. The goal theorem states the weak-learner guarantee (hweak), the OCO regret guarantee (hA), and the choice of T (hTreg) as explicit hypotheses, per BRIEF.md's own instruction that these are the theorem's real content, not incidental setup. h̄ is typed as an arbitrary X → ℝ, never coerced into H — the book's own explicit remark that the boosted hypothesis need not belong to the original weak-hypothesis class.

This chunk has no milestones: Chapter 11 is short and largely monolithic around Theorem 11.2, with Section 11.2.1 ("Simplification of the setting") and 11.2.2 ("Algorithm and analysis") building directly to it with no other numbered lemma on the relevant pages (PDF 207–211). Definition 11.1 (weak learnability) is drafted as a definition, not manufactured into a milestone, per CAPTAIN_BRIEF.md's own rule that definitions are never milestones and BRIEF.md's explicit allowance for a mission with fewer than 3. §11.2.3's AdaBoost specialization (a corollary discussion, not a separately numbered theorem on these pages) is not formalized.

Selected references

• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 11.
• R.E. Schapire, "The strength of weak learnability," Machine Learning 5(2), 1990, 197-227.
• Y. Freund, R.E. Schapire, "A decision-theoretic generalization of on-line learning and an application to boosting," Journal of Computer and System Sciences 55(1), 1997, 119-139 (AdaBoost).