← Mathematical handbook

Theorem 1: the full explicit xi--rho region and unique interior boundary copulas

noncomputable def Papers.AnsariRockel2026XiRho.upperRhoAtXi (x : ℝ) : ℝ

Exactly M_x in equation (5), with the displayed trigonometric/radical inverse.

Equations

• Papers.AnsariRockel2026XiRho.upperRhoAtXi x = if x = 0 then 0 else if x = 1 then 1 else Papers.AnsariRockel2026XiRho.bandRho (Papers.AnsariRockel2026XiRho.boundaryParameter x)

noncomputable def Papers.AnsariRockel2026XiRho.boundaryCopula (x : ℝ) (hx : 0 < x) (hx1 : x < 1) : ProbabilityTheory.Copula 2

Equations

• Papers.AnsariRockel2026XiRho.boundaryCopula x hx hx1 = Papers.AnsariRockel2026XiRho.sourceBand (Papers.AnsariRockel2026XiRho.boundaryParameter x) ⋯

theorem Papers.AnsariRockel2026XiRho.boundaryCopula_coefficients {x : ℝ} (hx : 0 < x) (hx1 : x < 1) : (boundaryCopula x hx hx1).chatterjeeXi = x ∧ (boundaryCopula x hx hx1).spearmanRho = upperRhoAtXi x

The original source family attains every interior positive boundary point.

theorem Papers.AnsariRockel2026XiRho.sharp_absolute_rho_bound (C : ProbabilityTheory.Copula 2) : |C.spearmanRho| ≤ upperRhoAtXi C.chatterjeeXi

Theorem 1: the sharp two-sided bound for every bivariate copula.

theorem Papers.AnsariRockel2026XiRho.exact_region (x y : ℝ) : (∃ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = x ∧ C.spearmanRho = y) ↔ x ∈ Set.Icc 0 1 ∧ |y| ≤ upperRhoAtXi x

Equations (4)--(5): necessary and sufficient conditions for the full exact region.

theorem Papers.AnsariRockel2026XiRho.upper_boundary_unique (C : ProbabilityTheory.Copula 2) {x : ℝ} (hx : 0 < x) (hx1 : x < 1) (hC : C.chatterjeeXi = x) : C.spearmanRho = upperRhoAtXi x ↔ C = boundaryCopula x hx hx1

The positive boundary identifies the actual copula uniquely at every interior xi.

theorem Papers.AnsariRockel2026XiRho.lower_boundary_unique (C : ProbabilityTheory.Copula 2) {x : ℝ} (hx : 0 < x) (hx1 : x < 1) (hC : C.chatterjeeXi = x) : C.spearmanRho = -upperRhoAtXi x ↔ C = (boundaryCopula x hx hx1).reflect {1}

The reflected source copula is the unique negative-boundary optimizer.