← Copula mathematical handbook

Exact Schur ordering of Nelsen's seventh family

theorem ProbabilityTheory.Copula.integral_convex_le_of_conditionalCDF_binary (C D : Copula 2) (v H : ↑unitInterval) (hC : ∀ᵐ (u : ↑unitInterval), C.conditionalCDF u v ≤ ↑H) (hD : ∀ᵐ (u : ↑unitInterval), D.conditionalCDF u v = 0 ∨ D.conditionalCDF u v = ↑H) (φ : ℝ → ℝ) (hc : Continuous φ) (hv : ConvexOn ℝ (Set.Icc 0 1) φ) : ∫ (u : ↑unitInterval), φ (C.conditionalCDF u v) ≤ ∫ (u : ↑unitInterval), φ (D.conditionalCDF u v)

A two-valued conditional CDF maximizes convex tests among conditional CDFs with the same mean and values bounded by its upper value.

theorem ProbabilityTheory.Copula.schurLE_nelsen7_iff {θ η : ↑unitInterval} : (nelsen7 θ).SchurLE (nelsen7 η) ↔ η ≤ θ

theorem ProbabilityTheory.Copula.schurBothLE_nelsen7_iff {θ η : ↑unitInterval} : (nelsen7 θ).SchurBothLE (nelsen7 η) ↔ η ≤ θ