Optimization

Motivation

Empirical-risk-minimization objectives in machine learning are finite sums: $\Psi(x) = \frac{1}{m}\sum_{i=1}^m f_i(x) + h(x)$, one smooth term $f_i$ per training example (or per worker, in a distributed setting), plus a simple nonsmooth regularizer $h$. Chapter 4's basic stochastic mirror descent handles this by sampling a single random component gradient $\nabla f_{i_t}(x)$ as an unbiased estimator of $\nabla f(x)$ — but that estimator's variance is a constant throughout the algorithm, which caps the achievable convergence rate. Variance-reduced mirror descent asks a sharper question: can an unbiased finite-sum gradient estimator be built whose variance itself vanishes as the algorithm approaches the optimum? The answer — periodic full-gradient snapshots combined with single-component corrections — is the SVRG-style idea this mission formalizes in Lan's general-norm mirror-descent framework, with an explicit, sampling-distribution-dependent constant rather than a generic $O(\cdot)$.

Setting

Fix a closed convex set $X$ in a real normed space $E$, and the finite-sum composite problem $\min_{x\in X}\{\Psi(x):=f(x)+h(x)\}$ (Eq. (5.3.1)), where $f(x)=\frac1m\sum_{i=1}^m f_i(x)$ is the average of $m$ smooth convex component functions, each with $L_i$-Lipschitz gradient $\nabla f_i$ ($\|\nabla f_i(x)-\nabla f_i(y)\|_*\le L_i\|x-y\|$), and $h$ is a simple, possibly nondifferentiable convex function. $f$ is possibly $\mu$-strongly convex, $\mu\ge0$ (Eq. (5.3.2)); this mission's goal takes $\mu=0$ (§5.3.1, "Smooth Problems Without Strong Convexity"). A fixed probability distribution $Q=\{q_1,\dots,q_m\}$ on the component indices governs the algorithm's random sampling, and

$$L_Q := \frac{1}{m}\max_{i=1,\dots,m}\frac{L_i}{q_i}$$

is the section's key aggregate smoothness constant (Eq. (5.3.4)), replacing the plain average $L$ wherever component-wise variance enters the analysis. Variance-reduced mirror descent (Algorithm 5.6) is a multi-epoch method: each epoch of length $T_s$ recomputes a full gradient $\nabla f(\tilde x)$ at a snapshot point $\tilde x$, then runs $T_s$ inner iterations using the estimator $G_t := \big(\nabla f_{i_t}(x_t)-\nabla f_{i_t}(\tilde x)\big)/(q_{i_t}m) + \nabla f(\tilde x)$ and the mirror-descent-with-composite-term update $x_{t+1}:=\arg\min_{x\in X}\{\gamma[\langle G_t,x\rangle+h(x)]+V(x_t,x)\}$, where $V$ is the Bregman divergence of a fixed distance-generating function, exactly as in Chapters 3-4.

Formalization targets

Goal — Corollary 5.8

With $\theta=1$, $\gamma=1/(16L_Q)$, and the doubling epoch schedule $T_1=7$, $T_s=2T_{s-1}$ (Eq. (5.3.17)),

$$\mathbb E[\Psi(\bar x_S)-\Psi(x^*)] \le \frac{8}{2^{S-1}}\left[\frac{11}{4}\big(\Psi(x_0)-\Psi(x^*)\big)+16L_Q\,V(x_0,x^*)\right]$$

for every epoch count $S\ge1$, where $\bar x_S$ is the weighted average of the epoch snapshots (Eq. (5.3.16)).

Supporting milestones, in attack order

• Lemma 5.12 — the per-component gradient-variation bound $\frac1m\sum_i\frac1{mq_i}\|\nabla f_i(x)-\nabla f_i(x^*)\|_*^2 \le 2L_Q[\Psi(x)-\Psi(x^*)]$, the basic smoothness consequence from which the estimator's variance bound is built.
• Lemma 5.13 — unbiasedness ($\mathbb E[\delta_t]=0$) and two variance bounds ($\mathbb E[\|\delta_t\|_*^2]\le 2L_Q[\dots]$ and $\le 4L_Q[\dots]$) for the variance-reduced estimator's error $\delta_t:=G_t-\nabla f(x_t)$.
• Lemma 5.14 — the one-step progress bound combining Lemma 5.13's variance control with the mirror-descent update's three-point inequality.
• Theorem 5.6 — the general epoch-level convergence bound (with an arbitrary epoch-length schedule $T_s$ and stepsize $\gamma$ satisfying $4L_Q\gamma\le1$) that Corollary 5.8 instantiates.

Every constant is exactly the book's: $L_Q$'s own sampling-distribution-dependent definition (never specialized to uniform $q_i=1/m$), and Corollary 5.8's explicit $8/2^{S-1}$, $11/4$, $16L_Q$ — not a generic $O(\cdot)$ — are all taken verbatim.

Significance

This is the series' first genuinely finite-sum result: unlike Chapters 3-4's single abstract objective $f$, here $f$ is structurally a named average of $m$ component functions, and the sampling distribution $\{q_i\}$ over those components is a first-class free parameter of both the algorithm and the analysis (not fixed to uniform sampling) — $L_Q$ itself depends on this choice, and a formalization that hard-codes $q_i=1/m$ would understate what Lemma 5.12's own proof needs. Getting Theorem 5.6/Corollary 5.8 right also requires keeping two nested indices straight: inner iterations $t$ within an epoch, and outer epoch counts $s$, with the convergence bound stated in terms of the epoch count $S$ alone — and keeping the two "gap" quantities $\Psi(x_0)-\Psi(x^*)$ (an objective-value gap) and $V(x_0,x^*)$ (a Bregman-divergence gap) distinct throughout, since they enter Corollary 5.8's final bound with different explicit coefficients ($11/4$ vs. $16L_Q$) and neither generically bounds the other.

No result on the platform models a finite-sum objective with $m$ named component functions sampled by a general index distribution $\{q_i\}$, a variance-reduction snapshot/anchor point, or this specific SVRG-style estimator, as of 2026-09-18 (q=finite sum, q=variance reduction, q=SVRG, q=component function, q=variance reduced gradient, q=mirror descent finite sum — see Prior art below).

Difficulty

The central difficulty is Theorem 5.6's own epoch-weight sequence $w_s$: the book defines $w_s:=(1-4L_Q\gamma)(T_{s-1}-1)-4L_Q\gamma T_s$ explicitly only for $s\ge2$ (Eq. (5.3.14)), yet the displayed sums $\sum_{s=1}^S w_s$ in (5.3.15)-(5.3.16) run from $s=1$. A 2026-09-19 revision found that this, combined with the epoch snapshot $\tilde x_s$ being constrained only by membership in $X$ and not tied to the algorithm's own dynamics, made the originally drafted statements false, not merely incomplete: an adversarial, unboundedly-large-$\Psi$, $\omega$-independent $\tilde x_1$ together with $w_1\to\infty$ violates the stated conclusion. The fix restores the connection via an auxiliary epoch-boundary sequence and the per-epoch progress inequality Theorem 5.6's own proof derives from Lemma 5.14 (see epoch_convergence_bound's hepoch hypothesis), and resolves $w_1$ by extending (5.3.14)'s domain to $s\ge1$ via a fixed "epoch 0" length $T_0$ — w_1 is no longer left free beyond positivity. finite_sum_variance_reduced_rate instantiates $T_0:=T_1/2=3.5$ concretely, reproducing the arithmetic Corollary 5.8's own proof is internally consistent with ($w_1 = 3/4(3.5-1)-1/4\cdot7 = 1/8$, matching the closed form $(1/8)T_1-3/4=1/8$) — this was previously only a documented-but-unresolved observation, not yet a stated hypothesis.

Formalization scope

All five items are stated over a general real normed space [NormedAddCommGroup E] [NormedSpace ℝ E], matching the mirror-descent chunks' general-norm convention (never specialized to Euclidean space or squared distance) — $V$ is a free two-point function throughout, and each $\nabla f_i$, $\nabla f$, $G_t$ are continuous linear functionals E →L[ℝ] ℝ, whose Mathlib operator norm supplies the dual norm $\|\cdot\|_*$ with no separate definition needed. This is the trivializing formalization this mission rules out: hard-coding $q_i=1/m$ (uniform sampling) or $V(x,y)=\frac12 \|x-y\|^2$ (Euclidean Bregman divergence) would understate both $L_Q$'s dependence on the sampling distribution (the whole point of Lemma 5.12's bound) and the general-norm apparatus the rest of this book series shares.

Ψ(x_0)-Ψ(x^*) and V(x_0,x^*) are kept as two syntactically distinct terms throughout — never conflated or bounded one by the other — matching Corollary 5.8's own two separate coefficients. Corollary 5.8's own explicit constants ($8/2^{S-1}$, $11/4$, $16L_Q$) are stated verbatim rather than left as an unspecified $O(\cdot)$, per Hard Rule 6.

Left out of scope, for time: the gradient-computation-count complexity bound (Eq. (5.3.19), an $O(\cdot)$ statement about total oracle calls, not a convergence-rate inequality on $\Psi$) and §5.3.2's strongly-convex case (Theorem 5.7, a geometric-decay bound $\Delta_s\le\rho\Delta_{s-1}$ under $\mu>0$) are natural continuations reusing this mission's variance_reduced_progress_bound milestone, not attempted here.

Prior art

q=finite sum, q=variance reduction, q=SVRG, q=component function, q=variance reduced gradient, and q=mirror descent finite sum were all searched on 2026-09-18. The only topically-adjacent hit across all six queries is ShiOptRates.Stochastic.variance_purchase_ classical ("Classical variance reduction is cost-neutral..."), which models plain minibatch SGD on a smooth objective with an i.i.d.-noise oracle characterized by a single scalar variance $\hat\sigma^2$ and a minibatch-size trade-off — no finite-sum structure with $m$ named component functions, no sampling distribution $\{q_i\}$, no snapshot/anchor point $\tilde x$, and a different question (cost-neutrality of minibatch size vs. this mission's convergence rate for a fixed variance-reduction scheme). Not reused; every item in this mission is drafted fresh.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 5, §5.3. https://doi.org/10.1007/978-3-030-39568-1
• R. Johnson, T. Zhang, "Accelerating stochastic gradient descent using predictive variance reduction," Advances in Neural Information Processing Systems (NeurIPS), 2013 (the SVRG estimator this section's gradient estimator generalizes to the composite mirror-descent setting).
• 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.

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

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

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

A recurring question in economics and operations research is: when a decision problem depends on a parameter, does the optimal decision move monotonically as the parameter changes? A firm's optimal input mix as a price rises, a consumer's optimal consumption bundle as income grows, a Cournot firm's optimal output as a rival's output changes — in each case one wants "more of the parameter implies (weakly) more of the optimum" without assuming convexity, differentiability, or a unique optimizer. The classical tool for such comparative statics questions is the implicit function theorem, which needs smoothness and a nondegenerate Hessian and breaks down the moment the optimum is not unique or the objective is not differentiable. Topkis [1978] showed that a purely order-theoretic condition — supermodularity of the objective jointly in the decision variable and the parameter — is sufficient on its own, with no smoothness, uniqueness, or convexity assumed at all, and Milgrom and Roberts [1990a, 1994] later showed this lattice-theoretic approach subsumes and strengthens the classical monotone-comparative-statics results in economics. This mission formalizes the two central results this book calls "Topkis's theorem" (Theorem 2.8.1 and Theorem 2.8.2), together with the structural fact about maximizers of a supermodular function (Theorem 2.7.1) that both rest on, and the strengthening to strictly ordered optimal selections (Theorem 2.8.4).

Setting

Let $X$ be a lattice: a partially ordered set $(X, \preceq)$ in which every pair $x, x'$ has a join $x \vee x'$ and a meet $x \wedge x'$. A real-valued function $f : X \to \mathbb{R}$ is supermodular on $X$ if $f(x') + f(x'') \le f(x' \vee x'') + f(x' \wedge x'')$ for all $x', x'' \in X$; this is the same relativized notion (SupermodularOn) used, with $S = X$, throughout chunk I of this series.

Now let $T$ also be a partially ordered set (the parameter set), and let $f : X \times T \to \mathbb{R}$ be a real-valued function of the pair $(x, t)$. $f$ has increasing differences in $(x, t)$ if, for every $t' \prec t''$ in $T$, the map $x \mapsto f(x, t'') - f(x, t')$ is monotone (order-preserving) in $x$; equivalently, the marginal gain from raising $t$ is itself increasing in $x$. Replacing "monotone" with "strictly monotone" gives strictly increasing differences. To compare the resulting sets of optimizers rather than single points, this mission reuses the induced set ordering $\sqsubseteq$ from chunk I: for $A, B \subseteq X$, $A \sqsubseteq B$ holds when $a \wedge b \in A$ and $a \vee b \in B$ for all $a \in A$, $b \in B$.

Formalization targets

Goal — Theorem 2.8.2 (Topkis's theorem)

Let $X$ and $T$ be lattices, let $S$ be a sublattice of the product lattice $X \times T$, and let $S_t = \{x \in X : (x, t) \in S\}$ be the section of $S$ at $t \in T$. If $f : X \times T \to \mathbb{R}$ is supermodular on $S$ (jointly in the pair $(x, t)$), then

$$t \;\longmapsto\; \operatorname{argmax}_{x \in S_t} f(x, t)$$

is increasing in $t$, with respect to $\sqsubseteq$, on $\{t \in T : \operatorname{argmax}_{x \in S_t} f(x, t) \neq \emptyset\}$.

Theorem 2.8.1 (the underlying, more elementary sufficient condition)

With $S_t \subseteq X$ increasing in $t$ (with respect to $\sqsubseteq$), $f(x,t)$ supermodular in $x$ for each fixed $t$, and $f(x,t)$ having increasing differences in $(x,t)$ on $X \times T$, the same conclusion — $t \mapsto \operatorname{argmax}_{x \in S_t} f(x,t)$ increasing in $\sqsubseteq$ — holds. Theorem 2.8.2's joint-supermodularity hypothesis on a sublattice of $X \times T$ automatically forces both of Theorem 2.8.1's hypotheses, so 2.8.1 is the logically weaker, more elementary statement from which 2.8.2's proof proceeds.

Theorem 2.8.4 (strict strengthening)

Under the hypotheses of Theorem 2.8.1 but with strictly increasing differences, every individual optimal solution at a larger parameter value dominates every individual optimal solution at a smaller one: $t' \prec t''$, $x' \in \operatorname{argmax}_{x \in S_{t'}} f(x,t')$, and $x'' \in \operatorname{argmax}_{x \in S_{t''}} f(x,t'')$ together force $x' \preceq x''$ — a genuinely stronger conclusion than $\sqsubseteq$ alone gives.

A supporting result is formalized as a milestone because both goals' proofs use it directly: Theorem 2.7.1, that $\operatorname{argmax}_{x \in X} f(x)$ is a sublattice of $X$ whenever $f$ is supermodular on $X$ — the structural fact that makes it meaningful to compare optimal-solution sets with $\sqsubseteq$ in the first place.

Significance

The result itself. Theorem 2.8.2 is the book's own headline theorem, cited throughout the rest of the monograph: it underlies the assortative-matching existence theorem (Chapter 3), monotone optimal policies in Markov decision processes (Chapter 3), and equilibrium comparative statics in supermodular games (Chapter 4) — each a later mission in this series. Its distinguishing feature relative to the implicit function theorem is that it needs no differentiability, no uniqueness of the optimizer, and no interiority: it applies equally to discrete decision problems (integer programming, combinatorial selection) and continuous ones.

Formalizing it. Nothing in Mathlib currently states a parametric monotone-comparative- statics result of this shape: the closest neighboring material (order-preserving maps, MonotoneOn, lattice structures) supplies only the vocabulary, not the theorem. This mission is the first formalization of Topkis's theorem on this platform and introduces the increasing-differences vocabulary (IncreasingDifferencesOn, StrictlyIncreasingDifferencesOn) that later missions in this series (matching, MDPs, supermodular games) reuse directly.

Difficulty

The natural first idea — differentiate $f$ in $x$, set the gradient to zero, and use the implicit function theorem on the resulting first-order condition — fails immediately because nothing here is assumed differentiable, and $\operatorname{argmax}_{x \in S_t} f(x,t)$ need not be a single point. The correct argument instead compares two arbitrary elements $x' \in S_{t'}$, $x'' \in S_{t''}$ directly through the supermodularity inequality applied to the pair $(x', t')$ against $(x' \vee x'', t')$ (a chain of inequalities Topkis calls "Lemma 2.8.1"), using increasing differences only to move the parameter from $t'$ to $t''$ inside that chain — at no point is a derivative, a selection function, or an interior point used. A second subtlety is that "increasing" in the conclusion is with respect to the induced set order $\sqsubseteq$, not a claim that some selection $t \mapsto x(t)$ is monotone: proving the stronger, pointwise-ordered conclusion (Theorem 2.8.4) genuinely needs the strict form of increasing differences, not merely increasing differences plus an extra hypothesis.

Formalization scope

$X$ and $T$ are kept as abstract Lattice/PartialOrder types throughout, matching the book's own generality — Theorem 2.8.1's and 2.8.2's $\mathbb{R}^n$/$\mathbb{R}^m$ corollary via second partial derivatives (discussed in the book's prose immediately after Theorem 2.8.2, p. 77) is not itself a numbered theorem and is not formalized here. Supermodularity, increasing differences, and strictly increasing differences are each formalized as a single relativized definition (SupermodularOn f S, IncreasingDifferencesOn f S, StrictlyIncreasingDifferencesOn f S) so the same declaration expresses both "supermodular on the whole lattice $X$" (used by Theorem 2.7.1 and Theorem 2.8.1's per-$t$ hypothesis) and "jointly supermodular on a sublattice $S$ of $X \times T$" (Theorem 2.8.2) — a formalization that instead only ever supermodularized $f(\cdot, t)$ for fixed $t$ would collapse Theorem 2.8.2's genuinely joint hypothesis into a restatement of Theorem 2.8.1, which is exactly the trivialization this mission's chunk brief warns against. $\operatorname{argmax}_{x \in S_t} f(x,t)$ is written out as the set of $x \in S_t$ that dominate every other element of $S_t$ under $f(\cdot, t)$, and every conclusion is stated only for pairs $t \preceq t'$ at which both argmax sets are assumed nonempty — matching the book's own restriction to $\{t \in T : \operatorname{argmax}_{x \in S_t} f(x,t) \neq \emptyset\}$, since $\sqsubseteq$ holds vacuously whenever either side is empty. This mission depends on chunk I's InducedSetOrder; it introduces no reusable infrastructure beyond its own three definitions, which later missions in the series (matching, MDPs, supermodular games) are expected to import directly rather than redefine.

Selected references

• Topkis, D. M., Minimizing a submodular function on a lattice, Operations Research 26(2), 1978, pp. 305–321. https://doi.org/10.1287/opre.26.2.305
• Topkis, D. M., Supermodularity and Complementarity, Princeton University Press, 2011 (DOI 10.1515/9781400822539), Chapter 2, §2.6–2.8.
• Milgrom, P. and Shannon, C., Monotone comparative statics, Econometrica 62(1), 1994, pp. 157–180. https://doi.org/10.2307/2951479
• Milgrom, P. and Roberts, J., Rationalizability, learning, and equilibrium in games with strategic complementarities, Econometrica 58(6), 1990, pp. 1255–1277. https://doi.org/10.2307/2938316

Motivation

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

Setting

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

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

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

Formalization targets

Goal — Lemma 8.4

$$\max_{y' \in \Delta_m} \bar{x}^{\mathsf T} A y' \;\le\; \lambda_R(A) + \frac{\sqrt{2 \log n}}{\sqrt{T}}$$

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

Supporting milestone — Eq. (8.1)

$$\sum_{t=0}^{T-1} x_t^{\mathsf T} A y_t \;\le\; \min_{x' \in \Delta_n} \sum_{t=0}^{T-1} (x')^{\mathsf T} A y_t \;+\; \sqrt{2T \log n}$$

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

Infinite-horizon dynamic programming is the mathematical core of Markov decision processes and reinforcement learning: Bellman equations, value iteration, policy iteration, and their guarantees. Chapter 7 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) develops the finite-state theory in its cleanest generality — stochastic shortest path (SSP) problems first (Prop. 7.2.1–7.2.2), with discounted problems (Prop. 7.3.1) and average-cost problems (Prop. 7.4.1–7.4.2) derived from the SSP analysis. These propositions are cited throughout the MDP/RL literature as the base case of the theory; none of them exists in Mathlib.

Setting

States $1, \dots, n$ plus an implicit cost-free absorbing termination state $t$; finite nonempty control sets $U(i)$; costs $g(i,u)$; sub-stochastic transitions $p_{ij}(u) \ge 0$, $\sum_j p_{ij}(u) \le 1$, the deficit being the termination probability (BertsekasSSPModel). Operators

$$(T_\mu J)(i) = g(i,\mu(i)) + \sum_j p_{ij}(\mu(i)) J(j), \qquad (TJ)(i) = \min_{u \in U(i)}\Big[g(i,u) + \sum_j p_{ij}(u) J(j)\Big]$$

(BertsekasSSPPolicyOp, BertsekasSSPBellmanOp), $N$-stage costs by backward recursion with policy shift (BertsekasSSPNCost), and the survival mass $P\{x_m \ne t\}$ (BertsekasSSPSurvival). Assumption 7.2.1: for some $m > 0$, every admissible policy has survival mass $< 1$ from every state after $m$ stages. The discounted setting reuses the same model with stochastic rows and $0 < \alpha < 1$ (BertsekasDiscounted*); the average-cost setting adds a designated state $s$ with the avoidance probability of Assumption 7.4.1 (BertsekasSSPAvoidProb).

Target

Under Assumption 7.2.1, there is a vector $J^*$ with

$$T^k J_0 \to J^* \ \ \forall J_0, \qquad J^* = T J^* \text{ uniquely}, \qquad J^*(i) \le J_\pi(i) = \lim_N J^N_\pi(i) \ \ \forall \pi \text{ admissible},$$

and a stationary policy attaining $J^*$ — BertsekasDP.ssp_main_theorem (goal, Prop. 7.2.1(a),(b)). Milestones: 7.2.1(c) policy evaluation, 7.2.1(d) optimality iff greediness, 7.2.2 policy iteration, 7.3.1 the full discounted counterpart, 7.4.1 the average-cost Bellman equation, 7.4.2 average-cost policy iteration.

Significance

These are the convergence guarantees behind value iteration and policy iteration — the two algorithms at the root of dynamic programming practice and of RL analyses (Q-learning's target operator is exactly $T$). The SSP form is the strongest of the three: the discounted theory is its special case (termination with probability $1 - \alpha$ per stage) and the average-cost theory reduces to it through cycles at the recurrent state. Formalized, the chapter yields a reusable finite-MDP theory: monotone operators, $m$-stage contractions, and the machinery for later Vol. II material. All results are proved in the book; the formalization is new.

Difficulty

$T$ is not a one-stage contraction in the sup-norm under Assumption 7.2.1 — only an $m$-stage contraction, uniformly over the finitely many $m$-stage policy prefixes; extracting the uniform contraction factor $\rho < 1$ (via finiteness of the policy space) is the crux of the whole chapter. The limit of $N$-stage costs for nonstationary policies must be established, not assumed (tail-sum estimate $\rho^{\lfloor N/m \rfloor}$). For the average-cost results the associated-SSP construction (stop on reaching $s$) must be built inside the proof. The liminf phrasing of average-cost optimality is deliberate: for arbitrary nonstationary policies the Cesàro limit need not exist.

Formalization scope

Finite states Fin n, finite control type, constraint sets as Finsets with attained minima; no termination state in the carrier — termination is the sub-stochastic deficit, exactly as the book treats it computationally. Policies are sequences of stage policies (Markov); costs of nonstationary policies via the shift recursion. Convergence is Tendsto in the product topology (equivalently sup-norm, $n$ finite). Average cost uses real liminf and division with the $N = 0$ term junk-valued at 0 (irrelevant at infinity). The discounted theorem packages parts (a)–(e) in one statement mirroring Prop. 7.3.1.

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§7.1–7.4.) http://www.athenasc.com/dpbook.html
• D. P. Bertsekas, J. N. Tsitsiklis, An analysis of stochastic shortest path problems, Math. Oper. Res. 16 (1991), 580–595. https://doi.org/10.1287/moor.16.3.580
• M. L. Puterman, Markov Decision Processes, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Linear approximation is only one instance of distance minimization. Feasible sets in optimization are typically convex rather than subspaces, so a useful certificate must compare a target point with an entire convex set and must allow an affine offset. Chapter 5 of Luenberger's Optimization by Vector Space Methods builds this certificate through geometric forms of the Hahn--Banach theorem, supporting hyperplanes, and separation of convex sets. The resulting minimum-distance theorem expresses the distance from a point to a convex set as an optimal gap measured by a norm-bounded continuous linear functional (Luenberger, §§5.12--5.13, pp. 130--137).

This mission advances the series from subspace annihilators to affine separation. It formalizes the Minkowski gauge used by the chapter, three progressively stronger separation statements, and a capstone distance-duality certificate. These results are standard infrastructure for constrained optimization: they turn a geometric exclusion or distance into a scalar inequality that can later become a multiplier or a dual bound.

Setting

Let $X$ be a real normed space and $K\subseteq X$ a nonempty convex set. Convexity is represented by Convex ℝ K, and topological interior, closure, and infimum distance use Mathlib's interior, closure, and Metric.infDist. A continuous affine separator is described by a continuous linear functional $f:X\toL[\mathbb R]\mathbb R$ and a scalar level $c$. The inequality $f(k)\le c$ for all $k\in K$ places $K$ in one closed half-space.

When a convex set contains zero in its interior, its Minkowski gauge is the functional gauge K. The source characterizes it by nonnegativity, positive homogeneity, subadditivity, continuity, and the level sets

$$\{x:g_K(x)\le 1\}=\overline K, \qquad \{x:g_K(x)<1\}=\operatorname{int}K.$$

These properties are bundled into the first milestone, following Lemma 1 of §5.12 (pp. 131--132).

For two convex sets $K_1,K_2$, Eidelheit separation means finding nonzero $f$ and $c$ with $f(x)\le c\le f(y)$ for $x\in K_1$ and $y\in K_2$. The source assumes that $K_1$ has nonempty interior and that its interior does not meet $K_2$. The Lean statement records the nonemptiness of $K_2$ explicitly, since otherwise nonzero separation is not forced.

Formalization targets

Gauge and geometric Hahn--Banach milestones

Formalize the six gauge properties above. Then, for a convex $K$ with nonempty interior and an affine subspace $V$ disjoint from that interior, produce $f\ne0$ and $c$ such that

$$f(v)=c\quad(v\in V), \qquad f(k)<c\quad(k\in\operatorname{int}K).$$

This is Mazur's geometric Hahn--Banach theorem as stated in §5.12, Theorem 1 (p. 133).

Supporting hyperplanes and convex-set separation

For $x\notin\operatorname{int}K$, formalize a nonzero functional satisfying $f(k)\le f(x)$ for all $k\in K$. Next formalize Eidelheit separation:

$$f(x)\le c\le f(y) \quad\text{for all }x\in K_1,\ y\in K_2.$$

These are Theorems 2 and 3 of §5.12 (pp. 133--134).

Convex minimum-distance duality

Let $x_1$ have positive distance $d$ from $K$. Produce $f$ and a real upper-bound level $c$ with $\|f\|\le1$, $f(k)\le c$ on $K$, and

$$f(x_1)-c=d.$$

Every other feasible pair $(g,b)$ must satisfy $g(x_1)-b\le d$. If $x_0\in K$ realizes the distance, require $-f$ to align with $x_0-x_1$. This is the finite real certificate form of §5.13, Theorem 1 (pp. 136--137).

Significance

The capstone is an exact strong-duality statement for distance to a convex set. A feasible pair $(g,b)$ yields a certified lower bound on the distance, and the distinguished pair reaches the primal value. Unlike a nearest-point characterization, it remains meaningful when $K$ is not closed and no minimizing point exists. The conditional alignment clause identifies the equality case when attainment is available.

Formalizing the chapter's progression creates more than one isolated equality. The gauge package links convex geometry to sublinear analysis; Mazur separation handles affine constraints; the supporting-hyperplane and Eidelheit statements provide reusable interfaces for later multiplier rules. The results are known and proved in the 1969 text; the mission's contribution is a coherent machine-checked Lean layer that preserves the source hypotheses and can support later chapters on duality and optimization.

Difficulty

A direct reuse of subspace distance duality is insufficient because a general convex set is neither closed under subtraction nor described by an annihilator. An affine level $c$ is unavoidable. The common shorthand $\sup_{k\in K} f(k)$ introduces a second problem: $K$ need not be bounded, so a real-valued supremum is not available for an arbitrary functional. The capstone therefore quantifies over a real upper bound $c$ and asserts its optimality through a universal inequality; this records the same finite support value without imposing boundedness absent from the source.

Topological hypotheses also differ across the milestones. Separation uses nonempty interior, whereas the final distance theorem only assumes convexity, nonemptiness, and positive distance. Replacing positive distance by mere exclusion $x_1\notin K$ would be invalid for a nonclosed set. Similarly, requiring closure or compactness would make formalization easier but would lose the theorem's intended infinite-dimensional scope.

Formalization scope

The mission is restricted to real normed spaces. Sets use Set X; affine varieties use AffineSubspace ℝ X; separators use ContinuousLinearMap. The gauge is Mathlib's existing gauge, so no competing definition is introduced. The bundled gauge milestone deliberately includes both level-set identities as well as continuity, positive homogeneity for positive real scalars, subadditivity, and nonnegativity.

The Eidelheit theorem includes K₂.Nonempty, an assumption used implicitly by the source's separating conclusion. The capstone includes K.Nonempty and 0 < Metric.infDist x₁ K; it does not assume closedness, boundedness, compactness, or attainment. Its pair $(f,c)$ represents a finite support level, and the universal comparison over all feasible $(g,b)$ rules out a weakened statement in which an arbitrarily loose upper bound could trivialize existence. The optional nearest-point clause uses the exact equality $\|x_0-x_1\|=d$ and fixes the sign of alignment. Contributions may add reusable lemmas on gauges, interiors, affine subspaces, or support bounds, but the public results should remain independent of finite-dimensionality and completeness.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, Chapter 5, §§5.11--5.13, pp. 127--137. Public scan.

Every full-dimensional convex body is sandwiched between an ellipsoid and its $n$-fold dilation: shrinking the minimum-volume covering (Löwner–John) ellipsoid $\mathcal{E}$ about its centre $x_0$ by the factor $1/n$ lands inside the body,

$$x_0 + \tfrac{1}{n}\,(\mathcal{E} - x_0) \;\subseteq\; C \;\subseteq\; \mathcal{E},$$

and the factor $n$ is tight on simplices. This rounding theorem underlies the ellipsoid method, John's theorem on the Banach–Mazur distance to the Euclidean ball, and much of modern convex geometry. The mission formalizes §8.4 of Boyd & Vandenberghe for polytopes $C = \operatorname{conv}\{x_1,\dots,x_m\}$, exactly as the book proves it: existence and uniqueness of the extremal ellipsoid, the KKT identities at the normalized optimum ($\sum_i \lambda_i x_i x_i^{T} = I$, $\sum_i \lambda_i x_i = 0$, $\sum_i \lambda_i = n$), the convex-combination step that produces the $1/n$ ball, and affine invariance.

Interior point methods solve linear programs by moving through the interior of the feasible set instead of along its edges — the approach that turned Karmarkar's 1984 breakthrough into today's practical large-scale solvers. This mission formalizes the primal path following algorithm of Chapter 9 of Bertsimas–Tsitsiklis. For $\mu > 0$ the logarithmic barrier

$$B_\mu(\mathbf{x}) = \mathbf{c}'\mathbf{x} - \mu\sum_{j=1}^n \log x_j$$

replaces the constraint $\mathbf{x} \ge \mathbf{0}$; the minimizers $\mathbf{x}(\mu)$ of $B_\mu$ over $\{A\mathbf{x} = \mathbf{b}\}$ trace the central path, characterized by the KKT conditions (9.17): $A\mathbf{x} = \mathbf{b}$, $\mathbf{x} \ge \mathbf{0}$, $A'\mathbf{p} + \mathbf{s} = \mathbf{c}$, $\mathbf{s} \ge \mathbf{0}$, $XS\mathbf{e} = \mu\mathbf{e}$ (Lemma 9.5). The algorithm follows the path with one Newton step of the barrier problem per shrink $\mu^{k+1} = \alpha\mu^k$, maintaining the proximity invariant

$$\|\frac{1}{\mu}XS\mathbf{e} - \mathbf{e}\| \le \beta$$

. The goal theorem is Theorem 9.7: with $\alpha = 1 - \frac{\sqrt{\beta}-\beta}{\sqrt{\beta}+\sqrt{n}}$ and a $\beta$-close start, after $K = \Big\lceil \frac{\sqrt{\beta}+\sqrt{n}}{\sqrt{\beta}-\beta}\,\log\frac{(\mathbf{s}^0)'\mathbf{x}^0(1+\beta)}{\varepsilon(1-\beta)} \Big\rceil$ iterations the algorithm reaches primal and dual feasible solutions with duality gap $(\mathbf{s}^K)'\mathbf{x}^K \le \varepsilon$ — the explicit form of the celebrated $O(\sqrt{n}\log(1/\varepsilon))$ iteration bound. Alongside it we formalize the generic potential-reduction scheme (Theorem 9.4): any algorithm cutting $G(\mathbf{x},\mathbf{s}) = q\log\mathbf{s}'\mathbf{x} - \sum_j \log x_j - \sum_j \log s_j$ by $\delta$ per step reaches gap $\varepsilon$ within an explicit $K$.