Operations Research

Ordering how strongly two variables move together

The first eight chapters of Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) compare single random variables — location, variability, convexity. Chapter IX turns to a different question: given two coordinates of a random vector, how strongly do they tend to move together? "Large values of $X_1$ go with large values of $X_2$" is a qualitative property (positive dependence); comparing how much two bivariate distributions exhibit it, holding their individual marginals fixed, is what this chapter's positive dependence orders make precise. This mission formalizes the two central ones — the PQD order and the supermodular order — and the supermodular order's closure properties, the chapter's own capstone result.

The PQD and supermodular orders

Let $X=(X_1,\dots,X_n)$ and $Y=(Y_1,\dots,Y_n)$ be two random vectors, with joint survival function $\bar F(x)=P\{X_1>x_1,\dots,X_n>x_n\}$ and joint distribution function $F(x)=P\{X_1\le x_1,\dots,X_n\le x_n\}$ (similarly $\bar G, G$ for $Y$). $X$ is smaller than $Y$ in the PQD order, written $X\le_{PQD}Y$, if

$$\bar F(x)\le\bar G(x)\ \text{ and }\ F(x)\le G(x) \quad\text{for every }x\in\mathbb{R}^n.$$

(It follows, though it need not be assumed, that $X$ and $Y$ then share the same univariate marginals — the two inequalities together pin the marginals down, unlike a single one alone.) This is Lehmann's positive-quadrant-dependence order in its general multivariate form: $Y$'s coordinates cluster together, in both the upper and lower "quadrants," at least as strongly as $X$'s.

A function $\varphi:\mathbb{R}^n\to\mathbb{R}$ is supermodular if $\varphi(x)+\varphi(y)\le\varphi(x\wedge y)+\varphi(x\vee y)$ for the coordinatewise meet/join — the function-level notion the platform's Topkis/Supermodularity series already formalizes for games and lattices, reused here directly. $X$ is smaller than $Y$ in the supermodular order, written $X\le_{sm}Y$, if $E[\varphi(X)]\le E[\varphi(Y)]$ for every supermodular $\varphi$ for which the two expectations exist. Because the indicator of any upper or lower orthant is itself supermodular, $X\le_{sm}Y\implies X\le_{PQD}Y$ (Eq. 9.A.17): the supermodular order is strictly finer than the PQD order, and for $n=2$ the two coincide.

Formalization targets

Goal: closure properties of the supermodular order (Theorem 9.A.9(a),(c))

$$(X_1,\dots,X_n)\le_{sm}(Y_1,\dots,Y_n) \implies (g_1(X_1),\dots,g_n(X_n))\le_{sm}(g_1(Y_1),\dots,g_n(Y_n))$$

whenever every $g_i$ is increasing, or every $g_i$ is decreasing (part a); and

$$X\le_{sm}Y \implies X_I\le_{sm}Y_I \quad\text{for every } I\subseteq\{1,\dots,n\}$$

(part c, closure under marginalization). These are two of Theorem 9.A.9's five closure properties — the theorem the brief for this mission recommends as its goal — chosen as the ones that need no further definitional machinery beyond the orders themselves (composition and a coordinate projection, both plain pushforwards of the vector's law).

Supporting milestone

• Theorem 9.A.4, the general multivariate closure of the PQD order under independent pairing: if $X\le_{PQD}Y$, $U\le_{PQD}V$, with $X,U$ independent and $Y,V$ independent, then $(\varphi_1(X_1,U_1),\dots,\varphi_n(X_n,U_n))\le_{PQD}(\varphi_1(Y_1,V_1),\dots,\varphi_n(Y_n,V_n))$ for all increasing $\varphi_i$ — the closure property the chapter opens with (as Theorem 9.A.1, the bivariate case), generalized to $n$ dimensions.

Significance

Positive dependence orders formalize a comparison operations research and risk management need constantly but rarely state precisely: two portfolios, insurance lines, or queueing networks with identical individual risk profiles can still differ sharply in how their components co-move, and that co-movement — not the marginals — is often what drives tail risk, correlated failures, or aggregate variability. The supermodular order is the standard tool for comparing this directly: Theorem 9.A.9's closure properties are what let a comparison established for primitive components survive the operations a model actually performs on them — relabeling by a monotone transform (part a), reading off a subset of coordinates (part c), combining independent sub-vectors (part b), conditioning on a covariate (part d), or passing to a distributional limit (part e). Chapter VI's multivariate stochastic order and Chapter VII's multivariate convex order are the two other multivariate orders in the book; the supermodular order is the one built specifically to compare dependence structure rather than location or spread, and it connects directly to the platform's existing Topkis/Supermodularity series, whose function-level predicate this mission reuses rather than restates.

Formalizing Theorem 9.A.9 fixes the exact shape a supermodular-order closure claim takes when built as a pushforward of the vector's law — the natural Mathlib-idiomatic rendering once the order is stated on laws rather than on variables tied to a fixed ambient space — for any future mission in this series or elsewhere that needs to state a closure property of a vector-valued stochastic order. No proof is attempted; both drafted parts of Theorem 9.A.9 have short book proofs (part (a) from the fact that composing a supermodular function with all-increasing or all-decreasing coordinate maps is again supermodular; part (c) the book calls "easy to prove"), making them plausible future proof targets.

Difficulty

The chapter's central definitional trap is that the PQD order's defining condition — even in its general multivariate form — determines the marginals as a consequence of the two joint inequalities holding together, not as a separate hypothesis to add; adding same-marginals as an extra explicit condition on top of Eqs. (9.A.13)-(9.A.14) would not be false, but it would present as a hypothesis something the theorem's own two conditions already force. A second trap is specific to Theorem 9.A.9(a): the $g_i$ must be uniformly increasing or uniformly decreasing across all coordinates, not an arbitrary per-coordinate mix — a mixed-monotonicity version is a materially different, unproven claim, since it is exactly the all-same-direction condition that keeps a composition with a supermodular function supermodular. A third, more basic trap common to every function-class order in this book: "for every supermodular $\varphi$" must be a genuine universal quantifier with the two expectations' existence stated as an explicit hypothesis, not a global assumption or a specific test function standing in for the whole class.

Formalization scope

Unlike the univariate orders formalized elsewhere in this series (which take random variables $X:\Omega\to\mathbb{R}$, $Y:\Omega'\to\mathbb{R}$ on two possibly-different probability spaces), PQDOrder and SupermodularOrder here are stated directly on the two vectors' laws — measures $P,Q$ on $\iota\to\mathbb{R}$ for a finite index type $\iota$ — since the book's own comparisons never reference a joint law of $X$ and $Y$ together, only their separate distributions. This is also what lets Theorem 9.A.9(a)'s coordinatewise composition and (c)'s marginalization be stated as plain pushforwards (Measure.map) of one law, without carrying an ambient sample space through the statement. The index type is left an arbitrary finite type (Fintype ι, not fixed to Fin n) so the same two declarations serve both a full $n$-vector and any marginal sub-vector obtained by restricting to a subset $I$ of coordinates — the shape Theorem 9.A.9(c) itself needs. Supermodularity reuses the platform's own Supermodularity.Monotonicity.SupermodularOn (from the Topkis series, via a kind: reference item) with its relativizing set argument fixed to Set.univ, its plain unrelativized form — checked to match the book's φ(x)+φ(y)≤φ(x∧y)+φ(x∨y) on ι → ℝ's own coordinatewise lattice structure exactly, not a games- or player-scoped variant. Independence in Theorem 9.A.4 is formalized by taking the joint law of the two independent vectors to be the product measure of their marginals — the standard way to construct an independent coupling with prescribed marginals — rather than adding a separate independence hypothesis about pre-existing random variables. Measurable hypotheses are added on every map a Measure.map is taken along, guarding against the pushforward's junk-zero-measure convention for a non-measurable map; none narrows what the book's own theorems claim, since every map used (a monotone/antitone composition, a coordinate projection) is genuinely measurable. A trivializing formalization is ruled out explicitly: the supermodular quantifier ranges over the reused, already-audited Topkis predicate rather than a hand-rolled or restricted one, and the "for all increasing $\varphi_i$" of Theorem 9.A.4 is a genuine universal over jointly-monotone functions of two arguments, not a fixed example.

This mission draws on the platform's own Topkis/Supermodularity series for its supermodular function-level building block (Supermodularity.Monotonicity.SupermodularOn, reused as a reference item — the strongest prior-art connection of the whole nine-chapter series, per the series plan) but on no prior art for the orders themselves (repeated searches for "PQD", "positive dependence", "Fréchet bound" and "supermodular" returned nothing on-topic beyond the Topkis series as of 2026-09-18). Reusable beyond this mission: the laws-only, arbitrary-Fintype- index formalization pattern is available to any later mission in this series needing a multivariate order (Chapter VI's multivariate stochastic order, Chapter VII's multivariate convex order) that wants marginalization or coordinatewise composition stated as plain pushforwards.

Selected references

• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5
• E. L. Lehmann, "Some concepts of dependence", Annals of Mathematical Statistics, 37(5), 1966, 1137–1153. https://doi.org/10.1214/aoms/1177699260

From "more spread out" to "more spread out in every direction"

Chapter III's convex order compares two real-valued random variables by "how spread out" they are, holding the mean fixed. Chapter VII lifts the same idea to random vectors: $X$ is smaller than $Y$ in the multivariate convex order if every convex function of $X$ has smaller expectation than the same function of $Y$. This mission formalizes that order, its increasing-convex companion, and their martingale-coupling characterizations — the direct $n$-dimensional generalizations of Chunk 03's and Chunk 04's own goal theorems — plus a cheap mean-equality corollary and a simple standalone scaling result.

The multivariate convex and increasing convex orders

Let $X$ be a random vector taking values in $\mathbb{R}^n$ on $(\Omega,\mu)$, and $Y$ a random vector taking values in $\mathbb{R}^n$ on $(\Omega',\nu)$. $X$ is smaller than $Y$ in the multivariate convex order, $X\le_{cx}Y$, if

$$E[\varphi(X)] \le E[\varphi(Y)] \quad \text{for every convex } \varphi:\mathbb{R}^n\to\mathbb{R} \text{ for which the two expectations exist},$$

and smaller than $Y$ in the increasing convex order, $X\le_{icx}Y$, if the same holds for every $\varphi$ that is both increasing (coordinatewise) and convex. Since each coordinate projection $\varphi_i(x)=x_i$ and its negation are both convex, $X\le_{cx}Y$ forces $E[X]=E[Y]$ componentwise (Eq. 7.A.5) — unlike $\le_{icx}$, which only forces $E[X]\le E[Y]$.

Formalization targets

Goal: the martingale-coupling characterization (Theorem 7.A.1)

$$X \le_{cx} Y \iff \exists\,(\Omega'',\rho),\ \hat X,\hat Y:\Omega''\to\mathbb{R}^n\text{ with } \hat X=_{st}X,\ \hat Y=_{st}Y,\ E[\hat Y\mid\hat X]=\hat X\text{ a.s.}$$

The direct $n$-dimensional generalization of Theorem 3.A.4 (Strassen's martingale coupling, Chunk 03's own goal theorem): a joint law on a common probability space realizing $X\le_{cx}Y$ as a genuine martingale pairing between copies of $X$ and $Y$. The book states no further "Furthermore" strengthening here, unlike the univariate and increasing-convex cases.

Companion: the submartingale-coupling characterization (Theorem 7.A.2, increasing convex case)

$X\le_{icx}Y$ iff there exist $\hat X,\hat Y$ on a common space with $\hat X=_{st}X$, $\hat Y=_{st}Y$, and $\{\hat X,\hat Y\}$ a submartingale, $E[\hat Y\mid\hat X]\ge\hat X$ a.s. — the direct generalization of Theorem 4.A.5's increasing-convex case (Chunk 04's own goal theorem), proved by the book's own cross-reference "by essentially the same method" as the goal. The book's bracketed increasing-concave companion is a genuinely separate statement (swapped conditioning) and is not drafted here for budget (see STATUS.md).

Supporting milestones

• Eq. (7.A.5), the mean-equality corollary: $X\le_{cx}Y\implies E[X]=E[Y]$ (componentwise), provided the expectations exist — a one-line consequence of ConvexOrder's own defining quantifier applied to $\pm$ each coordinate projection.
• Theorem 7.A.9, a simple standalone application: an independent, mean-one random scale factor $U$ always makes a random vector larger in the convex order, $X\le_{cx}UX$.

Significance

The multivariate convex order is the natural tool for comparing the variability of random vectors — portfolios of returns, multi-resource cost vectors, correlated component lifetimes — in a way that respects every direction of the space simultaneously rather than coordinate by coordinate. Its martingale-coupling characterization is the same tool that makes Strassen's theorem useful in the univariate case: it turns the intractable "for every convex $\varphi:\mathbb{R}^n\to\mathbb{R}$" quantifier into a single explicit joint construction, and because it generalizes directly (the book's own proof of Theorem 7.A.4, not drafted here, applies the univariate Theorem 3.A.4 coordinate by coordinate to build the multivariate coupling), it is the natural second data point — after Chunk 03's univariate case and Chunk 06's usual-order case — for what a "coupling-characterization" mission in this book's series looks like once both the order and the dimension vary. Theorem 7.A.9's scaling result is a compact, self-contained illustration of how the order behaves under a common operation (randomized scaling) that appears throughout the book's later risk and insurance examples.

No platform prior art exists: GET /theorems?q=convex+order and q=martingale return only false positives (checked at this book's triage time, re-confirmed this session). This mission restates the multivariate convex and increasing convex orders and their coupling characterizations as a self-contained pair, parallel in structure to Chunks 03 and 04's univariate missions but independently drafted, since drafts cannot import each other's Lean.

Difficulty

The chief formalization risk this chapter's own brief flags is confusing "convex" for $\varphi:\mathbb{R}^n\to\mathbb{R}$ (ordinary convexity, Mathlib's ConvexOn) with a coordinatewise or lattice-based notion — in particular, with Chunk 09's supermodular functions, a different and weaker condition. A second risk is the "increasing" half of IcxOrder: unlike convexity, "increasing" genuinely is the coordinatewise order (matching Chunk 06's convention), so IcxOrder mixes two different kinds of predicate on the same φ (Monotone in the coordinatewise sense, ConvexOn in the ordinary sense) and getting either one wrong silently changes which order is being stated. A third risk, specific to Theorem 7.A.2, is the bracketed icx/icv alternative: as in Chunk 04, the two cases are not symmetric rewrites of each other (the conditioning variable swaps), so a Lean statement conflating them with Or would misstate one case — this mission avoids the risk by drafting only the increasing-convex case and recording the omission explicitly rather than attempting an unsound unification.

Formalization scope

Random vectors are drafted as functions into Fin n → ℝ from arbitrary measurable spaces. ConvexOrder μ ν X Y quantifies over φ : (Fin n → ℝ) → ℝ with ConvexOn ℝ Set.univ φ (ordinary convexity) and Integrable (φ ∘ X) μ/Integrable (φ ∘ Y) ν inside the ∀; IcxOrder adds Monotone φ in Mathlib's default coordinatewise (Pi) order on Fin n → ℝ — the same order Chunk 06's MultivariateOrder uses — as a genuinely separate definition from ConvexOrder, not one derived from the other, since Theorem 7.A.12 (not drafted here) relates the two nontrivially and conflating them would trivialize such a relationship. Equality in law is ProbabilityTheory.IdentDistrib; the martingale/submartingale conditions use Mathlib's conditional-expectation notation ρ[Ŷ | m] =ᵐ[ρ] X̂ (resp. X̂ ≤ᵐ[ρ] ρ[Ŷ | m]) with m generated by X̂, here genuinely Fin n → ℝ-valued (well-defined since Fin n → ℝ is a finite-dimensional, hence complete, normed space over ℝ) — restated locally rather than imported from Chunks 03/06, since drafts cannot import another mission's definitions. Theorem 7.A.9's scaling U·X is Mathlib's scalar multiplication on the ℝ-module Fin n → ℝ.

Two deliberate scope restrictions, recorded rather than silently applied: (1) Theorem 7.A.2 is drafted only for the increasing-convex case, per this chapter's own pitfall 3 (the icv companion's swapped conditioning structure is a genuinely different predicate, not a sign-flipped rewrite, and budget did not justify a fourth definition/theorem pair to draft it separately, unlike Chunk 04 which had budget for both cases of its analogous theorem); (2) Theorem 7.A.5 through 7.A.8's closure properties (mixtures, convolutions, weak limits, the random-sum generalization) are left out entirely — each needs conditional-distribution or convergence-in-distribution machinery this mission's four items do not otherwise require, and none is on the goal's own attack chain.

A trivializing formalization this mission rules out: drafting IcxOrder by deriving it from ConvexOrder and a separate monotonicity wrapper in a way that makes their relationship (Theorem 7.A.12: $X\le_{st}Y\implies X\le_{icx}Y\wedge X\le_{icv}Y$, not drafted here) provable by unfolding rather than by genuine content — the two are kept as independently-quantified predicates for this reason. This mission draws on no platform prior art (searches for "convex order" and "martingale" as of 2026-09-18 return only false positives). Reusable beyond this mission: the ConvexOrder/IcxOrder pattern and their martingale/submartingale coupling shape parallel Chunks 03/04's univariate pair and Chunk 06's multivariate usual-order pair closely enough that a future pass drafting the icv companion, or Chapter VII's later dispersion and transform orders, 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 7 (Multivariate Variability and Related Orders), §7.A.1–7.A.2. https://doi.org/10.1007/978-0-387-34675-5
• This series' Chunk 03 (StochasticOrders.Convex) and Chunk 04 (StochasticOrders.MonotoneConvex), for the univariate convex and increasing convex orders and their martingale/submartingale couplings this chapter directly generalizes; Chunk 06 (StochasticOrders.Multivariate), for the multivariate usual stochastic order and its own coupling characterization.

Comparing distributions by their Laplace transforms

Many of the orders in Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) are built by fixing a class of test functions $\varphi$ and declaring $X \le Y$ whenever $E[\varphi(X)] \le E[\varphi(Y)]$ for every $\varphi$ in that class: all increasing functions give the usual stochastic order, all convex functions give the convex order. This mission formalizes the order obtained from the single function $\varphi_s(x) = -e^{-sx}$, $s > 0$ — the Laplace transform order — together with its principal alternative characterization and three of its closure properties. Unlike almost every other order in the book, this one has essentially no dependence on material from earlier chapters, which is why it is a natural standalone mission.

The Laplace transform order

Let $X$ be a real-valued random variable on a probability space $(\Omega,\mu)$, and let $Y$ be a real-valued random variable on a (possibly different) probability space $(\Omega',\nu)$. $X$ is smaller than $Y$ in the Laplace transform order, written $X \le_{Lt} Y$, if

$$E[e^{-sX}] \ge E[e^{-sY}] \quad \text{for every } s > 0.$$

The order is meant for nonnegative random variables: the book's own standing convention for the whole of §5.A is that every random variable mentioned is nonnegative, since otherwise $E[e^{-sX}]$ need not even be finite. Every theorem below carries that hypothesis explicitly rather than folding it into the order's own definition, so the definition itself is stated exactly as broadly as the book's raw equation (5.A.1) is — a comparison of two expectations, for two random variables that need not share a probability space, since $\le_{Lt}$ is a comparison of distributions.

A second definition supports one of the milestones: a function $\varphi : [0,\infty) \to \mathbb{R}$ is completely monotone if all its derivatives exist and $(-1)^n\varphi^{(n)}(x) \ge 0$ for every $x > 0$ and every $n = 0, 1, 2, \dots$. Every $\varphi_s(x) = e^{-sx}$, $s > 0$, is completely monotone, which is what connects the raw definition of $\le_{Lt}$ to its function-class characterization below.

Formalization targets

Goal: the integrated-survival-function characterization (Theorem 5.A.1)

$$X \le_{Lt} Y \iff \int_0^\infty e^{-sx}\bar F(x)\,dx \le \int_0^\infty e^{-sx}\bar G(x)\,dx \quad \text{for every } s > 0,$$

where $\bar F(x) = P\{X>x\}$ and $\bar G(x) = P\{Y>x\}$ are the survival functions of $X$ and $Y$. This is the book's principal restatement of the order, obtained from the identity $\int_0^\infty e^{-sx}\bar F(x)\,dx = s^{-1}(1-E[e^{-sX}])$: instead of comparing the raw Laplace transforms of $X$ and $Y$ themselves, it compares the Laplace transforms of their survival functions, weighted the same way. It is the natural goal for a standalone chapter mission: the chapter's own defining equation plus one elementary identity is exactly the book's own proof, and it is the form of the order that the chapter's closure properties are stated against.

Supporting milestones

• Eq. (5.A.5), the mean inequality: $X \le_{Lt} Y \implies E[X] \le E[Y]$, provided the expectations exist — obtained by dividing the defining inequality by $s$ and letting $s \downarrow 0$.
• Theorem 5.A.3, the function-class characterization: $X \le_{Lt} Y$ iff $E[\varphi(X)] \ge E[\varphi(Y)]$ for every completely monotone $\varphi$, provided the expectations exist — the order's analogue of "all increasing functions" for $\le_{st}$ or "all convex functions" for $\le_{cx}$.
• Theorem 5.A.7(a), closure under functions with a completely monotone derivative: $X \le_{Lt} Y$ and $g$ positive with $g'$ completely monotone gives $g(X) \le_{Lt} g(Y)$.
• Theorem 5.A.7(d), the convolution corollary: independent $X_i \le_{Lt} Y_i$, $i=1,\dots,m$, gives $\sum_i X_i \le_{Lt} \sum_i Y_i$.

Significance

The Laplace transform order is the natural comparison for nonnegative quantities that arise as sums or mixtures of exponential-type random variables — waiting times, workloads, service completion times — precisely because it is preserved under convolution (Theorem 5.A.7(d)) and under the broad class of transformations with a completely monotone derivative (Theorem 5.A.7(a)), which includes every concave power $x^p$, $0<p\le 1$. It sits strictly between the convex-type orders and weaker moment comparisons: Eq. (5.A.5) shows it implies ordered means, but (unlike $\le_{cx}$) it does not require equal means, and (unlike $\le_{icx}$) it is not implied by a pointwise comparison of integrated tails alone — it is its own, genuinely different order, useful whenever a modeler's comparison naturally arises through Laplace-transform (equivalently, moment-generating-function-at- negative-argument) calculations rather than through a coupling or a tail-probability argument. Theorem 5.A.3's function-class form is the bridge that lets the order be verified either way: by a single-parameter family of exponential test functions, or by the full class of completely monotone functions of which they are the extreme rays.

Difficulty

The chapter's own first warning applies directly: the order's every characterization requires $X,Y \ge 0$, and dropping that hypothesis anywhere — as opposed to carrying it explicitly on each theorem, per this mission's convention — would silently change which statements are even well-posed, since $E[e^{-sX}]$ can diverge for $X$ unbounded below. The quantifier "$\forall s > 0$" in both the raw definition and Theorem 5.A.1 ranges over the whole positive half-line, not a bounded or discretized set of test points; narrowing it would produce a strictly weaker order. In CompletelyMonotone, the phrase "all its derivatives exist" is a genuine hypothesis, not a formality: stating only the sign condition on iteratedDeriv n φ x without also requiring φ to be C^∞ would let the definition be satisfied vacuously wherever a derivative fails to exist (a classic junk-value trap), which is why the mission's definition bundles smoothness explicitly. Theorem 5.A.7(a)'s "$g$ positive" is a hypothesis on $g$'s values at the nonnegative reals that $X$ and $Y$ actually take, not on all of $\mathbb{R}$, and must not be silently strengthened to "$g$ everywhere positive" or weakened to "$g$ nonnegative" (which would let $g$ vanish and break the order's need for $e^{-sg(X)}$ to be well-behaved).

Formalization scope

LaplaceOrder μ ν X Y takes $X : \Omega \to \mathbb{R}$ on $(\Omega,\mu)$ and $Y : \Omega' \to \mathbb{R}$ on a separate $(\Omega',\nu)$, matching the series' convention (e.g. StochasticOrders.Usual.UsualOrder) that the order compares distributions, not jointly defined variables. Nonnegativity of $X$ and $Y$ is an explicit hypothesis ∀ ω, 0 ≤ X ω / ∀ ω, 0 ≤ Y ω on every theorem, never built into LaplaceOrder itself. CompletelyMonotone φ is ContDiff ℝ ⊤ φ ∧ ∀ n x, 0 < x → 0 ≤ (-1)^n * iteratedDeriv n φ x — the smoothness conjunct guards the junk-value trap described above. The survival function $\bar F(x) = P\{X>x\}$ in the goal theorem is formalized inline as (μ {ω | x < X ω}).toReal, valid since μ is a probability measure (so the underlying ENNReal value is finite and the conversion to ℝ loses no information); the integral $\int_0^\infty$ is Bochner integration over Set.Ici (0 : ℝ). "Provided the expectations exist" becomes explicit Integrable hypotheses per statement (on $X$, $Y$ themselves for Eq. 5.A.5; on $\varphi \circ X$, $\varphi \circ Y$ for each $\varphi$ in Theorem 5.A.3), rather than a blanket integrability assumption that would understate which expectations the book actually needs. Independence in the convolution corollary is ProbabilityTheory.iIndepFun, one family per side, as in Chunk 01's own convolution corollary. A trivializing formalization is ruled out: $\le_{Lt}$ is not restated as a comparison of one moment or of the raw random variables' means, and the "universal function class" of Theorem 5.A.3 is exactly the completely monotone functions the book names, not a fixed finite subfamily or a narrowed subclass (e.g. only the exponentials themselves, which would make Theorem 5.A.3 a restatement of the definition rather than its own theorem).

This mission draws on no platform prior art: repeated searches for "Laplace transform" and "completely monotone" during this session return only unrelated analytic-number-theory formalizations (a Langlands–Tunnell Laplace–Mellin transform identity) and no hits at all, respectively — confirming BRIEF.md's expectation that this subarea is untouched on the platform. It is one of nine missions in a series covering the whole book; per the series' own convention, its definitions are not imported by any other chapter's mission, and it does not import any other chapter's definitions in turn (the chapter itself has essentially no cross-chapter dependence, the reason it was flagged as the series' most self-contained chunk).

Selected references

• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

Comparing variability, not just location

Chapter I's usual stochastic order compares "how large" two random variables tend to be. A different, equally common question in operations research is "how spread out" a random variable is: two portfolios with the same expected loss can differ sharply in how much that loss varies, and a risk-averse decision maker or a convex cost function cares about exactly that difference. Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) formalizes this comparison as the convex order, the book's mean-preserving-spread order (known outside OR and probability circles as the Rothschild–Stiglitz order from economics). This mission formalizes the order and its central structural result: Strassen's martingale-coupling characterization.

The convex order

Let $X$ be a real-valued random variable on a probability space $(\Omega,\mu)$, and let $Y$ be a real-valued random variable on a (possibly different) probability space $(\Omega',\nu)$. $X$ is smaller than $Y$ in the convex order, written $X \le_{cx} Y$, if

$$E[\varphi(X)] \le E[\varphi(Y)] \quad \text{for every convex } \varphi:\mathbb{R}\to\mathbb{R} \text{ for which the two expectations exist.}$$

Convex functions take their relatively largest values on the "extreme" regions outside some interval, so $X \le_{cx} Y$ says $Y$ is more likely than $X$ to take extreme values: $Y$ is "more variable" than $X$. Unlike the usual stochastic order, $X \le_{cx} Y$ forces the two means to agree ($E[X]=E[Y]$, taking $\varphi(x)=\pm x$, both convex) — the convex order compares spread holding location fixed, exactly the mean-preserving-spread reading. Two equivalent forms make it tractable: comparing tail integrals of the survival/distribution functions (Theorem 3.A.1), and comparing mean absolute deviations $E|X-a|$ from every point $a$ (Theorem 3.A.2).

Formalization targets

Goal: Strassen's martingale-coupling characterization (Theorem 3.A.4)

$$X \le_{cx} Y \iff \exists\,(\Omega'',\rho),\ \hat X,\hat Y:\Omega''\to\mathbb{R}\text{ with } \hat X=_{st}X,\ \hat Y=_{st}Y,\ E[\hat Y\mid\hat X]=\hat X\text{ a.s.}$$

Furthermore, $\hat X,\hat Y$ can be chosen so that the conditional law $[\hat Y\mid\hat X=x]$ stochastically increases with $x$ (in $\le_{st}$). This is the convex-order analogue of Chapter I's Theorem 1.A.1: instead of one variable dominating the other pathwise, $Y$'s copy is a fair (martingale) randomization of $X$'s copy whose spread only grows in the conditioning value. The book itself calls the constructive direction "not easy to prove"; this mission states the theorem faithfully, including the "Furthermore" strengthening, without attempting a proof.

Supporting milestones

• Theorem 3.A.1, the tail-integral characterizations: for $X,Y$ with $E[X]=E[Y]$, $X\le_{cx}Y$ iff $\int_x^\infty\bar F(u)\,du\le\int_x^\infty\bar G(u)\,du$ for all $x$, and iff $\int_{-\infty}^x F(u)\,du\le\int_{-\infty}^x G(u)\,du$ for all $x$ — the two integrated forms the book's own sketch of Theorem 3.A.4 uses.
• Theorem 3.A.2, the absolute-deviation characterization: for $X,Y$ with $E[X]=E[Y]$, $X\le_{cx}Y$ iff $E|X-a|\le E|Y-a|$ for every real $a$.
• Theorem 3.A.12(d), closure under convolution: independent $X_i\le_{cx}Y_i$ for $i=1,\dots,m$ gives $\sum_i X_i \le_{cx} \sum_i Y_i$ — the convex-order analogue of Chapter I's Theorem 1.A.3(b).

Significance

The convex order is the standard way operations research and actuarial science formalize "more variable, same average": comparing the riskiness of two portfolios with matched expected return, the effect of aggregation or diversification on total claim size, or the value of information in a stochastic program (where a random variable degenerates to its mean exactly when the decision maker learns everything, the two extremes of a convex-order chain). Strassen's characterization is what turns "compare against every convex function" — an intractable universal quantifier — into a single explicit construction: exhibit one martingale coupling and the comparison is settled for every convex function at once, by Jensen's inequality. This is the technique behind bounding the effect of information or risk aggregation without checking convexity function by function, and the "Furthermore" monotonicity clause is what makes the coupling itself informative about how the spread grows with the conditioning variable, not merely that some fair coupling exists.

Formalizing this theorem fixes, for the whole book series, the exact shape every later coupling theorem for a variability-type order (the increasing convex/concave orders of Chapter IV via a submartingale, the multivariate convex order of Chapter VII) is expected to restate. No proof is attempted; the book's own remark that the constructive direction is "not easy" marks it as a genuine target for a future proof-bearing pass, not a formality.

Difficulty

The definitional trap mirrors Chapter I's: "for every convex $\varphi$" must be a genuine universal quantifier over Mathlib's own convexity predicate, with the existence of both expectations stated as an explicit integrability hypothesis inside the quantifier, not assumed globally or dropped. The coupling theorem doubles the difficulty of Theorem 1.A.1's: the conditional-expectation condition $E[\hat Y\mid\hat X]=\hat X$ a.s. is with respect to the $\sigma$-algebra generated by $\hat X$, not an informal "expected value given $\hat X$", and must use the martingale API's own convention (Mathlib's condExp) precisely. The "Furthermore" clause compounds this: it is a claim about the regular conditional distribution of $\hat Y$ given $\hat X=x$ for every point $x$, not merely the conditional expectation, and dropping it silently (as a "remark" rather than part of the theorem) would understate what Theorem 3.A.4 actually claims — the chapter brief flags this explicitly as a trap, and it is kept as a conjunct of the same existential witness here.

Formalization scope

Random variables are again measurable functions into $\mathbb{R}$ from arbitrary measurable spaces, ConvexOrder μ ν X Y taking $X$ on $(\Omega,\mu)$ and $Y$ on a separate $(\Omega',\nu)$, matching Chapter I's convention and this series' own pattern. Convexity is Mathlib's ConvexOn ℝ Set.univ φ; "equality in law" is again ProbabilityTheory.IdentDistrib. The martingale condition uses Mathlib's conditional-expectation notation ρ[Ŷ | m] =ᵐ[ρ] X̂ with m the $\sigma$-algebra MeasurableSpace.comap X̂ inferInstance generated by X̂ — the martingale API's own convention, not a hand-rolled gloss. The "Furthermore" clause uses Mathlib's ProbabilityTheory.condDistrib, the regular conditional distribution kernel of Ŷ given X̂ (available since ℝ is a standard Borel space), and states "increasing in x in ≤st" via the kernel's survival function being monotone in x at every threshold — restating, locally to this chapter's namespace, the same tail-probability shape Chapter I's UsualOrder uses (drafts cannot import another mission's definitions, per this series' convention). A trivializing formalization is ruled out explicitly: the martingale and monotonicity conjuncts are both kept as genuine content of the existential witness in the goal theorem, not weakened to a bare coupling or dropped as an optional remark.

This mission draws on no platform prior art (searches for "convex order", "Strassen", "martingale", "Jensen" returned only unrelated geometry/algorithm/physics results as of 2026-09-18); Mathlib's Probability/Martingale/* supplies the conditional-expectation and kernel machinery the coupling condition and its "Furthermore" clause are built from, but no platform theorem states the convex order or its coupling characterization itself. Reusable beyond this mission: the condExp/condDistrib-based martingale-coupling pattern is the shape Chapter IV's analogous submartingale coupling (Theorem 4.A.5) and Chapter VII's multivariate convex order (Theorem 7.A.1) are each expected to restate independently.

Selected references

• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5
• M. Rothschild and J. E. Stiglitz, "Increasing risk: I. A definition", Journal of Economic Theory, 2(3), 1970, 225–243. https://doi.org/10.1016/0022-0531(70)90038-4

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.

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

A multistage stochastic program's exact deterministic equivalent grows exponentially with the number of periods, even when each period's random data takes only a handful of values (Chapter 9's concern was the growth in the number of realizations; Chapter 10 adds growth in the number of periods). One remedy, generalizing Chapter 8's single-period Jensen bound, is to replace the exact per-period random data by a coarser, aggregated version — conditional expectations over a partition of the history space at each stage — and solve the resulting smaller deterministic equivalent instead. This is only useful if the aggregated problem's optimal value is provably a bound (here, a lower bound) on the exact problem's, and Birge & Louveaux's Chapter 10, §10.1, Theorem 1 is exactly the statement that makes this legitimate, together with a genuinely necessary extra condition the book states explicitly two paragraphs before the theorem: "if not [i.e. if the extra condition fails], then the conditional expectation form ... may not actually achieve a bound." This mission formalizes that theorem.

Setting

The book's exact multistage stochastic linear program (Eq. 1.1, p. 418) is

min c¹x¹ + E_Ω[c²x² + ⋯ + cᴴxᴴ]
s.t. W¹x¹ = h¹,  Tᵗ⁻¹xᵗ⁻¹ + Wᵗxᵗ = hᵗ (t=2,…,H, a.s.),  xᵗ ≥ 0 a.s., xᵗ nonanticipative (Σᵗ-measurable),

over the exact event space Ω = Ω₁ × ⋯ × Ω_H. Given a consistent nested partition of each Ωᵗ = Ω₁ × ⋯ × Ωₜ into finitely many blocks Sᵗ₁, …, Sᵗ_νₜ, and aggregated data (h̄ᵗᵢ, T̄ᵗᵢ) = E^{Sᵗᵢ}[(hᵗ,Tᵗ)] (the conditional expectation of the true random data over block i), the aggregated problem (Eq. 1.2, p. 419) replaces the exact recursion by a finite tree of blocks, one decision per block, linked to its parent block's decision. Both (1.1) and (1.2) are, structurally, the same kind of object — a finite-tree deterministic-equivalent recourse LP — differing only in which tree and which node data they use; this mission formalizes that shared shape once (Tree, Instance, Feasible, obj) and instantiates it twice.

Formalized as: a shared Tree H structure (a finite node type, per-node stage, anc, and a root), the same representation Chunk 06's Multistage.Tree uses for the exact scenario tree of its own (different) chapter, restated here rather than imported (a draft cannot import another chunk's draft). An Instance H n m T bundles a tree's node-varying LP data (c, W, Tmat, h, p); Feasible/obj give its feasible set and objective. The exact problem (1.1) is Instance H n m TFine for a fine/exact tree TFine; the aggregated problem (1.2) is Instance H n m TCoarse for a coarser tree TCoarse, connected to TFine by an aggregation map agg : TFine.Node → TCoarse.Node.

Formalization targets

Goal — Chapter 10, Theorem 1 (p. 419)

agg respects the tree structure (root, stage, ancestor);
W, c agree between the fine and coarse instances (up to agg);
coarse.h, coarse.Tmat are the p-weighted conditional expectations of fine.h, fine.Tmat over
  each aggregation fiber;
∀ coarse nodes i,i' at the same stage sharing a "current-period outcome",
  coarse.h i = coarse.h i' ∧ coarse.Tmat i = coarse.Tmat i'
  ⟹ zCoarse ≤ zFine

This is the mission's only formalization target: BRIEF.md records that no separately numbered lemma precedes Theorem 1's proof in this section to serve as an independent milestone (the proof is a direct LP-duality argument against the theorem's own hypotheses), and that Chapter 8's Theorem 1 — the two-period case this theorem generalizes — is a cross-chapter dependency belonging to Chunk 08's own mission, not a milestone here. milestones.yaml is accordingly empty; see STATUS.md for the explicit accounting of what else in this chapter was considered and left out (Theorem 3, the aggregation error bound of §10.2, an unrelated and substantially heavier result).

Significance

Theorem 1 is what licenses every aggregation-based approximation scheme the rest of the book's multistage material builds on: it says precisely when replacing a multistage recourse problem's random data by within-period conditional expectations preserves a valid lower bound, and precisely identifies the condition (aggregated nodes sharing a current-period outcome must carry identical aggregated data) whose failure breaks the bound — a condition the book states is not decorative ("if not, then the conditional expectation form ... may not actually achieve a bound," p. 418). Formalizing it gives Prove2Me a first structural result connecting Chapter 8's single-period Jensen bound (Chunk 08) to genuinely multistage approximation, using the same finite-scenario-tree deterministic-equivalent representation Chunk 06 uses for the exact nested Benders decomposition — the two missions' shared representation choice (documented in both STATUS.md files) means a future mission relating them formally (e.g. instantiating Chunk 06's exact tree as this mission's TFine) has a compatible object to work with, even though neither imports the other's draft.

Difficulty

The theorem's proof (p. 419-420) is a direct LP weak-duality argument: given an optimal dual solution to the aggregated problem, the book constructs a dual-feasible solution to the exact problem attaining the same value, using precisely the "common outcome ⟹ equal aggregated data" hypothesis to make the constructed dual solution well-defined across the exact tree's finer structure. This is a real argument, not a citation, but it is left as sorry: formalizing the proof would need the multistage LP duality machinery (the "multistage version of Theorem 3.13" the book's own proof invokes, itself left as Exercise 1) that no chunk of this series has built. The value of this mission is the faithful statement of the bound and its exact hypotheses.

Formalization scope

• The book's own printed typo, resolved and documented. Theorem 1's hypothesis clause reads, as printed, "such that (ωt−1,ωt) ∈ Stj if and only if there exist some (ω̂t−1,ωt) ∈ Stj" — S^t_j appears on both sides of the "if and only if," where the sentence's own subject ("S^t_i and S^t_j that have a common outcome") requires the left side to range over S^t_i. Confirmed against a direct render of PDF page 436 (uv run --with pymupdf python), not assumed from OCR: the PDF's own typesetting has this repetition, not an artefact of text extraction. This formalization reads the corrected clause as "S^t_i and S^t_j project onto the same set of period-t outcomes" and states it via an explicit label type Θ and curOutcome : TCoarse.Node → Θ, since the aggregated tree alone does not carry a literal per-period outcome space to project onto (see Setting above — Tree records only history-node structure, not the underlying product space Ω = Ω₁ × ⋯ × Ω_H).
• W, c shared exactly, not aggregated, matching the book's explicit assumption that the recourse matrix and per-stage cost are deterministic and identical across (1.1) and (1.2) ("Wt known and not random," "ct = ct," p. 418) — formalized as direct equality hypotheses (hW_agree, hc_agree) rather than folding W/c into the conditional-expectation machinery that h/Tmat go through.
• zFine/zCoarse are hypothesis-characterized, not sInf-defined, avoiding the real infimum's junk value 0 on an unbounded-below or empty feasible set (reference/FAITHFULNESS_TRAPS.md trap 5) — neither tree-LP's feasible set is shown bounded or nonempty by the hypotheses alone.
• The conditional-expectation defining equations are weighted, p·h/p·Tmat, not h/Tmat alone, matching the book's own E^{Sti}[·] = (h̄ti,T̄ti) read as "the fiber-sum of p·(h,T) equals p_i·(h̄ti,T̄ti)" — the standard definition of a conditional expectation against counting measure on a finite partition. Instance's own hp_pos (every node's probability is strictly positive) rules out the degenerate case a bare unweighted equation would need to guard separately (a coarse node of probability 0, which cannot occur, is what the read-back of this theorem flags as the one case where the weighted equation would not pin down h_coarse/ Tmat_coarse themselves — moot here since hp_pos excludes it).
• Trivialization risk (this chapter's own). A formalization that let coarse.h/coarse.Tmat be arbitrary constants unrelated to fine.h/fine.Tmat (dropping the conditional-expectation defining equations) would still typecheck a "lower bound" conclusion but assert nothing about aggregation — exactly the risk BRIEF.md flags: "a formalization that treats (h̄ti,T̄ti) as arbitrary constants rather than as conditional expectations over a partition of the scenario space at time t loses the theorem's actual content." Both hCoarse_h/hCoarse_T (the defining equations) and hCommonOutcome (the theorem's own extra hypothesis) are load-bearing and present.

Selected references

• Birge, J.R., Louveaux, F. Introduction to Stochastic Programming, 2nd ed., Springer 2011, Chapter 10, §10.1 (pp. 417-420), Theorem 1 (p. 419).
• Birge, J.R. "Decomposition and partitioning methods for multistage stochastic linear programs." Operations Research 33 (1985), 989-1007 — the source Chapter 10's aggregation bounds draw on (cited in §10.2, the neighboring section this mission does not formalize).

Motivation

Two-stage stochastic programs with recourse — choose a first-stage decision $x$ now, observe a random outcome $\xi$, then choose a second-stage recourse decision $y(\xi)$ to repair whatever $x$ left infeasible or suboptimal — are the workhorse model of the field, used for capacity planning, inventory and financial portfolio problems since the 1950s (Dantzig 1955; Beale 1955). When $\xi$ ranges over a finite set of scenarios, the recourse function $Q$ that averages the second-stage cost over scenarios is piecewise linear and convex in $x$, so the overall problem is itself a large linear program — but one whose constraint matrix has a scenario for every column block and can be far too large to hand to a general-purpose LP solver directly. Van Slyke and Wets' L-shaped method (1969), the subject of this mission, is the algorithm that made two-stage recourse problems with finite scenario sets practically solvable: it is Benders decomposition specialized to this block structure, alternating between a small master program over $x$ (and a scalar $\theta$ approximating the recourse cost) and, at each candidate $x$, a batch of second-stage linear programs that either certify $x$'s second-stage feasibility or supply a linear underestimate — a cut — of $Q$ around $x$. Birge & Louveaux's Introduction to Stochastic Programming (2nd ed., Springer 2011), Chapter 5 §5.1, gives the algorithm and proves its two central guarantees: a shortcut feasibility test for a special case (Theorem 1) and the algorithm's finite convergence in general (Theorem 2), which is this mission's goal.

Setting

A two-stage recourse instance consists of a first-stage feasible region $K_1 = \{x \mid Ax = b,\ x \ge 0\}$ for $x \in \mathbb{R}^{n_1}$, and, for each of $K$ finite scenarios $k = 1, \dots, K$ (occurring with probability $p_k$), second-stage data $(q_k, h_k, T_k)$ defining the recourse subproblem

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

where the recourse matrix $W$ is fixed — the same across every scenario, the case this chapter treats. $K_2 = \{x \mid Q(x,\xi_k) < \infty \text{ for all } k\}$ is the set of $x$ for which every scenario's subproblem is feasible, and the two-stage problem is

$$\min_{x} \ c^\top x + Q(x) \quad \text{s.t.} \quad x \in K_1 \cap K_2, \qquad Q(x) = \sum_{k=1}^K p_k\, Q(x, \xi_k).$$

A basis of the recourse subproblem is an injective choice of $m_2$ of $W$'s columns (where $m_2$ is $W$'s row count); each basis $b$ determines a simplex multiplier $\pi = (W_b^\top)^{-1} q_b$, and when $b$ attains the true optimum of $Q(x,\xi_k)$, LP duality gives $Q(x,\xi_k) = \pi^\top(h_k - T_k x)$ — the mechanism that turns a batch of second-stage LP solves into linear cuts on $x$.

Formalization targets

The L-shaped algorithm proceeds in three steps, repeated until neither applies:

• Step 1 solves the current master program (the $K_1$-feasible $x$, plus $\theta$ once at least one optimality cut exists, minimizing $c^\top x + \theta$ subject to every cut recorded so far — or just $c^\top x$ over $K_1$ before the first optimality cut, matching the book's convention that $\theta$ "is set equal to $-\infty$ and is not considered" until then).
• Step 2 tests each scenario's second-stage feasibility at the Step-1 optimum via an auxiliary LP; if some scenario fails (the LP's optimal value is positive), its optimal basis yields a feasibility cut and the algorithm returns to Step 1.
• Step 3, once every scenario is feasible, checks whether $\theta$ already dominates the true recourse cost at $x$ (using each scenario's optimal basis via LP duality); if not, an optimality cut is added and the algorithm returns to Step 1; if so, $x$ is optimal and the algorithm stops.

Goal — Chapter 5, Theorem 2 (p. 198)

$$\text{When } \xi \text{ is a finite random variable, the L-shaped algorithm finitely converges to}$$ $$\text{an optimal solution when it exists, or proves } K_1 \cap K_2 = \varnothing.$$

Formalized as: starting from the empty cut set, there is a finite-length run of the algorithm's Step-1/2/3 transition relation, of length bounded by the total number of distinct feasibility- and optimality-cut witnesses available, ending at a state admitting no further step — at which point either the master program has become infeasible (certifying $K_1 \cap K_2 = \varnothing$) or its optimum is second-stage feasible, passes every fresh Step-3 test, and is optimal for the two-stage problem.

Milestone — Chapter 5, Theorem 1 (p. 194)

$$\text{If } T \text{ is deterministic, } W \text{ is such that every } t \ge 0 \text{ lies in } \mathrm{pos}\,W,$$ $$\text{and } a = \min_k h_k \text{ (componentwise) is attained by some scenario } h_\ell,$$ $$\text{then } x \in K_2 \iff \exists\, y \ge 0,\ Wy = a - Tx.$$

A shortcut avoiding $K$ separate feasibility LPs at Step 2: under these structural assumptions on $W$, checking feasibility at the single componentwise-worst right-hand side certifies feasibility at every scenario simultaneously.

Significance

Van Slyke and Wets' method (and Benders decomposition more generally, of which it is the recourse-problem specialization) underlies essentially every large-scale two-stage stochastic program solved in practice, and its finite-convergence guarantee — not merely that an optimum exists, but that this specific cutting-plane procedure reaches it in finitely many outer iterations — is what makes the method a decision procedure rather than a heuristic. The proof's content is an explicit finiteness argument (the number of distinct simplex bases of the recourse subproblem and the feasibility-test LP is finite, so the algorithm cannot generate infinitely many distinct cuts before either exhausting the feasible region or converging), not a general compactness or fixed-point argument; formalizing it means formalizing the cutting-plane mechanism itself as a transition system and proving termination combinatorially, over the finite type of available bases, rather than proving only that some optimal $x$ exists.

Difficulty

The natural shortcut — state only "an optimal $x$ exists, or $K_1 \cap K_2 = \varnothing$" — is not Theorem 2's actual content and is not what this mission targets: that weaker claim would already follow from $K_1 \cap K_2$ being a nonempty polyhedron (or empty), with no reference to the algorithm at all, and would not require the finiteness-of-bases argument the book's proof turns on. The genuine difficulty is representing Steps 1-3 faithfully as a relation on accumulating cut sets, and pinning the termination bound to the actual combinatorial object the book cites (the finite set of bases of the two LPs the algorithm solves at each iteration) rather than to a numeral or an abstract compactness bound. A second, quieter difficulty is Step 1's own optimum: once optimality cuts exist, the master program optimizes $c^\top x + \theta$ jointly, but before the first one it optimizes $c^\top x$ alone; conflating the two (e.g. always requiring $\theta$ to be part of the optimum) does not match Step 1 as the book states it.

Formalization scope

First-stage and second-stage vectors are Fin n1 → ℝ / Fin n2 → ℝ; the finite scenario set is Fin K with probability vector p. A basis is {b : Fin m2 → Fin n2 // Function.Injective b} (m2 = the recourse matrix's row count), matching "an injective choice of $m_2$ columns of $W$"; its finiteness is definitional, from Fin m2 → Fin n2 being finite. Simplex multipliers use Matrix.inv, whose junk value 0 on a singular matrix is never reachable in a proof because multipliers are only ever used through an IsOptimalAt/IsFeasBasisOptimalAt hypothesis that pins the basis to one genuinely attaining the LP's true optimum. The recourse value $Q(x,\xi_k)$ is EReal-valued (reusing this series' Instance/QVal convention from Chunk 03), so an optimality-cut witness's claimed value is compared to it by an explicit EReal cast, never by EReal arithmetic. The algorithm's state is a pair of finite sets of witnesses recorded so far (Finset (Fin K × FeasBasis n2 m2) × Finset (Fin K → Basis n2 m2)); Step is an inductive relation with one constructor per Step-2 and Step-3 branch, each requiring its witness not already recorded, and the goal states a bounded-length Step-path from the empty state to a state admitting no further Step. This mission does not restate Chapter 3's polyhedrality fact about $K_2$ as a separate lemma: the finiteness fact it is invoked for is already exposed directly and structurally by the finite Fintype bound on the number of bases, so no additional axiom stands in for it (see MODERATION_NOTES.md). Lemmas 3-9 and Theorem 10 of §5.2 (Regularized Decomposition, a different algorithm) are out of scope. The trivializing formalization this mission rules out is exactly the one named under Difficulty above: a bare existence-of-optimal-or- infeasible-$x$ statement with no reference to Steps 1-3 or to a finite bound on the number of iterations — such a statement would be true of any nonempty polyhedron and would not be Theorem 2.

Selected references

• R. Van Slyke and R. Wets, L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming, SIAM Journal on Applied Mathematics, 17(4), 1969, pp. 638-663. https://doi.org/10.1137/0117061
• J. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Chapter 5. https://doi.org/10.1007/978-1-4614-0237-4
• G. Dantzig, Linear Programming under Uncertainty, Management Science, 1(3-4), 1955, pp. 197-206. https://doi.org/10.1287/mnsc.1.3-4.197

Motivation

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

Setting

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

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

Formalization targets

Goal — Theorem 2.8.2 (Topkis's theorem)

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

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

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

Theorem 2.8.1 (the underlying, more elementary sufficient condition)

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

Theorem 2.8.4 (strict strengthening)

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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