← Mathematical handbook

Absolute-displacement moment representations

These identities apply to arbitrary bivariate copula measures, including singular ones. They connect the CDF-based footrule and gamma definitions to the transport costs used in the rho-footrule and rho-gamma articles.

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.footrule_eq_abs_moment (C : Copula 2) : C.spearmanFootrule = 1 - 3 * ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂C.toMeasure

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.gamma_eq_abs_moments (C : Copula 2) : C.giniGamma = 2 * ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) + ↑(x 1) - 1| - |↑(x 0) - ↑(x 1)| ∂C.toMeasure