Operations Research

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

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

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

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

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

Setting

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

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

Formalization targets

Goal — Theorem 3.6, closed-form rate

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

Supporting milestones, in attack order

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

Selected references

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

Motivation

Erlang's formula, the subject of mission I of this series, sizes a single telephone link. Real networks are not single links: a call occupies a circuit on every link of its route simultaneously, and it is lost unless every one of those links has a free circuit. That is the loss network, the model of Chapter 3 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014), and it describes not only circuit-switched telephony but any system in which a request must acquire several resources at once or be refused: wavelength assignment in optical networks, radio channel allocation under interference constraints, slot booking, and admission control generally. The term used in those application areas is circuit-switched: before a request is accepted it is checked that enough resource is available for each stage of it.

The exact equilibrium distribution of a loss network is known and has product form. It is also useless for computation — its normalizing constant is a sum over the feasible states, and for a general resource matrix computing it is NP-hard. What practitioners use instead is the Erlang fixed point: pretend the links block independently, so that the traffic offered to link $j$ is the traffic on the routes through it thinned by the blocking probability of every other link on each route, and then apply Erlang's formula link by link. The result is a system of coupled copies of Erlang's formula. The chapter's aim, in its own words, is to give insight into why that approximation works as well as it does; the first step is to show that it is well posed at all.

Setting

The links are $\mathcal{J} = \{1,\dots,J\}$, link $j$ carrying $C_j$ circuits. A route $r$ belongs to a set $\mathcal{R}$ of $R$ routes, and the link-route incidence matrix $A$ records how much of each link a route needs: a call on route $r$ requires $A_{jr}$ circuits from link $j$ and is lost if any link has fewer than $A_{jr}$ free. (The classical case is $A$ a $0$–$1$ matrix and $A_{jr}=1$ exactly when $j\in r$; from section 3.3 the book allows any non-negative integers.)

Calls requesting route $r$ arrive as a Poisson process of rate $\nu_r$, independently across routes, and hold their circuits for an exponentially distributed time of unit mean. Writing $n_r$ for the number of calls in progress on route $r$, the process $n=(n_r)$ is Markov on

and is called a loss network with fixed routing.

Write $E(\nu,C)$ for Erlang's formula, $E(\nu,C)=\dfrac{\nu^{C}/C!}{\sum_{j=0}^{C}\nu^{j}/j!}$, published in mission I of this series. The Erlang fixed point equations are

The factor $(1-E_j)^{-1}$ removes link $j$'s own thinning from the product, so in the $0$–$1$ case the argument is $\sum_{r\ni j}\nu_r\prod_{i\in r\setminus\{j\}}(1-E_i)$, the reduced load offered to link $j$.

Formalization targets

Goal — Theorem 3.20, existence and uniqueness of the Erlang fixed point

The goal fixes no formula for $E$ and no rate of convergence: it asserts only that the approximation the field has used since the 1960s names a single, well-defined object. Existence alone is a short argument from Brouwer's theorem, since (3.7) defines a continuous self-map of the compact convex cube $[0,1]^J$; uniqueness is the substance.

Supporting levels

The exact theory that the fixed point approximates: Lemma 3.4 on truncating a reversible process; the uncapacitated network as an instance of the open migration product form of mission II; equation (3.3), the exact equilibrium distribution $\pi(n)=G(C)\prod_r \nu_r^{n_r}/n_r!$ on $S(C)$; and the acceptance probability $1-L_r=G(C)/G(C-Ae_r)$. Then the optimization side: that $E(\nu,C)$ and the utilization $\nu(1-E(\nu,C))$ are strictly increasing in $\nu$, which is what makes the revised dual objective strictly convex; and Theorem 3.10, that a minimizer of the Dual problem (3.5) over the positive orthant satisfies the conditions on $B$, equation (3.6).

Significance

The result itself. Without Theorem 3.20 the phrase "the Erlang fixed point" is not well formed, and neither is any engineering procedure that computes one — repeated substitution converges to a solution, and damped iteration is guaranteed to converge to one, but "the blocking probabilities predicted by the reduced-load approximation" names a unique vector only because of this theorem. The proof is also the interesting part: the fixed point equations are re-read as the stationary conditions of a strictly convex minimization, the revised dual (3.8), which is the Dual problem (3.5) of the maximum-probability analysis with its linear term replaced by $\int_0^{y_j}U(z,C_j)\,dz$. That connection is what later lets the book prove the approximation asymptotically exact in a limiting regime: Corollary 3.22 says the Erlang fixed point converges to the vector $B$ coming from the maximum-probability problem.

Formalizing it. Nothing here is open. What the mission produces is the loss network model in Lean — state space, truncated rates, normalizing constant, incidence matrix — and a machine-checked statement of the object the reduced-load approximation computes. It is also where this series' earlier missions pay off: the uncapacitated network is literally the open migration process of mission II with $\lambda\equiv 0$, $\mu\equiv 1$, $\varphi_j(n)=n$, and the exact distribution (3.3) is its truncation by Lemma 3.4 to the feasible set, using the DetailedBalance layer of mission I. Mathlib has no loss network theory and no Erlang formula beyond what mission I published.

Difficulty

Existence of a fixed point is easy and is not where the difficulty lies. Uniqueness resists every direct attack: the map defined by (3.7) is not a contraction in any obvious metric, its monotonicity structure is not the kind that forces a unique fixed point, and iterating it undamped can cycle. The book's route is indirect — exhibit a strictly convex function whose stationary conditions are exactly (3.7) — and finding that function is the whole content. Its strict convexity comes from a monotonicity fact about Erlang's formula, that the utilization $\nu\bigl(1-E(\nu,C)\bigr)$ is strictly increasing in $\nu$, which is itself a milestone here.

A second, formal difficulty: the equations involve $(1-E_j)^{-1}$, so a solution with $E_j=1$ would be meaningless. It is worth checking before starting that no such solution exists for $C_j\ge 1$, rather than assuming it.

Formalization scope

Routes and links are indexed by finite types, the incidence matrix has natural-number entries (the general case of section 3.3, not only $0$–$1$), capacities are natural numbers, and arrival rates are positive reals. The feasible set $S(C)$ is a subset of the state space, and a truncated process is the rate matrix restricted to that subset — which is exactly the book's truncation, since a transition leaving the set simply has no target.

Conventions: holding times have unit mean throughout, matching the book, so the departure rate from route $r$ is $n_r$ and no separate service-rate parameter appears. Normalizing constants are introduced through summability hypotheses that assert convergence and the value together, rather than as possibly-infinite quantities; $G(C)$ is the reciprocal of the sum in the book's notation. Capacities are assumed at least $1$ in the goal: a link with no circuits blocks everything, $E(\nu,0)=1$ identically, and the factor $(1-E_j)^{-1}$ would then be undefined rather than merely large.

The goal cannot be satisfied trivially: it is a uniqueness statement, so a vacuous or degenerate reading would have to produce no solution, and existence is half of what is asserted.

Contributions welcome beyond the listed items: the Brouwer argument for existence of a solution to the $0$–$1$ equations (3.1) of section 3.2; the utilization function $U(y,C)$ and the revised dual (3.8); the central limit theorem 3.14 and Corollary 3.17; Lemma 3.21 and Corollary 3.22 on the limiting regime; and the diverse-routing models of section 3.7.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 3 (pp. 49–82); Lemma 3.4, equation (3.3), Theorems 3.10 and 3.20, equations (3.1), (3.5)–(3.9). DOI 10.1017/cbo9781139565363
• F. P. Kelly, Loss networks, Annals of Applied Probability 1 (1991), 319–378. DOI 10.1214/aoap/1177005872
• F. P. Kelly, Blocking probabilities in large circuit-switched networks, Advances in Applied Probability 18 (1986), 473–505. DOI 10.2307/1427303
• R. B. Cooper and S. Katz, Analysis of alternate routing networks with account taken of the nonrandomness of overflow traffic, Bell Telephone Laboratories memorandum, 1964.
• Frank Kelly, Reversibility and Stochastic Networks, Cambridge University Press, 2011 (reissue of the 1979 edition), Chapter 1 on truncation.

Motivation

Existence of equilibrium is the first question any model of strategic interaction must answer, and the classical answer — Nash's theorem via Kakutani's fixed point theorem — asks for a convex, compact strategy space and continuous payoffs. Many of the models economists actually use do not have that: a firm's technology set can be discrete or irregular, and a payoff need only be upper semicontinuous, not continuous. Topkis [1979] showed that when a game's structure is instead order-theoretic — each player's strategies form a lattice, and the players' incentives reinforce each other in a precise sense — an equilibrium exists without any convexity or continuity assumption at all, and the proof method delivers something Kakutani's theorem cannot: a greatest and a least equilibrium point, with the whole equilibrium set forming a complete lattice. Zhou [1994] later showed the completeness of the equilibrium lattice in full generality; this mission formalizes the resulting theorem (Topkis's Theorem 4.2.1) together with its parametric extension (Theorem 4.2.2, established independently by Milgrom and Roberts [1990a] and Sobel [1988]), which shows how the greatest and least equilibria move as a parameter of the game — its technology, its cost structure — changes. This machinery underlies monotone comparative statics for games throughout economics: oligopoly models with strategic complements, coordination games, and search and matching models with increasing returns.

Setting

A noncooperative game $(N, S, \{f_i : i \in N\})$ consists of a finite player set $N$, a set $S \subseteq \mathbb{R}^m$ of feasible joint strategies $x = (x_i)_{i \in N}$ (allowing the set of strategies feasible for one player to depend on the others' choices, so $S$ need not be a product set), and a payoff function $f_i$ for each player $i$. Write $x_{-i}$ for the strategies of every player but $i$, $S_i(x_{-i})$ for the section of $S$ at $x_{-i}$ — player $i$'s feasible strategies given the others' choice — and $Y_i(x_{-i}) = \operatorname{argmax}_{y_i \in S_i(x_{-i})} f_i(y_i, x_{-i})$ for player $i$'s best-response set. The best joint response correspondence is $Y(x) = \prod_{i \in N} Y_i(x_{-i})$. A feasible $x'$ is an equilibrium point if $f_i(y_i, x'_{-i}) \le f_i(x')$ for every player $i$ and every feasible deviation $y_i \in S_i(x'_{-i})$ — no player can unilaterally improve.

A lattice is a partially ordered set in which every pair of elements has a join $\vee$ and a meet $\wedge$. A function $g$ is supermodular on a subset if $g(x) + g(y) \le g(x \vee y) + g(x \wedge y)$ for all $x, y$ in it, and has increasing differences in two of its arguments $(y,t)$ if $y \mapsto g(y, t'') - g(y, t')$ is monotone whenever $t' \prec t''$. A game $(N, S, \{f_i\})$ is a supermodular game if $S$ is a sublattice, $f_i(y_i, x_{-i})$ is supermodular in $y_i$ for every fixed $x_{-i}$ and every $i$, and $f_i(y_i, x_{-i})$ has increasing differences in $(y_i, x_{-i})$ for every $i$ — jointly, the conditions under which each player's own strategy components are complements and complementary to the other players' strategies (Theorem 2.6.1 of chunk 01-lattices/02-monotonicity's book).

Formalization targets

Goal — Theorem 4.2.1

If $(N, S, \{f_i\})$ is a supermodular game, $S$ is nonempty and compact, and each $f_i(y_i, x_{-i})$ is upper semicontinuous in $y_i$ on $S_i(x_{-i})$ for every $x_{-i}$ and every $i$, then

is nonempty, has a greatest and a least element, and, under the order it inherits from $\mathbb{R}^m$, is itself a nonempty complete lattice.

Theorem 4.2.2 (the parametric extension)

Let $T$ be a partially ordered set and, for each $t \in T$, $(N, S^t, \{f_i^t\})$ a supermodular game with $S^t$ nonempty, compact, and increasing in $t$; suppose each $f_i^t(y_i, x_{-i})$ is upper semicontinuous in $y_i$ and has increasing differences in $(y_i, t)$. Then for every $t$ there exist a greatest and a least equilibrium point of game $t$, and both are increasing functions of $t$ on $T$ — the equilibrium set moves monotonically as the parameter increases.

Two supporting results are formalized as milestones because Theorem 4.2.1's own proof uses them directly: Lemma 4.2.1 (equilibrium points are exactly the fixed points of the best joint response correspondence) and Lemma 4.2.2, parts (b) and (f) (the best joint response set is a nonempty compact sublattice for every feasible $x$, and the correspondence is increasing in $x$).

Significance

The result itself. Theorem 4.2.1 is the lattice-theoretic alternative to Nash/Kakutani existence: it needs no convexity of $S$ and no continuity of $f_i$ (upper semicontinuity suffices), and in exchange it delivers a greatest and a least equilibrium — with an explicit order-theoretic characterization via Theorem 2.5.1 of chunk 01-lattices — and the guarantee that the entire equilibrium set is a complete lattice, not merely nonempty. Theorem 4.2.2 gives this existence result teeth for applied comparative statics: it says that if a firm's cost structure, a market's demand parameter, or any other feature of the game increases (in the sense of the induced set order on $S^t$ and increasing differences in the payoffs), the extremal equilibria increase too — the qualitative content behind results such as "more competition leads to lower prices" in supermodular oligopoly models.

Formalizing it. The platform's existing Nash-equilibrium theorem (AGT.nash_existence, Theorem 1.8 of Algorithmic Game Theory) is a Brouwer/Kakutani argument for finite games with mixed strategies: it needs finiteness of every player's strategy set (so that mixed strategies form a compact convex simplex) and gives no lattice structure on the equilibrium set at all. Theorem 4.2.1 is a different technique entirely — it needs no finiteness, no mixing, and no convexity, and its conclusion (a complete lattice of equilibria) is exactly the content Brouwer/Kakutani cannot give. This mission is therefore not a restatement of Nash's theorem in different notation, but a second, independent existence technique with a strictly different structural payoff, formalized here for the first time on the platform. It builds directly on chunk 01-lattices's Theorem 2.5.1 (Zhou's fixed point theorem for increasing correspondences) and chunk 02-monotonicity's supermodularity/increasing differences definitions, both formalized earlier in this series.

Difficulty

The natural first idea for existence — "the best joint response correspondence has a fixed point by some general fixed-point theorem for correspondences" — needs the correspondence to be convex-valued and upper hemicontinuous for a Kakutani argument, neither of which supermodularity or upper semicontinuity alone supply: a best-response set under only upper semicontinuity can be a disconnected, non-convex set (e.g. the maximizers of a supermodular but non-quasiconcave function). The actual route goes through order instead of topology: Lemma 4.2.2 shows the best joint response set is a compact sublattice (hence subcomplete, by Theorem 2.3.1) and that the correspondence is increasing under the induced set order, which is exactly the hypothesis Theorem 2.5.1's non-constructive supremum/infimum construction needs — no convexity anywhere. A second subtlety, which the mission is careful not to elide: the equilibrium set of a supermodular game need be neither compact nor a sublattice of $\mathbb{R}^m$ when there are more than one player (Topkis's Examples 4.2.1 and 4.2.2 exhibit both failures); only the weaker claim — a complete lattice under the inherited order — is true in general, and that is what Theorem 2.5.1(b) supplies.

Formalization scope

A joint strategy is represented as a dependent function ∀ i, Fin (m i) → ℝ over a finite player type ι, with a player's own strategy accessed and overwritten via Function.update, so that $x_{-i}$ is never reified as a separate object — every statement about $f_i(y_i, x_{-i})$ or membership in $S_i(x_{-i})$ substitutes y for x's own i-th coordinate directly. IsSupermodularGame reuses chunk 02-monotonicity's SupermodularOn and IncreasingDifferencesOn verbatim, applied to each player's own payoff, rather than restating the supermodularity/increasing- differences conditions from scratch — a formalization that inlined a weaker, ad hoc notion here (e.g. supermodularity of the joint payoff vector rather than each player's own payoff in their own strategy) would trivialize the connection to chunk 02-monotonicity's theorems that the book's own proof relies on. Theorem 4.2.1's "nonempty complete lattice" conclusion is formalized, as in chunk 01-lattices, via IsLUB/IsGLB on the subtype of equilibrium points — never as membership of the ambient $\mathbb{R}^m$ supremum/infimum in the equilibrium set, which the book's own Examples 4.2.1–4.2.2 refute; a solution that instead proved the equilibrium set compact or a sublattice of $\mathbb{R}^m$ would be proving a strictly stronger and false claim. Only parts (b) and (f) of Lemma 4.2.2 are formalized, since those are the only two of its eight parts the proof of Theorem 4.2.1 uses; a complete development still needs chunk 01-lattices's Theorem 2.3.1 (subcomplete iff compact) and Theorem 2.5.1/2.5.2, and chunk 02-monotonicity's Theorem 2.8.1 and Corollary 2.7.1, none of which are restated here.

Selected references

• Topkis, D. M., Equilibrium points in nonzero-sum n-person submodular games, SIAM Journal on Control and Optimization 17(6), 1979, pp. 773–787. https://doi.org/10.1137/0317054
• Zhou, L., The set of Nash equilibria of a supermodular game is a complete lattice, Games and Economic Behavior 7(2), 1994, pp. 295–300. https://doi.org/10.1006/game.1994.1051
• 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
• Sobel, M. J., Isotone comparative statics for supermodular games, unpublished manuscript, 1988 (cited by Topkis [2011], Theorem 4.2.2).
• Topkis, D. M., Supermodularity and Complementarity, Princeton University Press, 2011 (DOI 10.1515/9781400822539), Chapter 4, §4.1–4.2.

Motivation

The separation theorem — certainty equivalence for linear-quadratic control with imperfect state information — is one of the celebrated structural results of stochastic control: the optimal controller splits into a least-squares estimator and the deterministic LQR actuator, designed independently. It underlies every LQG autopilot and Kalman-filter-based regulator. Section 5.2 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) proves it from the DP algorithm over information vectors, with Lemma 5.2.1 supplying the key fact that the estimation error is beyond the controller's influence. No formal analogue exists in Mathlib.

Setting

Linear dynamics and measurements

with quadratic cost $\mathbb{E}\big[x_N^\top Q_N x_N + \sum_{k<N}(x_k^\top Q_k x_k + u_k^\top R_k u_k)\big]$, $Q_k \succeq 0$, $R_k \succ 0$. The initial state and the zero-mean disturbances/noises are independent with finite ranges; independence is structural — the sample space is the product of an initial-state coordinate and per-stage noise coordinates (BertsekasLQGModel, BertsekasLQGSample, BertsekasLQGProb). A policy maps the realized measurement history $(z_0,\dots,z_k)$ to $u_k$; the closed-loop process is BertsekasLQGTraj, the expected cost BertsekasLQGCost. The estimator $\mathbb{E}[x_k \mid I_k]$ is an explicit conditional average (BertsekasCondExpVec, BertsekasLQGEstimate); the gains $L_k$ come from the time-varying Riccati recursion (BertsekasLQGRiccati, BertsekasLQGGain).

Target

— BertsekasDP.lqg_certainty_equivalence (goal). Milestone: Lemma 5.2.1 in pointwise form — the error $x_k - \mathbb{E}[x_k \mid I_k]$ is the same under any two policies, outcome by outcome (lqg_estimation_error_policy_independent).

Significance

This is the theorem that justifies designing estimator and controller separately — remove it and the entire LQG methodology loses its warrant. The formalization also yields the first machine-checked instance of the informational decomposition (control-dependent part + policy-independent error) that recurs throughout imperfect-information control. Notably the result needs no Gaussian assumption — only zero mean and independence — and the finite-support model makes that generality exact. The result is classical (Joseph–Tou 1961, Gunckel–Franklin 1963; the book's §5.2); the formal proof is new.

Difficulty

The heart is Lemma 5.2.1: showing the estimation error coincides, sample by sample, with the error of the control-free system — which requires proving that the observation-history σ-events under any policy coincide with those of the control-free system (controls are determined by the history, so they shift observations by a known amount). Then the DP argument over information histories must carry the quadratic decomposition through the backward recursion. Bookkeeping over histories-as-lists is the main formal burden; probability theory stays finite.

Formalization scope

Finite-support randomness (all expectations are finite sums); conditional expectation with the explicit junk value 0 on zero-probability events — the goal's hypothesis is accordingly restricted to outcomes of positive probability. Policies are functions of the measurement list only (equivalent to the book's information vector for deterministic policies, since past controls are recoverable from past measurements). Matrices are time-varying; positive definiteness of $R_k$ makes every matrix inverse in the gains genuine. Measurement noise covariance is not assumed positive definite — the estimator is the abstract conditional expectation, not the Kalman filter (whose recursive form, §5.2.1, would be a natural follow-up mission).

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§5.2, Lemma 5.2.1.) http://www.athenasc.com/dpbook.html
• P. D. Joseph, J. T. Tou, On linear control theory, Trans. AIEE 80 (1961), 193–196. https://doi.org/10.1109/TAI.1961.6371743
• T. L. Gunckel, G. F. Franklin, A general solution for linear sampled-data control, J. Basic Eng. 85 (1963), 197–201. https://doi.org/10.1115/1.3656559

Motivation

Label correcting methods are the workhorse family of shortest-path algorithms — Dijkstra's method, Bellman–Ford, SLF/LLL variants and A* all fit the template analyzed in §2.3.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005), where shortest paths appear as the purely deterministic face of dynamic programming. The correctness proof (Prop. 2.3.1) is short on paper but genuinely nondeterministic — any node may be removed from the candidate list, children processed in any order — so a formal proof certifies a whole family of concrete algorithms at once.

Setting

A finite directed graph with arc set $\mathcal{A}$, real arc lengths $a_{ij}$, origin $s$ and destination $t \ne s$ (BertsekasSPGraph). Walks are nonempty node lists whose consecutive pairs are arcs (BertsekasIsWalkFrom), with length the sum of arc lengths (BertsekasWalkLength); the shortest distance is the infimum of walk lengths in the extended reals, $+\infty$ if no walk exists (BertsekasShortestDistance). The standing assumption of §2.3: every cycle has nonnegative length (negative arcs allowed).

The algorithm state (BertsekasLCState) carries labels $d_j \in \overline{\mathbb{R}}$, the scalar UPPER, and the candidate list OPEN. Initially $d_s = 0$, all other labels $\infty$, UPPER $= \infty$, OPEN $= \{s\}$. One iteration (BertsekasLCStep, nondeterministic): remove any $i$ from OPEN; for each child $j$ of $i$ in any order, if $d_i + a_{ij} < \min\{d_j, \text{UPPER}\}$ set $d_j := d_i + a_{ij}$, and put $j$ in OPEN if $j \ne t$, or update UPPER if $j = t$. The algorithm terminates when OPEN is empty.

Target

for every execution, under the nonnegative arc length assumption of §2.3 ($a_{ij} \ge 0$ for every arc) — BertsekasDP.label_correcting_correctness_of_nonneg_arcs (goal). Milestones: termination — no infinite execution exists, which needs only the weaker nonnegative-cycle assumption (label_correcting_terminates) — and the workhorse invariant that every finite label is the length of an actual walk from $s$, which needs neither (label_correcting_invariant).

The nonnegative-arc hypothesis is essential and not a formalization artifact: the algorithm prunes with the test $d_i + a_{ij} < \min\{d_j, \mathrm{UPPER}\}$, and with a negative arc a longer prefix can still reach $t$ more cheaply, so the pruned node is never entered into OPEN. An earlier version of this mission's goal carried only the nonnegative-cycle assumption of §2.1 and was disproved by the counterexample $s=0$, $t=2$, $a_{02}=1$, $a_{01}=2$, $a_{12}=-2$ (a graph with no cycles at all), where the algorithm terminates with $\mathrm{UPPER}=1$ while the shortest distance is $0$. Exercise 2.7 of the source treats the nonnegative-cycle case, which requires a modified algorithm.

Significance

Prop. 2.3.1 certifies simultaneously breadth-first search, Dijkstra (best-first), depth-first and small-label-first variants — every removal discipline is one refinement of the nondeterministic relation. Formally, the development contributes a reusable small-step framework for label-setting/correcting algorithms on which sharper results (Dijkstra's single-pass property, A* admissibility, §2.3.3) can later be built. The result is classical; the formal content is the induction along the nondeterministic step relation.

Difficulty

Termination is the subtle half: labels do not decrease monotonically along the run in an obvious well-founded way; the book's argument counts the finitely many distinct walk lengths below a bound — this needs the nonnegative-cycle assumption and a careful bound relating labels to simple-path lengths. The invariant proof must thread through the fold over children within a single step.

Formalization scope

Finite node type with decidable equality; arcs as a Finset of ordered pairs; lengths total on $V \times V$ (only arc values matter). The step relation is fully nondeterministic in pivot choice and child order (a permutation quantifier); correctness quantifies over all reachable terminal states — there is no fixed schedule to exploit. Distances live in EReal, so the no-path case is the honest empty infimum, not a sentinel. The trivializing risk of restricting to nonnegative arcs is avoided: only cycles are constrained.

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (Prop. 2.3.1, §2.3.) http://www.athenasc.com/dpbook.html
• E. W. Dijkstra, A note on two problems in connexion with graphs, Numer. Math. 1 (1959), 269–271. https://doi.org/10.1007/BF01386390
• R. Bellman, On a routing problem, Quart. Appl. Math. 16 (1958), 87–90. https://doi.org/10.1090/qam/102435

Modern A/B tests must infer lifetime treatment effects — e.g. customer lifetime value under a new feature — from short-horizon experiment data. Chen, Simchi-Levi and Wang (arXiv:2407.19618) model the experiment as a Markov decision process and exploit a structural fact of many practical interventions: the treatment is local, modifying the system at a single crucial state only. This mission formalizes the core asymptotic theory of the paper: for any differentiable estimator built from the experiment's transition and reward statistics, information sharing — pooling across test arms the samples collected away from the treated state — keeps the estimator asymptotically normal with the same asymptotic bias and never increases its asymptotic variance (Theorem 9), and is asymptotically efficient among unbiased estimators (Theorem 5). The route runs through a Markov chain central limit theorem with the asymptotic variance identified as the autocovariance series, and the linearization/delta method for functionals of chain statistics.

The classical convergence theory of smooth convex minimization. For a function that is $m$-strongly convex and $M$-smooth ($mI \preceq \nabla^2 f(x) \preceq MI$), gradient descent converges linearly, while Newton's method exhibits its famous two phases: a damped phase in which every backtracking step decreases the objective by a fixed amount $\gamma$, and a quadratically convergent phase in which the scaled gradient norm squares at each step, $\tfrac{L}{2m^2}\lVert \nabla f(x^{+})\rVert_2 \le \bigl(\tfrac{L}{2m^2}\lVert \nabla f(x)\rVert_2\bigr)^2$. Together they give the iteration count of B&V (9.36),

with $L$ the Lipschitz constant of the Hessian and $\alpha,\beta$ the backtracking parameters. This mission formalizes Chapters 9–10 of Boyd & Vandenberghe with every constant exactly as printed — a quantitative theory entirely absent from Mathlib.

The Karush–Kuhn–Tucker conditions are the central result of convex optimization: for a convex differentiable problem satisfying Slater's condition, a point is optimal exactly when primal feasibility, dual feasibility, complementary slackness and Lagrangian stationarity hold. This mission formalizes Chapters 4–5 of Boyd & Vandenberghe end to end — the first-order optimality criterion, concavity of the Lagrange dual, weak duality, Slater's strong-duality theorem with dual attainment (via the separating-hyperplane argument of §5.3.2), the saddle-point characterization, sensitivity bounds and Pareto scalarization — culminating in the full KKT characterization.

Linear programming has a complete duality theory; integer programming does not — and the Lagrangean dual measures exactly how far duality reaches. This mission formalizes the duality theory of integer programming from Section 11.4 of Bertsimas–Tsitsiklis, built on the general linear programming duality of Section 4.10. For the integer program

with integer data, the complicating constraints $Ax \ge b$ are dualized with multipliers $p \ge 0$ over the tractable set $X = \{x \text{ integer} \mid Dx \ge d\}$: the dual function is

and the Lagrangean dual is $Z_D = \max_{p \ge 0} Z(p)$. Weak duality $Z_D \le Z_{IP}$ (Theorem 11.2) always holds, but strong duality can fail. The convex hull $CH(X)$ of the integer points of a polyhedron with integer data is itself a polyhedron (Theorem 11.3, Meyer's theorem), and the capstone — Theorem 11.4, the central result of Section 11.4 — identifies the Lagrangean dual exactly: $Z_D$ equals the optimal cost of the linear program

. This is the geometric explanation of the strength of Lagrangean relaxation, yields the bound ordering $Z_{LP} \le Z_D \le Z_{IP}$, and Corollary 11.1 characterizes exactly when the bounds collapse. The polyhedral engine is the general weak/strong duality pair (Theorems 4.17/4.18) over a primal $\min c'x$ s.t. $Ax \ge b$, $x \in P = \{x \mid Dx \ge d\}$, and the formulation-strength comparison $P_{sub} \subseteq P_{cut}$ of Theorem 10.1 supplies the motivating principle that tighter relaxations of the same integer set give sharper bounds.

How can an unbounded polyhedron be described by finitely many geometric objects? Sections 4.8-4.9 of Bertsimas-Tsitsiklis build the cone machinery: recession cones $\{d \mid Ad \ge 0\}$ and their rays, extreme rays (defined, like basic solutions, by $n-1$ linearly independent active constraints), the pointedness criterion (Theorem 4.12: $0$ is an extreme point of a polyhedral cone iff the cone contains no line iff $n$ of the constraint vectors are linearly independent), and the characterization of unbounded linear programs (Theorems 4.13-4.14: over a pointed polyhedral cone, and then over any polyhedron with an extreme point, the optimal cost is $-\infty$ iff some extreme ray $d$ has $c'd < 0$). The capstone is the resolution theorem (Theorem 4.15): a nonempty polyhedron $P$ with at least one extreme point equals $Q = \{\sum_i \lambda_i x^i + \sum_j \theta_j w^j \mid \lambda_i \ge 0, \theta_j \ge 0, \sum_i \lambda_i = 1\}$ — the convex hull of its extreme points plus the cone generated by a complete set of its extreme rays. It specializes to Theorem 2.9 / Corollary 4.4 (a nonempty bounded polyhedron is the convex hull of its extreme points) and Corollary 4.5 (a pointed polyhedral cone is generated by its extreme rays). The converse, Theorem 4.16, states that every finitely generated set is a polyhedron — in particular the convex hull of finitely many vectors is a polyhedron. Together these form the Minkowski-Weyl equivalence of the two representations of polyhedra, verified absent from Mathlib and the genuine content of this mission.

Matrix completion — recovering a low-rank matrix $M = ZZ^\top$ from a small random subset of its entries — powers recommender systems and collaborative filtering. In practice it is solved by running (stochastic) gradient descent on the non-convex objective

where $\Omega=\{(i,j)|M_{i,j} \text{ is observed}\}$ and $R(X)$ is a certain regularizer. from a random starting point, and it just works.

Ge, Lee and Ma (NeurIPS 2016 Best student paper award) explained why: the regularized objective has no spurious local minima — every local minimum is global and exactly recovers $M$. This mission formalizes that landmark theorem in Lean 4, in its strongest known form and along its simplest known proof: the unified landscape analysis of Ge–Jin–Zheng (ICML 2017) and an improved sampling bound in Chen–Li (JMLR 2019). Conditional on an explicit good-sample predicate (which holds with high probability under Bernoulli sampling), every local minimum $X$ of $f$ satisfies $XX^\top = ZZ^\top$.

Bandit feedback is only one point on a spectrum: a learner might see more than its own loss (full information) or less (a spam filter never learns what happened to mail it deleted). Chapter 37 of Lattimore–Szepesvári studies finite adversarial games $G = (\mathcal{L}, \Phi)$ where the loss matrix and the feedback matrix are decoupled. The goal theorem is the celebrated classification theorem: every finite partial-monitoring game has minimax regret exactly $0$, $\Theta(\sqrt{n})$, $\Theta(n^{2/3})$ or $\Omega(n)$ — determined by two purely combinatorial conditions, global and local observability, on the game's neighbourhood structure. A single geometric dichotomy thus governs the price of information in every online decision problem with finite actions and feedback.

When actions are feature vectors and the mean reward is linear — $X_t = \langle \theta_*, A_t\rangle + \eta_t$ — a bandit can generalize across arms: pulling one arm reveals information about all of them. Chapter 19 of Lattimore–Szepesvári carries the optimism principle into this setting: LinUCB (a.k.a. OFUL) plays the action maximizing $\max_{\theta\in\mathcal{C}_t}\langle\theta, a\rangle$ over the confidence ellipsoid $\mathcal{C}_t$ of Mission IX. The goal theorem: with probability $1-\delta$, $\hat R_n \le \sqrt{8n\beta_n \log\frac{\det V_n}{\det V_0}} \le \sqrt{8dn\beta_n\log\frac{d\lambda + nL^2}{d\lambda}}$ — regret $\tilde O(d\sqrt{n})$ independent of the number of actions. The combinatorial engine is the elliptical potential lemma, bounding how many times adaptively chosen directions can be surprising. Chapter 22's phased elimination with G-optimal design (Mission IX) sharpens this to $\tilde O(\sqrt{dn\log k})$ for finite action sets.

Least-squares estimation from adaptively collected data is the statistical heart of linear bandits: the actions $A_t$ depend on past noise, so classical fixed-design theory does not apply. Chapter 20 of Lattimore–Szepesvári resolves this with the method of mixtures: the process $M_t(x) = \exp(\langle x, S_t\rangle - \frac{1}{2}\|x\|^2_{V_t(\lambda)})$ is a supermartingale, and integrating over a Gaussian mixture yields the self-normalized bound — the goal theorem — $\mathbb{P}\big(\exists t : \|S_t\|^2_{V_t(\lambda)^{-1}} \ge 2\log\frac{1}{\delta} + \log\frac{\det V_t(\lambda)}{\lambda^d}\big) \le \delta$, valid uniformly over all times. The resulting confidence ellipsoids for the regularized least-squares estimator (Abbasi-Yadkori et al.) calibrate every algorithm of Mission X. The mission also formalizes the Kiefer–Wolfowitz theorem of Chapter 21: G-optimal and D-optimal experimental designs coincide, with optimal value exactly $d$ — the classical equivalence theorem of optimal design theory.

Motivation

Reinforcement learning in a changing environment has a difficulty that is absent from a fixed Markov decision process: transition data gathered earlier may describe a different system from the one the decision maker currently faces. A learning algorithm therefore estimates transitions from a recent window of observations. The estimate comes with a confidence region, a set of transition laws consistent with the data at a chosen statistical radius. In the general nonstationary setting studied by Cheung, Simchi-Levi and Zhu, their algorithm widens this region to ensure that it can contain a model whose states remain readily reachable. Such a model is needed for the paper's dynamic regret analysis. Section 7 isolates a structural condition under which widening is unnecessary: every destination is reachable from every state with a uniformly positive one-step probability under a suitable action. Cheung, Simchi-Levi and Zhu, §7.

This mission formalizes Proposition 4 of that paper, the precise claim that the original, unwidened transition region contains a model with a controlled diameter. It is one of three separate missions for the paper. The result supports the paper's no-widening variant of its learning algorithm; it is not a claim that every model in the confidence region has small diameter. Cheung, Simchi-Levi and Zhu, Proposition 4.

Setting

There are finitely many states $\mathcal S$ and, for each state $s$, a nonempty finite set $\mathcal A_s$ of permitted actions. At each time $t\in[T]$, the system has a reward $r_t(s,a)\in[0,1]$ and a probability distribution $p_t(\cdot\mid s,a)$ for the next state. The distribution may change with $t$. A trajectory records the observed state $s_q$, chosen action $a_q$, and successor state $s_{q+1}$ at each time $q$. These are the model primitives in §2.2. Cheung, Simchi-Levi and Zhu, pp. 6–7.

An episode begins at $\tau(m)$ and uses a window of length $W$. At time $t$ in that episode, $N_t(s,a)$ counts how often the pair $(s,a)$ appears between $(\tau(m)-W)\vee1$ and $t-1$; $N_t^+(s,a)=\max\{1,N_t(s,a)\}$. The empirical row $\hat p_t(\cdot\mid s,a)$ counts observed successors and divides by $N_t^+(s,a)$. The corresponding average true row $\bar p_t$ averages the time-varying transition probabilities over the same visits. Both are zero vectors when there are no visits. Cheung, Simchi-Levi and Zhu, equations (3) and (5).

Write $SA=\sum_s|\mathcal A_s|$, so this is the number of allowed state-action pairs. At confidence level $\delta$, the transition radius is $\operatorname{rad}_{p,t}(s,a)=2\sqrt{2S\log(SAT/\delta)/N_t^+(s,a)}$. The region $H_{p,t}(s,a;\eta)$ consists of probability vectors within $\ell_1$ distance $\operatorname{rad}_{p,t}(s,a)+\eta$ of $\hat p_t$. Here $\eta=0$ means no widening. The estimation event $E_p$ bounds the $\ell_1$ distance between $\bar p_t$ and $\hat p_t$ by that radius for each allowed pair. Cheung, Simchi-Levi and Zhu, pp. 12, 14.