← Mathematical handbook

Stochastic monotonicity and maximal Chatterjee xi

The proof applies to arbitrary copulas, including singular ones. Maximal xi makes the conditional CDF binary almost everywhere. Concavity then forces each CDF section to equal the comonotonic section.

theorem Verification.conditionalCDF_binary_of_xi_one {C : ProbabilityTheory.Copula 2} (h : C.chatterjeeXi = 1) : ∀ᵐ (v : ↑unitInterval) (u : ↑unitInterval), C.conditionalCDF u v = 0 ∨ C.conditionalCDF u v = 1

theorem Verification.cdfSection_concave_of_isSI {C : ProbabilityTheory.Copula 2} (hC : C.IsSI) (v : ↑unitInterval) : ConcaveOn ℝ (Set.Icc 0 1) (C.cdfSection v)

theorem Verification.cdfSection_differentiable_ae (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : ∀ᵐ (u : ↑unitInterval), DifferentiableAt ℝ (C.cdfSection v) ↑u

theorem Verification.cdf_eq_min_of_isSI_binary {C : ProbabilityTheory.Copula 2} (hC : C.IsSI) (v : ↑unitInterval) (hb : ∀ᵐ (u : ↑unitInterval), C.conditionalCDF u v = 0 ∨ C.conditionalCDF u v = 1) (u : ↑unitInterval) : C.cdf ![u, v] = min ↑u ↑v

theorem Verification.isSI_xi_eq_one_iff (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) : C.chatterjeeXi = 1 ↔ C = ProbabilityTheory.Copula.comonotonic 2

In the SI class, maximal xi characterizes comonotonicity.

theorem Verification.isSD_xi_eq_one_iff (C : ProbabilityTheory.Copula 2) (hC : C.IsSD) : C.chatterjeeXi = 1 ↔ C = ProbabilityTheory.Copula.countermonotonic

In the SD class, maximal xi characterizes countermonotonicity.