Eq. (7.A.5) — the multivariate convex order forces equal means
ProvedStochasticOrders.MultivariateVariability.convex_order_imp_mean_eqFor any , the coordinate projection and the function are both convex. Therefore, from the definition of it follows that
provided the expectations exist (componentwise equality of the two mean vectors in
). A cheap but useful corollary of ConvexOrder's own defining quantifier,
applied to each coordinate projection.
Formalization Note The integrability of and (i.e. that the mean vectors exist)
is carried as explicit hypotheses Integrable X μ, Integrable Y ν, matching the book's own
"provided the expectations exist" qualifier — not automatic, per this chapter's pitfall 4.
The conclusion ∫ X ∂μ = ∫ Y ∂ν is Bochner-integral equality of two Fin n → ℝ-valued
vectors, i.e. componentwise equality.
import Mathlib import Definitions.Def_StochasticOrders_MultivariateVariability_ConvexOrder
namespace StochasticOrders.MultivariateVariability
open MeasureTheory
/-- Eq. (7.A.5) (Shaked & Shanthikumar, *Stochastic Orders*, Springer 2007, p. 324): for any
`i = 1, …, n`, the coordinate projection `φᵢ(x) = xᵢ` and its negation `ψᵢ(x) = −xᵢ` are both
convex, so `X ≤cx Y` implies `E[X] = E[Y]` (componentwise), provided the expectations exist. -/
theorem convex_order_imp_mean_eq {Ω Ω' : Type*} [MeasurableSpace Ω] [MeasurableSpace Ω']
{n : ℕ} (μ : Measure Ω) (ν : Measure Ω') [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
(X : Ω → Fin n → ℝ) (Y : Ω' → Fin n → ℝ) (hX : Integrable X μ) (hY : Integrable Y ν)
(hord : ConvexOrder μ ν X Y) :
∫ ω, X ω ∂μ = ∫ ω, Y ω ∂ν := by sorry
end StochasticOrders.MultivariateVariability
Confirmed by the mission captain (proposal self-audit).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.