← Copula mathematical handbook

The exact Spearman footrule–Gini gamma region

Kokol Bukovšek–Mojškerc, On the exact region determined by Spearman's footrule and Gini's gamma (2022). The quadrilateral is also stated as Proposition 2.1 in Kokol Bukovšek–Mojškerc (2026). The bounds below use absolute moments; mixtures fill its edges and fibres.

theorem ProbabilityTheory.Copula.integral_unit_abs_sub (a : ↑unitInterval) : ∫ (u : ↑unitInterval), |↑u - ↑a| = ↑a ^ 2 - ↑a + 1 / 2

theorem ProbabilityTheory.Copula.footrule_le_giniGamma (C : Copula 2) : 4 / 3 * C.spearmanFootrule - 1 / 3 ≤ C.giniGamma

theorem ProbabilityTheory.Copula.giniGamma_le_footrule (C : Copula 2) : C.giniGamma ≤ min (4 / 3 * C.spearmanFootrule + 1 / 6) (2 / 3 * C.spearmanFootrule + 1 / 3)

theorem ProbabilityTheory.Copula.RankRegion.FootruleGamma.exists_lower {p : ℝ} (hp : p ∈ Set.Icc (-1 / 2) 1) : ∃ (C : Copula 2), C.spearmanFootrule = p ∧ C.giniGamma = 4 / 3 * p - 1 / 3

theorem ProbabilityTheory.Copula.RankRegion.FootruleGamma.exists_upper {p : ℝ} (hp : p ∈ Set.Icc (-1 / 2) 1) : ∃ (C : Copula 2), C.spearmanFootrule = p ∧ C.giniGamma = min (4 / 3 * p + 1 / 6) (2 / 3 * p + 1 / 3)

theorem ProbabilityTheory.Copula.RankRegion.FootruleGamma.exists_copula_iff (p g : ℝ) : (∃ (C : Copula 2), C.spearmanFootrule = p ∧ C.giniGamma = g) ↔ p ∈ Set.Icc (-1 / 2) 1 ∧ 4 / 3 * p - 1 / 3 ≤ g ∧ g ≤ min (4 / 3 * p + 1 / 6) (2 / 3 * p + 1 / 3)