The exact rho–footrule region #
The lower boundary is explicit in lowerBoundary. The upper boundary is the
countable collection of polynomial arcs UpperParameter.footrule and
UpperParameter.rho. Both descriptions use only real arithmetic, an integer
parameter, and the stated nonnegativity/normalization constraints.
Necessity uses global transport duality inequalities. Sufficiency uses the constructed boundary copulas and interpolation at fixed footrule.
theorem
ProbabilityTheory.Copula.RankRegion.RhoFootrule.exists_copula_iff
(p r : ℝ)
:
(∃ (C : Copula 2), C.spearmanFootrule = p ∧ C.spearmanRho = r) ↔ p ∈ Set.Icc (-1 / 2) 1 ∧ lowerBoundary p ≤ r ∧ ∃ (a : UpperParameter), a.footrule = p ∧ r ≤ a.rho
Exact membership, with the upper boundary given parametrically.
theorem
ProbabilityTheory.Copula.RankRegion.RhoFootrule.upperParameter_rho_unique
(a b : UpperParameter)
(h : a.footrule = b.footrule)
:
Every upper-boundary fibre has a unique value, even at arc junctions.