Theorem 3.A.2 — the absolute-deviation characterization of the convex order

Proved

StochasticOrders.Convex.convex_order_abs_iff

by mikedeng1 · Sep 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-orderprobabilitystochastic-orders

Let $X$ on $(\Omega,\mu)$ and $Y$ on $(\Omega',\nu)$ be integrable random variables with $E[X]=E[Y]$ . Then

X \le_{cx} Y \iff E|X-a| \le E|Y-a| \quad \text{for all } a \in \mathbb{R}.

This is a fully self-contained alternative to Theorem 3.A.1's tail-integral form, needing no external equation references: $X \le_{cx} Y$ holds exactly when $Y$ 's mean absolute deviation from every point $a$ dominates $X$ 's. (The function $-E|X-\cdot|$ is called the potential of $X$ 's law, so this restates $X \le_{cx} Y$ as a pointwise comparison of the two potentials.)

Formalization Note |X ω - a| is Mathlib's absolute value on ℝ; no separate "potential" definition is introduced since the theorem's content is fully captured by the raw inequality.

Preamble

import Mathlib
import Definitions.Def_StochasticOrders_Convex_ConvexOrder

Formal statement

namespace StochasticOrders.Convex

open MeasureTheory

/-- Theorem 3.A.2 (Shaked & Shanthikumar, *Stochastic Orders*, Springer 2007, p. 111): let `X`
and `Y` be two random variables with `E[X] = E[Y]`. Then `X ≤cx Y` iff `E|X - a| ≤ E|Y - a|` for
all `a ∈ ℝ`. -/
theorem convex_order_abs_iff {Ω Ω' : Type*} [MeasurableSpace Ω] [MeasurableSpace Ω']
    (μ : Measure Ω) (ν : Measure Ω') [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (X : Ω → ℝ) (Y : Ω' → ℝ) (hX : Integrable X μ) (hY : Integrable Y ν)
    (hmean : ∫ ω, X ω ∂μ = ∫ ω, Y ω ∂ν) :
    ConvexOrder μ ν X Y ↔ ∀ a : ℝ, ∫ ω, |X ω - a| ∂μ ≤ ∫ ω, |Y ω - a| ∂ν := by sorry

end StochasticOrders.Convex

Source

Shaked & Shanthikumar, Stochastic Orders, Springer 2007, p. 111, Theorem 3.A.2

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).
Endorsed by labuka · Oct 20, 2026
Confirmed by the mission captain (proposal self-audit).

View graph