Convex Optimization

Motivation

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

Setting

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

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

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

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

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

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

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

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

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

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

Formalization targets

Building block (Proposition 8.1)

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

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

Intermediate (Theorem 8.1(a))

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

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

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

Goal (Corollary 8.1(a))

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

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 multistage stochastic program's exact deterministic equivalent grows exponentially with the number of periods, even when each period's random data takes only a handful of values (Chapter 9's concern was the growth in the number of realizations; Chapter 10 adds growth in the number of periods). One remedy, generalizing Chapter 8's single-period Jensen bound, is to replace the exact per-period random data by a coarser, aggregated version — conditional expectations over a partition of the history space at each stage — and solve the resulting smaller deterministic equivalent instead. This is only useful if the aggregated problem's optimal value is provably a bound (here, a lower bound) on the exact problem's, and Birge & Louveaux's Chapter 10, §10.1, Theorem 1 is exactly the statement that makes this legitimate, together with a genuinely necessary extra condition the book states explicitly two paragraphs before the theorem: "if not [i.e. if the extra condition fails], then the conditional expectation form ... may not actually achieve a bound." This mission formalizes that theorem.

Setting

The book's exact multistage stochastic linear program (Eq. 1.1, p. 418) is

min c¹x¹ + E_Ω[c²x² + ⋯ + cᴴxᴴ]
s.t. W¹x¹ = h¹,  Tᵗ⁻¹xᵗ⁻¹ + Wᵗxᵗ = hᵗ (t=2,…,H, a.s.),  xᵗ ≥ 0 a.s., xᵗ nonanticipative (Σᵗ-measurable),

over the exact event space Ω = Ω₁ × ⋯ × Ω_H. Given a consistent nested partition of each Ωᵗ = Ω₁ × ⋯ × Ωₜ into finitely many blocks Sᵗ₁, …, Sᵗ_νₜ, and aggregated data (h̄ᵗᵢ, T̄ᵗᵢ) = E^{Sᵗᵢ}[(hᵗ,Tᵗ)] (the conditional expectation of the true random data over block i), the aggregated problem (Eq. 1.2, p. 419) replaces the exact recursion by a finite tree of blocks, one decision per block, linked to its parent block's decision. Both (1.1) and (1.2) are, structurally, the same kind of object — a finite-tree deterministic-equivalent recourse LP — differing only in which tree and which node data they use; this mission formalizes that shared shape once (Tree, Instance, Feasible, obj) and instantiates it twice.

Formalized as: a shared Tree H structure (a finite node type, per-node stage, anc, and a root), the same representation Chunk 06's Multistage.Tree uses for the exact scenario tree of its own (different) chapter, restated here rather than imported (a draft cannot import another chunk's draft). An Instance H n m T bundles a tree's node-varying LP data (c, W, Tmat, h, p); Feasible/obj give its feasible set and objective. The exact problem (1.1) is Instance H n m TFine for a fine/exact tree TFine; the aggregated problem (1.2) is Instance H n m TCoarse for a coarser tree TCoarse, connected to TFine by an aggregation map agg : TFine.Node → TCoarse.Node.

Formalization targets

Goal — Chapter 10, Theorem 1 (p. 419)

agg respects the tree structure (root, stage, ancestor);
W, c agree between the fine and coarse instances (up to agg);
coarse.h, coarse.Tmat are the p-weighted conditional expectations of fine.h, fine.Tmat over
  each aggregation fiber;
∀ coarse nodes i,i' at the same stage sharing a "current-period outcome",
  coarse.h i = coarse.h i' ∧ coarse.Tmat i = coarse.Tmat i'
  ⟹ zCoarse ≤ zFine

This is the mission's only formalization target: BRIEF.md records that no separately numbered lemma precedes Theorem 1's proof in this section to serve as an independent milestone (the proof is a direct LP-duality argument against the theorem's own hypotheses), and that Chapter 8's Theorem 1 — the two-period case this theorem generalizes — is a cross-chapter dependency belonging to Chunk 08's own mission, not a milestone here. milestones.yaml is accordingly empty; see STATUS.md for the explicit accounting of what else in this chapter was considered and left out (Theorem 3, the aggregation error bound of §10.2, an unrelated and substantially heavier result).

Significance

Theorem 1 is what licenses every aggregation-based approximation scheme the rest of the book's multistage material builds on: it says precisely when replacing a multistage recourse problem's random data by within-period conditional expectations preserves a valid lower bound, and precisely identifies the condition (aggregated nodes sharing a current-period outcome must carry identical aggregated data) whose failure breaks the bound — a condition the book states is not decorative ("if not, then the conditional expectation form ... may not actually achieve a bound," p. 418). Formalizing it gives Prove2Me a first structural result connecting Chapter 8's single-period Jensen bound (Chunk 08) to genuinely multistage approximation, using the same finite-scenario-tree deterministic-equivalent representation Chunk 06 uses for the exact nested Benders decomposition — the two missions' shared representation choice (documented in both STATUS.md files) means a future mission relating them formally (e.g. instantiating Chunk 06's exact tree as this mission's TFine) has a compatible object to work with, even though neither imports the other's draft.

Difficulty

The theorem's proof (p. 419-420) is a direct LP weak-duality argument: given an optimal dual solution to the aggregated problem, the book constructs a dual-feasible solution to the exact problem attaining the same value, using precisely the "common outcome ⟹ equal aggregated data" hypothesis to make the constructed dual solution well-defined across the exact tree's finer structure. This is a real argument, not a citation, but it is left as sorry: formalizing the proof would need the multistage LP duality machinery (the "multistage version of Theorem 3.13" the book's own proof invokes, itself left as Exercise 1) that no chunk of this series has built. The value of this mission is the faithful statement of the bound and its exact hypotheses.

Formalization scope

• The book's own printed typo, resolved and documented. Theorem 1's hypothesis clause reads, as printed, "such that (ωt−1,ωt) ∈ Stj if and only if there exist some (ω̂t−1,ωt) ∈ Stj" — S^t_j appears on both sides of the "if and only if," where the sentence's own subject ("S^t_i and S^t_j that have a common outcome") requires the left side to range over S^t_i. Confirmed against a direct render of PDF page 436 (uv run --with pymupdf python), not assumed from OCR: the PDF's own typesetting has this repetition, not an artefact of text extraction. This formalization reads the corrected clause as "S^t_i and S^t_j project onto the same set of period-t outcomes" and states it via an explicit label type Θ and curOutcome : TCoarse.Node → Θ, since the aggregated tree alone does not carry a literal per-period outcome space to project onto (see Setting above — Tree records only history-node structure, not the underlying product space Ω = Ω₁ × ⋯ × Ω_H).
• W, c shared exactly, not aggregated, matching the book's explicit assumption that the recourse matrix and per-stage cost are deterministic and identical across (1.1) and (1.2) ("Wt known and not random," "ct = ct," p. 418) — formalized as direct equality hypotheses (hW_agree, hc_agree) rather than folding W/c into the conditional-expectation machinery that h/Tmat go through.
• zFine/zCoarse are hypothesis-characterized, not sInf-defined, avoiding the real infimum's junk value 0 on an unbounded-below or empty feasible set (reference/FAITHFULNESS_TRAPS.md trap 5) — neither tree-LP's feasible set is shown bounded or nonempty by the hypotheses alone.
• The conditional-expectation defining equations are weighted, p·h/p·Tmat, not h/Tmat alone, matching the book's own E^{Sti}[·] = (h̄ti,T̄ti) read as "the fiber-sum of p·(h,T) equals p_i·(h̄ti,T̄ti)" — the standard definition of a conditional expectation against counting measure on a finite partition. Instance's own hp_pos (every node's probability is strictly positive) rules out the degenerate case a bare unweighted equation would need to guard separately (a coarse node of probability 0, which cannot occur, is what the read-back of this theorem flags as the one case where the weighted equation would not pin down h_coarse/ Tmat_coarse themselves — moot here since hp_pos excludes it).
• Trivialization risk (this chapter's own). A formalization that let coarse.h/coarse.Tmat be arbitrary constants unrelated to fine.h/fine.Tmat (dropping the conditional-expectation defining equations) would still typecheck a "lower bound" conclusion but assert nothing about aggregation — exactly the risk BRIEF.md flags: "a formalization that treats (h̄ti,T̄ti) as arbitrary constants rather than as conditional expectations over a partition of the scenario space at time t loses the theorem's actual content." Both hCoarse_h/hCoarse_T (the defining equations) and hCommonOutcome (the theorem's own extra hypothesis) are load-bearing and present.

Selected references

• Birge, J.R., Louveaux, F. Introduction to Stochastic Programming, 2nd ed., Springer 2011, Chapter 10, §10.1 (pp. 417-420), Theorem 1 (p. 419).
• Birge, J.R. "Decomposition and partitioning methods for multistage stochastic linear programs." Operations Research 33 (1985), 989-1007 — the source Chapter 10's aggregation bounds draw on (cited in §10.2, the neighboring section this mission does not formalize).

Motivation

Two-stage stochastic programs with recourse — choose a first-stage decision $x$ now, observe a random outcome $\xi$, then choose a second-stage recourse decision $y(\xi)$ to repair whatever $x$ left infeasible or suboptimal — are the workhorse model of the field, used for capacity planning, inventory and financial portfolio problems since the 1950s (Dantzig 1955; Beale 1955). When $\xi$ ranges over a finite set of scenarios, the recourse function $Q$ that averages the second-stage cost over scenarios is piecewise linear and convex in $x$, so the overall problem is itself a large linear program — but one whose constraint matrix has a scenario for every column block and can be far too large to hand to a general-purpose LP solver directly. Van Slyke and Wets' L-shaped method (1969), the subject of this mission, is the algorithm that made two-stage recourse problems with finite scenario sets practically solvable: it is Benders decomposition specialized to this block structure, alternating between a small master program over $x$ (and a scalar $\theta$ approximating the recourse cost) and, at each candidate $x$, a batch of second-stage linear programs that either certify $x$'s second-stage feasibility or supply a linear underestimate — a cut — of $Q$ around $x$. Birge & Louveaux's Introduction to Stochastic Programming (2nd ed., Springer 2011), Chapter 5 §5.1, gives the algorithm and proves its two central guarantees: a shortcut feasibility test for a special case (Theorem 1) and the algorithm's finite convergence in general (Theorem 2), which is this mission's goal.

Setting

A two-stage recourse instance consists of a first-stage feasible region $K_1 = \{x \mid Ax = b,\ x \ge 0\}$ for $x \in \mathbb{R}^{n_1}$, and, for each of $K$ finite scenarios $k = 1, \dots, K$ (occurring with probability $p_k$), second-stage data $(q_k, h_k, T_k)$ defining the recourse subproblem

$$Q(x, \xi_k) = \min_{y \ge 0} \{ q_k^\top y \mid W y = h_k - T_k x \},$$

where the recourse matrix $W$ is fixed — the same across every scenario, the case this chapter treats. $K_2 = \{x \mid Q(x,\xi_k) < \infty \text{ for all } k\}$ is the set of $x$ for which every scenario's subproblem is feasible, and the two-stage problem is

$$\min_{x} \ c^\top x + Q(x) \quad \text{s.t.} \quad x \in K_1 \cap K_2, \qquad Q(x) = \sum_{k=1}^K p_k\, Q(x, \xi_k).$$

A basis of the recourse subproblem is an injective choice of $m_2$ of $W$'s columns (where $m_2$ is $W$'s row count); each basis $b$ determines a simplex multiplier $\pi = (W_b^\top)^{-1} q_b$, and when $b$ attains the true optimum of $Q(x,\xi_k)$, LP duality gives $Q(x,\xi_k) = \pi^\top(h_k - T_k x)$ — the mechanism that turns a batch of second-stage LP solves into linear cuts on $x$.

Formalization targets

The L-shaped algorithm proceeds in three steps, repeated until neither applies:

• Step 1 solves the current master program (the $K_1$-feasible $x$, plus $\theta$ once at least one optimality cut exists, minimizing $c^\top x + \theta$ subject to every cut recorded so far — or just $c^\top x$ over $K_1$ before the first optimality cut, matching the book's convention that $\theta$ "is set equal to $-\infty$ and is not considered" until then).
• Step 2 tests each scenario's second-stage feasibility at the Step-1 optimum via an auxiliary LP; if some scenario fails (the LP's optimal value is positive), its optimal basis yields a feasibility cut and the algorithm returns to Step 1.
• Step 3, once every scenario is feasible, checks whether $\theta$ already dominates the true recourse cost at $x$ (using each scenario's optimal basis via LP duality); if not, an optimality cut is added and the algorithm returns to Step 1; if so, $x$ is optimal and the algorithm stops.

Goal — Chapter 5, Theorem 2 (p. 198)

$$\text{When } \xi \text{ is a finite random variable, the L-shaped algorithm finitely converges to}$$ $$\text{an optimal solution when it exists, or proves } K_1 \cap K_2 = \varnothing.$$

Formalized as: starting from the empty cut set, there is a finite-length run of the algorithm's Step-1/2/3 transition relation, of length bounded by the total number of distinct feasibility- and optimality-cut witnesses available, ending at a state admitting no further step — at which point either the master program has become infeasible (certifying $K_1 \cap K_2 = \varnothing$) or its optimum is second-stage feasible, passes every fresh Step-3 test, and is optimal for the two-stage problem.

Milestone — Chapter 5, Theorem 1 (p. 194)

$$\text{If } T \text{ is deterministic, } W \text{ is such that every } t \ge 0 \text{ lies in } \mathrm{pos}\,W,$$ $$\text{and } a = \min_k h_k \text{ (componentwise) is attained by some scenario } h_\ell,$$ $$\text{then } x \in K_2 \iff \exists\, y \ge 0,\ Wy = a - Tx.$$

A shortcut avoiding $K$ separate feasibility LPs at Step 2: under these structural assumptions on $W$, checking feasibility at the single componentwise-worst right-hand side certifies feasibility at every scenario simultaneously.

Significance

Van Slyke and Wets' method (and Benders decomposition more generally, of which it is the recourse-problem specialization) underlies essentially every large-scale two-stage stochastic program solved in practice, and its finite-convergence guarantee — not merely that an optimum exists, but that this specific cutting-plane procedure reaches it in finitely many outer iterations — is what makes the method a decision procedure rather than a heuristic. The proof's content is an explicit finiteness argument (the number of distinct simplex bases of the recourse subproblem and the feasibility-test LP is finite, so the algorithm cannot generate infinitely many distinct cuts before either exhausting the feasible region or converging), not a general compactness or fixed-point argument; formalizing it means formalizing the cutting-plane mechanism itself as a transition system and proving termination combinatorially, over the finite type of available bases, rather than proving only that some optimal $x$ exists.

Difficulty

The natural shortcut — state only "an optimal $x$ exists, or $K_1 \cap K_2 = \varnothing$" — is not Theorem 2's actual content and is not what this mission targets: that weaker claim would already follow from $K_1 \cap K_2$ being a nonempty polyhedron (or empty), with no reference to the algorithm at all, and would not require the finiteness-of-bases argument the book's proof turns on. The genuine difficulty is representing Steps 1-3 faithfully as a relation on accumulating cut sets, and pinning the termination bound to the actual combinatorial object the book cites (the finite set of bases of the two LPs the algorithm solves at each iteration) rather than to a numeral or an abstract compactness bound. A second, quieter difficulty is Step 1's own optimum: once optimality cuts exist, the master program optimizes $c^\top x + \theta$ jointly, but before the first one it optimizes $c^\top x$ alone; conflating the two (e.g. always requiring $\theta$ to be part of the optimum) does not match Step 1 as the book states it.

Formalization scope

First-stage and second-stage vectors are Fin n1 → ℝ / Fin n2 → ℝ; the finite scenario set is Fin K with probability vector p. A basis is {b : Fin m2 → Fin n2 // Function.Injective b} (m2 = the recourse matrix's row count), matching "an injective choice of $m_2$ columns of $W$"; its finiteness is definitional, from Fin m2 → Fin n2 being finite. Simplex multipliers use Matrix.inv, whose junk value 0 on a singular matrix is never reachable in a proof because multipliers are only ever used through an IsOptimalAt/IsFeasBasisOptimalAt hypothesis that pins the basis to one genuinely attaining the LP's true optimum. The recourse value $Q(x,\xi_k)$ is EReal-valued (reusing this series' Instance/QVal convention from Chunk 03), so an optimality-cut witness's claimed value is compared to it by an explicit EReal cast, never by EReal arithmetic. The algorithm's state is a pair of finite sets of witnesses recorded so far (Finset (Fin K × FeasBasis n2 m2) × Finset (Fin K → Basis n2 m2)); Step is an inductive relation with one constructor per Step-2 and Step-3 branch, each requiring its witness not already recorded, and the goal states a bounded-length Step-path from the empty state to a state admitting no further Step. This mission does not restate Chapter 3's polyhedrality fact about $K_2$ as a separate lemma: the finiteness fact it is invoked for is already exposed directly and structurally by the finite Fintype bound on the number of bases, so no additional axiom stands in for it (see MODERATION_NOTES.md). Lemmas 3-9 and Theorem 10 of §5.2 (Regularized Decomposition, a different algorithm) are out of scope. The trivializing formalization this mission rules out is exactly the one named under Difficulty above: a bare existence-of-optimal-or- infeasible-$x$ statement with no reference to Steps 1-3 or to a finite bound on the number of iterations — such a statement would be true of any nonempty polyhedron and would not be Theorem 2.

Selected references

• R. Van Slyke and R. Wets, L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming, SIAM Journal on Applied Mathematics, 17(4), 1969, pp. 638-663. https://doi.org/10.1137/0117061
• J. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Chapter 5. https://doi.org/10.1007/978-1-4614-0237-4
• G. Dantzig, Linear Programming under Uncertainty, Management Science, 1(3-4), 1955, pp. 197-206. https://doi.org/10.1287/mnsc.1.3-4.197

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

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

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

Setting

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

$$\Bigl| \sum_{i=1}^m \sum_{j=1}^n a_{ij}\, x_i y_j \Bigr| \;\le\; 1.$$

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

Formalization targets

Grothendieck's inequality (Theorem 3.5.1)

$$A \text{ normalized} \;\Longrightarrow\; \Bigl| \sum_{i,j} a_{ij}\, \langle u_i, v_j\rangle \Bigr| \;\le\; K$$

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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