The OR Formalization Drive

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

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

Composite convex programs — objectives split into a smooth piece and a nonsmooth piece — are ubiquitous in data analysis: LASSO-type inverse problems, regularized empirical-risk minimization, and total-variation-type image reconstruction all minimize $f(x)+h(x)+\chi(x)$ over a convex set, where $f$ is smooth (a data-fidelity term, often expensive to differentiate — a large matrix-vector product, a PDE solve, a black-box simulation), $h$ is nonsmooth but structurally cheap (an $\ell_1$-type penalty, a simple subgradient), and $\chi$ enforces a "relatively simple" constraint absorbed into the proximal step. Classical accelerated proximal-gradient methods (Nesterov; Beck–Teboulle) solve such problems by computing $\nabla f$ and a subgradient $h'$ once per iteration, giving an optimal $O(1/\varepsilon^2)$ bound on evaluations of both. But in every example above, the two oracle calls have wildly different costs, and paying for $\nabla f$ as often as for $h'$ is wasteful. Ghadimi, Lan and Zhang (SIAM J. Optim., 2014, arXiv:1406.5613, "Generalized Uniformly Optimal Methods for Nonlinear Programming") posed the resulting question: given separate first-order access to $f$ and $h$, can the number of $\nabla f$-evaluations be reduced without inflating the (already-optimal) number of $h'$-evaluations? The gradient sliding (GS) algorithm formalized here, from Lan's textbook treatment (Chapter 8, building on Lan's own 2016 Mathematical Programming paper "Gradient sliding for composite optimization"), answers this in the affirmative: it "slides" past $\nabla f$-evaluations on most iterations while still achieving the optimal $O(1/\varepsilon^2)$ subgradient count for $h'$.

Setting

Fix a real inner-product space $E$ and a closed convex set $X\subseteq E$. The composite problem is

$$\Psi^* \equiv \min_{x\in X}\{\Psi(x) := f(x)+h(x)+\chi(x)\}, \qquad (8.1.1)$$

where $\chi$ is a "relatively simple" convex function (its own proximal step is assumed cheap), $f:X\to\mathbb R$ is convex with $L$-Lipschitz gradient,

$$f(x)\le f(y)+\langle\nabla f(y),x-y\rangle+\tfrac L2\|x-y\|^2, \qquad \forall x,y\in X, \quad (8.1.2)$$

and $h:X\to\mathbb R$ is convex and $M$-Lipschitz-like in the sense that for every subgradient $h'(y)\in\partial h(y)$,

$$h(x)\le h(y)+\langle h'(y),x-y\rangle+M\|x-y\|, \qquad \forall x,y\in X. \quad (8.1.3)$$

Let $V(a,b)$ be a Bregman-type prox-function built from a 1-strongly-convex distance-generating function $\nu$ (Sect. 3.2), so $V(a,b)\ge\tfrac12\|b-a\|^2$.

The gradient sliding (GS) algorithm (Algorithm 8.1) keeps an outer iterate $x_k$, model point $g_k(\cdot)\equiv l_f(x_k,\cdot):=f(x_k)+\langle\nabla f(x_k),\cdot-x_k\rangle$, and running average $\bar x_k$ ($\bar x_0=x_0$). Each outer step $k=1,\dots,N$ delegates to the prox-sliding (PS) procedure: given the affine model $g_k$, prox-center $x_{k-1}$, parameter $\beta_k$, and sliding length $T_k$, PS runs $T_k$ inner iterations

$$u_t = \arg\min_{u\in X}\{g(u)+l_h(u_{t-1},u)+\beta V(x,u)+\beta p_tV(u_{t-1},u)+\chi(u)\}, \qquad \tilde u_t = (1-\theta_t)\tilde u_{t-1}+\theta_tu_t, \quad (8.1.17)\text{--}(8.1.18)$$

where $l_h(y;u):=h(y)+\langle h'(y),u-y\rangle$ (8.1.14), without ever recomputing $\nabla f$ during these $T_k$ steps — the single affine model $g$ is reused throughout. This is the mechanism by which GS "slides" past most $\nabla f$-evaluations. PS returns $(x_k,\tilde x_k)$, and the outer loop updates $\bar x_k=(1-\gamma_k)\bar x_{k-1}+\gamma_k\tilde x_k$.

Formalization targets

Building block (Proposition 8.1)

$$\beta(1-P_t)^{-1}V(u_t,u)+[\Phi(\tilde u_t)-\Phi(u)] \le P_t(1-P_t)^{-1}\Big[\beta V(u_0,u)+ \frac{M^2}{2\beta}\sum_{i=1}^t(p_i^2P_{i-1})^{-1}\Big], \quad \forall u\in X, \, t\ge1,$$

where $\Phi(u):=g(u)+h(u)+\beta V(x,u)+\chi(u)$ and $\{p_t\},\{\theta_t\},\{P_t\}$ satisfy the recursion (8.1.20). This is the per-inner-iteration guarantee on how close $(u_t,\tilde u_t)$ comes to solving $\Phi$'s own minimization.

Intermediate (Theorem 8.1(a))

Assuming the PS schedule (8.1.20) and GS schedule conditions (8.1.25), (8.1.33) (the case where $X$ may be unbounded),

$$\Psi(\bar x_N)-\Psi(x^*) \le \frac{\Gamma_N\beta_1}{1-P_{T_1}}V(x_0,x^*) + \frac{M^2\Gamma_N}{2}\sum_{k=1}^N\sum_{i=1}^{T_k}\frac{\gamma_kP_{T_k}} {\Gamma_k\beta_k(1-P_{T_k})p_i^2P_{i-1}}, \qquad \forall N\ge1,$$

a general bound in terms of the abstract schedule, obtained by telescoping Proposition 8.1's guarantee (via Proposition 8.2's per-outer-step recursion, cited but not restated here) across outer iterations.

Goal (Corollary 8.1(a))

With the concrete schedule $p_t=t/2$, $\theta_t=2(t+1)/(t(t+3))$ (8.1.39), and, for a fixed horizon $N$ and free parameter $\tilde D>0$,

$$\beta_k=\frac{2L}{k}, \qquad \gamma_k=\frac2{k+1}, \qquad T_k=\Big\lceil\frac{M^2Nk^2}{\tilde DL^2}\Big\rceil, \quad (8.1.40)$$ $$\Psi(\bar x_N)-\Psi(x^*) \le \frac{2L}{N(N+1)}\big[3V(x_0,x^*)+2\tilde D\big], \qquad \forall N\ge1. \quad (8.1.41)$$

This is the explicit-constant complexity bound: it is the weakest statement stable under changing $L,M,N,\tilde D$, obtained purely algebraically from Theorem 8.1(a)'s general bound once the schedule is plugged in.

Significance

Corollary 8.1(a), together with the schedule of $T_k$, shows the total number of outer iterations — and hence $\nabla f$-evaluations — needed for an $\varepsilon$-solution is $O(L/ \varepsilon)$, matching the optimal rate for smooth-only minimization (no penalty for the nonsmooth term's presence), while the total number of inner iterations $\sum_kT_k$ — and hence $h'$-evaluations — remains $O(1/\varepsilon^2)$, the rate that is already known to be unimprovable for nonsmooth convex minimization. GS is thus the first method (per the section's own account) to decouple the two oracle costs at their respective optimal rates, rather than paying the worse of the two for both. This underlies later chapters' extensions (accelerated gradient sliding, decentralized optimization over networks) and is directly applicable whenever a composite objective's two components have asymmetric evaluation cost, as in the LASSO-type and regularized-loss examples above. Formalizing it contributes a machine-checked account of the telescoping/recursion argument across two nested loops (outer GS, inner PS) — a pattern distinct from the single-loop accelerated-gradient arguments already in this series (Chapters 3, 7) and not otherwise present in the corpus (q=gradient sliding, q=prox sliding, q=composite optimization all return zero hits as of 2026-09-18).

Difficulty

The obvious first idea — treat the PS procedure's inexact inner solve as adding an error term to a standard accelerated-gradient argument and bound that error by the number of inner steps — fails because a naive termination criterion (the function-value optimality gap of the PS subproblem) does not yield the accelerated rate; the book's own analysis (the paragraph preceding Proposition 8.1) states this explicitly. The working criterion instead combines the optimality gap and the distance to the optimal solution, weighted by the $P_t$-sequence — this is exactly the left-hand side of (8.1.21), not a simpler quantity, and it is this specific combination that telescopes cleanly across both the inner PS loop and, subsequently, the outer GS loop.

Formalization scope

E is NormedAddCommGroup E, InnerProductSpace ℝ E; X : Set E. The Bregman divergence V, model function g/lh, and constraint function chi are hypothesis-carrying objects (functions with the defining (in)equalities as hypotheses), matching this series' convention rather than fixing them to the Euclidean/entropic special case. ps_procedure_bound (Proposition 8.1) takes the three-point inequality that the argmin in (8.1.17) yields (a standard consequence of Lemma 3.5, cited but not re-derived) as an explicit hypothesis on the sequence u, rather than proving well-posedness of the argmin itself. gs_convergence_bound (Theorem 8.1(a)) similarly takes Proposition 8.2's per-outer-step recursion (8.1.26) as a hypothesis — its own proof composes Proposition 8.1 with model-function inequalities (8.1.27)-(8.1.31) that are outside this mission's selected scope — and formalizes only part (a) (unbounded X), not part (b) (compact X, reverse monotonicity), since only (a) is on the goal's dependency path. explicit_gs_rate (Corollary 8.1(a)) uses the closed forms $P_t=2/((t+1)(t+2))$ and $\Gamma_k=2/(k(k+1))$ that the specific schedule (8.1.39)-(8.1.40) produces (8.1.44, 8.1.46 — cited, not restated), rather than the general recursion, and takes Theorem 8.1(a)'s bound, specialized to this schedule, as a hypothesis: its own content is the purely algebraic simplification (8.1.45)-(8.1.48) into the closed-form bound (8.1.41), not a re-derivation of the general theorem. The source PDF's own printed $\beta_k=2L/(\nu k)$ (8.1.40) is a text-extraction artifact (no such $\nu$-indexed quantity appears anywhere in this section); the proof's own algebra ($\gamma_k\beta_k/(\Gamma_k(1-P_{T_k}))=2L/(1-P_{T_k})$, using $\Gamma_k=2/(k(k+1))$, $\gamma_k=2/(k+1)$) is consistent only with $\beta_k=2L/k$, which is what is formalized. A trivializing formalization would fix $h\equiv0$ or $\chi\equiv0$, collapsing the composite problem to plain smooth minimization and making the entire PS-procedure apparatus vacuous; this is ruled out by keeping $h$ and $\chi$ as free convex functions throughout with hMLip an active, non-degenerate hypothesis. Proposition 8.2 (the recursion gs_convergence_bound cites) and Theorem 8.1(b) (the compact-X case) are natural extensions a further contribution could add.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, 2020, Chapter 8. https://doi.org/10.1007/978-3-030-39568-1
• G. Lan, Gradient sliding for composite optimization, Mathematical Programming 159 (2016), 201–235. https://doi.org/10.1007/s10107-015-0955-5
• S. Ghadimi, G. Lan, H. Zhang, Generalized Uniformly Optimal Methods for Nonlinear Programming, Journal of Scientific Computing, 2019 (arXiv preprint 2015). arXiv:1406.5613

Motivation

Which workers end up at which firms, and does higher quality always land at the more productive employer? This is the question of assortative matching: whether an efficient assignment pairs the best workers with the best firms, the second-best with the second-best, and so on down the line. The question has a long history in labor economics. Becker [1973] showed, for the simplest case of two-sided homogeneous firms and a single worker characteristic, that profit maximization under complementarity forces exactly this kind of sorting. Kremer [1993] extended the analysis to firms with many workers of a single type, under a specific Cobb–Douglas production function. What was missing was a general theory: one that covers firms hiring several types of workers simultaneously, firms that differ in efficiency, and labor markets of any degree of tightness, while still deriving sorting from a single primitive economic condition rather than from functional-form assumptions.

Topkis's Chapter 3, §3.2 supplies exactly that theory, as an application of the book's central tool — supermodularity — to the assignment problem. The condition that drives every result in this mission is a single complementarity hypothesis on the firms' profit functions: no concavity, no differentiability, no specific functional form. That a purely order-theoretic hypothesis pins down the qualitative shape of an optimal assignment is the mission's central content, and the platform currently has no lattice-theoretic treatment of matching at all — its one matching result formalizes Gale–Shapley two-sided stable matching by preference, an entirely different mechanism (see Formalization scope below).

Setting

Fix $n$ worker types, indexed $i = 1,\dots,n$, each with a lattice $X_i$ of available worker qualities, and $m$ firms, indexed $j = 1,\dots,m$. A matching assigns to each firm $j$ a vector of qualities $x^j = (x^j_1,\dots,x^j_n) \in \prod_{i=1}^n X_i$ — one worker of each type hired by that firm (a firm that hires no worker of some type, or several, is accommodated by adjoining an artificial "no worker" element to $X_i$, or by splitting a type into several, as Topkis notes on p. 97; the model itself needs neither device). If firm $j$ hires the quality vector $x$, it earns profit $f(x,j) \in \mathbb{R}$; the dependence on $j$ reflects differences among firms such as technology or management efficiency. A matching is optimal if it maximizes the total profit $\sum_{j=1}^m f(x^j,j)$ over every matching.

A matching is increasing if $x^1 \preceq x^2 \preceq \cdots \preceq x^m$ — a single chain, firm by firm, under the pointwise order on $\prod_i X_i$ — and ordered if every two of its firm-assignments are comparable (a weaker, only pairwise, condition). The labor market is loose if each firm's hiring problem can be solved by unconstrained maximization over the whole quality space $\prod_i X_i$, without regard to the other firms' decisions, and tight if the supply of each worker type is exactly $m$, so a feasible matching must assign every available worker to exactly one firm.

The hypothesis common to every result is that $f(x,j)$ is supermodular in the joint variable $(x,j)$ on $\bigl(\prod_i X_i\bigr) \times \{1,\dots,m\}$: for every $(x,j)$ and $(x',j')$, $f(x,j) + f(x',j') \le f(x\vee x', j\vee j') + f(x\wedge x', j\wedge j')$. By Theorem 2.6.1 of Chapter 2, this is equivalent to $f$ having increasing differences both between any two worker types' qualities (complementarity among the worker types) and between each worker type's quality and the firm index (complementarity between quality and firm efficiency).

Formalization targets

Goal — Theorem 3.2.3

$$f \text{ supermodular in } (x,j) \text{ on } \Bigl(\textstyle\prod_{i=1}^n X_i\Bigr)\times\{1,\dots,m\} \ \Longrightarrow\ \exists\, x \text{ increasing and optimal.}$$ $$\text{If, in addition, the labor market is tight, every increasing (tight) matching is optimal.}$$

Existence of an increasing optimal matching, with no loose-market hypothesis — the general case, and the harder of this mission's results to formalize, since its proof is a non-constructive lexicographic-minimization argument rather than a direct reduction to per-firm optimization.

Supporting milestones

• Theorem 3.2.1 (the loose case): under an unconstrained labor market, each firm's set of optimal hiring decisions is increasing in the firm index with respect to the induced set ordering, and an increasing optimal matching exists — proved directly from Chapter 2's monotone-comparative-statics theorems (mission II of this series).
• Theorem 3.2.4: joint supermodularity in $(x,j)$ together with strict supermodularity in $x$ alone, for each fixed $j$, forces every optimal matching to be ordered.
• Theorem 3.2.5: joint strict supermodularity in $(x,j)$ forces every optimal matching to be increasing, the stronger of the two conclusions.

Significance

The result gives a clean, hypothesis-light account of assortative matching: sorting by quality is a structural consequence of complementarity in the profit function, not an artifact of a particular production technology. It generalizes Becker's and Kremer's special cases to arbitrarily many worker types, heterogeneous firms, and any degree of labor-market tightness, identifying supermodularity in $(x,j)$ as the single condition doing all the work. Formalizing it contributes a genuinely new object to the platform: a firm-quality matching model driven by lattice-theoretic complementarity rather than by preference orderings, together with the four distinct comparative-statics conclusions (loose-market optimality, general existence, orderedness, increasingness) that the strength of the supermodularity hypothesis buys. No prior formalized proof of any of these four theorems exists on the platform or, to the author's knowledge, in any other proof assistant library.

Difficulty

The obvious approach — prove the goal (Theorem 3.2.3) by reducing to the loose case, firm by firm, as in Theorem 3.2.1 — does not work, because the loose-market argument crucially uses that each firm's decision does not constrain any other's; without that, a locally optimal per-firm choice need not combine into a globally optimal matching. Topkis's actual proof is non-constructive: among all optimal matchings, pick one that lexicographically minimizes the "latest" failure of the increasing property (a well-ordering argument over the finite but unbounded set of optimal matchings, not an inequality chase), then show that if it still fails to be increasing, exchanging the two offending firms' assignments via $\vee,\wedge$ strictly increases total profit — contradicting optimality by supermodularity. Formalizing this requires setting up the lexicographic minimization (over pairs $(j,i)$ ordered by $j$ then $i$) as a well-founded induction, not merely restating the inequality (3.2.3) at the end of the proof.

Formalization scope

Worker-type quality spaces $X_i$ are modeled as finite, nonempty lattices (Lattice, Fintype, Nonempty); firms are indexed by Fin m. A matching is Fin m → ∀ i, X i with no constraint beyond membership — the general matching problem (3.2.1) imposes no injectivity or supply constraint on its own, a modeling choice Topkis's own text supports (p. 96: the "$\{x^1_i,\dots,x^m_i\}\subseteq X_i$" representation of a matching "may not distinguish between all distinct assignments of workers to firms if the qualities of different workers of any given type are not all distinct, but that ambiguity is inconsequential"). Tightness is instead formalized as an explicit feasibility predicate (a bijection between firms and the $m$ available workers of each type) supplied as a hypothesis exactly where a tight-market theorem needs it, never folded into the general optimality predicate.

A trivializing formalization to avoid: collapsing Theorem 3.2.4's "ordered" conclusion and Theorem 3.2.5's "increasing" conclusion into the same statement, or conflating their two distinct supermodularity hypotheses (joint-non-strict-plus-per-firm-strict versus jointly strict) — the mission's four milestones are kept as four genuinely different claims with their own hypotheses, not variations proved once and restated. AGT.stable_matching_exists (Gale–Shapley) is not reused here, despite the shared word "matching": it produces a two-sided, preference-based stable matching with no notion of aggregate profit, a mechanism unrelated to this mission's profit-maximizing, supermodularity-driven assignment.

Reused from earlier missions in this series: the induced set ordering InducedSetOrder (mission I) and joint supermodularity SupermodularOn (mission II), both published platform definitions. Contributions most welcome on the goal theorem's lexicographic-minimization argument, the mission's hardest step.

Selected references

• G. S. Becker, A Theory of Marriage: Part I, Journal of Political Economy 81 (1973), 813–846. https://doi.org/10.1086/260084
• M. Kremer, The O-Ring Theory of Economic Development, Quarterly Journal of Economics 108 (1993), 551–575. https://doi.org/10.2307/2118400
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 2011 (orig. 1998). https://doi.org/10.1515/9781400822539

Motivation

A device's mean residual life at age $t$ — its conditional expected remaining lifetime given that it has survived to $t$ — is one of the oldest and most interpretable summaries in reliability and survival analysis: it is what an insurer, a maintenance planner, or a hospital outcomes researcher actually wants to know about a unit still in service. Comparing two mean residual life functions pointwise gives the mean residual life order $\le_{mrl}$, a natural "the survivor of $X$ is worn less, on average, than the survivor of $Y$" comparison that is weaker than the usual stochastic order but not directly comparable to it (the book states plainly that neither implies the other in general). This mission formalizes the order's definition and its precise relationship to the stronger hazard rate order $\le_{hr}$: under an extra monotone-ratio condition the two orders coincide, and one direction of that coincidence always holds. A third milestone gives one of the chapter's closure properties, showing that "decreasing mean residual life" (DMRL) — an aging notion used throughout reliability theory to describe units that wear out, rather than improve, with age — is preserved under adding independent noise.

Setting

Fix a probability space $(\Omega,\mu)$ and a real-valued random variable $X$ with survival function $\bar F(x) = P\{X>x\}$ and finite mean. The mean residual life function of $X$ at $t$ is

$$m(t) = \begin{cases} E[X-t \mid X>t], & t < t^*; \\ 0, & \text{otherwise,} \end{cases} \qquad t^* = \sup\{t : \bar F(t) > 0\}.$$

For a second random variable $Y$ on $(\Omega',\nu)$ with mrl function $l$, $X$ is smaller than $Y$ in the mean residual life order, $X \le_{mrl} Y$, if $m(t) \le l(t)$ for every $t$. The hazard rate order, restated in this mission's own namespace (Chapter 1's version cannot be imported — see Formalization scope), is the general, absolute-continuity-free comparison $\bar F(x)\bar G(y) \ge \bar F(y)\bar G(x)$ for all $x \le y$, where $\bar G$ is $Y$'s survival function. A random variable $X$ is DMRL (decreasing mean residual life) if its mrl function $m$ is decreasing in $t$.

Formalization targets

Goal — Theorem 2.A.2

$$\left(\frac{m(t)}{l(t)}\text{ increases in }t\right)\ \text{and}\ X \le_{mrl} Y \ \implies\ X \le_{hr} Y.$$

Combined with the companion milestone below, this is a genuine conditional equivalence: under the monotone-ratio hypothesis, $\le_{mrl}$ and $\le_{hr}$ coincide, and in particular $X \le_{mrl} Y \implies X \le_{st} Y$ under that condition. Without the hypothesis, the book states explicitly (the paragraph immediately preceding Theorem 2.A.1) that neither $\le_{st}$ nor $\le_{mrl}$ implies the other.

Milestones, in attack order

• Theorem 2.A.1. $X \le_{hr} Y \implies X \le_{mrl} Y$ — the one-directional link that motivates the goal theorem: the hazard rate order, strictly stronger in general, always implies the mean residual life order.
• Theorem 2.A.11. If $X$ is DMRL and $Z$ is a nonnegative random variable independent of $X$, then $X \le_{mrl} X+Z$ — one of the chapter's closure properties (§2.A.3): adding independent nonnegative noise to a DMRL random variable can only increase it in the mean residual life order.

Each milestone is stated exactly as the book states it: no constant is hard-coded, no $O(\cdot)$ or asymptotic approximation is involved, and the goal's monotone-ratio hypothesis is the genuine ratio $m(t)/l(t)$, not two separately-monotone functions (a different, unrelated condition the book itself does not state).

Significance

The mean residual life order sits at a specific point in the book's own hierarchy of orders: strictly implied by the hazard rate order (Theorem 2.A.1), and — the goal theorem — reversible into the hazard rate order under one extra monotonicity hypothesis on the ratio of the two mrl functions. This "sandwich" structure is exactly the kind of comparison-of-orders result that makes Chapter 1's usual and hazard rate orders (already formalized in Chunk 01 of this series, restated locally here since drafts cannot import each other) into a genuinely connected theory rather than a list of unrelated definitions. The DMRL closure property (Theorem 2.A.11) is separately significant: DMRL is one of the book's standard "aging" notions, used in reliability engineering to model components that wear out over time, and its preservation under adding independent noise is a basic tool for building compound reliability models (e.g. a component with an added, uncorrelated failure mode) from simpler DMRL parts.

No prior art exists on the platform for either order: GET /theorems?q=mean+residual+life returns zero hits, and GET /theorems?q=hazard+rate returns exactly one hit (DQJSQ.theorem2_ifr), an unrelated queueing-theory IFR (increasing failure rate) lemma about patience densities in a fluid queueing model, not this order — it names a different object under a coincidentally similar keyword and is not reused. This mission is a foundational island for the mean residual life order.

Difficulty

The mrl function is a genuinely two-case object: a real conditional expectation on $\{t : \bar F(t) > 0\}$, and a hard $0$ outside that region. The goal theorem's proof (not formalized here; only the statement is a milestone) differentiates $m$ and $l$, uses the identity $r(t) = m'(t)/m(t) + 1/m(t)$ relating the mrl function to the hazard rate, and compares the two resulting hazard-rate expressions using the ratio's monotonicity — a genuinely analytic argument, not a routine unfolding of definitions. The chief formalization difficulty is keeping the shape of $\le_{mrl}$ (a pointwise comparison of a derived function) visibly distinct from the function-class shape of $\le_{st}$ used in Chapter 1, since the book explicitly warns that conflating the two orders is a live error (neither implies the other in general) — see Formalization scope below for how each shape is kept separate.

Formalization scope

All three random variables in this mission's milestones are real-valued measurable functions on a MeasureTheory.Measure space, matching this series' Chapter 1 convention (Chunk 01). The mrl function mrl μ X t is defined as if 0 < P{X>t} then (∫ ω in {X>t}, (X ω - t) ∂μ) / P{X>t} else 0, formalizing the case split on $t < t^*$ directly via positivity of the survival probability (its defining equivalent under the survival function's monotonicity) rather than through the derived quantity $t^*$ itself. MrlOrder μ ν X Y is ∀ t : ℝ, mrl μ X t ≤ mrl ν Y t — a direct pointwise comparison of two functions, deliberately kept a different shape from Chapter 1's UsualOrder (a ∀ φ ∈ 𝒞, E[φ∘X] ≤ E[φ∘Y] function-class quantifier), since the book's own warning that $\le_{st}$ and $\le_{mrl}$ neither implies the other is a warning against treating them as interchangeable comparison shapes.

The hazard rate order is restated locally in this chapter's own namespace (StochasticOrders.MeanResidualLife.HazardRateOrder) rather than imported from Chunk 01's StochasticOrders.Usual.HazardRateOrder, because each chapter's mission is drafted and reviewed as an independent Prove2Me proposal and one draft cannot import another draft's unpublished Lean; its definition is identical in shape to Chunk 01's own restatement of the general, absolute-continuity-free survival-function form of $\le_{hr}$ (not the density-ratio form, which requires absolute continuity the book does not assume at this level of generality).

Every milestone that consumes mrl carries explicit Integrable hypotheses on the random variables involved (Integrable X μ, and Integrable Y ν or Integrable Z μ as applicable), formalizing the book's own standing "finite mean" hypothesis from §2.A.1's definition of the mrl function: without it, the Bochner integral inside mrl would return its junk value 0 for a non-integrable variable on some tail set, letting a hypothesis like MrlOrder μ ν X Y hold of a function that is not actually the book's mean residual life function. DMRL μ X is Antitone (mrl μ X), the book's own "$m(t)$ is decreasing in $t$" in the weak, non-strict monotone sense used throughout the book for "increasing"/"decreasing".

A trivializing formalization this mission rules out: stating the goal theorem with the ratio hypothesis as two separate monotonicity conditions on $m$ and $l$ individually (rather than genuine monotonicity of the ratio $m(t)/l(t)$ on the region where $l(t)>0$) would be a different, strictly stronger and easier-to-satisfy hypothesis than the book's own — the milestone here states MonotoneOn (fun t => mrl μ X t / mrl ν Y t) {t | 0 < mrl ν Y t}, the genuine ratio restricted to where the denominator does not vanish, matching Theorem 2.A.2's own "$m(t)/l(t)$ increases in $t$" verbatim.

Selected references

• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer 2007, Chapter 2 (Mean Residual Life Orders), §2.A. https://doi.org/10.1007/978-0-387-34675-5
• W. Whitt, "Uniform Conditional Stochastic Order," Journal of Applied Probability, 1980 (characterizations of IFR/DFR by the likelihood ratio order, cited by the book's remarks section as background for the chapter's aging notions).
• This series' Chunk 01 (StochasticOrders.Usual), for the usual and hazard rate orders this chapter's own restated definitions parallel.