Operations Research

Motivation

A decision-maker has $n$ projects, each a Markov reward process, and at every decision time may advance exactly one of them; the others stay frozen. Which project to advance so as to maximize the expected total discounted reward? Posed as a dynamic program the problem has a state space that is the product of the $n$ state spaces, and the size of that product defeats every general method. The index theorem of Gittins and Jones (1974) says the dynamic program is solved exactly by an index policy: there is a real number $\nu(B, x)$, computable for each bandit process $B$ from its own data and its own current state $x$, such that always advancing a process of greatest index is optimal. Chapter 2 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), introduces the index, proves the theorem three times, and works out the properties of the index that the rest of the book, from jobs and superprocesses to restless bandits, is built on: which stopping time attains it, how it is computed, how it moves with the discount factor, and when it collapses to the myopic rule.

The index theorem itself is already on the platform, proved, as BanditAlgorithm.gittins_index_theorem in the Bandit Algorithms series (Lattimore and Szepesvári, Theorem 35.9). This mission cites it and formalizes what Chapter 2 establishes around it.

Setting

A bandit process $B$ (§2.3–2.4) is a Markov reward process on a countable state space $E$: transition probabilities $P(y \mid x)$, a bounded reward $r(x)$ received each time the continuation control is applied in state $x$, and a discount factor $a \in (0, 1)$; the freeze control leaves the state unchanged and yields nothing. The law of the process started at $x$ is $\mathbb{P}_x$ and $x(t)$ is its state at process time $t = 0, 1, 2, \dots$. A stopping time $\tau$ is a past-measurable rule for switching from continuation to freezing, taking values in $\{1, 2, \dots\} \cup \{\infty\}$. For such $\tau$, $R_\tau(B, x) = \mathbb{E}_x[\sum_{t < \tau} a^t r(x(t))]$ is the expected discounted reward and $W_\tau(B, x) = \mathbb{E}_x[\sum_{t < \tau} a^t]$ the expected discounted time; their ratio $\nu_\tau(B, x)$ (2.7) is the equivalent constant reward rate of that portion of $B$. The Gittins index is

$$\nu(B, x) = \sup_{\tau > 0} \frac{R_\tau(B, x)}{W_\tau(B, x)} \tag{2.6}$$

and, equivalently, the fair charge (2.5): the greatest rent $\lambda$ per period for which continuing $B$ for one or more periods, paying $\lambda$ each period, can be done without expected loss. A simple family of alternative bandit processes (SFABP) is $n$ such processes with a common discount factor, one of which is continued at each decision time; an index policy continues a process of greatest index. In the Lean development the single-arm model is the platform's (GittinsIndex): the chain law is built by the Ionescu–Tulcea construction, stopping times are adapted $\mathbb{N}\cup\{\infty\}$-valued maps on trajectories, and gittinsIndex P r a x is (2.6).

Formalization targets

Goal: Lemma 2.2, the optimal stopping set

The supremum in (2.6) is attained. For the initial state $\xi$, the attaining stopping rule may be taken to be "stop at the first time $t \ge 1$ at which the state lies in $\Sigma_0$" for any set $\Sigma_0$ with

$$\{x : \nu(B, x) < \nu(B, \xi)\} \subseteq \Sigma_0 \subseteq \{x : \nu(B, x) \le \nu(B, \xi)\},$$

and every such rule has $\nu_\tau(B, \xi) = \nu(B, \xi)$.

Milestones

Theorem 2.1 as a reference to the proved platform theorem; Eq. (2.5), the fair-charge characterization of the index; the restart-in-state formulation of §2.6.4 as the convergence of the Katehakis–Veinott value iteration; Theorem 2.3, monotonicity in the discount factor; Lemma 2.4, the interchange of two bandit portions; Propositions 2.5–2.8, the monotone-index cases in which the index is the immediate reward, or is attained only after the first step, or only at $\tau = \infty$.

Significance

Lemma 2.2 is the working form of the index: it turns the supremum over all stopping times into a specific rule, the first time the index falls below its starting value, and it is what the interchange proof of §2.7, the modified-forwards-induction policies of §2.6.6, the monotone-index propositions of §2.11 and the treatment of jobs in Chapter 3 all use. The fair-charge form (2.5) is the prevailing-charge proof of the theorem (Weber 1992) and the interpretation that carries over to superprocesses and restless bandits. The restart formulation is how indices are computed in practice (Katehakis and Veinott 1987), and Theorem 2.3 is the first of the comparative statics used throughout Chapters 7 and 8. Lemma 2.4 is the elementary inequality behind the original proof of Gittins and Jones.

Of these, only the index theorem has a machine-checked proof today. Formalizing the rest gives the platform the index as a usable object: a characterization of the optimal stopping rule, a convergent algorithm for it, and the monotonicity facts, all stated against the existing model so that every later mission of this series and every future use of the L&S model can build on them.

Difficulty

The obvious first move for Lemma 2.2, "take the stopping time that achieves the supremum", is what has to be proved: the supremum is over an uncountable family, and attainment comes from the optimal stopping problem with charge $\lambda = \nu(B, \xi)$, whose value function satisfies $\varphi(x) = \max\{0, r(x) - \lambda + a\mathbb{E}[\varphi(x(1)) \mid x(0) = x]\}$, together with the fact that its optimal stopping set is characterized by the strict and non-strict inequalities $\lambda > \nu(B, x)$ and $\lambda \ge \nu(B, x)$. That last step is the content: it identifies the local decision "stop or continue" with a comparison of indices, which is why any set between the two level sets works. On the platform's model this requires the dynamic-programming theory of discounted optimal stopping on a countable space (Theorem 2.10 of the book), the identification of fairChargeProfit with that value function, and the strong Markov property of markovChainMeasure at a trajectory stopping time. Theorem 2.3 needs randomized stopping times (a geometric kill) and the fact that they do not enlarge the supremum. The restart iteration is monotone and bounded but its operator is not a contraction in the restart value, so its limit has to be identified with the restart problem's value directly; that value is $\max(0, \nu/(1-a))$, not $\nu/(1-a)$, because restarting forever is free.

Formalization scope

The state space is a countable type with measurable singletons, so every subset is measurable; rewards are bounded; $a \in (0, 1)$. The chain law, stopping times, the discounted stopped sums and the index are the platform's, unchanged. Expectations are Bochner integrals; with bounded rewards they are finite and no total-function default value enters. IsPositiveStoppingTime fixes $\tau \ge 1$ everywhere, so $W_\tau \ge 1$ and the ratio (2.7) is a genuine quotient. The stopping rule of Lemma 2.2 is the hitting time from time $1$ of a set, with $\infty$ when the set is never hit. The fair-charge profit is a real supremum over the nonempty bounded family of positive stopping times, and (2.5) is stated with the outer supremum over $\{\lambda : \text{profit}(\lambda) \ge 0\}$, a nonempty set bounded above. The restart iteration is stated as a limit, with the value $\max(0, \nu(B, \xi)/(1-a))$: for a nonnegative index this is the book's $\nu/(1-a)$, and the maximum is forced by a one-state example with negative reward. The propositions' hypotheses are almost-sure events under $\mathbb{P}_x$, written as events of measure one.

Two trivializing readings are excluded: the index is never taken over all $\mathbb{N}\cup\{\infty\}$-valued maps but over adapted stopping times, and the stopping set of the goal is not restricted to the two extreme level sets. Contributions welcome: the optimal-stopping dynamic program on markovChainMeasure (value iteration, the strong Markov property at a stopping time), the equivalence of randomized and non-randomized stopping times for the supremum, and the monotone convergence of the restart iteration.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 2. doi:10.1002/9780470980033
• J. C. Gittins, D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (Gani, ed.), North-Holland, 1974.
• R. Weber, On the Gittins index for multiarmed bandits, Annals of Applied Probability 2(4), 1992. doi:10.1214/aoap/1177005588
• M. N. Katehakis, A. F. Veinott, The multi-armed bandit problem: decomposition and computation, Mathematics of Operations Research 12(2), 1987. doi:10.1287/moor.12.2.262
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401

Which fares to open, and when to close them

An airline sells one flight, a hotel one night, a car-rental firm one day of one car: a fixed capacity, perishable at a deadline, sold to customers who arrive over time and are willing to pay different amounts. Chapter 2 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) is the theory of that single resource. Its three models answer the same question with increasing generality: Littlewood's two-class rule, the $n$-class static model and its dynamic-arrival version give the seller a protection level per class, a booking limit or a bid price, all three equivalent; the discrete-choice model, in which customers buy down when a cheaper fare is open, replaces classes by offer sets and shows that only the efficient sets, ordered by their purchase probability, are ever offered, with a higher set the more capacity or the less time remains. This mission formalizes that last result, Theorem 2.3, together with the structural results of the two earlier models that it generalizes.

Setting

Static model. Classes $1, \dots, n$ with prices $p_1 \ge \dots \ge p_n \ge 0$ arrive in stages, lowest class first, with demands $D_j$ distributed on $\mathbb N$. With $x$ units left at stage $j$ the seller observes $D_j$ and accepts $u \le \min\{D_j, x\}$ units; the value function is the Bellman equation (2.3), $V_j(x) = \mathbb E[\max_u \{p_j u + V_{j-1}(x-u)\}]$, $V_0 = 0$ (staticValue), and $\Delta V_j(x) = V_j(x) - V_j(x-1)$ is the marginal value of capacity. The protection level $y_j^* = \max\{x : p_{j+1} < \Delta V_j(x)\}$ (protLevel), the booking limit $b_j^* = C - y_{j-1}^*$ (bookLimit) and the bid price $\pi_{j+1}(x) = \Delta V_j(x)$ (bidPrice) define the three controls of Theorem 2.1.

Dynamic model. Over $T$ periods at most one request arrives per period, of class $j$ with probability $\lambda_j(t)$; the value function (2.17) is $V_t(x) = V_{t+1}(x) + \mathbb E[\max_{u \in \{0,1\}} (R(t) - \Delta V_{t+1}(x))u]$ (dynValue), with time-dependent protection levels (2.19), booking limits (2.20) and bid prices (2.18).

Choice model. When the set $S$ of classes is open an arriving customer buys class $j \in S$ with probability $P_j(S)$; $Q(S) = \sum_{j \in S} P_j(S)$ is the purchase probability and $R(S) = \sum_{j \in S} P_j(S) p_j$ the expected revenue (purchaseProb, expRevenue). The value function (2.26) is $V_t(x) = \max_{S} \lambda_t (R(S) - Q(S)\Delta V_{t+1}(x)) + V_{t+1}(x)$ (choiceValue). A set $T$ is inefficient (Definition 2.1, IsInefficient) if a randomization $\alpha$ over the subsets has $\sum_S \alpha(S) Q(S) \le Q(T)$ and $\sum_S \alpha(S) R(S) > R(T)$, and efficient otherwise.

Formalization targets

Goal: Theorem 2.3

In every period with capacity left, some efficient set maximizes (2.26); and, the efficient sets being ordered by $Q$, the largest optimal set is nondecreasing in the remaining capacity $x$ and nondecreasing in the period $t$: choice_optimal_policy. Monotonicity is stated as "every efficient optimal set at $(t, x)$ is matched by one at $(t, x')$, $x' \ge x$, with at least as large a purchase probability", and likewise in $t$.

Supporting targets

Littlewood's rule (2.1), $\Delta V_1(x) = p_1 \mathbb P(D_1 \ge x)$ and the acceptance criterion; Proposition 2.1, the marginal values of the static model are decreasing in $x$ and increasing in the stages remaining; Theorem 2.1, nested protection levels, nested booking limits and bid-price tables each attain the Bellman maximum at every stage; Proposition 2.2 and Theorem 2.2, the same two results for the dynamic model, with marginal values now decreasing in time; Proposition 2-2.A.4 of the appendix, the marginal values of the choice model are decreasing in $x$ and in $t$; Proposition 2.3, an inefficient set is never optimal; and the ordering of efficient sets, $Q(S) \le Q(S')$ implies $R(S) \le R(S')$ when $S'$ is efficient.

The continuous-demand optimality conditions (2.9) of Sect. 2.2.2.3, stated without proof, the computational and heuristic methods of Sects. 2.2.3-2.2.4, the overbooking models of Sect. 2.7 and the nested-policy characterization of Sect. 2.6.2.5 are not targets.

Significance

Theorem 2.3 is the structural result behind choice-based revenue management: it reduces the $2^n$ offer sets to the efficient frontier of $(Q(S), R(S))$, orders that frontier, and shows the optimal policy walks up it as capacity grows or the deadline nears. It was the analytical core of Talluri and van Ryzin's (2004) choice-model paper and is the reason the efficient sets, not the fare classes, are the unit of control when customers substitute between fares. The static and dynamic results, from Littlewood (1972) and Brumelle and McGill (1993) to Lee and Hersh (1993), are the foundation of every airline seat inventory control system; the equivalence of protection levels, booking limits and bid prices is what lets the same optimal policy be implemented on any of the three kinds of reservation system. None of these results has a machine-checked proof.

Difficulty

The two marginal-value propositions are inductions in which the inductive step is the discrete concavity of a max-plus convolution, Lemma 2-2.A.1 of the appendix: $x \mapsto \max_{0 \le a \le m}\{ap + g(x-a)\}$ is concave when $g$ is, which in Lean requires reasoning about the argmax on $\mathbb N$ and the truncated subtraction. The static model's expectation is a tsum against a pmf, so every step also needs summability of a bounded family. The protection-level theorems then need the down-set structure of $\{x : p_{j+1} < \Delta V_j(x)\}$ under monotonicity of $\Delta V_j$, and the three controls have to be shown to coincide unit by unit. For the choice model, Proposition 2.3 is a one-line convexity argument once $\Delta V \ge 0$ is known, and the monotonicity in Theorem 2.3 is a monotone comparative-statics argument on the objective $R(S) - Q(S)\Delta$, which is easy in $\Delta$ but must be combined with Proposition 2-2.A.4 in both $x$ and $t$; the existence of an efficient maximizer uses Proposition 2.3 and the finiteness of the subsets.

Formalization scope

Capacities, stages and periods are natural numbers, the value functions recurse on the stage or on the number of periods to go, and the book's ranges ($x \le C$, $t \le T$, $j \le n$) are hypotheses of the theorems. Demand in the static model is a pmf on $\mathbb N$ rather than a random variable, so the expectation in (2.3) is a tsum; the dynamic model's expectation over $R(t)$ is written out, including the no-arrival term, which vanishes under nonnegative prices. The choice model is defined by its compact form (2.26), and the maximization includes the empty offer set. Optimality of a control means attaining the inner maximum of the Bellman equation at every state, which is what the book's proofs establish. The bid-price control is formalized with the bid price $\pi_{j+1}(x + 1 - z)$ of the $z$-th unit allocated; the book prints $x - z$, which is one unit off from (2.5). The appendix's Proposition 2-2.A.4 prints its time monotonicity in the reverse direction; the formal statement is the direction consistent with Proposition 2.2 and Theorem 2.3. The ordering of efficient sets is stated with non-strict inequalities, since Definition 2.1 admits ties in revenue.

Selected references

• K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer/Springer, 2004, Chapter 2. https://doi.org/10.1007/b139000
• K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 2005. https://doi.org/10.1057/palgrave.rpm.5170134
• S. L. Brumelle and J. I. McGill, Airline seat allocation with multiple nested fare classes, Operations Research 41(1), 1993. https://doi.org/10.1287/opre.41.1.127
• T. C. Lee and M. Hersh, A model for dynamic airline seat inventory control with multiple seat bookings, Transportation Science 27(3), 1993. https://doi.org/10.1287/trsc.27.3.252
• K. T. Talluri and G. J. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• C. J. Lautenbacher and S. Stidham, The underlying Markov decision process in the single-leg airline yield-management problem, Transportation Science 33(2), 1999. https://doi.org/10.1287/trsc.33.2.136

Motivation

Regularization — adding a penalty on model complexity to an empirical risk minimization objective — is one of the oldest and most reliably effective tools in statistical learning: ridge regression, LASSO, and margin-based support vector machines all fit this template. For decades the regularization weight and penalty function were chosen heuristically or by cross-validation, with only asymptotic or worst-case generalization bounds explaining why they help. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter on Wasserstein distributionally robust optimization (DRO) gives regularization a different, non-asymptotic justification: a decision rule that is robust to adversarial perturbations of its training data, measured in Wasserstein distance, is exactly a regularized empirical risk minimizer — no approximation, no asymptotics. This mission formalizes the general form of that equivalence, Theorem 10 (p. 14), which underlies every regularization-by-robustification result the chapter derives for classification and regression alike.

Setting

Fix a normed space $\Xi = \mathbb{R}^m$, a convex loss function $\ell : \Xi \to \mathbb{R}$, a radius $\varepsilon \ge 0$, and $N$ training samples $\hat\xi_1,\dots,\hat\xi_N \in \Xi$ ($N \ge 1$). The empirical distribution is $\hat P_N = \frac{1}{N}\sum_{i=1}^N \delta_{\hat\xi_i}$. The worst-case risk of $\ell$ at radius $\varepsilon$ (eq. (6), p. 6) is

$$R_{\varepsilon,p}(\hat P_N,\ell) = \sup_{Q \in B_{\varepsilon,p}(\hat P_N)} E_Q[\ell(\xi)],$$

where $B_{\varepsilon,p}(\hat P_N)$ is the type-$p$ Wasserstein ball of radius $\varepsilon$ around $\hat P_N$ (Definition 1, p. 3) — the set of probability measures on $\Xi$ within Wasserstein distance $\varepsilon$ of the empirical distribution, under a norm $\|\cdot\|$ on $\Xi$ and its transportation exponent $p$. The Lipschitz modulus $\mathrm{Lip}(\ell) = \sup_{\xi\ne\xi'} \frac{|\ell(\xi)-\ell(\xi')|}{\|\xi-\xi'\|}$ (possibly $+\infty$) measures how fast $\ell$ can grow.

Formalization targets

Goal (Theorem 10, convex loss and $p=1$). If $\ell$ is convex and $p=1$, then the worst-case risk of $\ell$ over the type-1 Wasserstein ball around the empirical distribution coincides with the Lipschitz-regularized empirical loss:

$$R_{\varepsilon,1}(\hat P_N,\ell) = R(\hat P_N,\ell) + \varepsilon \cdot \mathrm{Lip}(\ell),$$

where $R(\hat P_N,\ell) = \frac{1}{N}\sum_{i=1}^N \ell(\hat\xi_i)$ is the ordinary empirical risk. The left side is the worst-case expected loss under adversarial perturbations of the training data of bounded aggregate Wasserstein cost; the right side is the ordinary empirical risk plus a regularization term proportional to the perturbation radius $\varepsilon$ and the loss's own Lipschitz modulus — no approximation, an exact equality for every convex $\ell$.

Significance

This is the single result underlying every specific regularization-by-robustification corollary the chapter derives — the $\ell_2$-regularized SVM and its $\ell_1$/$\ell_\infty$ variants, regularized logistic regression, and the regression analogue with a Lipschitz loss (Proposition 3) — because each of those is obtained by substituting a specific convex, Lipschitz loss (hinge, logloss, a linear-model margin loss) for the general $\ell$ here and reading off $\mathrm{Lip}(\ell)$ in closed form. Theorem 10 is exact ($p=1$, Ξ = R^m) precisely because a type-1 transportation cost is dual to the Lipschitz modulus (a consequence of the Kantorovich- Rubinstein duality this book's earlier duality theorems establish), whereas the corresponding statement for $p \ge 2$ (Theorem 11 elsewhere in the chapter) needs a strictly stronger hypothesis on $\ell$. Formalizing Theorem 10 fixes, machine-checkably, the exact scope of the equivalence — which losses qualify (convex, no boundedness or smoothness needed), which transportation exponent is required ($p=1$, not any $p\ge1$), and that the equality is exact, not an upper or lower bound — the single fact every classification- and regression-specific robustification corollary in the chapter cites without re-deriving.

Difficulty

The natural first attempt treats the worst-case risk as an instance of the general finite convex reduction (Theorem 8, which needs $\ell$ or a related concave/convex-conjugate structure and applies for a general norm exponent $p,q$ with $1/p+1/q=1$) and specializes it to $p=1$. This is not the paper's own route for Theorem 10: at $p=1$ the dual exponent $q=\infty$, and the general finite-convex-program reduction (11) degenerates in a way that is more naturally derived directly from the type-1 Wasserstein distance's own dual (Kantorovich-Rubinstein) representation — a Lipschitz test function pairs exactly with a type-1 transportation cost, which is why the answer is Lipschitz-regularization and not some other penalty. The Lean statement records only the final equality (the proof itself, via Theorem 8 or the direct Kantorovich-Rubinstein route, is left as sorry, as required for a draft item), but the choice of which milestones would support that proof is exactly this: the type-1/Lipschitz-modulus duality is a structurally different argument from the finite-convex-program machinery Theorem 8 needs for other $p$, which is why this chapter's earlier draft mistakenly tried to reach a specialization of Theorem 10 (Proposition 2, restated for a labeled, $\kappa=\infty$ ambiguity set) through a finite-atom shortcut that does not actually capture the general type-1 ball Theorem 10's own proof needs — see Formalization scope.

Formalization scope

$\Xi$ is EuclideanSpace ℝ (Fin m) (fixed to Set.univ, matching the theorem's own "Ξ = R^m" hypothesis) with an arbitrary fixed norm as a type-class parameter, not specialized to Euclidean. The worst-case risk, Wasserstein distance, ambiguity set, nominal risk, empirical distribution and Lipschitz modulus are all redefined locally in this chapter's own namespace, verbatim restatements of 01-duality's own drafts of the same objects (identical EReal/ENNReal/Integrable conventions), because 01-duality is not yet a published mission (CAPTAIN_ADDENDUM_WAVE2.md rule 5); a later upload can retire the duplication once it is live. hN : 0 < N excludes the empty-sample case the paper's own "N training samples" presupposes; hℓ : Integrable ℓ (empiricalDistribution ξhat) guards the empirical risk's Bochner integral (automatically satisfied under any real-valued ℓ since the empirical distribution is a finite convex combination of Dirac masses, but stated explicitly rather than assumed silently). No constant is pinned to a numeral. This mission originally targeted Proposition 2 (regularization by robustification for classification, p. 25), a specialization of Theorem 10 to a labeled, κ=∞ input-output ambiguity set — but that draft's κ=∞ ambiguity set restricted admissible perturbations to a finite family of exactly N atoms, each sample's entire mass moving as one indivisible unit, which is a strict, non-faithful subset of the true κ=∞ Wasserstein ball (splitting a sample's mass across several destinations is a legitimate, and for a convex loss strictly more powerful, perturbation by Jensen's inequality). This made the goal theorem false for at least one of the three loss functions (Table 1) the mission itself certified as covered (logloss), not merely narrower than the paper's claim — moderation caught this and required either a faithful general-ambiguity-set reformulation or retargeting the goal. This mission takes the latter: Theorem 10 itself, already correctly and generally stated using the unrestricted Wasserstein ball throughout, is now the goal, with no further milestone (no other numbered result in this chunk's scope is needed for Theorem 10's own statement beyond the shared definitions above). A future mission in this series can revisit Proposition 2/3 with a properly general labeled ambiguity set once that construction (label-pinned marginal plus an aggregate coupling condition on the input coordinate, rather than a finite atom family) is built.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research. https://doi.org/10.1287/educ.2019.0198
• Shafieezadeh-Abadeh, S., Esfahani, P. M., & Kuhn, D. (2015). Distributionally robust logistic regression. Advances in Neural Information Processing Systems, 28.
• Blanchet, J., Kang, Y., & Murthy, K. (2019). Robust Wasserstein profile inference and applications to machine learning. Journal of Applied Probability, 56(3), 830–857.

Motivation

A decision maker who solves a distributionally robust optimization (DRO) problem over a Wasserstein ball chooses a radius $\varepsilon$ by hand, and it is natural to ask what guarantee that choice actually buys: how large must $\varepsilon$ be, as a function of the sample size $N$ and a desired confidence level, before the resulting worst-case risk is provably not an underestimate of the true (unknown-distribution) risk? Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter answers this for the mean-covariance relaxation of Wasserstein DRO introduced via the Gelbrich hull (Section 2.3): Theorem 21 gives a concentration inequality for how fast the sample mean and covariance approach the true mean and covariance, and Theorem 22 turns that concentration bound into a finite-sample statistical guarantee for the Gelbrich risk itself. This mission formalizes both.

Setting

Fix $m \in \mathbb{N}$. Let $P$ be the unknown true distribution on $\mathbb{R}^m$ with mean vector $\mu$ and covariance matrix $\Sigma \in S^m_+$, and suppose $P$ is light-tailed: there exist $\alpha > 2$ and $A > 0$ with $E_P[\exp(\|\xi\|_2^\alpha)] \le A$. Let $\hat\xi_1,\dots,\hat \xi_N$ be $N$ independent, identically distributed samples from $P$; write $P^N$ for their joint law (the $N$-fold product measure) and $\hat\mu, \hat\Sigma$ for the resulting sample mean and sample covariance, i.e. the mean and covariance of the empirical distribution $\hat P_N = \frac{1}{N}\sum_i \delta_{\hat\xi_i}$. Recall from the Gelbrich construction the mean-covariance uncertainty set $U_\varepsilon(\hat\mu,\hat\Sigma) = \{(\mu,\Sigma) \in \mathbb{R}^m \times S^m_+ : \|\hat\mu-\mu\|_2^2 + \mathrm{Tr}[\hat\Sigma+\Sigma-2(\hat\Sigma^{1/2} \Sigma\hat\Sigma^{1/2})^{1/2}] \le \varepsilon^2\}$, and the Gelbrich risk $R_\varepsilon(\hat\mu,\hat\Sigma,\ell) = \sup_{Q \in G_\varepsilon(\hat\mu,\hat\Sigma)} E_Q[\ell(\xi)]$ of a loss function $\ell$ over the Gelbrich hull $G_\varepsilon(\hat\mu,\hat \Sigma)$.

Formalization targets

Milestone (Theorem 21, concentration inequalities II). There is $c > 1$, depending on $P$ only through $\mu,\Sigma,\alpha,A,m$ (not on any finer feature of $P$), such that for every $\eta \in (0,1]$,

$$P^N\big[(\mu,\Sigma) \in U_\varepsilon(\hat\mu,\hat\Sigma)\big] \ge 1-\eta \quad \text{whenever} \quad \varepsilon \ge \varepsilon_N(\eta) := \frac{\log(c/\eta)}{\sqrt N}.$$

Goal (Theorem 22(a), finite sample guarantees II). Under the same hypotheses, for every $\eta \in (0,1)$ and $\varepsilon \ge \varepsilon_N(\eta)$,

$$P^N\Big\{R(P,\ell) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell) \;\; \forall \ell \in L\Big\} \ge 1-\eta.$$

With probability at least $1-\eta$ over the draw of the training sample, the Gelbrich risk computed from that sample upper-bounds the true risk of every admissible loss function simultaneously — not just of one fixed $\ell$ chosen in advance. (The paper's part (b), the analogous guarantee $P^N\{R(P,\ell^\star) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell^\star)\} \ge 1-\eta$ for the specific optimizer $\ell^\star$ of the Gelbrich risk minimization problem, is not formalized in this mission — see Formalization scope.)

Significance

Theorem 22 is what makes the Gelbrich-risk relaxation of Wasserstein DRO more than a computational convenience: it certifies that solving the tractable Gelbrich risk minimization problem gives a decision whose true out-of-sample risk is, with high probability, no worse than the value the solver reports — a genuine confidence guarantee, not merely an approximation of the Wasserstein worst-case risk. Theorem 21's rate, $\varepsilon_N(\eta) = O(N^{-1/2})$, is also of independent interest: it is dimension-free (no curse of dimensionality), in contrast to the paper's earlier general-distribution concentration result (Theorem 18, out of scope for this mission) whose rate degrades with $m$. Formalizing Theorem 21 fixes, machine-checkably, the exact functional form of $\varepsilon_N(\eta)$ and the precise sense in which $c$ is "distribution-free" given $(\mu,\Sigma,\alpha,A,m)$ — a subtlety easy to state informally but easy to get wrong formally (see Difficulty).

Difficulty

The central formalization difficulty is not proving the theorems (both are left as sorry in this draft) but stating the existential constant $c$ correctly. The paper says $c$ "depends on $P$ only through $\mu,\Sigma,\alpha,A,m$" — informally, a promise that $c$ is uniform across every distribution $P$ sharing those five parameters, not merely that some $c$ exists for each $P$ separately (a vacuously true, much weaker statement obtained by naively quantifying $c$ after $P$). The correct encoding places $\exists c$ before the universal quantifier over $P$: for fixed $(\mu,\Sigma,\alpha,A,m)$, one $c$ must work for every $P$ with that mean, covariance, and tail bound. Getting this quantifier order backwards silently converts a genuine finite-sample guarantee into a triviality (FAITHFULNESS_TRAPS.md trap 8).

Formalization scope

Distributions live on EuclideanSpace ℝ (Fin m); $P^N$, the law of $N$ iid samples, is the $N$-fold product measure MeasureTheory.Measure.pi (fun _ => P) on Fin N → EuclideanSpace ℝ (Fin m) — an event about the random sample sequence is a set of such tuples, and "$P^N[\text{event}] \ge 1-\eta$" is that product measure's mass on the event set. All risk and uncertainty-set definitions (meanVector, covarianceMatrix, meanCovarianceUncertaintySet, gelbrichHull, gelbrichRisk, nominalRisk, empiricalDistribution) are redefined locally in this chapter's own namespace, matching 02-gelbrich's conventions exactly, since neither 01-duality nor 02-gelbrich is yet a published mission (CAPTAIN_ADDENDUM_WAVE2.md rule 5); a later upload can retire the duplication once those missions are live. The existential constant c is placed before the universal quantifier over P in both theorems, exactly capturing "depends on P only through µ,Σ,α,A,m" — see Difficulty. Only Theorem 22's part (a) (the uniform bound over a loss class L) is formalized; part (b) — the bound for the specific optimizer ℓ* of the Gelbrich risk minimization problem (19) — is left out, because it requires first formalizing "ℓ* is an optimizer of problem (19)" as an object (an infimum-attaining selection over a data-dependent optimization problem), which is additional infrastructure this mission's time budget did not cover; formalizing it as an unconditional bound over an arbitrary data-dependent ℓ* (dropping the optimality hypothesis) would be unfaithful — the guarantee genuinely depends on ℓ* being an optimizer, not an arbitrary measurable function of the sample. The goal theorem also carries hΞ, stating Ξ contains the support of P (the paper's own standing assumption, p. 6, for every later use of Ξ), and hLInt, an Integrable ℓ P guard for every ℓ ∈ L, matching Assumption 1 (p. 9); both were added after moderation found the goal's original statement, without them, admitted a counter-instance (Ξ = ∅ collapses the Gelbrich hull to empty and the risk supremum to ⊥, making the guarantee provably false rather than merely undisclosed). Theorem 18 (the general, dimension- dependent concentration inequality with its piecewise ε_N(η) formula) and Theorems 19/20/23 (its downstream guarantees and the asymptotic-consistency results) are out of scope for this mission, which targets the Gelbrich-risk branch (Theorems 21/22) specifically.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research. https://doi.org/10.1287/educ.2019.0198
• Fournier, N., & Guillin, A. (2015). On the rate of convergence in Wasserstein distance of the empirical measure. Probability Theory and Related Fields, 162(3), 707–738.
• Gao, R., & Kleywegt, A. J. (2023). Distributionally robust stochastic optimization with Wasserstein distance. Mathematics of Operations Research, 48(2), 603–655.

From "larger" to "larger in every direction"

Chapter I's usual stochastic order compares two real-valued random variables by "how large" they tend to be. Chapter VI lifts the same idea to random vectors: $X$ is smaller than $Y$ in the usual multivariate stochastic order if $X$ is less likely than $Y$ to land in any upper set of $\mathbb{R}^n$ — any region defined by "at least this large in every coordinate." This mission formalizes that order and its two founding characterizations: a coupling theorem (the direct $n$-dimensional generalization of Chapter I's own coupling theorem) and a common-source representation, plus two closure properties that make the order usable in practice.

The usual multivariate stochastic order

Let $X$ be a random vector taking values in $\mathbb{R}^n$ on a probability space $(\Omega,\mu)$, and let $Y$ be a random vector taking values in $\mathbb{R}^n$ on a (possibly different) probability space $(\Omega',\nu)$. $X$ is smaller than $Y$ in the usual multivariate stochastic order, written $X \le_{st} Y$, if

$$P\{X\in U\} \le P\{Y\in U\} \quad \text{for every upper set } U\subseteq\mathbb{R}^n,$$

where an upper set is one closed upward under the coordinatewise partial order on $\mathbb{R}^n$ ($x\le y$ iff $x_i\le y_i$ for every $i$). Equivalently, $X\le_{st}Y$ iff $E[\varphi(X)]\le E[\varphi(Y)]$ for every increasing $\varphi:\mathbb{R}^n\to\mathbb{R}$ (increasing with respect to that same coordinatewise order) for which the two expectations exist — the form this mission drafts as the definition, exactly parallel to the univariate order's own equivalent form.

Formalization targets

Goal: the coupling characterization (Theorem 6.B.1)

$$X \le_{st} Y \iff \exists\,(\Omega'',\rho),\ \hat X,\hat Y:\Omega''\to\mathbb{R}^n\text{ with } \hat X=_{st}X,\ \hat Y=_{st}Y,\ P\{\hat X\le\hat Y\}=1.$$

This is the direct $n$-dimensional generalization of Chunk 01's Theorem 1.A.1: a joint law on the random vectors' shared space realizing $X\le_{st}Y$ as an almost-sure coordinatewise inequality between copies. The book does not give this direction's proof here (an explicit construction appears later, in a special case irrelevant to a statements-only mission), and the claim is exactly as citable either way.

Supporting milestones

• Theorem 6.B.2, the common-source restatement: $X\le_{st}Y$ iff there is a real-valued random variable $Z$ and $\mathbb{R}^n$-valued functions $\psi_1\le\psi_2$ (coordinatewise, at every $z\in\mathbb{R}$) with $X=_{st}\psi_1(Z)$, $Y=_{st}\psi_2(Z)$ — the multivariate analogue of Theorem 1.A.2, an immediate restatement of the goal.
• Theorem 6.B.16(b), closure under conjunctions: independent $X_i\le_{st}Y_i$ ($i=1,\dots,m$) give $\psi(X_1,\dots,X_m)\le_{st}\psi(Y_1,\dots,Y_m)$ for any increasing $\psi:\mathbb{R}^k\to\mathbb{R}$ — note the codomain $\mathbb{R}$, so this closure conclusion is itself the univariate order applied to vector-valued inputs. Specializing $\psi$ to a coordinatewise sum gives closure under convolutions.
• Theorem 6.B.16(c), closure under marginalization: $X\le_{st}Y$ implies $X_I\le_{st}Y_I$ for every sub-index set $I\subseteq\{1,\dots,n\}$ — a special case of part (b), included separately for its own simple, widely-used content.

Significance

The usual multivariate stochastic order is the natural tool for comparing random vectors — costs, resource-usage profiles, portfolio returns — that must be ranked simultaneously across several coordinates rather than reduced to a single scalar summary first. It underlies simulation comparisons (via the coupling and common-source characterizations, both constructive), reliability comparisons of multi-component systems (whose component lifetimes are naturally vector-valued), and comparative-statics arguments in queueing and inventory models with several state variables. The closure properties are what make the order compositional: conjunction closure says a vector-by-vector comparison of independent inputs survives any coordinatewise-increasing post-processing, and marginalization closure says a joint comparison restricts consistently to any sub-collection of coordinates — together they are the two properties an analyst reaches for first when reducing a multivariate comparison to a more tractable one.

No platform prior art exists: GET /theorems?q=stochastic+order and q=coupling return zero genuine hits (checked at this book's triage time, re-confirmed this session). This mission restates the usual multivariate stochastic order and its two founding theorems as a self-contained foundation, in the same spirit as Chunk 01's univariate mission but independently drafted, since drafts cannot import each other's Lean.

Difficulty

The chief formalization risk this chapter's own brief flags is conflating "increasing" for $\varphi:\mathbb{R}^n\to\mathbb{R}$ with some order other than the coordinatewise one (a total order via a fixed embedding, or a lexicographic order): the book's order on $\mathbb{R}^n$ is always the componentwise partial order, and Mathlib gives Fin n → ℝ exactly that order by default (its Pi/product order), so Monotone φ for φ : (Fin n → ℝ) → ℝ already means what the book means with no extra predicate to get wrong — but it would be easy to instead encode ℝ^n-valued objects some other way (e.g. a fixed linear functional into ℝ) that silently swaps in a different, weaker order. The second risk is Theorem 6.B.16(b)'s literal codomain: the book states $\psi:\mathbb{R}^k\to\mathbb{R}$ (scalar), so the closure conclusion is a genuinely univariate stochastic-order statement about $\psi$ applied to vector inputs, not a vector-to-vector closure (that is part (a), not drafted here) — stating it as a multivariate conclusion by mistake would silently strengthen a theorem the book does not claim.

Formalization scope

Random vectors are drafted as functions into Fin n → ℝ from arbitrary measurable spaces, which inherit Mathlib's default coordinatewise (Pi) order — the same order the book uses throughout this chapter, requiring no separate order predicate. MultivariateOrder μ ν X Y quantifies over φ : (Fin n → ℝ) → ℝ with Monotone φ in that order and Integrable (φ ∘ X) μ/Integrable (φ ∘ Y) ν stated inside the ∀, exactly matching "for which the expectations exist." Equality in law is ProbabilityTheory.IdentDistrib. Theorem 6.B.2's random variable $Z$ is drafted as $\mathbb{R}$-valued specifically (not an arbitrary-type common source), matching the book's own "for all $z\in\mathbb{R}$" quantification exactly.

Theorem 6.B.16(b) is drafted for a common dimension $n$ across all $X_i,Y_i$ rather than the book's per-$i$ dimension $k_i$: the concatenated input then lives in Fin m → Fin n → ℝ (nested Pi types, carrying the coordinatewise order on $\mathbb{R}^{mn}$ exactly as needed), avoiding a dependent-sum concatenation of vectors of genuinely different lengths that a mission of this size does not justify. This is the "closed under convolutions" special case the book itself names as a corollary of the general statement, not a different claim — but it is a genuine restriction of scope, recorded here rather than silently applied, and the general varying-dimension statement is left for a future pass (see STATUS.md). The theorem's conclusion is stated as the univariate order's own defining inequality on ℝ (∀ x, μ {ω | x < ψ(X_∙ ω)} ≤ ν {ω | x < ψ(Y_∙ ω)}), restated locally rather than importing Chunk 01's UsualOrder, since drafts cannot import another mission's definitions. Theorem 6.B.16(c)'s sub-index set $I\subseteq\{1,\dots,n\}$ of size $k$ is encoded as an injective reindexing r : Fin k → Fin n, with $X_I,Y_I$ drafted as X, Y precomposed coordinatewise with r, matching the book's own subvector notation (6.A.1) exactly.

A trivializing formalization this mission rules out: drafting MultivariateOrder with an order on Fin n → ℝ other than the coordinatewise one (for instance, a fixed linear functional collapsing the vector to a scalar and reusing the univariate order), which would silently state a different, generally weaker order under the same name; and drafting Theorem 6.B.16(b)'s conclusion with a vector-valued (rather than the book's literal scalar-valued) $\psi$, which would silently strengthen a theorem the book states only for real-valued $\psi$. This mission draws on no platform prior art (searches for "stochastic order" and "coupling" as of 2026-09-18 return zero genuine matches). Reusable beyond this mission: the MultivariateOrder definition pattern and its coupling/common-source characterization parallel Chunk 01's univariate pair closely enough that a future chapter needing a multivariate order's own coupling theorem (Chapter VII's multivariate convex order is the direct next instance in this series) could restate the same shape with minimal adaptation.

Selected references

• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007, Chapter 6 (Multivariate Stochastic Orders), §6.A–6.B. https://doi.org/10.1007/978-0-387-34675-5
• This series' Chunk 01 (StochasticOrders.Usual), for the univariate usual stochastic order and its coupling/common-source characterizations this chapter directly generalizes.

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

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

Setting

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

Formalization targets

Goal — Theorem 4.1

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

Supporting milestones, in attack order

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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