← Mathematical handbook

Gini gamma and reflected footrule of a centered ordinal sum

theorem ProbabilityTheory.Copula.RankRegion.centered_abs_sum (C : Copula 2) (r : ↑unitInterval) : ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) + ↑(x 1) - 1| ∂(centered C r).toMeasure = (1 - ↑r ^ 2) / 2 + ↑r ^ 2 * ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) + ↑(x 1) - 1| ∂C.toMeasure

theorem ProbabilityTheory.Copula.RankRegion.centered_gamma (C : Copula 2) (r : ↑unitInterval) : (centered C r).giniGamma = 1 - ↑r ^ 2 * (1 - C.giniGamma)

theorem ProbabilityTheory.Copula.RankRegion.centered_reflect_footrule (C : Copula 2) (r : ↑unitInterval) : ((centered C r).reflect {1}).spearmanFootrule = -1 / 2 + ↑r ^ 2 * (1 / 2 + (C.reflect {1}).spearmanFootrule)