Convex Optimization

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).

Motivation

Every regret guarantee through Chapter IX compares the algorithm to the single best fixed decision in hindsight. That comparison is meaningless when the environment itself changes: a commuter's best route differs on weekdays versus weekends, an investor's best portfolio differs in a bull versus a bear market. A standard sublinear-regret algorithm, competing against one static comparator, will converge to some average compromise between regimes — exactly the wrong behavior when the regimes are genuinely different. Chapter 10 develops adaptive regret, a strictly stronger performance metric that demands low regret on every contiguous sub-interval of time simultaneously, and an efficient algorithm (Simple-FLH) that attains it for any base OCO algorithm at only a logarithmic additive cost.

Setting

For a comparator sequence $u_1,\dots,u_T$ with path length $P(u_1,\dots,u_T) = \sum_{t=1}^{T-1}\|u_t-u_{t+1}\|+1$, the dynamic regret $\mathrm{DynamicRegret}_T(A,u) = \sum_t f_t(x_t) - \sum_t f_t(u_t)$ measures performance against a moving target (§10.1). The chapter's central object, adaptive regret (Definition 10.2), instead takes the supremum of ordinary regret over every contiguous sub-interval $[r,s]\subseteq[T]$:

$$\mathrm{AdaptiveRegret}_T(A) = \sup_{[r,s]\subseteq[T]}\Big\{\sum_{t=r}^s f_t(x_t) - \min_{x^\star\in K}\sum_{t=r}^s f_t(x^\star)\Big\}.$$

An algorithm is strongly adaptive if its adaptive regret matches its ordinary regret up to logarithmic factors in $T$ (§10.2.1).

The chapter builds toward this via the Fixed-Share algorithm (§10.3, Algorithm 30) — a variant of Hedge for the discrete expert-tracking problem, adding a uniform exploration term to each round's multiplicative update so that no expert's weight can vanish entirely — and then lifts it (§10.4) to the continuous OCO setting via Simple-FLH (Algorithm 32): run one fresh copy of a base OCO algorithm $A$ per starting time $1,\dots,T$, and apply Fixed-Share to this set of $T$ "experts."

Formalization targets

Theorem 10.1 (dynamic regret, milestone)

Online gradient descent with constant step size $\eta > 0$ satisfies, for every comparator sequence $u \in K$,

$$\mathrm{DynamicRegret}_T(A,u) \le \frac{3D^2}{2\eta}P(u_1,\dots,u_T) + \frac\eta2 G^2T.$$

Theorem 10.3 (Fixed-Share tracking regret, milestone)

Given $\alpha$-exp-concave losses, Fixed-Share with $\delta=1/(2T)$ guarantees, for every interval $[r,s]$ and every expert $i$,

$$\sum_{t=r}^s f_t(x_t) - \sum_{t=r}^s f_t(x^i_t) \le \frac1\alpha\log(2NT) + \frac1\alpha.$$

Theorem 10.6 — the mission's goal

Simple-FLH guarantees

$$\mathrm{AdaptiveRegret}_T(\text{Simple-FLH}) \le \mathrm{Regret}_T(A) + \frac1\alpha\log(2T^2) + \frac1\alpha.$$

Significance

Theorem 10.6 answers §10.2.1's own question — are there algorithms simultaneously optimal in ordinary regret and adaptive regret? — affirmatively and constructively: Simple-FLH pays only an additive $O(\frac1\alpha\log T)$ over whatever regret its base algorithm $A$ already achieves, for any $\alpha$-exp-concave-loss algorithm $A$ (in particular, taking $A$ to be the Online Newton Step algorithm of Chapter IV gives an adaptive-regret algorithm with no asymptotic cost at all). This is the chapter's capstone reduction, structurally similar to Chapter IX's OCO-to-PAC reduction: a generic wrapper around any algorithm in a broad class, converting one guarantee into a strictly stronger one. No prior art was found on the platform for adaptive regret, dynamic regret, or Fixed-Share (planning search: q=adaptive+regret, q=dynamic+regret, q=tracking+regret — no hits); this mission drafts all three results fresh.

Difficulty

Theorem 10.1's proof adapts Theorem 3.1's telescoping-sum argument to a moving comparator, picking up an extra term $\sum_t x_t^\top(u_{t-1}-u_t)$ that Cauchy–Schwarz and the diameter bound convert into the path length $P(u)$ — a genuinely different quantity from $\sqrt T$ regret, not a trivial corollary. Theorem 10.3's proof (Lemma 10.4, an exp-concavity-driven potential argument structurally parallel to Hedge's own analysis in Chapter I) tracks how the fixed-share exploration term $\delta/N$ prevents any expert's weight from decaying below a usable floor, so that even an expert active only over a short sub-interval $[r,s]$ still has enough accumulated weight at time $r$ for the argument to close — the sup-over-all-intervals form of the guarantee is exactly what this floor buys. Theorem 10.6's own proof is comparatively short (a direct application of Theorem 10.3 to Simple-FLH's experts, instantiated at the expert matching the interval's own start point), but depends on both of the preceding results' analyses for its correctness.

Formalization scope

AdaptiveRegretT is stated as a genuine supremum over a finite index set (subintervals of [0,T-1]), so it is a maximum, never a real-suprema-of-an-unbounded-set junk value — the chapter brief's own flagged pitfall (do not state it as a sum or average). ExpConcave is redeclared locally (Chapter IV's own exp-concavity is not yet a published series definition; see MODERATION_NOTES.md). IsFixedShareRun gives expert decisions xi as external data (matching the book's own treatment, where "an expert i suggests decision x^i_t" is not itself part of Fixed-Share's specification) — Theorem 10.3 is drafted at this level of generality, applying to Fixed-Share on any experts, matching how the book itself proves it once and reuses it for Simple-FLH. The goal (Theorem 10.6) connects Simple-FLH's experts to the base algorithm A via the one property the book's own proof actually uses — each expert's interval-regret bound inherited from A — rather than mechanizing Algorithm 32's exact re-indexing formula for starting a fresh copy of A at each round, which never enters the numerical bound; see MODERATION_NOTES.md. Three of this chapter's headline results (Theorems 10.1, 10.3, 10.6) are stated in the book with a bare O(·); per CAPTAIN_BRIEF.md rule 7 and BRIEF.md's explicit guidance, this mission uses the explicit constant each proof actually derives instead (Theorem 10.1's own η-parametrized inequality before the unstated optimal choice of η; Theorems 10.3 and 10.6's own final displayed bounds before they are folded into O(·) notation).

Not formalized: Definition 10.2's own generalization to $k$-shifting comparators (a remark, not a numbered theorem), §10.2.1's tightness/lower-bound claims (left as exercises in the book, no proof given), Lemma 10.4 (an intermediate step whose content is folded directly into Theorem 10.3's own explicit bound), and §10.5's starred FLH2 (Theorem 10.7, poly-logarithmic running time) — an advanced, optional stretch goal per BRIEF.md, not attempted given the chapter's non-starred primary goal (Theorem 10.6) was reachable within budget.

Selected references

• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 10.
• M. Herbster, M. Warmuth, "Tracking the best expert," Machine Learning 32(2), 1998, 151-178 (the Fixed-Share algorithm).
• A. Daniely, A. Gonen, S. Shalev-Shwartz, "Strongly adaptive online learning," ICML 2015 (FLH/Simple-FLH).

Motivation

Convex optimization — minimizing a convex function over a convex set — is the offline problem that online convex optimization (OCO) generalizes: an OCO algorithm run against a single, fixed cost function repeated every round is exactly an algorithm for this classical problem. Its convergence theory, developed over decades and surveyed comprehensively in Nesterov [Introductory Lectures on Convex Optimization, 2004] and Boyd and Vandenberghe [Convex Optimization, 2004], supplies the analytical toolkit — potential functions, strong convexity, smoothness — that every regret bound in the rest of this book reuses. This chapter is the book's own self-contained account of that toolkit: it proves nothing about regret or adversaries, but the algorithms and inequalities it establishes for gradient descent recur, essentially unchanged, in the online setting three chapters later.

The chapter's own capstone, a linear convergence rate under a joint strong-convexity and smoothness assumption, traces to Nesterov's classical analysis of gradient descent under a condition-number bound; the Polyak step size predates it, going back to Polyak's 1969 subgradient method for problems with a known optimal value.

Setting

Fix a real, complete inner product space $E$ (a Hilbert space) and a convex, closed set $K \subseteq E$, the decision set. A function $f : E \to \mathbb{R}$ is $\alpha$-strongly convex (with gradient map $g : E \to E$) if for every $x, y \in E$,

$$f(y) \ge f(x) + \langle g(x), y - x\rangle + \frac{\alpha}{2}\|y-x\|^2,$$

and $\beta$-smooth if for every $x, y \in E$,

$$f(y) \le f(x) + \langle g(x), y - x\rangle + \frac{\beta}{2}\|y-x\|^2.$$

Strong convexity lower-bounds $f$ by a quadratic of curvature at least $\alpha$ at every point; smoothness upper-bounds it by a quadratic of curvature at most $\beta$. When $f$ is twice differentiable these say $\alpha I \preceq \nabla^2 f(x) \preceq \beta I$ for every $x$. A function that is both is called $\gamma$-well-conditioned, where $\gamma := \alpha/\beta \le 1$ is its condition number.

Write $x^\star$ for a minimizer of $f$ (over $E$, or over $K$ in the constrained case), and for any point $x$ define three measures of distance to optimality: the value gap $h_x := f(x) - f(x^\star)$, the Euclidean distance $d_x := \|x - x^\star\|$, and the gradient norm $\|\nabla_x\| := \|g(x)\|$. Gradient descent starts at $x_0$ and iterates $x_{t+1} = x_t - \eta_t g(x_t)$ for a step-size schedule $\eta_t$; in the constrained case each step is followed by a projection $x_{t+1} = \Pi_K(y_{t+1})$ back onto $K$.

Formalization targets

Goal: Theorem 2.6 (linear convergence for well-conditioned functions)

$$h_{t+1} \le h_1 \cdot e^{-\gamma t / 4} \qquad \text{for every } t \ge 0,$$

for constrained gradient descent (Algorithm 4) on a $\gamma$-well-conditioned $f$ over $K$, with the constant step size $\eta_t = 1/\beta$. This is the chapter's strongest rate: for the best-conditioned class of functions it considers, the optimality gap shrinks by a constant factor every round, rather than polynomially in $t$.

Milestone: Theorem 2.2 (KKT optimality condition)

$$\langle \nabla f(x^\star), y - x^\star\rangle \ge 0 \quad \text{for every } y \in K,$$

when $x^\star$ minimizes $f$ over a convex $K$. The multi-dimensional first-order optimality condition for constrained minimization, generalizing $\nabla f(x^\star) = 0$ in the unconstrained case ($K = E$).

Milestone: Theorem 2.3 (GD with the Polyak step size)

$$f(\bar{x}) - f(x^\star) \le \min\left\{\frac{Gd_0}{\sqrt{T}},\ \frac{2\beta d_0^2}{T},\ \frac{3G^2}{\alpha T},\ \beta d_0^2\Big(1-\frac{\gamma}{4}\Big)^T\right\},$$

for unconstrained gradient descent with step size $\eta_t = h_t/\|\nabla_t\|^2$, where $\bar x$ achieves the smallest value among $x_0,\dots,x_T$. A single algorithm, needing no prior knowledge of $\alpha$, $\beta$, or $G$ beyond the (assumed available) optimal value $f(x^\star)$, automatically attains whichever of the four rates applies to $f$.

Milestone: Lemma 2.4 (potential-function relations)

For $\alpha$-strongly-convex and $\beta$-smooth $f$, at every point $x$:

$$\frac{\alpha}{2}d_x^2 \le h_x, \qquad h_x \le \frac{\beta}{2}d_x^2, \qquad \frac{1}{2\beta}\|\nabla_x\|^2 \le h_x, \qquad h_x \le \frac{1}{2\alpha}\|\nabla_x\|^2.$$

The chapter's basic toolkit: four inequalities letting a proof substitute one measure of progress (value gap, distance, gradient norm) for another as needed.

Significance

Theorem 2.6 is the model result behind every subsequent linear-rate claim in convex optimization: it isolates the exact mechanism (strong convexity plus smoothness, combined multiplicatively through the condition number) that turns a $1/\sqrt{T}$ or $1/T$ rate into an $e^{-\Omega(t)}$ one. Theorem 2.3 demonstrates the opposite phenomenon — a single step-size rule that adapts to whatever structure $f$ happens to have, without needing to know which structure that is — a design principle the book's later chapters (adaptive regret, adaptive gradient methods) return to repeatedly. Lemma 2.4 is used directly inside the book's own proof of Theorem 2.6 and is stated separately because later chapters cite its four bounds individually.

None of these four statements has a machine-checked proof on the platform prior to this mission (see Formalization scope). Formalizing them establishes strong convexity and smoothness, in the book's own quadratic-bound form, as reusable definitions, together with the constrained- and unconstrained-gradient-descent update rules that Chapter III's online algorithm specializes.

Difficulty

The linear rate of Theorem 2.6 does not follow from Lemma 2.4 alone: chaining the smoothness upper bound and the strong-convexity lower bound gives only a bound relating $h_{t+1}$ to $d_t^2$, not to $h_t$ itself, and a naive one-step decrease argument stalls at a rate of $1 - \gamma$ per round rather than $1 - \gamma/4$ — the factor of four comes from combining the projection's contraction property (the constrained analogue of Theorem 2.3's telescoping argument) with the smoothness bound simultaneously, not from either alone. The Polyak step size of Theorem 2.3 is remarkable, and its analysis correspondingly delicate, because the step size $\eta_t = h_t/\|\nabla_t\|^2$ depends on the unknown optimal value $f(x^\star)$ through $h_t$; the proof must derive all four regimes (general convex, smooth, strongly convex, well-conditioned) of $B_T$ from the same one-line per-round inequality, rather than running four separate arguments.

Formalization scope

$E$ is formalized as an arbitrary real, complete inner product space, not fixed to $\mathbb{R}^d$, matching this book's chapter-wide convention (Chapter III's mission of this series does the same). Strong convexity and smoothness are formalized in the book's own quadratic-bound form with an explicit gradient map $g$ as a separate parameter (not tied to $f$ by automatic differentiation), rather than via the second-derivative characterization; a theorem needing $g$ to be the actual gradient of $f$ adds that as a separate hypothesis. This avoids a trivializing formalization under which the predicate could be satisfied by an unrelated $g$: every theorem here that uses StronglyConvexOn/SmoothOn also assumes g is a global gradient map for f. Theorem 2.3's realized-gradient bound $\|\nabla_t\| \le G$ is formalized only over the run's own iterates $x_0,\dots,x_T$ (not as a global Lipschitz bound on $f$), matching the book's own statement ("assuming $\|\nabla_t\|\le G$"): a global gradient bound would be jointly unsatisfiable with global strong convexity on any infinite-dimensional or unbounded $E$, since a strongly convex function's gradient grows without bound away from its minimizer. Sequences are 0-indexed, so a book statement at round $t{+}1$ (1-indexed) is stated here at index $t$; each theorem's docstring records the exact shift. The projection in Algorithm 4 reuses OnlineConvexOpt.FirstOrder.IsMetricProjection, already published for this series' Chapter III, rather than redeclaring it.

Theorem 2.10 (the chapter's further, book-stated-without-proof rate) is out of scope: the book explicitly defers its proof to outside references, so it cannot be a faithful milestone under this platform's provenance requirement. Section 2.4's reductions of non-smooth or non-strongly-convex problems to this chapter's setting (via randomized smoothing) are left for a future extension, since they introduce a new construction not needed by the goal or its milestones.

Selected references

• Hazan, E. Introduction to Online Convex Optimization, 2nd ed. arXiv:1909.05207v3, Chapter 2. https://arxiv.org/abs/1909.05207
• Nesterov, Y. Introductory Lectures on Convex Optimization: A Basic Course. Springer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• Boyd, S. and Vandenberghe, L. Convex Optimization. Cambridge University Press, 2004. https://web.stanford.edu/~boyd/cvxbook/
• Polyak, B. T. Minimization of Unsmooth Functionals. USSR Computational Mathematics and Mathematical Physics 9(3), 1969. https://doi.org/10.1016/0041-5553(69)90061-5

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:

$$\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 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)

$$\mathrm{Regret}_T \le \frac{3}{2} G D \sqrt{T} \quad \text{for all } T \ge 1,$$

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

$$\mathrm{Regret}_T \le \frac{G^2}{2\alpha}(1 + \log T).$$

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

Two-stage stochastic programs with recourse require evaluating $Q(x) = \mathbb E_\xi[Q(x,\xi)]$, the expected value of a recourse function, at every candidate first-stage decision $x$. When $\xi$ is high-dimensional or continuously distributed, this expectation is a multivariate integral of a piecewise-linear, generally nondifferentiable integrand, and classical quadrature rules — built for smooth integrands in low dimension — do not apply (Birge & Louveaux, §8.1). What does apply is convexity: $Q(x,\cdot)$ is convex whenever the recourse problem is a linear program in $\xi$, and convexity alone is enough to sandwich $\mathbb E_\xi[Q(x,\xi)]$ between two computable discrete approximations. This chapter develops that sandwich, and it is the standard device used throughout the stochastic-programming literature to bound and iteratively refine the recourse function: the lower bound goes back to Jensen [1906]; the upper bound is due to Edmundson [1956] and Madansky [1959], with the mean-consistent LP refinement due to Madansky [1960] and Gassmann & Ziemba [1986]. Refinements of both bounds appear in Huang, Ziemba & Ben-Tal [1977], Kall & Stoyan [1982] and Frauendorfer [1988].

Setting

Fix a probability space $(\Omega, \mathcal F, P)$ and an integrand $g : D \times \Xi \to \mathbb R$, where $\Xi \subseteq E$ is the (convex, closed) support of a random vector $\xi : \Omega \to \Xi$ and $E$ is a real vector space (in the recourse application, $g(x,\cdot) = Q(x,\cdot)$ and $D$ is the first-stage feasible region). Write $\mathbb E(g(x)) = \mathbb E_\xi[g(x,\xi)] = \int_\Xi g(x,\xi)\, P(d\xi)$.

A partition of $\Xi$ into $\nu$ measurable blocks $S^\nu = \{S_1,\dots,S_\nu\}$ determines, for each block, its probability $p_l = P[\xi \in S_l]$ and its conditional mean $\xi^l = \mathbb E[\xi \mid S_l]$. Equivalently — and this is the convention this mission's Lean development uses — the blocks may be taken directly on the sample space as the pulled-back sets $S_l = \xi^{-1}(\text{region}_l) \subseteq \Omega$, with $p_l = P(S_l)$ and $\xi^l = p_l^{-1}\int_{S_l}\xi\,dP$ the Bochner integral average of $\xi$ over the block; the two descriptions coincide.

Formalization targets

Goal — Chapter 8, Theorem 1 (Jensen lower bound), p. 346

$$g(x,\cdot) \text{ convex on } \Xi \ \Longrightarrow\ \mathbb E(g(x)) \ \ge\ \sum_{l=1}^{\nu} p_l\, g(x,\xi^l).$$

This is the sharpest statement the chapter proves for the lower bound: it holds for every finite measurable partition, with no assumption beyond convexity of $g(x,\cdot)$ and integrability.

Chapter 8, Theorem 2 (Edmundson-Madansky upper bound), pp. 347-348

For $\Xi$ compact, let $\mathrm{ext}\,\Xi$ be the extreme points of $\mathrm{co}\,\Xi$, carrying the Borel field of all its subsets. If, for every $\xi \in \Xi$, $\varphi(\xi,\cdot)$ is a probability measure on $\mathrm{ext}\,\Xi$ with barycenter $\xi$ (i.e. $\int_{\mathrm{ext}\,\Xi} e\,\varphi(\xi,de) = \xi$) and $\omega \mapsto \varphi(\xi(\omega), A)$ is measurable for every $A$, then

$$\mathbb E(g(x)) \ \le\ \int_{\mathrm{ext}\,\Xi} g(x,e)\, \lambda(de), \qquad \lambda(A) = \int_\Omega \varphi(\xi(\omega), A)\, P(d\omega).$$

Together the two targets give the chapter's headline sandwich: for convex $g(x,\cdot)$, the finite-partition Jensen value and the Edmundson-Madansky value bracket the true expectation, and refining the partition (resp. the disintegration) tightens both sides toward it.

Significance

The Jensen bound is the workhorse of discrete-distribution approximation in stochastic programming: it is what makes $Q^\nu(x) = \sum_l p_l Q(x,\xi^l)$ a valid, refinable lower-approximation of the true recourse function, and it underlies the partition-refinement schemes (§8.2, following Birge & Wets [1986] and Frauendorfer & Kall [1988]) used inside the $L$-shaped method and separable-programming solvers described later in the chapter (§8.3). The Edmundson-Madansky bound is its indispensable upper counterpart: without it there is no certificate of how far a lower approximation can be from the truth, and the mean-consistent LP refinement (eq. 2.9, not part of this mission) reduces to a moment-problem computation over $\lambda$. Both bounds are, to date, unformalized: the platform holds no theorem matching either a finite-partition conditional-Jensen inequality or an extreme-point disintegration bound (searched GET /theorems?q=... for "Jensen", "conditional expectation", "Edmundson Madansky", "partition convex" — no relevant hits), so this mission is a first formalization of both, not a reformulation of existing platform content. Mathlib supplies the raw convexity substrate this mission is built from — finite Jensen (Analysis/Convex/Jensen.lean) and, critically, the set-average integral Jensen inequality (ConvexOn.map_set_average_le in Analysis/Convex/Integral.lean), exactly the per-block step the book's proof of Theorem 1 performs — but no existing lemma assembles these into the partitioned, conditional-mean statement the book actually states.

Difficulty

The obvious shortcut is to prove "convex functions lie above their tangent line" and stop — this captures no partition structure at all and is not the theorem the book states (the theorem is about $\Sigma_l p_l g(x,\xi^l)$, a sum over blocks, not a single linearization). The real content is bookkeeping across the partition: writing $\mathbb E(g(x))$ as $\sum_l P(S_l)\,\mathbb E[g(x,\xi)\mid S_l]$ (an exact identity, no convexity needed), then applying ordinary Jensen inside each block to replace $\mathbb E[g(x,\xi)\mid S_l]$ by $g(x,\xi^l)$ from below — the inequality only enters at the second step, once per block. Proving this in Lean means correctly discharging, for every block, the side conditions Mathlib's integral-Jensen lemma needs (closedness of $\Xi$, continuity of $g(x,\cdot)$ on $\Xi$, integrability on the block) and then summing the $\nu$ per-block inequalities against weights $p_l$ that themselves depend on the partition — an easy step to get wrong by, e.g., letting $\xi^l$ be an arbitrary point of $S_l$ rather than exactly its conditional mean, which understates what Jensen actually forces. Theorem 2 additionally requires setting up the disintegration $\lambda$ correctly: $\lambda$ is a probability measure defined as an integral of the kernel-like family $\varphi$ against $P\circ\xi^{-1}$, and both the barycenter condition on $\varphi$ and the measurability of $\omega \mapsto \varphi(\xi(\omega),A)$ are load-bearing — dropping either makes $\lambda$ ill-defined or the bound's proof inapplicable.

Formalization scope

$\Xi \subseteq E$ for $E$ a complete real normed vector space (NormedAddCommGroup E, NormedSpace ℝ E, CompleteSpace E); no finite-dimensionality is assumed since neither theorem's proof needs it. The parameter $x$ ranges over an arbitrary type $\alpha$ with $D \subseteq \alpha$, and $g$ is left as a bare function α → E → ℝ, matching the book's level of abstraction (the recourse LP's own data $A,b,c,q,W,T,h$ is never used in either proof).

The partition is formalized directly on the sample space $\Omega$ (a Partition structure: pairwise-disjoint measurable blocks covering $\Omega$, each of positive measure) rather than on $\Xi$, per the equivalence noted under Setting; $\xi^l$ is defined as the Bochner-integral average $p_l^{-1}\int_{S_l}\xi\,dP$, so it is forced to be the conditional mean and cannot be weakened to an arbitrary sample point of the block — the change the chunk brief flags as the main faithfulness trap for this chapter.

Two explicit hypotheses are added beyond the book's own statement of Theorem 1, both needed by Mathlib's integral-Jensen lemma rather than narrowings of the mathematical content: ContinuousOn (g x) Ξ (finite-dimensional convex functions are automatically continuous on the interior of their domain, which is what the book implicitly relies on; stated explicitly since $E$ is not assumed finite-dimensional) and integrability of $\xi$ and of $g(x,\xi(\cdot))$ (needed for $\mathbb E(g(x))$ and each $\xi^l$ to be well-defined). For Theorem 2, the disintegrating family $\varphi$ is E → Measure Ext for an abstract type Ext (standing for $\mathrm{ext}\,\Xi$) with the discrete MeasurableSpace (every subset measurable, matching the book's "Borel field ... the collection of all subsets"), mapped into $E$ by an embedding toE whose range is exactly (convexHull ℝ Ξ).extremePoints ℝ; the measure $\lambda$ (named μExt in the Lean code, since λ is a reserved keyword) is a hypothesis satisfying its defining equation (2.6) rather than constructed, since constructing a measure from a set function is a separate, book-external piece of measure theory the chapter's own proof does not perform either — it simply asserts $\lambda$ is the probability measure with that value on every set.

A trivializing formalization is ruled out explicitly: a version that lets $\xi^l$ range over an arbitrary point of $S_l$, or that proves only the ordinary (unconditional) Jensen inequality without ever introducing the partition, states something strictly weaker than the book and is not what is formalized here.

Both draft theorems end in := by sorry; a full Lean proof of Theorem 1 combines Mathlib's ConvexOn.map_set_average_le applied per block with the exact decomposition of $\int_\Omega$ into $\sum_l \int_{S_l}$ over the partition's disjoint, covering blocks. Reusable beyond this mission: the Partition structure and its weight/condMean accessors generalize to any chapter needing a finite measurable partition with conditional means (this book's later approximation schemes, §8.2-8.5 and Chapter 10, all build on the same device). Contributions solving either theorem, or formalizing the partition-refinement monotonicity $\mathbb E(g(x)) \ge \mathbb E^{\nu+1}(g(x)) \ge \mathbb E^\nu(g(x))$ (eq. 2.3, not part of this mission's milestone list since it is not itself a numbered theorem) as a follow-up, are welcome.

Selected references

• J.R. Birge, F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4
• J.L.W.V. Jensen, Sur les fonctions convexes et les inégalités entre les valeurs moyennes, Acta Mathematica 30 (1906), 175-193. https://doi.org/10.1007/BF02418571
• H.P. Edmundson, Bounds on the expectation of a convex function of a random variable, The RAND Corporation, Paper 982, 1956.
• A. Madansky, Bounds on the expectation of a convex function of a multivariate random variable, Annals of Mathematical Statistics 30 (1959), 743-746. https://doi.org/10.1214/aoms/1177706207
• A. Madansky, Inequalities for stochastic linear programming problems, Management Science 6 (1960), 197-204. https://doi.org/10.1287/mnsc.6.2.197
• H.I. Gassmann, W.T. Ziemba, A tight upper bound for the expectation of a convex function of a multivariate random variable, Mathematical Programming Study 27 (1986), 39-53. https://doi.org/10.1007/BFb0121114
• J.R. Birge, R.J-B. Wets, Designing approximation schemes for stochastic optimization problems, in particular for stochastic programs with recourse, Mathematical Programming Study 27 (1986), 54-102. https://doi.org/10.1007/BFb0121122