← Copula mathematical handbook

The exact Spearman rho–Kendall tau region

The boundary parameters are the polynomial arcs of Schreyer–Paulin–Trutschnig, together with their limiting endpoint. The lower inequality follows from finite weighted permutations and dominated convergence. Reflection gives the upper inequality; mixtures at fixed rho fill every horizontal section between the boundary copulas.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.universal_upper (C : Copula 2) : ∃ (p : LowerParameter), p.tau = -C.kendallTau ∧ C.spearmanRho ≤ -p.rho

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.exists_copula_iff (r t : ℝ) : (∃ (C : Copula 2), C.spearmanRho = r ∧ C.kendallTau = t) ↔ t ∈ Set.Icc (-1) 1 ∧ (∃ (a : LowerParameter), a.tau = t ∧ a.rho ≤ r) ∧ ∃ (b : LowerParameter), b.tau = -t ∧ r ≤ -b.rho

Exact membership, with arithmetic boundary parameters and no copula assumptions.