← Copula mathematical handbook

Quadratic mixture identities and strict convexity of Chatterjee's xi

Mixture weights stay constant under conditioning because every first marginal is uniform. Xi is a quadratic, strictly convex functional of the copula, and mixing with independence scales xi by the square of the retained weight.

theorem ProbabilityTheory.Copula.chatterjeeXi_mix (C D : Copula 2) (a : ↑unitInterval) : (C.mix D a).chatterjeeXi = ↑a ^ 2 * C.chatterjeeXi + (1 - ↑a) ^ 2 * D.chatterjeeXi + 2 * ↑a * (1 - ↑a) * C.chatterjeeCross D

theorem ProbabilityTheory.Copula.chatterjeeXi_mix_eq_sub_distance (C D : Copula 2) (a : ↑unitInterval) : (C.mix D a).chatterjeeXi = ↑a * C.chatterjeeXi + (1 - ↑a) * D.chatterjeeXi - 6 * ↑a * (1 - ↑a) * C.conditionalCDFDistanceSq D

The exact nonnegative defect in the convexity inequality.

theorem ProbabilityTheory.Copula.chatterjeeXi_mix_le (C D : Copula 2) (a : ↑unitInterval) : (C.mix D a).chatterjeeXi ≤ ↑a * C.chatterjeeXi + (1 - ↑a) * D.chatterjeeXi

theorem ProbabilityTheory.Copula.chatterjeeXi_mix_lt {C D : Copula 2} (hne : C ≠ D) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : (C.mix D a).chatterjeeXi < ↑a * C.chatterjeeXi + (1 - ↑a) * D.chatterjeeXi

Every nontrivial mixture of distinct copulas gives strict convexity.

theorem ProbabilityTheory.Copula.chatterjeeXi_mix_eq_iff (C D : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : (C.mix D a).chatterjeeXi = ↑a * C.chatterjeeXi + (1 - ↑a) * D.chatterjeeXi ↔ C = D

theorem ProbabilityTheory.Copula.chatterjeeXi_mix_independence (C : Copula 2) (a : ↑unitInterval) : (C.mix (independence 2) a).chatterjeeXi = ↑a ^ 2 * C.chatterjeeXi

Mixing with independence attenuates xi quadratically in the retained copula weight.

theorem ProbabilityTheory.Copula.chatterjeeXi_independence_mix (C : Copula 2) (a : ↑unitInterval) : ((independence 2).mix C a).chatterjeeXi = (1 - ↑a) ^ 2 * C.chatterjeeXi

theorem ProbabilityTheory.Copula.chatterjeeXi_mix_comonotonic (C : Copula 2) (a : ↑unitInterval) : (C.mix (comonotonic 2) a).chatterjeeXi = ↑a ^ 2 * C.chatterjeeXi + (1 - ↑a) ^ 2 + 2 * ↑a * (1 - ↑a) * C.spearmanFootrule

Mixing with the upper Fréchet bound links xi to Spearman's footrule.

theorem ProbabilityTheory.Copula.chatterjeeXi_mix_comonotonic_countermonotonic (a : ↑unitInterval) : ((comonotonic 2).mix countermonotonic a).chatterjeeXi = ↑a ^ 2 + (1 - ↑a) ^ 2 - ↑a * (1 - ↑a)