← Mathematical handbook

Proposition 5(i)--(ii): exact xi and rho for every positive diagonal band

noncomputable def Papers.AnsariRockel2026XiRho.bandXi (b : ℝ) : ℝ

Equations

• Papers.AnsariRockel2026XiRho.bandXi b = if b ≤ 1 then b ^ 2 / 2 - b ^ 3 / 5 else 1 - 1 / b + 3 / (10 * b ^ 2)

noncomputable def Papers.AnsariRockel2026XiRho.bandRho (b : ℝ) : ℝ

Equations

• Papers.AnsariRockel2026XiRho.bandRho b = if b ≤ 1 then b - 3 * b ^ 2 / 10 else 1 - 1 / (2 * b ^ 2) + 1 / (5 * b ^ 3)

theorem Papers.AnsariRockel2026XiRho.sourceBand_xi (b : ℝ) (hb : 0 < b) : (sourceBand b hb).chatterjeeXi = bandXi b

Proposition 5(i): the exact Chatterjee coefficient throughout b>0.

theorem Papers.AnsariRockel2026XiRho.sourceBand_rho (b : ℝ) (hb : 0 < b) : (sourceBand b hb).spearmanRho = bandRho b

Proposition 5(ii): the exact Spearman coefficient throughout b>0.

theorem Papers.AnsariRockel2026XiRho.normalizedBand_coefficients (b : ℝ) (hb : 0 ≤ b) : (normalizedBand b hb).chatterjeeXi = bandXi b ∧ (normalizedBand b hb).spearmanRho = bandRho b

The normalization-defined optimizer has exactly the source coordinates, including b=0.

theorem Papers.AnsariRockel2026XiRho.explicit_band_support (C : ProbabilityTheory.Copula 2) (b : ℝ) (hb : 0 ≤ b) : b * C.spearmanRho - C.chatterjeeXi ≤ b * bandRho b - bandXi b

The exact support bound expressed solely in the closed coefficient formulas.