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

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)

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

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)

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

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)

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

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

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.

Multi-agent reinforcement learning approximates a global value function by summing per-agent local value functions learned independently — a trick that works surprisingly well in practice (ride-hailing dispatch, restless bandits) but had no general theoretical justification. Chen and Peng (arXiv:2506.02385) explain why: they define a Markov entanglement measure for the joint transition dynamics of a multi-agent MDP, directly analogous to quantum entanglement of a two-party state, and show it controls exactly how much error this value-decomposition trick incurs. This mission formalizes their sharpest quantitative bound (Theorem 4): the error of decomposing the global Q-function into per-agent local Q-functions is controlled, entrywise, by the agent-wise total-variation measure of Markov entanglement.

Motivation

A delivery company can assign each driver a permanent district instead of allowing every driver to serve the whole city. This makes dispatching simpler, but it raises a service question: if the districts receive almost equal shares of demand and travel workload, how different can their expected delivery times be? Carlsson, Liu, Salari and Yu study this question for a region partitioning policy in which one vehicle serves each district. Their Proposition 3 gives an explicit error bound for a partition whose shares are accurate within a tolerance ε. The proposition complements their exact equitability result, Theorem 6, by quantifying the effect of a partition that can only be computed approximately.

Setting

The service region R is a compact convex subset of the Euclidean plane, with depot x₀ ∈ R. Orders arrive at a rate λ and have locations distributed with density f on R. The density is nonnegative, Lipschitz on R, and normalized by ∫_R f(x) dx = 1. There are m ≥ 1 identical vehicles, each with speed v > 0 and capacity q ≥ 1. An order requires a mean on site service time s̄ ≥ 0. The positive constant β is the geometric constant in the paper's heavy traffic delivery time expression. A partition R₁, …, R_m covers R, with districts disjoint up to area zero; vehicle i serves R_i.

For a measurable district S, let p(S) = ∫_S f(x) dx be its share of demand. Its arrival rate is λ_S = λp(S), and its conditional density is f_S(x) = f(x)/p(S) when p(S) > 0. The paper uses two partition measures:

The first controls the leading travel term. The second combines service time and radial travel from the depot. A partition is ε equitable when, for every district i and each j ∈ {1,2}, the difference between μ_j(R_i) and μ_j(R)/m has absolute value at most ε.

For vehicle count k, arrival rate a, region S, and density g, write the workload factor as

The heavy traffic expression from the paper's Theorem 3 is

The comparison value is L* = L(m,λ,R,f). For district i, the value L_i = L(1,λ_{R_i},R_i,f_{R_i}) uses that district's own arrival rate, density, and workload factor.

Formalization targets

Proposition 3: approximate districts

For λ > 0 with W(m,λ,R,f) < 1, ε ≥ 0, and an ε equitable partition, define the corrected tolerance factor

When η < 1, the target is the two sided estimate

The first milestone rewrites each district's Theorem 3 expression using μ₁(R_i) and μ₂(R_i). The next two milestones give upper and lower comparisons with L*. The final algebraic milestone evaluates the larger of the two relative deviations. These are the displayed steps on the paper's e companion pages ec6 and ec12–ec13.

The printed Proposition 3 uses max in the denominator defining η. Its proof requires min: when the two entries are 1 and 100 and ε = 0.1, a district can have L_i/L* = (1.1/0.999)² ≈ 1.212, while the printed η = 0.001 permits a deviation of only about 0.004. The correction is recorded in the theorem statements and audit notes.

Significance

The bound makes partition accuracy interpretable as a service guarantee. Once both shares are close enough that η < 1, every district's leading delivery time lies in a controlled interval around the flexible policy's benchmark. It states a guarantee for each district, rather than just for a demand weighted average, so it addresses unequal service across the region.

The authors prove the displayed comparison in their accepted manuscript. This mission formalizes the comparison between explicit heavy traffic expressions; it does not claim a new queueing theorem or a machine checked proof of the stochastic model. The reusable output is a precise Lean interface for spatial demand integrals, workload, conditional district densities, and perturbation bounds involving both numerator and denominator errors. The theorem items are proof targets.

Difficulty

The denominator responds to the μ₂ error in the opposite direction from the numerator's response to the μ₁ error. Bounding their ratio requires both the district workload and the lower numerator estimate to stay in their proper sign ranges. Simply squaring the ε share inequalities is invalid until those signs are known. The condition η < 1 supplies the required room; it also rules out a zero probability district under the other hypotheses. The printed choice of max for η fails to control the error in whichever of the two scales is smaller.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin 2), Lebesgue set integrals, and real valued leading terms. The density, region, depot, fleet parameters, and positive β are fixed while λ and ε vary. The source's compactness, convexity, Lipschitz density, normalization, positive vehicle count, speed, and capacity, and nonnegative mean service time are included in a single standing predicate. A partition has null measurable pieces, pairwise disjoint almost everywhere, and exact union R; shared district boundaries have area zero. The goal also states λ > 0, global workload < 1, ε ≥ 0, and η < 1, matching the stable regime and the proof's small ε condition. Capacity q = 1 remains admitted: both leading terms then vanish and the inequality still holds.

The stochastic renewal arrivals, routing policy, and queueing process are outside this development. Theorem 3 supplies the paper's leading expression, applied separately to the full region and each district. Thus L_i and L* here are leading expressions at one fixed λ, not the underlying expected delivery time functions. A fixed positive ε makes η grow near the heavy traffic boundary, so the page's parenthetical “in heavy traffic” is read through the leading expressions used by its proof. The district value is formed from λ_{R_i} and f_{R_i}; it is not defined from the global benchmark or from the right hand side of the first milestone.

A complete proof will need standard facts about set integrals and square roots, the normalization of a conditional density, and inequalities for positive real denominators. The setting definitions can support other region partition comparisons. Contributions establishing these identities and the upper and lower estimates are welcome.

Selected references

• J. G. Carlsson, S. Liu, N. Salari, and H. Yu, Provably Good Region Partitioning for On-Time Last-Mile Delivery, accepted manuscript, SSRN 3915544; published in Operations Research 72(1), 91–109 (2024), DOI: 10.1287/opre.2021.0588. Proposition 3, printed p. 21; proofs on pp. ec6 and ec12–ec13.
• D. J. Bertsimas and G. J. van Ryzin, Stochastic and Dynamic Vehicle Routing with General Demand and Interarrival Time Distributions, Advances in Applied Probability 25(4), 947–978 (1993), DOI: 10.2307/1427801. Source of the heavy traffic expression cited as Theorem 3 in the Carlsson et al. manuscript.