← Copula mathematical handbook

Pairwise attainable regions of five rank coefficients

All ten pairs among the five classical coefficients, plus the xi–beta and xi–rho and xi–Blest pairs, have exact membership theorems, including boundary attainment and every point in between. The coverage and mathematical references are in docs/rank-regions.md.

theorem ProbabilityTheory.Copula.RankRegion.attainable_footrule_tau_iff (p t : ℝ) : (p, t) ∈ attainable Coefficient.footrule Coefficient.tau ↔ p ∈ Set.Icc (-1 / 2) 1 ∧ 4 / 3 * p - 1 / 3 ≤ t ∧ t ≤ 2 / 3 * p + 1 / 3

theorem ProbabilityTheory.Copula.RankRegion.attainable_gamma_tau_iff (g t : ℝ) : (g, t) ∈ attainable Coefficient.gamma Coefficient.tau ↔ g ∈ Set.Icc (-1) 1 ∧ max (2 / 3 * g - 1 / 3) (2 * g - 1) ≤ t ∧ t ≤ min (2 / 3 * g + 1 / 3) (2 * g + 1)

theorem ProbabilityTheory.Copula.RankRegion.attainable_footrule_gamma_iff (p g : ℝ) : (p, g) ∈ attainable Coefficient.footrule Coefficient.gamma ↔ p ∈ Set.Icc (-1 / 2) 1 ∧ 4 / 3 * p - 1 / 3 ≤ g ∧ g ≤ min (4 / 3 * p + 1 / 6) (2 / 3 * p + 1 / 3)

theorem ProbabilityTheory.Copula.RankRegion.attainable_beta_rho_iff (b r : ℝ) : (b, r) ∈ attainable Coefficient.beta Coefficient.rho ↔ b ∈ Set.Icc (-1) 1 ∧ 3 / 16 * (1 + b) ^ 3 - 1 ≤ r ∧ r ≤ 1 - 3 / 16 * (1 - b) ^ 3

theorem ProbabilityTheory.Copula.RankRegion.attainable_beta_tau_iff (b t : ℝ) : (b, t) ∈ attainable Coefficient.beta Coefficient.tau ↔ b ∈ Set.Icc (-1) 1 ∧ 1 / 4 * (1 + b) ^ 2 - 1 ≤ t ∧ t ≤ 1 - 1 / 4 * (1 - b) ^ 2

theorem ProbabilityTheory.Copula.RankRegion.attainable_beta_footrule_iff (b p : ℝ) : (b, p) ∈ attainable Coefficient.beta Coefficient.footrule ↔ b ∈ Set.Icc (-1) 1 ∧ 3 / 16 * (1 + b) ^ 2 - 1 / 2 ≤ p ∧ p ≤ 1 - 3 / 8 * (1 - b) ^ 2

theorem ProbabilityTheory.Copula.RankRegion.attainable_beta_gamma_iff (b g : ℝ) : (b, g) ∈ attainable Coefficient.beta Coefficient.gamma ↔ b ∈ Set.Icc (-1) 1 ∧ 3 / 8 * (1 + b) ^ 2 - 1 ≤ g ∧ g ≤ 1 - 3 / 8 * (1 - b) ^ 2

theorem ProbabilityTheory.Copula.RankRegion.attainable_footrule_rho_iff (p r : ℝ) : (p, r) ∈ attainable Coefficient.footrule Coefficient.rho ↔ p ∈ Set.Icc (-1 / 2) 1 ∧ RhoFootrule.lowerBoundary p ≤ r ∧ ∃ (a : RhoFootrule.UpperParameter), a.footrule = p ∧ r ≤ a.rho

Exact rho–footrule membership; the upper boundary is a countable family of polynomial arcs.

theorem ProbabilityTheory.Copula.RankRegion.attainable_gamma_rho_iff (g r : ℝ) : (g, r) ∈ attainable Coefficient.gamma Coefficient.rho ↔ g ∈ Set.Icc (-1) 1 ∧ (∃ (a : RhoGamma.UpperParameter), a.gamma = g ∧ r ≤ a.rho) ∧ ∃ (b : RhoGamma.UpperParameter), b.gamma = -g ∧ -b.rho ≤ r

Exact rho–gamma membership, including both sharp boundaries and every interior point.

theorem ProbabilityTheory.Copula.RankRegion.attainable_rho_tau_iff (r t : ℝ) : (r, t) ∈ attainable Coefficient.rho Coefficient.tau ↔ t ∈ Set.Icc (-1) 1 ∧ (∃ (a : RhoTau.LowerParameter), a.tau = t ∧ a.rho ≤ r) ∧ ∃ (b : RhoTau.LowerParameter), b.tau = -t ∧ r ≤ -b.rho

The exact Schreyer–Paulin–Trutschnig rho–tau region.

theorem ProbabilityTheory.Copula.RankRegion.attainable_xi_beta_iff (x b : ℝ) : (∃ (C : Copula 2), C.chatterjeeXi = x ∧ C.blomqvistBeta = b) ↔ x ∈ Set.Icc 0 1 ∧ b ∈ Set.Icc (-1) 1 ∧ |b| ^ 3 ≤ 2 * x

Exact xi–beta region, including singular boundary witnesses and every interior point.

theorem ProbabilityTheory.Copula.RankRegion.attainable_xi_rho_iff (x r : ℝ) : (∃ (C : Copula 2), C.chatterjeeXi = x ∧ C.spearmanRho = r) ↔ x ∈ Set.Icc 0 1 ∧ |r| ≤ XiRho.upperRhoAtXi x

Exact xi–rho region with its trigonometric/radical upper boundary.

theorem ProbabilityTheory.Copula.RankRegion.attainable_xi_blest_iff (x n : ℝ) : (∃ (C : Copula 2), C.chatterjeeXi = x ∧ XiBlest.blestNu C = n) ↔ x = 1 ∧ |n| ≤ 1 ∨ ∃ (b : ℝ), 0 ≤ b ∧ x = XiBlest.xiFormula b ∧ |n| ≤ XiBlest.nuFormula b

Exact xi–Blest region, with both boundary branches and every interior point.

theorem ProbabilityTheory.Copula.RankRegion.attainable_tau_footrule_beta_iff (t p b : ℝ) : (∃ (C : Copula 2), C.kendallTau = t ∧ C.spearmanFootrule = p ∧ C.blomqvistBeta = b) ↔ b ∈ Set.Icc (-1) 1 ∧ 3 / 16 * (1 + b) ^ 2 - 1 / 2 ≤ p ∧ p ≤ 1 - 3 / 8 * (1 - b) ^ 2 ∧ 4 / 3 * p - 1 / 3 ≤ t ∧ t ≤ 2 / 3 * p + 1 / 3

The exact three-coordinate Kendall tau, footrule, and Blomqvist beta region.

theorem ProbabilityTheory.Copula.RankRegion.attainable_mean_distance_variance_iff (m v : ℝ) : (∃ (C : Copula 2), MeanVariance.meanDistance C = m ∧ MeanVariance.distanceVariance C = v) ↔ m ∈ Set.Icc 0 (1 / 2) ∧ MeanVariance.minimumVariance m ≤ v ∧ v ≤ MeanVariance.maximumVariance m

Exact region of the absolute coordinate-distance mean and its variance.