Machine Learning

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

Machine learning's canonical training objective — minimize an expected or empirical risk over a data distribution — is almost never observed exactly: at each step an algorithm sees only a noisy gradient sample (a minibatch gradient, a single-example gradient, a simulation draw). Stochastic mirror descent (Nemirovski, Juditsky, Lan & Shapiro 2009) is the modern, general-norm answer to "what happens to first-order convergence guarantees when the gradient itself is a random variable": it takes the deterministic mirror-descent scheme of the previous chapter and replaces the exact subgradient with an unbiased stochastic estimate, and asks for both an expected convergence rate and, when the noise is well-behaved, an explicit probability-of-large-deviation guarantee. This is the theoretical backbone of stochastic gradient descent as used in practice.

Setting

Fix a nonempty closed convex set $X$ in a real normed space $E$, and a convex $f:X\to\mathbb R$ with $f^*:=\min_{x\in X}f(x)$ and $x^*$ an arbitrary minimizer, exactly as in Chapter 3. A stochastic oracle $G(x,\xi)$, queried at a point $x$ with a fresh random sample $\xi$, returns an estimate of a subgradient $g(x)\in\partial f(x)$: $\mathbb E[G(x,\xi)] = g(x)$ (unbiasedness), $\|g(x)\|_*\le M$ (a dual-norm Lipschitz bound, Eq. (4.1.7)), and $\mathbb E[\|G(x,\xi)-g(x)\|_*^2]\le\sigma^2$ (a second-moment/variance bound). The stochastic mirror-descent update is exactly Chapter 3's mirror-descent update with $G_t := G(x_t,\xi_t)$ in place of the deterministic $g_t$: $x_{t+1} := \arg\min_{x\in X}\gamma_t\langle G_t,x\rangle + V(x_t,x)$ (Eq. (4.1.6)), where $V$ is the Bregman divergence of a fixed distance-generating function $\nu$.

Formalization targets

Goal — Theorem 4.1

$$\mathbb E[f(\bar x^k_s)] - f^* \le \Big(\sum_{t=s}^k\gamma_t\Big)^{-1}\Big(\mathbb E[V(x_s,x^*)] + (M^2+\sigma^2)\sum_{t=s}^k\gamma_t^2\Big).$$

Supporting milestones, in attack order

• Lemma 3.4, invoked for the stochastic update: the same three-point inequality as the deterministic mirror-descent update, restated with the stochastic gradient functional $G_t$ in place of $g_t$ — the book's own remark ("It can be easily seen that the result in Lemma 3.4 holds with $g_t$ replaced by $G_t$") is exactly what licenses treating this as the same algebraic fact for a fixed sample path.
• Lemma 4.1: the martingale-difference deviation bound, a Chernoff-type concentration inequality for a conditionally sub-Gaussian martingale-difference sequence — the chapter's general-purpose probabilistic tool, proved independently of the optimization setting.

Every constant is exactly the book's; $M^2+\sigma^2$ (not a generic $O(\cdot)$) is the goal's own noise-dependent constant, taken verbatim.

Significance

This is the first mission in the series to leave the purely deterministic, real-analytic setting of Chapters 2-3 and formalize a genuinely probabilistic convergence guarantee: an expectation taken over an entire random algorithm trajectory $\xi_1,\dots,\xi_k$, not merely over a single random variable. Getting the goal theorem's statement right requires being explicit about exactly which quantities are random (the iterates $x_t$, hence $f(\bar x_s^k)$ and $V(x_s,x^*)$) and which are deterministic constants fixed in advance ($M,\sigma,\gamma_t$), and about the precise mathematical content of "the stochastic gradient's bias vanishes after conditioning on the past" — Lemma 4.1 is included specifically because it is the general machine that makes that vanishing rigorous, independent of the optimization application.

No result matching stochastic mirror descent, Assumption 4's sub-Gaussian/light-tail condition, or this martingale-difference concentration lemma exists on the platform as of 2026-09-18 (q= stochastic gradient, q=stochastic mirror descent, q=martingale, q=sub-Gaussian — see Prior art below for what these queries actually returned).

Difficulty

The central difficulty is disentangling which facts in the chapter's proof genuinely need measure theory and which do not. The per-step algorithmic relations — $x_{t+1}$'s minimality, $f$'s subgradient inequality at $x_t$, the dual-norm bound on $g$ — hold for every sample path individually and are formalized pointwise in $\omega$, exactly as chunk 03-deterministic formalizes its deterministic analogues; only the second-moment bound and the final expectation inequality are genuine integrals. The one place this pointwise treatment cannot simply mirror the deterministic case is the noise cross-term $\mathbb E[\gamma_t\langle\delta_t,x_t-x^*\rangle]=0$: in the book's proof this vanishes because $\delta_t=G_t-g(x_t)$ is conditionally mean-zero given the past and $x_t$ is a function of the past (the martingale-difference property, via the tower property of conditional expectation) — a genuinely non-pointwise fact. Rather than thread an explicit filtration through the goal theorem's own statement (which Lemma 4.1 already does, as the chapter's dedicated home for that machinery), the goal theorem takes this post-tower-property consequence directly as a named hypothesis (hcross); see Formalization scope.

Formalization scope

stochastic_mirror_iterate_three_point and stochastic_mirror_descent_bound are stated over a general real normed space [NormedAddCommGroup E] [NormedSpace ℝ E], matching chunk 03-deterministic's general-norm milestones (mirror_iterate_three_point/mirror_descent_bound) rather than the Euclidean/inner-product specialization of that chunk's §3.1 items — Chapter 4's own stochastic mirror descent is presented directly in the general-norm framework of §3.2, with no Euclidean-only warm-up. $V$ is left a free two-point function (never hard-coded to a squared Euclidean distance), and the stochastic gradient $G_t$ and the subgradient selector $g$ are continuous linear functionals E →L[ℝ] ℝ, whose Mathlib operator norm supplies the dual norm $\|\cdot\|_*$ with no separate definition needed — the same trivializing formalization chunk 03-deterministic rules out (specializing $V$ to the Euclidean case) applies here and is ruled out the same way.

martingale_difference_deviation_bound (Lemma 4.1) is a standalone probabilistic result, formalized with Mathlib's MeasureTheory.Filtration and condExp machinery: the sequence $\xi_{[t]}$'s generated filtration, $\zeta_t$'s $\mathcal F_t$-measurability, and the two conditional-expectation hypotheses (conditional mean zero, conditional sub-Gaussian tail) are all literal translations of the book's own E|ξ[t-1] notation.

Left out of scope, for time: Assumption 4 (the light-tail/sub-Gaussian oracle assumption), Proposition 4.1 (the large-deviation bound under Assumption 4, which chains Lemma 4.1's concentration bound with the constant stepsize policy (4.1.11) and a second Markov-inequality argument on $\sum\gamma_t^2\|\delta_t\|_*^2$), Lemma 4.2 and Theorem 4.2 (the smooth-$f$ case, §4.1.2, requiring a separate recursion and averaging convention $x_t^{av}$). All four are natural continuations reusing this mission's stochastic_mirror_iterate_three_point and/or martingale_difference_deviation_bound; a later mission or an amendment to this one could add them without touching what is here. Per Hard Rule 7 (faithfulness over coverage), a genuinely faithful formalization of Proposition 4.1 in particular — which needs Assumption 4's own conditional-MGF hypothesis threaded consistently with Lemma 4.1's, plus the constant-stepsize substitution and a second concentration argument — was judged to need more time than this session's budget allowed to do without shortcuts; it is named here rather than approximated.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 4, §4.1. https://doi.org/10.1007/978-3-030-39568-1
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, "Robust stochastic approximation approach to stochastic programming," SIAM Journal on Optimization, 19(4), 2009, pp. 1574-1609.
• H. Robbins, S. Monro, "A stochastic approximation method," Annals of Mathematical Statistics, 22(3), 1951, pp. 400-407 (origin of stochastic approximation).

Motivation

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

Setting

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

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

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

Formalization targets

Lemma 12.3 (extension operator properties, milestone)

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

Lemma 12.5 (smoothed-loss regret comparison, milestone)

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

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

Setting

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

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

Formalization targets

Theorem 9.1 (No Free Lunch, milestone)

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

Theorem 9.5 — the mission's goal

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

$$\mathrm{error}(\bar h) \le \mathrm{error}(h^\star) + \frac{\mathrm{Regret}_T(A)}{T} + \sqrt{\frac{8\log(2/\delta)}{T}}, \qquad h^\star = \arg\min_{h\in H}\{\mathrm{error}(h)\}.$$

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 9.
• V. Vapnik, A. Chervonenkis, "On the uniform convergence of relative frequencies of events to their probabilities," Theory of Probability and its Applications 16(2), 1971, 264-280.

Motivation

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

Setting

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

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

Formalization targets

Theorem 7.1 (offline CG convergence, milestone)

$$h_t \le \frac{2\beta D^2}{t}, \quad t \ge 1, \qquad h_t := f(x_t) - f(x^\star).$$

Lemma 7.4 (per-round iterate bound, milestone)

$$h_t \le 2D^2\sigma_t, \quad t \ge 1, \qquad h_t := F_t(x_t) - F_t(x^\star_t),\ \ x^\star_t := \arg\min_{x\in K} F_t(x).$$

Theorem 7.3 — the mission's goal

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

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

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

Every RL guarantee proved earlier in this series — UCB-VI's regret bound, the contextual bandit oracle reductions — scales with the size of the state space $S$, because the algorithms maintain a separate statistic per state. Real environments (images, sensor readouts, natural language) have combinatorially or infinitely many states, so a tabular guarantee is vacuous there: the only hope is to generalize across states via a class of value functions, the way supervised learning generalizes across inputs via a hypothesis class. The chapter develops two algorithms along this line: LSVI-UCB, the linear-function-approximation analogue of UCB-VI whose regret is independent of $|S|$ (a low-rank MDP result originating with Jin, Yang, Wang, and Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation, COLT 2020, arXiv:1907.05388), and BiLinUCB, which attains an analogous sample-complexity guarantee under the strictly more general structural condition of low Bellman rank (Jiang, Krishnamurthy, Agarwal, Langford, and Schapire, Contextual Decision Processes with Low Bellman Rank are PAC-Learnable, ICML 2017, arXiv:1610.09512; the Q-type variant formalized here follows Du, Kakade, Wang, and Yang, Is a Good Representation Sufficient for Sample Efficient Reinforcement Learning?, ICLR 2020, arXiv:1910.03016). This mission formalizes the second, strictly more general track: BiLinUCB and its Bellman-rank guarantee; LSVI-UCB is left out of scope (see Formalization scope).

Setting

Both algorithms act on the finite-horizon episodic MDP $M = (S,A,\{P_h\}_{h=1}^H, \{R_h\}_{h=1}^H,d_1)$ of the earlier chapters of this series (RLBasics.Core), with value $f^M(\pi) = \mathbb E_{s_1\sim d_1}[V_1^{M,\pi}(s_1)]$. For a state-action value function $Q = (Q_h)_{h=1}^H$ (with the convention $Q_{H+1}\equiv 0$), the Bellman residual of $Q$ under policy $\pi$ at layer $h$ is

$$E_h(\pi,Q) := \mathbb E^{M,\pi}\Big[Q_h(s_h,a_h) - R_h(s_h,a_h) - \max_{a'} Q_{h+1}(s_{h+1},a')\Big],$$

which vanishes identically when $Q = Q^{M,\star}$, the optimal value function (Bellman optimality). Given a class $\mathcal Q$ of candidate value functions, $M$ has Bellman rank $d$ relative to $\mathcal Q$ (Definition 8) if $d$ is the least integer such that, at every layer $h$, there exist embeddings $X_h(\pi), W_h(Q) \in \mathbb R^d$ with $E_h(\pi,Q) = \langle X_h(\pi), W_h(Q)\rangle$ for every policy $\pi$ and $Q\in\mathcal Q$ — equivalently, the least rank of the $\Pi\times\mathcal Q$ matrix of Bellman residuals, at any layer. A linear MDP (the setting of LSVI-UCB, §7.2) is the special case where the transition kernel and reward themselves factor through a known feature map $\phi : S\times A \to \mathbb R^d$; every linear MDP has Bellman rank at most $d$ relative to the linear value-function class, but Bellman rank captures far more (kernel/neural function classes, and low-rank MDPs whose feature map is unknown).

The chapter presents two algorithms. LSVI-UCB (§7.2.1) runs $T$ episodes of ridge regression per layer against the linear feature map, forming a confidence ellipsoid of radius $\rho \propto \sqrt d$ around each layer's estimated parameter and acting greedily with respect to an upper-confidence bonus built from that ellipsoid — the same optimism-under-uncertainty template as UCB-VI, now regularized rather than tabular; it motivates Bellman rank but is not itself formalized by this mission (see Formalization scope). BiLinUCB (§7.3.1), the algorithm this mission formalizes, instead proceeds in $K$ iterations of $n$ episodes: each iteration plays the greedy policy for the current optimistic-on-average value function $Q_k = \arg\max_{Q\in\mathcal Q_k}\mathbb E_{s_1\sim d_1}[Q_1(s_1, \pi_Q(s_1))]$, collects $n$ fresh episodes, and shrinks the confidence set $\mathcal Q_{k+1}$ by discarding value functions whose empirical Bellman residual along the played policy is large; after $K$ iterations it outputs the policy with the best empirical return observed at any iteration.

Formalization targets

Goal — Proposition 47 (BiLinUCB, sample complexity under Bellman rank)

$$\exists\, c_1,c_2,c_3>0,\ \forall\,\varepsilon,\delta>0,\ \ n\gtrsim \frac{H^3d\log(|\mathcal Q|/\delta)}{\varepsilon^2},\ \ K\gtrsim Hd\log(1+n/d),\ \ \beta\propto\frac{K\log|\mathcal Q|+\log(HK/\delta)}n\ \Longrightarrow$$ $$\Pr\big[f^{M^\star}(\pi^{M^\star}) - f^{M^\star}(\hat\pi) \le \varepsilon\big] \ge 1-\delta,$$

for $M^\star$ of Bellman rank $d$ relative to $\mathcal Q\ni Q^{M^\star,\star}$, where $\hat\pi$ is BiLinUCB's output policy after $K$ iterations of $n$ episodes. This is the weakest stable form: it fixes the shape of the sample complexity (polynomial in $H,d,\log|\mathcal Q|,1/\varepsilon$, logarithmic in $1/\delta$, independent of $|S|$) and leaves the leading constants — which the book itself introduces only as "a sufficiently large numerical constant" — outside the formal claim. Unlike every other goal in this series, this is a PAC (sample-complexity) guarantee on the algorithm's final output policy, not a bound on cumulative regret accrued while learning: BiLinUCB commits to $\hat\pi$ only after the training phase ends, and its suboptimality is measured post-training.

Reaching it rests on two structural facts about BiLinUCB's confidence sets, each formalized as a milestone in attack order:

• Lemma 29 (confidence-set validity): with the stated threshold $\beta$, with probability at least $1-\delta$, simultaneously at every iteration $k$, every retained value function has true (population) Bellman residual along the played policies bounded by $\beta$ up to a constant, and the realizable $Q^{M^\star,\star}$ is itself always retained.
• Lemma 30 (optimism and elliptic-norm bound): conditioned on Lemma 29's event, every retained value function's embedding $W_h(Q)$ has bounded norm with respect to the Gram matrix of the played policies' embeddings, and the optimistic value function $Q_k$ BiLinUCB selects at each iteration has initial-state value at least $f^{M^\star}(\pi^{M^\star})$.

Significance

Proposition 47 shows that a single structural parameter — Bellman rank — is sufficient for sample-efficient RL with function approximation, with a sample complexity that depends only on the horizon, the rank, and the value-function class's log-cardinality, never on $|S|$. This subsumes the linear-MDP guarantee of Proposition 46 (LSVI-UCB, §7.2.1; not itself a target of this mission, see Formalization scope) as a special case — every linear MDP has Bellman rank $\le d$ — while covering strictly more models (kernelized and neural value-function classes with a low-dimensional Bellman-residual factorization that need not come from a known linear feature map). The result is proved in the source and this mission formalizes its statement and the two structural lemmas its proof rests on, as stated; no new mathematics is contributed. Formalizing it commits, for the first time on this platform, to machine-checkable statements of the Bellman rank abstraction, the elliptic-norm confidence-set machinery it drives, and a PAC- (rather than regret-) style learning guarantee, none of which appear in the platform's existing bandit or tabular-RL missions.

Difficulty

The obvious first attempt is to formalize Bellman rank as an unconstrained integer parameter $d$ attached to the MDP, sidestepping the actual rank condition on the Bellman-residual matrix; this is a trivializing formalization; Bellman rank must be the least dimension admitting the stated bilinear factorization; see Formalization scope. A second obstacle is that BiLinUCB's optimism is only "on average" with respect to the initial state distribution (initValue), unlike LSVI-UCB's pointwise optimism over every state and action — conflating the two confidence-set constructions collapses the chapter's main conceptual contrast. Finally, the two technical lemmas (29 and 30) separate a purely probabilistic statement (validity of the empirical confidence set, via Hoeffding and a union bound) from a purely deterministic consequence (the elliptic-norm bound and optimism, which hold on any sample path where the probabilistic event occurred); keeping this separation is what lets Proposition 47's proof combine them cleanly, and collapsing it into one monolithic high-probability statement would misrepresent the book's proof structure.

Formalization scope

The MDP, policy, and trajectory/history machinery (EpisodicMDP, Policy, IsPolicy, Trajectory, Learner, probEvent) are reused unchanged from the series' published RLBasics.Core/RLBasics.UCBVI definitions. The value-function class $\mathcal Q$ is realized as an abstract finite, nonempty type Qc together with an evaluation map qeval : Qc → ℕ → S → A → ℝ, kept fully abstract rather than specialized to any concrete function class — specializing it to, e.g., linear functions would collapse Proposition 47 back into a restatement of Proposition 46, which is exactly the trivializing formalization this mission avoids. Bellman rank (IsBellmanRank) is defined as the least natural number admitting the bilinear factorization (an IsLeast over the coercion to HasBellmanRankLE), never as a free parameter. Every realized per-step reward is taken equal to its conditional mean $R_h(s,a)$ throughout (exact, by the tower property, and not a restriction to deterministic rewards). The elliptic norm of Lemma 30 is expressed via the direct sum-of-squared-inner-products identity $\|v\|^2_\Sigma = \sum_{x\in xs}\langle x,v\rangle^2$ rather than introducing Matrix/matrix-inverse machinery, since no milestone here needs an explicit matrix inverse. Every place the book writes ≲/∝/"a sufficiently large numerical constant" is formalized as an existentially quantified universal constant, fixed ahead of every MDP, value-function class, and $(\varepsilon,\delta)$ instance — never depending on the instance itself. This mission scopes entirely to the Bellman-rank track (Definition 8, BiLinUCB, Lemmas 29-30, Proposition 47); Proposition 46 (LSVI-UCB) and its supporting Lemmas 27-28 are the chapter's motivating linear special case (Section 7.2) but are left out of this mission's scope for time and are not claimed as proved by it — LSVI-UCB's confidence-ellipsoid construction is materially different from BiLinUCB's empirical-Bellman-residual confidence set (see Difficulty) and would need its own milestone chain. A complete development needs no infrastructure beyond what is already published in RLBasics.Core/RLBasics.UCBVI; contributions completing the sorrys in the two technical lemmas and the goal are welcome.

Selected references

• Foster, D. J. and Rakhlin, A. Foundations of Reinforcement Learning and Interactive Decision Making. arXiv:2312.16730v1, 2023. arXiv:2312.16730
• Jin, C., Yang, Z., Wang, Z., and Jordan, M. I. Provably Efficient Reinforcement Learning with Linear Function Approximation. COLT 2020. arXiv:1907.05388
• Jiang, N., Krishnamurthy, A., Agarwal, A., Langford, J., and Schapire, R. E. Contextual Decision Processes with Low Bellman Rank are PAC-Learnable. ICML 2017. arXiv:1610.09512
• Du, S. S., Kakade, S. M., Wang, R., and Yang, L. F. Is a Good Representation Sufficient for Sample Efficient Reinforcement Learning? ICLR 2020. arXiv:1910.03016

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

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