← Mathematical handbook

Moment representation and interpolation at fixed footrule

Lemma 3.2 and the interpolation step of Corollary 1.2 use no regularity assumption beyond being a copula. Optimal boundary constructions are pending.

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.moment_representation (C : Copula 2) : C.spearmanRho = 1 - 6 * ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 ∂C.toMeasure ∧ C.spearmanFootrule = 1 - 3 * ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂C.toMeasure

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.quadratic_upper_bound (C : Copula 2) : C.spearmanRho ≤ 1 - 2 / 3 * (1 - C.spearmanFootrule) ^ 2

The classical quadratic upper envelope (equations (16)-(17)), before the article's strictly sharper transport correction is imposed.

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.fixed_footrule_intermediate (C D : Copula 2) {p r : ℝ} (hC : C.spearmanFootrule = p) (hD : D.spearmanFootrule = p) (hrC : C.spearmanRho ≤ r) (hrD : r ≤ D.spearmanRho) : ∃ (E : Copula 2), E.spearmanFootrule = p ∧ E.spearmanRho = r