Stochastic Systems

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.

Motivation

On-demand delivery platforms for meals and groceries promise delivery within minutes, and the main operational lever they control is how a courier is dispatched. A courier can carry each order as soon as it is ready (dedicated delivery), or wait until two orders are available and deliver them in one trip (batch delivery). Batching saves travel per order but makes the first customer wait for a second order to arrive. Which mode gives the shorter wait, and hence the higher revenue, is a question practitioners face daily; it is the subject of M. Chen and M. Hu, Courier Dispatch in On-Demand Delivery (SSRN 3675063; published in Management Science, DOI 10.1287/mnsc.2023.4858).

The paper answers the question in closed form for a stylized disk model. This mission formalizes its first headline result, for the case in which the demand rate is fixed exogenously (for example by a growth target or by kitchen capacity), as stated in Propositions 1 and 2 of the authors' version dated 2022-09-21.

Setting

A vendor sits at the centre of a disk of radius $r>0$ and employs one courier with unit travel speed, so travel time equals travel distance. Customer orders arrive as a Poisson process of rate $\lambda>0$, the demand rate, and each customer's location is independent and uniformly distributed on the disk.

Under dedicated delivery each trip is a round trip to one customer, of length $X_D=2\|U\|$ with $U$ uniform on the disk. Its moments are $\mathbb E[X_D]=\tfrac43 r$ and $\mathbb E[X_D^2]=2r^2$, so the courier is an M/G/1 server with

where $\mu_D$ is the service rate and $C_D$ the summed coefficients of variation. The paper defines the expected wait under dedicated delivery as the M/G/1 in-line delay

Under batch delivery the courier leaves only with two orders and visits both, so a trip has length $X_B=\|U\|+\|U-U'\|+\|U'\|$ for two independent uniform points, with $\mathbb E[X_B]=\big(\tfrac{128}{45\pi}+\tfrac43\big)r$. This gives

and a variability coefficient $C_B\approx 0.583$ that the paper obtains by numerical integration. The paper defines the batch wait as the time for a second order to arrive, plus Kingman's approximation of the E$_2$/G/1 in-line delay, plus the expected delay of being second in a batch:

Customers have valuations with c.d.f. $F$ on $[0,1]$ and a wait cost $c>0$ per unit time; at price $p$ the potential arrival rate $\Lambda r^2$ thins to $\lambda$. The vendor's revenue rate at demand rate $\lambda$ and expected wait $w$ is

Dedicated delivery is stable exactly when $\lambda r<\tfrac34$; batch delivery when $\lambda r<T_2=\frac{45\pi}{2(32+15\pi)}\approx0.893$.

Formalization targets

Goal: one threshold in $\lambda r$ (Propositions 1 and 2)

For every $C_B\in[0.58,0.59]$ there is a constant $a_1\in(0,\tfrac34)$ such that for all $r>0$, $\lambda>0$ with $\lambda r<\tfrac34$,

and the same two equivalences hold for the revenues $V(\lambda,W_D)$ and $V(\lambda,W_B)$, for every $F^{-1}$, every $\Lambda>0$ with $\lambda\le\Lambda r^2$, and every $c>0$. The paper reports $a_1\approx0.5689$; the goal asserts only the existence and the location in $(0,\tfrac34)$.

Milestones

1. The dedicated trip moments $\mathbb E[X_D]=\tfrac43r$, $\mathbb E[X_D^2]=2r^2$, and the resulting $\mu_D$, $C_D$ (display (3)).
2. The mean batch trip $\mathbb E[X_B]=(\tfrac{128}{45\pi}+\tfrac43)r$ and the resulting $\mu_B$ (display (8), first moment).
3. The reduction (A.1): $W_D(\lambda,\mu_D,C_D)-W_B(\lambda,\mu_B,C_B)=f_A(\lambda r)/\lambda$ for an explicit rational function $f_A$ of one variable.
4. The single crossing: $f_A$ has exactly one zero $a_1$ on $(0,\tfrac34)$, negative before and positive after, with $0.56<a_1<0.58$.
5. Proposition 1: for each $r$, a threshold $\lambda_{ex}\in(0,\mu_D)$ in the demand rate.
6. Proposition 2: for each $\lambda$, a threshold $r_{ex}\in(0,\tfrac3{4\lambda})$ in the radius.

Significance

The result says that, with demand fixed, the choice between dedicated and batch delivery depends on the market only through the product $\lambda r$: dedicated delivery is better when demand is low or the area small, batching when demand is high or the area large. The threshold is a single universal number, independent of the valuation distribution and of the wait-cost rate, because at a fixed demand rate the strategy with the shorter wait always earns more. This is the efficiency-driven benchmark against which the paper's second main result (endogenous demand in a crowded market, where the order reverses) is contrasted.

To our knowledge none of this has been machine-checked. The mission produces a checked version of the paper's closed-form comparison and, in milestones 1–2, checked computations of classical geometric-probability moments of the disk (the mean distance $128r/(45\pi)$ between two uniform points). The paper's own argument for the single crossing is numerical ("solved using standard methods"); a formal proof must replace it by an exact argument with rigorous bounds on $\pi$.

Difficulty

The reduction to one variable is algebra. The difficulty is the sign analysis of $f_A$ on $(0,\tfrac34)$: it is a difference of two rational functions with poles at $\tfrac34$ and $T_2\approx0.893$, involving $\pi$, and clearing denominators gives a cubic whose roots the paper only reports numerically. The natural first idea, showing $f_A$ is monotone on the whole interval, does not apply directly, since $f_A$ starts at $-\tfrac12$, first decreases, and only later rises to $+\infty$; a proof must establish that it crosses zero exactly once. A further point is that $C_B$ is not a closed-form number, so the crossing must be shown uniformly over an interval of values.

The moment milestones need integration in polar coordinates on the plane; the mean distance between two uniform points of a disk is a classical but nontrivial four-dimensional integral.

Formalization scope

All objects live in the namespace CourierDispatch.Exogenous. Real numbers are ℝ, $\lambda$ is lam, $\Lambda$ is Lam, and $F^{-1}$ is an arbitrary function Q : ℝ → ℝ (no property of it is needed, since at equal $\lambda$ the price terms cancel). The plane is EuclideanSpace ℝ (Fin 2) and the uniform law on the disk is Lebesgue measure conditioned on the closed ball.

Committed conventions:

• The expected waits are the paper's closed-form formulas (5) and (12): the M/G/1 in-line delay for dedicated delivery and Kingman's approximation for the E$_2$/G/1 batch queue. The paper introduces them as definitions ("$:=$"), and the mission does not formalize the queues behind them; no statement here is about the true stationary delay of an E$_2$/G/1 queue.
• $C_B$ is a real parameter with the standing hypothesis $0.58\le C_B\le 0.59$, which contains the paper's value $0.583$ and a Monte-Carlo estimate $0.58297$.
• Every comparison is restricted to $r>0$, $\lambda>0$, $\lambda r<\tfrac34$, the range where both queues are stable; above it only batch delivery is defined and the paper makes no comparison. This also keeps every formula away from Lean's junk values for division by zero.
• Revenue comparisons additionally require $\Lambda>0$ and $\lambda\le\Lambda r^2$, the effective-demand range in §3, p. 8. The arbitrary function Q stands for $F^{-1}$; its properties cancel when the two strategies are compared at the same demand rate.
• Both directions of each threshold are stated as strict equivalences, so equality at $\lambda r=a_1$ follows.

The threshold $a_1$ (and $\lambda_{ex}$, $r_{ex}$) is existential in every statement; it is never a definition and never an infimum of a sign set, and $W_D$, $W_B$ are never defined through $f_A$, so the goal cannot be made true by construction.

Needed infrastructure: polar-coordinate integration on the plane (Mathlib's integral_comp_polarCoord_symm), and rigorous rational bounds on $\pi$ (Real.pi_gt_d6, Real.pi_lt_d6). The goal does not depend on the moment milestones 1–2, which ground the constants $\mu_D$, $C_D$, $\mu_B$ in the geometry of the disk and are welcome as separate contributions.

Selected references

• M. Chen, M. Hu, Courier Dispatch in On-Demand Delivery, SSRN 3675063, version of 2022-09-21; Management Science, 2023. https://ssrn.com/abstract=3675063, https://doi.org/10.1287/mnsc.2023.4858
• J. F. C. Kingman, On queues in heavy traffic, Journal of the Royal Statistical Society B 24 (1962). https://doi.org/10.1111/j.2517-6161.1962.tb00465.x
• H. Solomon, Geometric Probability, SIAM CBMS-NSF Regional Conference Series 28, 1978. https://doi.org/10.1137/1.9781611970418
• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651

Motivation

The Black–Scholes model (Black and Scholes, 1973; Merton, 1973) is the reference model for pricing European options. Its closed-form price, the Black–Scholes formula, is quoted daily by options markets, its partial derivatives (the Greeks) are the standard risk measures that trading desks limit and hedge, and the Black–Scholes equation is the prototype of the parabolic pricing PDEs that are solved numerically when no closed form exists. Merton and Scholes received the 1997 Nobel Memorial Prize in Economic Sciences for this work.

Timeline. Bachelier (1900) first applied Brownian motion to option pricing. In the 1960s Sprenkle, Boness, Samuelson and Merton refined the theory. Black and Scholes found the risk-neutral hedging argument in 1968 and published the formula in The Pricing of Options and Corporate Liabilities (Journal of Political Economy, 1973); Merton's paper of the same year extended the mathematical framework and coined the name.

Setting

Fix a strike $K>0$, an expiry $T$, a constant risk-free rate $r\in\mathbb R$ and a constant volatility $\sigma>0$. At time $t<T$ the time to maturity is $\tau=T-t>0$ and the spot price of the (non-dividend-paying) stock is $S>0$. Let

be the standard normal distribution and density functions, and set

The Black–Scholes call and put prices are

In the alternative (Black '76) parametrisation one uses the discount factor $D=e^{-r\tau}$ and the forward price $F=e^{r\tau}S$, with $d_\pm=\frac1{\sigma\sqrt\tau}\big[\ln\frac FK\pm\frac12\sigma^2\tau\big]$, and $C=D[N(d_+)F-N(d_-)K]$. Under the risk-neutral measure the terminal price is $S_T=S\exp\big((r-\tfrac12\sigma^2)\tau+\sigma\sqrt\tau\,Z\big)$ with $Z$ standard normal.

Formalization targets

Goal: the formula solves the Black–Scholes equation

On the domain $\{S>0,\ t<T\}$ the call price $C$ is $C^\infty$ and satisfies

together with the boundary and terminal conditions $C(S,t)\to0$ as $S\to0^+$, $C(S,t)-(S-Ke^{-r(T-t)})\to0$ as $S\to\infty$, and $C(S,t)\to\max\{S-K,0\}$ as $t\to T^-$.

Milestones

1. The density $N'$ is the derivative of $N$.
2. The alternative (forward) formulation of the call and put prices.
3. Put–call parity, $P=Ke^{-r\tau}-S+C$, and its forward form $C-P=D(F-K)$.
4. The Greeks table: Delta, Gamma, Vega, Theta and Rho for calls and puts.
5. Risk-neutral pricing: $C=e^{-r\tau}\,\mathbb E[\max(S_T-K,0)]$.
6. Binary options: cash-or-nothing values $e^{-r\tau}N(\pm d_-)$ and asset-or-nothing values $SN(\pm d_+)$.

Significance

The result. The goal is the statement that ties the model's two faces together: the closed-form price is a classical solution of the pricing PDE with the payoff as terminal datum. The Greeks are what hedging strategies are built from (delta hedging is the core of the model's replication argument), put–call parity is the basic no-arbitrage relation, and the risk-neutral and binary-option identities are the probabilistic reading of the two terms in the formula.

Formalizing it. All results here are classical and proved in textbooks (e.g. Hull, Options, Futures, and Other Derivatives). The work is formalization: building a reusable, machine-checked library for the normal distribution function, the Black–Scholes price and its sensitivities, and Gaussian expectations of log-normal payoffs, on top of Mathlib's real analysis and its Gaussian measure gaussianReal.

Difficulty

Each identity is elementary on paper, but the calculus is long: every Greek requires differentiating $N\circ d_\pm$ through a logarithm, a square root and a quotient, and the simplifications rest on the identity $SN'(d_+)=Ke^{-r\tau}N'(d_-)$. The limits in the goal need Gaussian tail estimates (e.g. $SN(-d_+)\to0$ as $S\to\infty$, where $S$ grows while $N(-d_+)$ decays). The risk-neutral identities require computing Gaussian integrals over half-lines with an exponential weight, i.e. a change of variables shifting the mean of the normal distribution.

Formalization scope

All objects are real-valued and deterministic: $N$ is defined by the integral formula above (a Lebesgue integral over $(-\infty,x]$), $N'$ by its closed form, and prices by the formulas, as functions of $(S,t)$ with parameters $(K,r,\sigma,T)$. Partial derivatives are stated with HasDerivAt (genuine differentiability plus the value), except in the goal's PDE, where deriv is used together with an explicit $C^\infty$ clause on the open domain. Each theorem carries the standing assumptions $K>0$, $\sigma>0$, $S>0$, $t<T$ where they are needed; the parity identities hold without them and are stated unconditionally. At $S=0$ and $t=T$ the formula is undefined in the source, so the boundary and terminal conditions are stated as one-sided limits rather than values. Risk-neutral expectations are integrals against the standard Gaussian gaussianReal 0 1 of an explicit log-normal terminal price; no stochastic calculus (Itô integrals, SDEs, Girsanov, Feynman–Kac) is required or formalized. The dividend-paying extensions, American options and the perpetual put are out of scope; binary options are formalized for the non-dividend case $q=0$.

Contributions of reusable lemmas (derivative of $N$, symmetry $N(x)+N(-x)=1$, limits of $N$ at $\pm\infty$, Gaussian half-line integrals) are welcome.

Selected references

• F. Black, M. Scholes, The Pricing of Options and Corporate Liabilities, Journal of Political Economy 81(3), 1973. https://doi.org/10.1086/260062
• R. C. Merton, Theory of Rational Option Pricing, Bell Journal of Economics and Management Science 4(1), 1973. https://doi.org/10.2307/3003143
• J. C. Hull, Options, Futures, and Other Derivatives, Pearson.
• Wikipedia, Black–Scholes model. https://en.wikipedia.org/wiki/Black%E2%80%93Scholes_model

Motivation

A forward–backward stochastic differential equation (FBSDE) couples a forward diffusion $X$ with a backward equation for a pair $(Y,Z)$ whose terminal value depends on $X_T$. FBSDEs are the probabilistic form of quasilinear parabolic PDEs and appear in stochastic control (the stochastic maximum principle), in mathematical finance (hedging with large investors, stochastic differential utility) and in mean-field games. Their solvability over an arbitrary horizon is delicate: the coupling can make a solution exist only on short time intervals.

Ma, Wu, Zhang and Zhang (arXiv:1110.4658v2, Ann. Appl. Probab. 25 (2015)) reduce well-posedness of a general one-dimensional FBSDE to the behaviour of two scalar dominating ODEs: when these have solutions that stay bounded on $[0,T]$, the FBSDE has a regular decoupling field and a unique solution. Section 5.1 of the paper tests this programme on the simplest class, the linear FBSDE with constant coefficients, and obtains necessary and sufficient conditions. The authors describe these as setting the "limits" for the solvability of general FBSDEs.

Earlier approaches each covered part of the picture: the method of contraction mappings for small time (Antonelli 1993, MR1233625), the four-step scheme for Markovian FBSDEs with regular coefficients (Ma, Protter, Yong 1994, MR1262970), and the method of continuation under monotonicity conditions (Hu, Peng 1995, MR1355060; Peng, Wu 1999, MR1675098; later Yong 1997, MR1440146). The unified approach of the paper contains these as special cases.

Setting

Let $b_1,b_2,b_3,\sigma_1,\sigma_2,f_1,f_2,f_3,h$ be real numbers and consider the linear FBSDE (4.1)

in Case 1, $\sigma_3=0$. Then the two dominating ODEs coincide and become the scalar backward equation

with the cubic

In the Appendix's notation (A.3), $F(y)=f_1+a_1y+a_2y^2+a_3y^3$ with $a_1=f_2+b_1+\sigma_1f_3$, $a_2=b_2+f_3\sigma_2+b_3\sigma_1$, $a_3=\sigma_2b_3$.

A solution on $[0,T]$ of $y_t=h+\int_t^TG(s,y_s)\,ds$ is a function $y$ such that, for every $t\in[0,T]$, $s\mapsto G(s,y_s)$ is integrable on $[t,T]$ and the equation holds at $t$. A bounded solution additionally has $\sup_{[0,T]}|y|<\infty$. In Lean the coefficients form the structure UnifiedFBSDE.Cubic.Coeffs, $F$ is Coeffs.F, and the predicates are IsSolution and IsBoundedSolution.

Formalization targets

Goal: Theorem 5.3

Milestones

1. Lemma 5.1: comparison for backward ODEs. Between a bounded sub-solution and a bounded super-solution, (5.1) has a unique solution.
2. Remark 5.2: a checkable sufficient condition for hypothesis (iv) of Lemma 5.1.
3. Sufficiency of (i), (ii): the solution stays in $[h,\lambda]$ (resp. $[\lambda,h]$).
4. (5.5): under (iii), (5.3) is linear and has a bounded solution.
5. (A.4): if $a_3>0$ and $F$ has no zero in $[h,\infty)$, then $F(y)\ge\varepsilon(y-y_1)^3$ on $[h,\infty)$ for some $\varepsilon>0$, $y_1<h$.
6. (A.6): the explicit comparison solution $\tilde y_t-y_1=(2\varepsilon(t-T)+(h-y_1)^{-2})^{-1/2}$ and its blow-up time $T-1/(2\varepsilon(h-y_1)^2)$.
7. Blow-up by comparison: a continuous $G\ge\varepsilon(y-y_1)^3$ on $[h,\infty)$ admits no solution on $[0,T]$ when $T>1/(2\varepsilon(h-y_1)^2)$.
8. Case 2: if $a_3=0$, $a_2>0$, $F(h)>0$ and $F$ has no zero above $h$, then $F(y)\ge\varepsilon(y-y_1)^2$ on $[h,\infty)$ and (5.3) has no solution for $T$ large.

Companion: Theorem 5.4

For a fixed horizon $T$: (i) $\sigma_2b_3<0$ or $F(h)=0$; (ii) $F(h)>0$, $\sigma_2b_3\le\varepsilon$, $a_2\le\varepsilon$; (iii) $F(h)<0$, $\sigma_2b_3\le\varepsilon$, $a_2\ge-\varepsilon$, with $\varepsilon=\varepsilon(T)$ small. Each guarantees a bounded solution on $[0,T]$.

Significance

Theorem 5.3 turns the existence of a global bounded solution of the dominating ODE into a finite check on a cubic polynomial: the sign of $F(h)$, the location of a real root, and two coefficient identities. Through the paper's main construction, a bounded solution yields a uniformly Lipschitz decoupling field, and hence well-posedness of the linear FBSDE on any horizon. When none of (i)–(iii) holds, the dominating ODE explodes in finite time. This is the sense in which the paper says the constant-coefficient results "more or less set the 'limits'" for the solvability of general FBSDEs: the conditions it later imposes on random coefficients (§5.2, §7) are modelled on the cases (i)–(iii).

The result is proved in the paper: sufficiency on p. 21, necessity in the Appendix (pp. 46–47). To our knowledge none of it is machine-checked. A formalization produces a reusable comparison theorem for scalar backward integral equations with Lipschitz-on-a-band nonlinearities (Lemma 5.1), explicit finite-time blow-up criteria for polynomial ODEs, and a complete, checked classification of global solvability for the cubic Riccati-type equation (5.3).

Difficulty

Sufficiency rests on Lemma 5.1, which requires Carathéodory existence and uniqueness for an equation that is only Lipschitz on a time-dependent band, followed by an integrating-factor comparison argument. Mathlib's Picard–Lindelöf and Gronwall tools are stated for forward equations with continuous right-hand sides, so they need adaptation.

Necessity is a case analysis whose obvious version fails at two points. First, one cannot simply bound $F$ below by $a_3(y-y_1)^3$ using the smallest real root: the intermediate inequality (A.5) as printed points the wrong way for some root orderings, and the correct bound uses the largest root or an infimum over $[h,\infty)$. Second, the blow-up step compares a solution of (5.3) with an explicit exploding solution. This needs the solution to stay above $h$ for the whole interval, which in turn needs continuity of the right-hand side. For a discontinuous right-hand side the comparison fails.

Formalization scope

Time is real, with $0<T$ and $t\in[0,T]$. Solutions are functions $\mathbb R\to\mathbb R$ whose values outside $[0,T]$ are irrelevant. The integral $\int_t^T$ is Mathlib's interval integral. "For arbitrary $T$" is $\forall T>0,\ \exists y$, with the universal quantifier outside. "A zero point in $[h,\infty)$" is $\exists\lambda\ge h,\ F(\lambda)=0$.

Pinned readings, all disclosed in the items:

• Lemma 5.1 adds $y^1\le y^2$ on $[0,T]$ (the lemma is false without it), $L\ge0$, and integrability of $c^1,c^2$. Its $\alpha$ ranges over measurable functions with $|\alpha|\le L$, and $F^i$ is measurable on $\mathbb R\times\mathbb R$.
• The blow-up milestone assumes $G$ continuous.
• In Theorem 5.4(ii)–(iii), $\varepsilon$ is chosen after $T$, $h$, $f_1$ and $a_1$, the data its proof uses.
• (A.5) is not stated.

Trivializing formalizations are ruled out. The solution predicate carries integrability of the integrand, so Lean's junk value $0$ for a non-integrable integral cannot make an arbitrary $y$ with $y_t=h$ a solution. The goal assumes neither a zero of $F$ nor a blow-up: both are proved in the milestones. Lemma 5.1's uniqueness is over solutions in the band.

The needed infrastructure is scalar ODE theory on Mathlib: existence for Lipschitz Carathéodory equations, differentiation of $t\mapsto\int_t^T g$, comparison of sub- and super-solutions, and elementary real-root facts for cubics. The comparison lemma and the blow-up lemma are reusable beyond this mission. Contributions of either the sufficiency or the necessity chain are welcome independently.

Selected references

• J. Ma, Z. Wu, D. Zhang, J. Zhang, On well-posedness of forward–backward SDEs—a unified approach, Ann. Appl. Probab. 25(4):2168–2214, 2015. https://arxiv.org/abs/1110.4658 , https://doi.org/10.1214/14-AAP1046
• F. Antonelli, Backward–forward stochastic differential equations, Ann. Appl. Probab. 3(3):777–793, 1993. MR1233625, https://mathscinet.ams.org/mathscinet-getitem?mr=1233625
• J. Ma, P. Protter, J. Yong, Solving forward–backward stochastic differential equations explicitly—a four step scheme, Probab. Theory Related Fields 98:339–359, 1994. MR1262970, https://mathscinet.ams.org/mathscinet-getitem?mr=1262970
• Y. Hu, S. Peng, Solution of forward–backward stochastic differential equations, Probab. Theory Related Fields 103:273–283, 1995. MR1355060, https://mathscinet.ams.org/mathscinet-getitem?mr=1355060
• S. Peng, Z. Wu, Fully coupled forward–backward stochastic differential equations and applications to optimal control, SIAM J. Control Optim. 37(3):825–843, 1999. MR1675098, https://mathscinet.ams.org/mathscinet-getitem?mr=1675098
• J. Yong, Finding adapted solutions of forward–backward stochastic differential equations: method of continuation, Probab. Theory Related Fields 107:537–572, 1997. MR1440146, https://mathscinet.ams.org/mathscinet-getitem?mr=1440146

Multiscale reaction networks and the balance condition

Stochastic models of chemical reaction networks in cell biology routinely combine species present in a handful of copies with species present in thousands, and rate constants that differ by orders of magnitude. Simulating such a system exactly is expensive, and model reduction replaces it with a lower-dimensional limit. A systematic approach, developed by Ball, Kurtz, Popovic and Rempala (2006) and by Kang and Kurtz (arXiv:1011.1672), normalizes species numbers and rate constants by powers of a large parameter $N$ and derives limits as $N\to\infty$ on several time-scales.

For such limits to exist, the normalized species numbers must stay of order one. For a single species this is the species balance condition: either the fastest reaction producing it is as fast as the fastest reaction consuming it, or the time-scale considered is short enough that the imbalance does not show. Kang and Kurtz observed (arXiv:1011.1672v1, §3.2, p. 9) that this is not enough: a collection of species can be produced collectively at a different order of magnitude from the rate at which it is consumed, even when every member is balanced. They therefore impose a balance condition on every nonnegative linear combination of species, which is infinitely many conditions. Section 3.4 of their paper proves combinatorial lemmas that reduce the work of checking them. This mission formalizes the lemmas on positive combinations of two weight vectors.

Setting

A reaction network has $s_0$ species $S_1,\dots,S_{s_0}$ and $r_0$ reactions. Reaction $k$ consumes $\nu_{ik}\in\mathbb N$ molecules of $S_i$ and produces $\nu'_{ik}\in\mathbb N$; its net change is the vector $\zeta_k=\nu'_k-\nu_k$. Each species carries a scaling exponent $\alpha_i\ge0$ and each reaction an exponent $\beta_k\in\mathbb R$; put

the order of magnitude (as a power of $N$) of the rate of reaction $k$.

A weight vector $\theta\in[0,\infty)^{s_0}$ describes the linear combination $\theta\cdot X=\sum_i\theta_iX_i$. Its sign sets (Definition 3.1) are