← Copula mathematical handbook

Kendall tau and Gini gamma

The inequalities and boundary families of Kokol Bukovšek–Stopar (2023), Theorem 6. The proof uses their reflection reduction to tau–footrule.

theorem ProbabilityTheory.Copula.giniGamma_eq_footrule_sub_reflect (C : Copula 2) : C.giniGamma = 2 / 3 * (C.spearmanFootrule - (C.reflect {1}).spearmanFootrule)

theorem ProbabilityTheory.Copula.kendallTau_le_gamma (C : Copula 2) : C.kendallTau ≤ min (2 / 3 * C.giniGamma + 1 / 3) (2 * C.giniGamma + 1)

theorem ProbabilityTheory.Copula.gamma_le_kendallTau (C : Copula 2) : max (2 / 3 * C.giniGamma - 1 / 3) (2 * C.giniGamma - 1) ≤ C.kendallTau

theorem ProbabilityTheory.Copula.giniGamma_ordinalSum_countermonotonic (a : ↑unitInterval) : (countermonotonic.ordinalSum countermonotonic a).giniGamma = 6 * ↑a * (1 - ↑a) - 1

The two-countermonotonic-block family in Example 5 of the source.

noncomputable def ProbabilityTheory.Copula.RankRegion.TauGamma.corner : Copula 2

The non-Fréchet positive-gamma vertex of the parallelogram.

Equations

• ProbabilityTheory.Copula.RankRegion.TauGamma.corner = ProbabilityTheory.Copula.countermonotonic.ordinalSum ProbabilityTheory.Copula.countermonotonic ProbabilityTheory.Copula.unitHalf

theorem ProbabilityTheory.Copula.RankRegion.TauGamma.corner_coefficients : corner.giniGamma = 1 / 2 ∧ corner.kendallTau = 0 ∧ corner.spearmanFootrule = 1 / 4

theorem ProbabilityTheory.Copula.RankRegion.TauGamma.lower_boundary_left (a : ↑unitInterval) : (countermonotonic.ordinalSum countermonotonic a).kendallTau = 2 / 3 * (countermonotonic.ordinalSum countermonotonic a).giniGamma - 1 / 3

theorem ProbabilityTheory.Copula.RankRegion.TauGamma.lower_boundary_right (a : ↑unitInterval) : (corner.mix (comonotonic 2) a).giniGamma = 1 - ↑a / 2 ∧ (corner.mix (comonotonic 2) a).kendallTau = 1 - ↑a

theorem ProbabilityTheory.Copula.RankRegion.TauGamma.exists_lower {g : ℝ} (hg : g ∈ Set.Icc (-1) 1) : ∃ (C : Copula 2), C.giniGamma = g ∧ C.kendallTau = max (2 / 3 * g - 1 / 3) (2 * g - 1)

theorem ProbabilityTheory.Copula.RankRegion.TauGamma.exists_upper {g : ℝ} (hg : g ∈ Set.Icc (-1) 1) : ∃ (C : Copula 2), C.giniGamma = g ∧ C.kendallTau = min (2 / 3 * g + 1 / 3) (2 * g + 1)

theorem ProbabilityTheory.Copula.RankRegion.TauGamma.exists_copula_iff (g t : ℝ) : (∃ (C : Copula 2), C.giniGamma = g ∧ C.kendallTau = t) ↔ g ∈ Set.Icc (-1) 1 ∧ max (2 / 3 * g - 1 / 3) (2 * g - 1) ≤ t ∧ t ≤ min (2 / 3 * g + 1 / 3) (2 * g + 1)