← Mathematical handbook

The exact rho–gamma region

The upper boundary is given by explicit algebraic parameters. Reflection supplies the lower boundary, and mixtures attain every point between them. The parameters and their coordinates contain no variational optimization.

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.exists_copula_iff (g r : ℝ) : (∃ (C : Copula 2), C.giniGamma = g ∧ C.spearmanRho = r) ↔ g ∈ Set.Icc (-1) 1 ∧ (∃ (a : UpperParameter), a.gamma = g ∧ r ≤ a.rho) ∧ ∃ (b : UpperParameter), b.gamma = -g ∧ -b.rho ≤ r

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.upperParameter_rho_unique (a b : UpperParameter) (h : a.gamma = b.gamma) : a.rho = b.rho