← 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 Verification.footrule_eq_abs_moment (C : ProbabilityTheory.Copula 2) : C.spearmanFootrule = 1 - 3 * ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂C.toMeasure

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