Theorem 3.A.4 — Strassen's martingale-coupling characterization of the convex order (corrected: finite means, random variables)

Let $X$ on $(\Omega,\mu)$ and $Y$ on $(\Omega',\nu)$ be random variables with finite means (measurable and integrable, the standing assumption of §3.A). Then

i.e. $E[\hat Y \mid \hat X] = \hat X$ a.s. Furthermore, $\hat X$ and $\hat Y$ can be selected such that $[\hat Y \mid \hat X = x]$ is increasing in $x$ in the usual stochastic order $\le_{st}$. This is Strassen's martingale-coupling characterization of the convex order (the mean-preserving spread of Rothschild–Stiglitz): $X \le_{cx} Y$ holds exactly when a copy of each can be built on a common probability space so that the copy of $Y$ is, conditionally on the copy of $X$, a fair randomization of it whose conditional law grows in $\le_{st}$ with the conditioning value. The reverse direction is Jensen's inequality; the book calls the constructive direction "not easy to prove".

Formalization Note. The retired version assumed no integrability: Mathlib's conditional expectation of a non-integrable $\hat Y$ is the junk value $0$, so for $X = Y = 1/x$ on $(0,1]$ the order held reflexively while the martingale clause forced $\hat X = 0$ a.s., and the forward direction was refuted. The new statement makes the standing finite-mean assumption explicit (Integrable X μ, Integrable Y ν), so $\hat Y$ is integrable and $E[\hat Y\mid\hat X]$ is the honest conditional expectation; it also requires $X$, $Y$, $\hat X$, $\hat Y$ to be measurable (random variables) — Measurable X̂ is moreover what makes $\sigma(\hat X)$ a sub-σ-algebra of the ambient one, without which Mathlib's ρ[Ŷ | σ(X̂)] is again $0$ (condExp_of_not_le). The martingale condition is Mathlib's ρ[Ŷ | MeasurableSpace.comap X̂ _] =ᵐ[ρ] X̂. The book's "$[\hat Y \mid \hat X = x]$ is increasing in $x$ in $\le_{st}$" is a property of a version of the conditional distribution, which is defined only up to null sets; it is formalized as the existence of a Markov kernel $\kappa$ disintegrating the joint law, $\rho\circ(\hat X,\hat Y)^{-1} = (\rho\circ\hat X^{-1}) \otimes \kappa$ (ρ.map (X̂, Ŷ) = ρ.map X̂ ⊗ₘ κ), whose survival functions $t \mapsto \kappa(x,(t,\infty))$ are monotone in $x$ at every threshold $t$ — the usual stochastic order between the measures $\kappa(x_1,\cdot)$ and $\kappa(x_2,\cdot)$. The retired version demanded this of Mathlib's specific condDistrib at every real $x$, including points outside the support of $\hat X$ where that version is construction-dependent (a Lean artefact, not the book's claim). The convex order is the imported ConvexOrder (test functions convex $\varphi:\mathbb{R}\to\mathbb{R}$ with both $\varphi(X)$, $\varphi(Y)$ integrable), which for integrable $X$, $Y$ is equivalent to the book's "whenever the expectations exist". Conventions made explicit: random variables are measurable functions on probability spaces (the book's standing convention, stated as Measurable hypotheses and IsProbabilityMeasure instances); "$=_{st}$" is ProbabilityTheory.IdentDistrib; the common space $(\Omega'',\rho)$ is existentially quantified, and the coupled copies are themselves random variables. No correction to the printed source.