Motivation

A Markov decision process (MDP) chooses a decision in every period of a dynamic system whose state evolves stochastically in response to the decision, so as to maximize expected discounted return. Firms use this model for inventory, pricing, and advertising decisions that respond to a randomly evolving demand state; engineers use it for maintaining or replacing equipment that degrades stochastically. A recurring practical question is qualitative rather than numerical: does the optimal decision increase with the state — should a firm price higher after a period of strong sales, or replace a machine sooner the worse its observed condition — without having to solve the dynamic program numerically for every instance of the model? Topkis's Chapter 3, Section 3.9 (Topkis, Supermodularity and Complementarity, 2011, building on Topkis [1968]) answers this by isolating the lattice-theoretic structure — supermodularity of the return function and of the transition law — under which monotone optimal policies are guaranteed on structural grounds alone. A closely related but logically independent question was studied earlier by Lehmann [1955], who characterized when a family of distributions is stochastically increasing in a parameter; Topkis generalizes Lehmann's characterization to any property of the parameter dependence whose defining set of functions forms a closed convex cone, of which stochastic monotonicity, supermodularity, and convexity are three instances (Theorem 3.9.1, Corollary 3.9.1). Serfozo [1976] independently develops related conditions for partially observed Markov decision processes, and Amir [1996] and Amir, Mirman, and Perkins [1991] give analogous monotonicity results for other classes of dynamic programming models.

Setting

Fix a finite planning horizon of $k$ periods, $i = 1, \dots, k$. In period $i$ the state $t$ ranges over a set $T_i \subseteq \mathbb{R}^m$; given state $t$, the decision $x$ is restricted to a finite, nonempty set $X_{t,i} \subseteq \mathbb{R}^n$ (finiteness guarantees that an optimal decision always exists — no continuity or compactness argument is used). Write $S_i = \{(x,t) : t \in T_i,\, x \in X_{t,i}\}$ for the set of admissible (decision, state) pairs in period $i$. The (bounded) expected net return of choosing decision $x$ in state $t$, period $i$, is $r_i(x,t)$. A discount rate $\beta \in [0,1]$ gives $\gamma = 1/(1+\beta)$, the value in period $i$ of one unit of return in period $i+1$. Given decision $x$, state $t$, and period $i$, the state $w$ of period $i+1$ is drawn from a distribution $F(x,t,i,\cdot)$ on $\mathbb{R}^m$.

The optimal-value function $f_i(t)$ (present value of acting optimally from state $t$, period $i$, onward) and the decision-value function $g_i(x,t)$ (present value of choosing $x$ in state $t$, period $i$, then acting optimally thereafter) are defined by backward induction from period $k$:

$$g_k(x,t) = r_k(x,t), \qquad f_i(t) = \max_{x \in X_{t,i}} g_i(x,t), \qquad g_i(x,t) = r_i(x,t) + \gamma \int f_{i+1}(w)\, dF(x,t,i,w) \quad (i < k).$$

A subset $S$ of a Euclidean space is increasing if it is upward closed under the coordinatewise order. A family of distributions $\{F(a,\cdot) : a \in D\}$ indexed by a parameter $a$ is stochastically increasing on $D$ if the probability $\int_S dF(a,w)$ of every increasing set $S$ is a monotone (non-decreasing) function of $a$ on $D$; when $D$ is a sublattice, the family is stochastically supermodular on $D$ if that same probability is a supermodular function of $a$ on $D$. A real-valued function $\varphi$ on a lattice is supermodular on a set $D$ if $\varphi(a_1) + \varphi(a_2) \le \varphi(a_1 \vee a_2) + \varphi(a_1 \wedge a_2)$ for all $a_1, a_2 \in D$ — the mission series' shared notion, defined once in chunk 02-monotonicity and reused here as Supermodularity.Monotonicity.SupermodularOn.

Formalization targets

Goal — Theorem 3.9.2 (monotone optimal policies)

$$g_i(x,t) \text{ supermodular on } S_i, \qquad f_i(t) \text{ supermodular on } T_i, \qquad \arg\max_{x \in X_{t,i}} g_i(x,t) \text{ increasing in } t,$$

together with the existence of a greatest and a least optimal decision at every state, each increasing in the state, in every period $i$ — under the hypotheses that $S_i$ is a sublattice of $\mathbb{R}^{n+m}$, $X_{t,i}$ is expanding in $t$, $r_i$ is increasing in $t$ (on sections) and jointly supermodular in $(x,t)$, and $F(x,t,i,\cdot)$ is stochastically increasing in $t$ (on sections) and stochastically jointly supermodular in $(x,t)$, for every period $i$.

This is the weakest of the targets that is still worth stating on its own: it packages four related conclusions (parts (a)–(d) of Theorem 3.9.2) that share one hypothesis set, rather than isolating just the headline monotone-decision claim, because the book's own proof derives all four together and a solver attacking part (c) or (d) needs part (a) and (b) established first.

Supporting milestones

• Lemma 3.9.4: under the monotonicity half of the goal's hypotheses alone (no supermodularity), $f_i(t)$ is increasing in $t$ for every period $i$. This is the induction Theorem 3.9.2 reuses and strengthens.
• Corollary 3.9.1(b): on a sublattice $T$, a family of distributions is stochastically supermodular in $t$ iff $\int h(w)\,dF(t,w)$ is supermodular in $t$ for every increasing $h$. This is what lets the goal's hypothesis "$F(x,t,i,\cdot)$ stochastically supermodular in $(x,t)$" be converted into "$\int f_{i+1}(w)\,dF(x,t,i,w)$ supermodular in $(x,t)$", the step that feeds $g_i$'s supermodularity.
• Theorem 3.9.1: the general closed-convex-cone characterization of which Corollary 3.9.1(b) is the supermodularity instance (monotonicity and convexity are the other two instances, not formalized here since the goal's proof only needs the supermodularity case).

Significance

The result gives a purely structural sufficient condition — no smoothness, convexity of the decision set, or specific functional form — for monotone comparative statics in dynamic optimization: whenever the one-period return and the state transition are individually monotone and jointly supermodular in (decision, state), so is the whole multi-period value function, and so are the optimal decisions. Textbook applications include optimal advertising that decreases with prior-period sales, optimal pricing that increases with prior-period sales, and optimal maintenance of a deteriorating system, none of which need to be re-derived from scratch once the structural hypotheses are checked for the specific return and transition functions at hand.

Formalizing it contributes a genuinely new layer to the mission series and, per the paper's own triage (substrate.md), to the platform's application of Mathlib's probability-kernel infrastructure: a finite-horizon MDP with a Lebesgue–Stieltjes-style transition law and its associated stochastic-dominance vocabulary (stochastically increasing / stochastically supermodular families of distributions) did not previously exist on the platform or in this mission series, and both are reusable beyond this mission by any future formalization of dynamic programming under uncertainty. The proof itself is not open — Topkis [2011] (unchanged from the 1968/1998 original) gives a complete, elementary backward-induction argument — so what this mission produces is the formalization of a known, structurally distinctive proof technique, not a new mathematical result.

Difficulty

The naive argument — "supermodularity of $r_i$ plus supermodularity of the transition kernel obviously gives supermodularity of $g_i$" — breaks exactly at the integral: supermodularity of $(x,t) \mapsto F(x,t,i,\cdot)$ is a statement about the whole family of distributions, not about a single number, so "the transition is jointly supermodular" has to be unpacked into "the probability of every increasing set is jointly supermodular in $(x,t)$" before it says anything about $\int f_{i+1}(w)\,dF(x,t,i,w)$ for a specific function $f_{i+1}$. Corollary 3.9.1(b) is exactly the step that licenses this unpacking, and it is not free: it needs Theorem 3.9.1's closed-convex-cone argument (approximating $f_{i+1}$ from below by increasing step functions and invoking monotone convergence), not a pointwise argument on $r_i$ and $F$ separately. A second place the naive argument fails is at the constraint sets: because $X_{t,i}$ only grows with $t$ rather than being fixed, monotonicity of $f_i$ (Lemma 3.9.4) needs its own induction combining that growth with monotonicity of $g_i$ — supermodularity of $g_i$ alone does not hand you monotonicity of the arg max without it.

Formalization scope

States and decisions are represented as Fin m → ℝ and Fin n → ℝ (finite-dimensional Euclidean coordinate spaces with the coordinatewise/product order, matching the book's own restriction to $\mathbb{R}^m$ and $\mathbb{R}^n$ — no abstract lattice is used where the book itself specializes). Distributions are represented as MeasureTheory.Measure on the relevant coordinate space, with IsProbabilityMeasure supplied explicitly wherever a stochastic-dominance hypothesis is used (the probability of a set is read off as (μ S).toReal, which is only faithful to $\int_S dF$ when μ is a probability measure — an unconstrained arbitrary measure would let .toReal collapse an infinite value to $0$ and make the hypothesis trivially satisfiable, a formalization this mission rules out). Integrands h are required integrable against every measure in the family wherever an integral is asserted to lie in a set V, since the Bochner integral of a non-integrable function is definitionally 0 in Lean/Mathlib and would otherwise make Theorem 3.9.1 and Corollary 3.9.1(b) trivially true. Decision sets $X_{t,i}$ are finite (Finset, not merely a bounded or compact Set) and required nonempty exactly where the book assumes it: this finiteness, not any compactness or semicontinuity argument, is what guarantees an optimal decision exists, and dropping it would silently substitute Chapter 2's compactness-based existence machinery for the different argument this section actually uses. The optimal-value and decision-value functions $f_i, g_i$ are represented as any functions satisfying the two backward-recursion equations that define them, rather than being constructed by explicit backward recursion in Lean; since the equations determine $f_i, g_i$ uniquely from $r_i$ and $F$, this is a faithful reading of "define $f_i, g_i$ by (3.9.1) and (3.9.2)," not a weakening of the theorem. The goal's part (c) is stated using the mission series' InducedSetOrder (the Veinott/strong set order, chunk 01-lattices) and part (d) as the existence of two selection functions (greatest, least optimal decision), each monotone in the state — matching the book's "there is a greatest (least) optimal decision ... and this greatest (least) optimal decision is increasing in $t$." The infinite-horizon stationary extension that the book gives immediately after Theorem 3.9.2 (relying on an unproved citation to Blackwell [1965]) is out of scope for this mission.

Reusable infrastructure: the StochasticallyIncreasingOn/StochasticallySupermodularOn definitions are parametric in the ambient preorder/lattice and in the measure's target dimension, so a future mission on stochastic convexity (Corollary 3.9.1(c), not formalized here) or on Topkis's §3.10 stochastic inventory model (which explicitly depends on §3.9, per the book's own reading-order note) can reuse them without modification. Contributions extending this mission to the infinite-horizon case, or completing Corollary 3.9.1's monotonicity and convexity halves, are welcome.

Selected references

• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 2011 (unchanged from the 1998 original), Chapter 3, Section 3.9. DOI: 10.1515/9781400822539.
• D. M. Topkis, "Ordered Optimal Solutions," PhD dissertation / working paper, Stanford University, 1968 (the original source for this section's results).
• E. L. Lehmann, "Ordered Families of Distributions," Annals of Mathematical Statistics 26(3), 1955, pp. 399–419. https://doi.org/10.1214/aoms/1177728487
• R. Serfozo, "Monotone Optimal Policies for Markov Decision Processes," Mathematical Programming Study 6, 1976, pp. 202–215.
• R. Amir, "Sensitivity Analysis of Multisector Optimal Economic Dynamics," Journal of Mathematical Economics 25(1), 1996, pp. 123–141.
• R. Amir, L. J. Mirman, and W. R. Perkins, "One-Sector Nonclassical Optimal Growth: Optimality Conditions and Comparative Dynamics," International Economic Review 32(3), 1991, pp. 625–644.
• D. Blackwell, "Discounted Dynamic Programming," Annals of Mathematical Statistics 36(1), 1965, pp. 226–235. https://doi.org/10.1214/aoms/1177700285

Motivation

Random matrices with independent entries appear whenever a system is measured through many noisy, roughly independent channels: shot noise in a sensor array, edges in an Erdős–Rényi-type random graph, or the design matrix of a linear model with independent covariates. A basic question about any such matrix $A$ is how far it can stretch a vector — its operator norm $\|A\|$ — since this single number controls the stability of every linear statistic computed from $A$: least-squares estimates, spectral clustering, covariance estimation, and random projections all reduce, at some point, to bounding $\|A\|$.

The theory traces to Marchenko and Pastur's 1967 asymptotic law for the spectrum of large random matrices, and to Bai and Yin's 1988 almost-sure limit $\|A\|/\sqrt n \to 2$ for $n \times n$ matrices with i.i.d. mean-zero, unit-variance entries. Those results are asymptotic: they say what happens as the dimension $n \to \infty$, for a fixed matrix shape. The result formalized here, Theorem 4.4.5 of Vershynin's High-Dimensional Probability (2018) (DOI 10.1017/9781108231596), belongs to the more recent non-asymptotic strand of the theory: it gives an explicit, dimension-free bound that holds at every fixed $m, n$, with an explicit failure probability — the form of statement needed for finite-sample guarantees in statistics and data science, rather than limiting behavior.

Setting

Let $A$ be an $m \times n$ real matrix. Equip $\mathbb R^n$ and $\mathbb R^m$ with the Euclidean norm $\|\cdot\|_2$; $A$ acts as a linear map $\ell_2^n \to \ell_2^m$. Its operator norm (§4.1.2) is

$$\|A\| \;:=\; \max_{x \in S^{n-1}} \|Ax\|_2 ,$$

the largest factor by which $A$ can stretch a unit vector; equivalently, the largest singular value of $A$.

A real random variable $X$ is sub-gaussian with the mission's own convention (matching the Orlicz $\psi_2$ norm this series already carries as a published definition, HighDimProb.Concentration.subgaussianNorm) if

$$\|X\|_{\psi_2} \;:=\; \inf\{t > 0 : \mathbb E \exp(X^2/t^2) \le 2\} \;<\; \infty .$$

Bounded random variables and Gaussians are sub-gaussian; a Bernoulli($p$) variable and a $\pm 1$-valued coin flip both qualify, which is why the theorem below directly covers random matrices with i.i.d. Rademacher or Gaussian entries as special cases.

The mission's proof technique is the ε-net argument, developed in §4.2 and used nowhere before this chapter of the book: a metric space $(T,d)$, a subset $K \subseteq T$, and $\varepsilon > 0$ give rise to an ε-net $N \subseteq K$ — a finite set such that every point of $K$ is within $\varepsilon$ of some point of $N$ — and a covering number $N(K, d, \varepsilon)$, the smallest cardinality of such a net. The technique reduces a statement that must hold uniformly over an infinite (compact) set to a statement about finitely many points, paid for by a union bound whose cost is controlled by the covering number.

Formalization targets

Goal (Theorem 4.4.5)

$$\exists\, C > 0 \;\text{such that}\; \forall\, t > 0,\quad \mathrm{Prob}\bigl\{\, \|A\| \le CK(\sqrt m + \sqrt n + t) \,\bigr\} \;\ge\; 1 - 2\exp(-t^2),$$

for any $m \times n$ random matrix $A$ with independent, mean-zero, sub-gaussian entries $A_{ij}$ and $K = \max_{i,j} \|A_{ij}\|_{\psi_2}$. This is the weakest stable form of the bound — it fixes no numerical value for $C$, only its existence and absoluteness (independence from $m$, $n$, $A$, $t$), so later refinements of the constant do not invalidate it.

Significance

The result itself. The bound $\|A\| \lesssim \sqrt m + \sqrt n$ is sharp up to the constant: for entries of unit variance, $\mathbb E\|A\| \ge \tfrac14(\sqrt m + \sqrt n)$ for large $m, n$ (the book's Exercise 4.4.7), so no non-asymptotic bound of this shape can be improved beyond constants. It is the entry point to the rest of the book's random matrix theory: Corollary 4.4.8 specializes it to symmetric matrices, and it underlies the community-detection (§4.5) and covariance-estimation (§4.7) applications later in the same chapter, neither of which is part of this mission.

Formalizing it. The theorem is a classical, fully proved result; nothing about its truth is open. What this mission contributes is a machine-checked formal statement — together with the two pieces of chapter infrastructure its own textbook proof names by number (Corollary 4.2.13, Exercise 4.4.3(a)) — and a third, self-contained application of the same covering-number machinery (Theorem 4.3.5) that exercises the shared IsEpsNet/coveringNumber definitions on a different metric space (the Hamming cube), independently of the Euclidean case. Mathlib and the Prove2Me platform currently have no ε-net, covering-number, or packing-number infrastructure (checked by q=random matrix, q=operator norm, q=covering number, q=net on the platform, and by filename search in Mathlib): this mission is the first to introduce it, restated inside its own namespace since it is not otherwise available to build on.

Difficulty

The obvious first approach is to bound $\|A\| = \max_{x \in S^{n-1}} \|Ax\|_2$ directly by union-bounding a concentration inequality over the sphere $S^{n-1}$. This fails outright: $S^{n-1}$ is infinite (indeed uncountable) for $n \ge 2$, so no union bound over its points can converge — the naive approach gives $\infty \cdot (\text{tail probability})$. The ε-net argument is the fix, but it is not just "discretize and hope": the reduction from the sphere to a finite net (quadratic_form_on_net, Exercise 4.4.3(a)) loses a multiplicative factor $1/(1-2\varepsilon)$ that must be tracked, and the net's cardinality (covering_numbers_of_euclidean_ball_and_sphere, Corollary 4.2.13) is exponential in the dimension ($9^n$ at $\varepsilon = 1/4$) — so the per-point tail probability from Hoeffding-type concentration must itself decay fast enough (quadratically in the exponent) to survive multiplying by $9^{m+n}$ many points. Getting the union bound to close requires choosing the threshold $u$ in the tail bound proportionally to $\sqrt m + \sqrt n + t$, not to $t$ alone — the $\sqrt m + \sqrt n$ term is exactly what pays for the net's exponential size.

Formalization scope

$A$ is represented as Ω → Matrix (Fin m) (Fin n) ℝ; its entries A ω i j are the individual real random variables. Independence of the $mn$ entries is iIndepFun over the index type Fin m × Fin n; mean-zero is the vanishing of each entry's Bochner integral. The operator norm is the norm of the associated continuous linear map between EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m) (matrixOpNorm, every linear map between finite-dimensional normed spaces being automatically continuous), matching the book's maxₓ∈Sⁿ⁻¹ ‖Ax‖₂ exactly. The sub-gaussian norm $K$ reuses this series' own published definition, HighDimProb.Concentration.subgaussianNorm, rather than a re-derivation. Covering numbers (coveringNumber) are restricted to finite (Finset) ε-nets, the only kind this chapter uses; this is a deliberate restriction, not a general-purpose covering-number formalization, and is disclosed as such. A hard-coded numeral for $C$, or an unquantified "with high probability" in place of the explicit failure probability $2\exp(-t^2)$, would each trivialize the statement and is ruled out: $C$ is existentially bound ahead of every other quantifier, and $t > 0$ is a free parameter with its own explicit bound, exactly as the book states it.

Definitions reusable beyond this mission: IsEpsNet and coveringNumber are stated for a general PseudoMetricSpace and apply unchanged to any later chapter's covering-number needs (e.g. Chapter 8's VC-dimension covering numbers), though per this series' rule that drafts cannot import drafts, a later chunk would restate rather than import them until this mission is published. matrixOpNorm is likewise chapter-agnostic. Contributions completing the sorry proofs of any of the four theorem items are welcome and independent of one another; the covering number and net-reduction items (covering_numbers_of_euclidean_ball_and_sphere, quadratic_form_on_net) are the standard prerequisites for the goal's own volumetric/ε-net proof.

Selected references

• Vershynin, R. High-Dimensional Probability: An Introduction with Applications in Data Science. Cambridge University Press, 2018. DOI 10.1017/9781108231596
• Bai, Z. D., Yin, Y. Q. "Necessary and sufficient conditions for almost sure convergence of the largest eigenvalue of a Wigner matrix." Annals of Probability 16 (1988), 1729–1741.
• Marchenko, V. A., Pastur, L. A. "Distribution of eigenvalues for some sets of random matrices." Mathematics of the USSR-Sbornik 1 (1967), 457–483.

Motivation

Every method in Chapters 2-4 of this series solves a projection or proximal subproblem at every step — a Euclidean projection, or a Bregman-divergence prox-mapping — which can itself be as hard as the original problem when $X$ is a complicated feasible set (a spectrahedron, a flow polytope, a matroid base polytope). The conditional gradient method (Frank & Wolfe, 1956) sidesteps this entirely: instead of a projection, each step calls a linear optimization (LO) oracle — minimize a linear function over $X$ — which is frequently far cheaper (over a spectrahedron, this reduces to a single eigenvector computation; over many combinatorial polytopes, to a greedy algorithm). This is the origin of the modern "projection-free" family of optimization methods widely used at the scale where projections are the bottleneck.

Setting

Fix a nonempty compact convex set $X$ in a real normed space $E$ and a convex $f:X\to \mathbb R$ with $L$-Lipschitz gradient (Eq. (7.1.4)): $\|f'(x)-f'(y)\|_*\le L\|x-y\|$. The classic conditional gradient (CndG) method, Algorithm 7.1, sets $x_0\in X$, $y_0=x_0$, and for $k=1,2,\dots$: calls the LO oracle $x_k\in\arg\min_{z\in X}\langle f'(y_{k-1}),z\rangle$, then sets $y_k=(1-\alpha_k)y_{k-1}+\alpha_kx_k$ for a stepsize $\alpha_k\in[0,1]$, either the fixed schedule $\alpha_k=2/(k+1)$ (Eq. (7.1.9)) or exact line search (Eq. (7.1.10)).

Section 7.1.1.2 extends this to bilinear saddle-point problems, where $f$ itself is the (generally nonsmooth) function $f(x)=\max_{y\in Y}\{\langle Ax,y\rangle-\hat f(y)\}$ (Eq. (7.1.5)) for a compact convex $Y$ and linear operator $A$. Since $f$ is nonsmooth, the method is applied instead to a family of smooth approximations $f_\eta$ built from a strongly convex $\omega$ on $Y$ (Eq. (7.1.21)-(7.1.23)), with the smoothing parameter $\eta_k$ allowed to vary across iterations rather than being fixed in advance.

Formalization targets

Goal — Theorem 7.1

$$f(y_k) - f^* \le \frac{2L}{k(k+1)}\sum_{i=1}^k\|x_i-y_{i-1}\|^2.$$

Supporting milestones, in attack order

• Lemma 7.1: the smoothed objective family $f_\eta$ is monotone nondecreasing in $\eta\ge0$ — the one-line fact ($V(y)-D_Y^2\le0$ pointwise) that licenses a variable, decreasing smoothing schedule $\eta_k$ rather than a schedule fixed in advance from knowledge of the target accuracy.
• Theorem 7.2: the saddle-point counterpart of the goal theorem, running the same CndG algorithm on the smoothed gradients $f_{\eta_k}'$ instead of $f'$ directly, with the explicit rate $f(y_k)-f^*\le\frac{2}{k(k+1)}\sum_{i=1}^k[i\eta_iD_Y^2+\frac{\|A\|^2}{\sigma_v\eta_i} \|x_i-y_{i-1}\|^2]$.

Every constant here is exactly the book's; the goal theorem's bound is left in terms of the actual step distances $\sum\|x_i-y_{i-1}\|^2$, not a diameter-based simplification (see Difficulty).

Significance

This mission formalizes the founding convergence result of the entire projection-free family (Frank-Wolfe methods), which has become central to large-scale machine learning precisely because its per-iteration cost can be orders of magnitude below that of a projection-based method on structured feasible sets. Theorem 7.1's specific form — a rate depending on the realized step distances rather than a fixed diameter — is also the more informative, tighter statement (the book's own remarks show it recovers the classical diameter-based $O(LD_X^2/\varepsilon)$ complexity as a corollary, but also explains why the rate can be much better in practice when the iterates settle near an extreme point).

No result matching conditional gradient / Frank-Wolfe methods exists on the platform as of 2026-09-18 (q=Frank-Wolfe and q=conditional gradient both return zero hits — see Prior art in MODERATION_NOTES.md).

Difficulty

The chief formalization difficulty is representing "with the stepsize policy in (7.1.9) or (7.1.10)" faithfully without either restricting to one policy (weaker than the book's stated theorem) or introducing an awkward disjunction of two separate algorithm definitions. The book's own proof resolves this by a single observation used for both policies at once: $f(y_k)\le f(\tilde y_k)$ for $\tilde y_k$ the point the fixed schedule $\gamma_k=2/(k+1)$ would have produced — trivially by equality under (7.1.9), or because $y_k$ is chosen to minimize $f$ over the entire line segment under (7.1.10), of which $\tilde y_k$ is one point. This mission's hyk_le hypothesis states exactly this shared consequence, which is genuinely what the proof uses and genuinely covers both policies, rather than picking one arbitrarily.

A second difficulty is not collapsing $\sum_{i=1}^k\|x_i-y_{i-1}\|^2$ into a diameter bound $kD_X^2$ inside the milestone itself — the book's own remarks perform that substitution as a separate, weaker corollary (Eq. (7.1.19)) after stating Theorem 7.1 in its sharper form; folding the substitution into the goal statement itself would silently prove a different, weaker theorem.

Formalization scope

conditional_gradient_rate and saddle_point_cndg_rate state the LO oracle's exactness (x k ∈ Argmin_{z∈X}⟨fGrad(y(k-1)),z⟩) as a pointwise hypothesis rather than deriving it from IsCompact X via an existence lemma — matching the pointwise-hypothesis convention this series uses throughout for argmin-defined algorithmic steps (chunk 03-deterministic's mirror-descent updates, chunk 04-stochastic's stochastic mirror-descent update). X compact convex is still included as a hypothesis, matching the book's own standing assumption on the problem class, even though it is not itself needed to derive the stated conclusion from the other hypotheses.

smoothed_objective_monotone and saddle_point_cndg_rate realize $f_\eta$/$f$ via sSup of the image of $Y$ under the pointwise saddle-point objective, matching the book's own max_{y∈Y}{...} definition (Eq. (7.1.5), (7.1.23)) directly rather than introducing a separate Def_ file for a "bilinear saddle-point objective" structure — no other item in this mission reuses that definition verbatim, so per this series' convention (no shared substrate bundled into a structure unless reused), it is inlined at each use.

A trivializing formalization this mission rules out: stating the LO oracle via an $\varepsilon$-approximate minimizer ((fGrad (y(k-1))) (x k) ≤ (fGrad (y(k-1))) z + ε for some ε) rather than an exact one — this is explicitly a different, weaker algorithm the book does not analyze in Theorem 7.1/7.2 (the book studies approximate LO oracles separately, later in the chapter, not selected here).

Left out of scope, for time: Theorem 7.7 (the matching lower complexity bound for LO-oracle methods, Eq. (7.1.60)) — formalizing it faithfully requires first modeling the abstract class of "LCP methods" (any algorithm restricted to LO-oracle calls) as a universally-quantified object, a substantially different and more involved formalization task than the two upper-bound convergence theorems selected here; named per Hard Rule 7 rather than approximated. The d(x)=\sum x_i\log x_i entropy-smoothing remark and the primal/primal-dual averaging CndG variants (§7.1.2, not covered by this mission's page range) are likewise not attempted.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 7, §7.1.1. https://doi.org/10.1007/978-3-030-39568-1
• M. Frank, P. Wolfe, "An algorithm for quadratic programming," Naval Research Logistics Quarterly, 3(1-2), 1956, pp. 95-110.
• M. Jaggi, "Revisiting Frank-Wolfe: projection-free sparse convex optimization," ICML, 2013 (the modern machine-learning revival of the method).

Motivation

Most machine learning training objectives — deep network losses, matrix factorization, regularized empirical risk with a nonconvex loss — are not convex, yet the great majority of convergence theory available before Ghadimi and Lan's 2013 work applied only to convex problems or gave no non-asymptotic rate at all. Ghadimi and Lan (2013) established the first non-asymptotic complexity bounds for stochastic first-order methods on smooth nonconvex problems, using the norm of a gradient mapping (rather than function-value suboptimality, which is meaningless without convexity) as the convergence measure, together with a randomized stopping rule that removes the need to know in advance which iterate will be best. This mission formalizes the constrained, composite generalization of that theory — Lan's own extension (2020) to problems with a nonsmooth term $h$ and a general Bregman geometry rather than the Euclidean norm — culminating in the stochastic complexity bound for the randomized stochastic mirror descent (RSMD) algorithm.

Setting

Fix a nonempty closed convex $X\subseteq\mathbb{R}^n$, a continuously differentiable (possibly nonconvex) $f:X\to\mathbb{R}$ with $L$-Lipschitz gradient, and a simple convex (possibly nonsmooth) $h:X\to\mathbb{R}$ (e.g. $h=\|\cdot\|_1$ or $h\equiv0$); write $\Psi:=f+h$, $\Psi^*:=\min_{x\in X}\Psi(x)$ (assumed finite). For a distance-generating function $\nu$ with modulus 1 and its prox-function $V(z,x):=\nu(x)-\nu(z)-\langle\nabla\nu(z),x-z\rangle$, the generalized projection at $x$ with gradient-like input $g$ and stepsize $\gamma>0$ is

$$x^+ := \arg\min_{u\in X}\Big\{\langle g,u\rangle + \tfrac1\gamma V(x,u) + h(u)\Big\}, \qquad P_X(x,g,\gamma) := \tfrac1\gamma(x-x^+),$$

which reduces to $\nabla f(x)$ itself when $X=\mathbb{R}^n$ and $h\equiv0$: $P_X$ is a generalized projected gradient (or gradient mapping) of $\Psi$ at $x$, and its norm going to zero is the right notion of "approximately stationary" for the composite, possibly-nonconvex problem $\min_{x\in X}\Psi(x)$.

The randomized stochastic mirror descent (RSMD) algorithm, given only a stochastic first-order oracle returning $G(x,\xi)$ with $\mathbb{E}[G(x,\xi)]=\nabla f(x)$ and $\mathbb{E}[\|G(x,\xi)- \nabla f(x)\|^2]\le\sigma^2$ (Assumption 13), forms a mini-batch average $G_k$ of $m_k$ oracle calls at each step $k$, updates $x_{k+1}$ via the generalized projection with $g=G_k$, and stops at a randomly chosen index $R$ (drawn from a prescribed pmf $P_R$, independently of the optimization process) rather than a deterministic final iterate.

Formalization targets

Goal — Theorem 6.6(a), RSMD complexity

$$\mathbb{E}\big[\|\tilde g_{X,R}\|^2\big] \le \frac{LD_\Psi^2 + \sigma^2\sum_{k=1}^N(\gamma_k/ m_k)}{\sum_{k=1}^N(\gamma_k-L\gamma_k^2)}, \qquad \tilde g_{X,k}:=P_X(x_k,G_k,\gamma_k),$$

for $0<\gamma_k\le1/L$ (strict for at least one $k$) and $P_R$ chosen as in (6.2.30), the expectation over both $R$ and the oracle randomness $\xi_{[N]}$.

Supporting milestones, in attack order

• Lemma 6.4: $\langle g,P_X(x,g,\gamma)\rangle \ge \|P_X(x,g,\gamma)\|^2 + \tfrac1\gamma[h(x^+) -h(x)]$ — the bound that lets a smoothness inequality on $f$ become a descent inequality on the whole composite $\Psi$.
• Lemma 6.6: the three-point characterization of $x^+$, the composite-problem analogue of Chapter 3's Lemma 3.4.
• Theorem 6.5 (deterministic ancestor): $\|g_{X,R}\|^2 \le LD_\Psi^2/\sum_{k=1}^N(\gamma_k- L\gamma_k^2/2)$ for the exact-gradient nonconvex MD algorithm.
• Corollary 6.4: the constant-stepsize instantiation $\|g_{X,R}\|^2\le2L^2D_\Psi^2/N$.

Every result states its constants exactly as the book derives them; no milestone or the goal hides a rate behind an unspecified $O(\cdot)$.

Significance

The goal theorem gives the complexity of the RSMD algorithm in terms of a squared generalized gradient-mapping norm — the correct convergence criterion for constrained, composite, possibly nonconvex stochastic optimization, since function-value suboptimality is not controllable without convexity and unconstrained gradient norms are meaningless once $X\ne\mathbb{R}^n$ or $h$ is nonsmooth. Choosing $m_k$ and $N$ appropriately (a corollary this mission does not formalize) turns this bound into the celebrated $O(\sigma^2/\varepsilon^2)$ total-oracle-call complexity for finding an $\varepsilon$-stationary point in expectation — the standard benchmark every later stochastic nonconvex method (variance-reduced SGD, SPIDER, and their composite/constrained variants) is compared against.

No result in this mission has a machine-checked proof on Prove2Me under this exact hypothesis set. The two closest platform results, both from lean-optrates (Shi), are genuinely different objects: ShiOptRates.gd_exact_rate is plain, unconstrained, deterministic gradient descent ($x_{k+1}=x_k-L^{-1}g(x_k)$, no set $X$, no composite $h$, no generalized projection), and ShiOptRates.Stochastic.sgd_rate is plain SGD under the same unconstrained, non-composite setup — its filtration/conditional-expectation formalization pattern (a Filtration ℕ, μ[·|ℱ k] for the unbiasedness and variance-bound hypotheses) is the same one this mission's goal theorem uses, confirming it as the platform's established idiom for this class of result, but the mathematical content (plain gradient step vs. generalized-projection/mirror-descent step, no $X$ or $h$) is different. Neither is reused; both are noted as the platform's nearest existing work.

Difficulty

The generalized projection $x^+$ replaces the Euclidean projection with an arbitrary Bregman-based prox-mapping and absorbs the nonsmooth term $h$ directly into the subproblem — a formalization that quietly assumes $h\equiv0$ or $X=\mathbb{R}^n$ would collapse every milestone here into the $\nabla f(x)$ special case and prove nothing about the constrained composite problem the chapter is actually about. The harder difficulty is in the goal theorem's own randomness: the book's proof does not use an unconditional (marginal) form of Assumption 13, because from step 2 onward $x_k$ is itself a random variable (a function of the history $\xi_{[k-1]}$), so the cross-term $\mathbb{E}[\langle\delta_k,g_{X,k}\rangle]$ the proof needs to vanish requires a conditional statement — "$\mathbb{E}[\langle\delta_k,g_{X,k}\rangle\mid\xi_{[k-1]}]=0$" is the book's own phrasing. A formalization using only marginal moment bounds would either be unprovable as stated or, worse, would misstate the theorem by using hypotheses too weak for the claimed conclusion.

Formalization scope

generalized_projection_gradient_bound, generalized_projection_characterization, nonconvex_md_bound and nonconvex_md_rate are stated over a real inner product space (Chapter 6's own generality — unlike Chapter 3, §6.2.3 explicitly restricts to "the norm associated with the inner product"), with every argmin-defined point ($x^+$, and the iterate sequence $x_k$) represented by its pointwise minimality property rather than an argmin term, consistent with this series' convention. The goal theorem, rsmd_complexity_bound, additionally introduces a probability space (Ω,P) and a Mathlib Filtration ℕ 𝒢, with x k/G k required 𝒢(k-1)-strongly-measurable and Assumption 13 stated via MeasureTheory.condExp (𝒢 (k-1)) (conditional mean 0, conditional second moment ≤ σ²/m_k) — the conditional form the book's own proof actually needs, not a weaker marginal substitute. The σ²/m_k bound is (6.2.40)'s conclusion for the m_k-sample batch average, taken as a hypothesis on the already-averaged G k directly rather than re-derived from m_k raw i.i.d. calls (that derivation is not itself a numbered result of the book). $R$'s independence from the process is stated via ProbabilityTheory.IndepFun; every integrability side condition the conclusion's Bochner integral needs to be non-vacuous is stated explicitly, guarding against the well-known trap of an uninhabited/non-integrable hypothesis silently defaulting condExp/the integral to 0 and making the theorem trivially true.

A trivializing formalization this mission rules out: taking $X=\mathbb{R}^n$ and $h\equiv0$ throughout would make every generalized projection collapse to the ordinary gradient, reducing this entire mission to a restatement of plain (stochastic) gradient descent — exactly the ShiOptRates results already on the platform — rather than the constrained composite theory the chapter develops; $X$, $h$ and $V$ are kept as genuine free parameters in every milestone and the goal.

Left out of scope, for time: Theorem 6.6(b) (the convex-case corollary on $\mathbb{E}[\Psi (x_R)-\Psi(x^*)]$, requiring the nondecreasing/nonincreasing stepsize side-conditions of (6.2.33)/(6.2.35)); the raw-sample derivation of (6.2.40); Lemma 6.3 (the stationarity consequence of a small gradient mapping, using $\partial h$ and the normal cone $N_X$); the 2-RSMD algorithm and its large-deviation improvement; and the gradient-free (RSMDF) variant.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, §6.2. https://doi.org/10.1007/978-3-030-39568-1
• S. Ghadimi and G. Lan, "Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming," SIAM Journal on Optimization, 23(4), 2013, pp. 2341–2368.
• S. Ghadimi, G. Lan and H. Zhang, "Mini-batch Stochastic Approximation Methods for Nonconvex Stochastic Composite Optimization," Mathematical Programming, 155(1–2), 2016, pp. 267–305 (the RSMD algorithm's original source).

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

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$:

$$\tilde x_t = (1-q_t)\bar x_{t-1}+q_tx_{t-1},\quad x_t = \arg\min_{x\in X}\{\gamma_t[\langle f'(\tilde x_t),x\rangle+\mu V(\tilde x_t,x)]+V(x_{t-1},x)\},\quad \bar x_t = (1-\alpha_t)\bar x_{t-1}+\alpha_tx_t.$$

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$:

$$f(\bar x_k) - f(x^*) \le \frac{4L}{k(k+1)}V(x_0,x^*).$$

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

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

Two-stage stochastic linear programming with recourse models a decision made before uncertainty resolves (the first-stage variables $x$) followed by a corrective decision made after (the second-stage, or recourse, variables $y$). Solving such a program means minimizing $c^{\mathsf T}x + Q(x)$, where $Q(x)$ is the expected cost of the best recourse action given $x$ -- an object defined only implicitly, as the value of an embedded linear program that must be solved (or bounded) for every realization of the uncertain data. Before any algorithm for this problem can be justified -- the L-shaped method, stochastic decomposition, scenario decomposition, all developed in later chapters of Birge & Louveaux, Introduction to Stochastic Programming (Springer, 2011) -- one needs to know that $Q$ is well-behaved enough to optimize over at all: that the feasible region is closed and convex, that $Q$ itself is a finite, Lipschitz, convex function on it, that an optimal solution is actually attained rather than only approached in the limit, and finally what an optimality condition for the resulting nonsmooth convex program even looks like. This mission formalizes exactly that foundational layer, Chapter 3, Section 3.1 of the book.

Setting

Fix natural numbers $n_1, n_2, m_1, m_2$ and a finite scenario count $K$. A two-stage recourse instance consists of first-stage data $A \in \mathbb{R}^{m_1 \times n_1}$, $b \in \mathbb{R}^{m_1}$, $c \in \mathbb{R}^{n_1}$, a fixed recourse matrix $W \in \mathbb{R}^{m_2 \times n_2}$, and, for each scenario $k = 1,\dots,K$, a cost vector $q_k \in \mathbb{R}^{n_2}$, a right-hand side $h_k \in \mathbb{R}^{m_2}$, a technology matrix $T_k \in \mathbb{R}^{m_2 \times n_1}$, and a probability $p_k \ge 0$ with $\sum_k p_k = 1$ (Eq. (1.1)). The first-stage feasible region is $K_1 = \{x \mid Ax = b,\ x \ge 0\}$.

For a fixed $x$ and scenario $k$, the second-stage value is

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

(Eq. (1.6)), taken as an extended real: $+\infty$ if no feasible $y$ exists, $-\infty$ if the inner program is unbounded below. The expected recourse value is $Q(x) = \sum_k p_k\, Q(x,\xi_k)$ (Eq. (1.3)), combined so that $+\infty + (-\infty) = +\infty$ -- the book's own convention (p. 109): infeasibility in one scenario is treated as fatal even if another scenario is unboundedly favorable. The second-stage feasibility set is $K_2 = \{x \mid Q(x) < \infty\}$, and the deterministic-equivalent objective is $z(x) = c^{\mathsf T}x + Q(x)$ (Eq. (1.2)). For $x$ with $Q(x)$ finite, the subdifferential $\partial Q(x)$ is the set of $\eta$ satisfying $Q(x) + \eta^{\mathsf T}(y-x) \le Q(y)$ for every $y$ (p. 115).

A simple-recourse instance is the special case $W = [I,-I]$: the recourse cost splits as $q = (q^+,q^-)$, and $Q(x)$ decomposes componentwise via the closed form of Eq. (1.9)-(1.10) using the (left- and right-limit) distribution functions $F_i^-, F_i^+$ of each $h_i$.

Formalization targets

Goal -- Chapter 3, Theorem 9 (p. 116)

$$x^* \in K_1 \text{ is optimal in (1.2)} \iff \exists\, \lambda^* \in \mathbb{R}^{m_1},\ \mu^* \in \mathbb{R}^{n_1}_{\ge 0},\ (\mu^*)^{\mathsf T}x^* = 0,\ \text{ s.t. } -c + A^{\mathsf T}\lambda^* + \mu^* \in \partial Q(x^*),$$

given that (1.2) has a finite optimal value. This is the KKT-style necessary and sufficient optimality condition for the two-stage recourse LP, and the weakest of the mission's targets in the sense that everything else supports it: convexity and finiteness of $Q$ (Theorem 6) are what make the left-to-right implication meaningful, closedness/convexity of $K_2$ (Theorem 5) makes the feasible region well-posed, and attainment (Theorem 8) is what makes "$x^*$ is optimal" a statement about a point that exists rather than an infimum that may not be reached.

Supporting milestones

• Theorem 5(a) (p. 111): $K_2$ is closed and convex.
• Theorem 6(a) (p. 112): $Q$ is finite on $K_2$, and Lipschitzian and convex there.
• Theorem 8 (p. 115): under boundedness of $K_1 \cap K_2$ or eventual linearity of $Q$ along recession directions, a finite optimal value is attained.
• Corollary 10 (p. 116): Theorem 9 specialized to simple recourse, with $\partial Q(x^*)$ replaced by its explicit componentwise description.

Significance

Theorem 9 is the hinge on which the rest of the book's algorithmic chapters turn. The L-shaped method (Chapter 5) is a cutting-plane scheme whose cuts are literally elements of $\partial Q(x)$; stochastic decomposition and sampling-based methods use the same subdifferential structure with estimated cuts; the differentiable specialization (Eq. (1.14), $c + \nabla Q(x^*) = A^{\mathsf T}\lambda^* + \mu^*$) underlies nonlinear-programming approaches to the smooth case. None of this is meaningful without first knowing $Q$ is convex, finite where it needs to be, and that a minimizer exists to characterize. Formalizing this mission's four milestones from the actual definition of $Q$ as an embedded linear program's value -- rather than assuming these properties -- is exactly the content the book itself proves (or, for Theorem 6, explicitly cites to Wets [1972] and Kall [1976] rather than proving); this mission asks for genuine Lean proofs of Theorems 5, 8, 9 and Corollary 10 from the LP structure of $Q$, and records Theorem 6 as a stated (not re-derived) input, matching the book's own presentation.

Difficulty

The obvious shortcut is to treat $Q$ as an opaque convex function and apply a textbook convex-KKT theorem off the shelf. This fails to capture what Theorem 9 actually is: a statement about the specific function $Q(x) = \sum_k p_k \min_y\{q_k^{\mathsf T}y \mid Wy = h_k - T_k x,\ y \ge 0\}$, built from finitely many parametric linear programs, each of which can be infeasible ($Q(x,\xi_k) = +\infty$) or unbounded ($Q(x,\xi_k) = -\infty$) depending on $x$. Convexity of $Q$ must come from convexity of the value function of a parametric LP in its right-hand side (the book's Theorem 2 argument: a convex combination of optimal solutions at two right-hand sides is feasible, hence suboptimal, at the combined right-hand side) -- not from an assumed hypothesis. Handling $\pm\infty$ correctly is a second, easy-to-miss source of error: the book fixes an explicit, non-default convention ($+\infty$ dominates $-\infty$) for combining per-scenario values, the opposite of the convention Mathlib's own extended-real arithmetic uses, so any formalization that reaches for EReal's built-in addition to aggregate $Q$ silently states a different theorem. Theorem 8's attainment condition is a genuine existence result, not an automatic consequence of convexity: continuity alone does not give attainment on an unbounded feasible region, and the book's own counterexample (Eq. (1.11), a negative-exponential tail with infimum $0$ attained by no finite $x$) shows the boundedness/recession hypotheses are load-bearing.

Formalization scope

The scenario set is modeled as Fin K, a finite discrete random variable, matching Section 3.1b's development; under this model "$\xi$ has finite second moments" (the standing hypothesis of Theorems 4-11 in the general, possibly-continuous case) holds automatically and so does not appear as a separate hypothesis anywhere in this mission. Q(x,\xi_k) is defined as an EReal via sInf of the second-stage LP's feasible objective values -- sInf of the empty set is ⊤, and of a set unbounded below is ⊥ -- and is genuinely derived from that inner minimization rather than assumed convex; this rules out the chapter's trivializing formalization, which the paper-level triage explicitly warns against: taking Q(x) as an opaque convex-function hypothesis instead of deriving its properties from the inner LP's structure. Aggregating the $K$ per-scenario values into $Q(x)$ uses a bespoke bookAdd operation implementing the book's stated convention $+\infty+(-\infty)=+\infty$, since Mathlib's EReal addition is defined with the opposite convention ($\bot+\top=\top+\bot=\bot$). $\partial Q(x)$ is the ordinary subgradient-inequality set for this extended-real-valued function.

Theorem 8's condition (b) is stated with the book's own quantifier structure: the threshold $\bar\lambda$ and the recession value depend on the point $x$ and direction $v$ exactly as written, with no strengthening. Theorem 6(a)'s Lipschitz bound is stated, not derived -- the book itself cites it to Wets [1972] and Kall [1976] without proof -- so a faithful Lean proof of that milestone is expected to remain out of scope for this mission. Corollary 10 similarly takes the closed form of $\partial Q_i(x)$ from Eq. (1.10) as a hypothesis on an abstract $Q$, matching how the book itself uses (1.10) as an already-established fact rather than re-deriving it from the second-stage LP in the corollary's own proof. Theorem 11's subdifferential-decomposition result ($\partial Q(x) = E_\omega[\partial Q(x,\xi(\omega))] + N(K_2,x)$) is deliberately left out of this mission's scope: it is not needed by Theorem 9's own proof, and its normal-cone term would require relatively-complete-recourse machinery this mission does not otherwise need. No prior-art match was found on the platform: VectorSpaceOpt.fenchel_duality and the Luenberger-derived VectorSpaceOpt.generalized_kuhn_tucker / kkt_complementary_slackness family use a differentiable (Gateaux-derivative) or conjugate-function KKT model over general normed spaces, not this chapter's finite-dimensional, possibly-nondifferentiable subgradient formulation over the specific polyhedral set $K_1$, so none is a faithful match and all items here are original drafts.

Selected references

• J.R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4
• R.J-B. Wets, "Programming Under Uncertainty: The Equivalent Convex Program," SIAM Journal on Applied Mathematics 14 (1966), 89-105 (Lipschitz continuity of the recourse function, cited by the book as Wets [1972] for the closely related result used in Theorem 6). https://doi.org/10.1137/0114008
• D.P. Walkup and R.J-B. Wets, "Stochastic Programs with Recourse," SIAM Journal on Applied Mathematics 15 (1967), 1299-1314 (finiteness of the recourse function and coincidence of the possibility and expectation feasibility sets, underlying Proposition 3 and Theorem 4). https://doi.org/10.1137/0115113