← Mathematical handbook

Equivalence of Schur and orthant order for monotone conditional distributions

theorem Verification.rowMeanTest_le_of_lowerOrthantLE (C D : ProbabilityTheory.Copula 2) (hC : C.IsSI) (h : C.LowerOrthantLE D) (m : ℕ) (hm : 0 < m) (v : ↑unitInterval) (φ : ℝ → ℝ) (hc : Continuous φ) (hφ : ConvexOn ℝ (Set.Icc 0 1) φ) : rowMeanTest (ProbabilityTheory.Copula.IntervalPartition.uniform m hm) C v φ ≤ rowMeanTest (ProbabilityTheory.Copula.IntervalPartition.uniform m hm) D v φ

Ordered CDF prefixes imply every convex test inequality for finite row averages. Only the smaller copula needs to be conditionally increasing.

theorem Verification.schurLE_of_lowerOrthantLE_isSI (C D : ProbabilityTheory.Copula 2) (hC : C.IsSI) (h : C.LowerOrthantLE D) : C.SchurLE D

CDF order above a conditionally increasing copula implies Schur order; the larger copula need not be conditionally increasing.

theorem Verification.schurLE_iff_lowerOrthantLE_isSI (C D : ProbabilityTheory.Copula 2) (hC : C.IsSI) (hD : D.IsSI) : C.SchurLE D ↔ C.LowerOrthantLE D

Lemma 2.6(ii), including singular conditionally increasing copulas.

theorem Verification.schurLE_iff_lowerOrthantLE_isSD (C D : ProbabilityTheory.Copula 2) (hC : C.IsSD) (hD : D.IsSD) : C.SchurLE D ↔ D.LowerOrthantLE C

Lemma 2.8(ii): for conditionally decreasing copulas the CDF direction reverses.