← Mathematical handbook

The unique optimizer of the exact rho--footrule upper boundary

theorem Papers.AnsariRockel2026RhoFootrule.boundary_optimizer_unique (a : BoundaryParameter) (C : ProbabilityTheory.Copula 2) (hp : C.spearmanFootrule = ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.footrule a) (hr : C.spearmanRho = upperRho (ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.footrule a)) : C = ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.copula a

Theorem 1.1 and Proposition 5.8: the arithmetic boundary copula is the only copula with its footrule and maximal rho, including all contacts and endpoints.

theorem Papers.AnsariRockel2026RhoFootrule.upper_boundary_exists_unique (p : ℝ) (hp : p ∈ Set.Icc (-1 / 2) 1) : ∃! C : ProbabilityTheory.Copula 2, C.spearmanFootrule = p ∧ C.spearmanRho = upperRho p

At every admissible footrule, exactly one copula attains the upper boundary.

theorem Papers.AnsariRockel2026RhoFootrule.boundary_copula_junction (a b : BoundaryParameter) (h : ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.footrule a = ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.footrule b) : ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.copula a = ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.copula b

Overlapping arcs agree as copulas, not only in their boundary values.