← Mathematical handbook

Remark 3: radial symmetry and the negative-parameter family

theorem Papers.AnsariRockel2026XiRho.normalizedBand_radially_symmetric (b : ℝ) (hb : 0 ≤ b) : (normalizedBand b hb).IsRadiallySymmetric

Every normalized band is radially symmetric, by uniqueness of its support optimizer.

theorem Papers.AnsariRockel2026XiRho.sourceBand_radially_symmetric (b : ℝ) (hb : 0 < b) : (sourceBand b hb).IsRadiallySymmetric

noncomputable def Papers.AnsariRockel2026XiRho.negativeSourceBand (b : ℝ) (hb : 0 < b) : ProbabilityTheory.Copula 2

Source equation (21), with the parameter magnitude represented as b>0.

Equations

• Papers.AnsariRockel2026XiRho.negativeSourceBand b hb = (Papers.AnsariRockel2026XiRho.sourceBand b hb).reflect {0}

theorem Papers.AnsariRockel2026XiRho.negativeSourceBand_cdf (b : ℝ) (hb : 0 < b) (u v : ↑unitInterval) : (negativeSourceBand b hb).cdf ![u, v] = ↑v - (sourceBand b hb).cdf ![unitInterval.symm u, v]

theorem Papers.AnsariRockel2026XiRho.negativeSourceBand_coefficients (b : ℝ) (hb : 0 < b) : (negativeSourceBand b hb).chatterjeeXi = bandXi b ∧ (negativeSourceBand b hb).spearmanRho = -bandRho b

theorem Papers.AnsariRockel2026XiRho.negativeSourceBand_eq_response_reflection (b : ℝ) (hb : 0 < b) : negativeSourceBand b hb = (sourceBand b hb).reflect {1}

For the radially symmetric source family either single-coordinate reflection agrees.