← Copula 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 ProbabilityTheory.Copula.RankRegion.Common.conditionalCDF_binary_of_xi_one {C : Copula 2} (h : C.chatterjeeXi = 1) : ∀ᵐ (v : ↑unitInterval) (u : ↑unitInterval), C.conditionalCDF u v = 0 ∨ C.conditionalCDF u v = 1

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

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

theorem ProbabilityTheory.Copula.RankRegion.Common.cdf_eq_min_of_isSI_binary {C : 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 ProbabilityTheory.Copula.RankRegion.Common.isSI_xi_eq_one_iff (C : Copula 2) (hC : C.IsSI) : C.chatterjeeXi = 1 ↔ C = comonotonic 2

In the SI class, maximal xi characterizes comonotonicity.

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

In the SD class, maximal xi characterizes countermonotonicity.