← Mathematical handbook

Rank coefficients as probabilities of coordinatewise comparison

Fubini identifies cross-CDF integrals with probabilities that one independent copula observation is below another coordinatewise. This gives Kendall tau using two copies of the copula and Spearman rho using an independent copula.

theorem Verification.integral_cdf_probability (C D : ProbabilityTheory.Copula 2) : ∫ (y : Fin 2 → ↑unitInterval), C.cdf y ∂D.toMeasure = (C.toMeasure.prod D.toMeasure).real {p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval) | p.1 ≤ p.2}

theorem Verification.spearmanRho_probability (C : ProbabilityTheory.Copula 2) : C.spearmanRho = 12 * ((ProbabilityTheory.Copula.independence 2).toMeasure.prod C.toMeasure).real {p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval) | p.1 ≤ p.2} - 3

theorem Verification.kendallTau_probability (C : ProbabilityTheory.Copula 2) : C.kendallTau = 4 * (C.toMeasure.prod C.toMeasure).real {p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval) | p.1 ≤ p.2} - 1