← Mathematical handbook

Proposition 5(iii): Kendall tau for the entire source family

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

Equations

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

theorem Papers.AnsariRockel2026XiRho.sourceBand_sampling (b : ℝ) (hb : 0 < b) : (sourceBand b hb).toMeasure = MeasureTheory.Measure.map (Verification.bandSample b) MeasureTheory.volume

An exact sampling representation, proved to equal the original source copula law.

theorem Papers.AnsariRockel2026XiRho.sourceBand_tau (b : ℝ) (hb : 0 < b) : (sourceBand b hb).kendallTau = bandTau b

The source Kendall formula, including its parameter junction at b=1.

theorem Papers.AnsariRockel2026XiRho.normalizedBand_tau (b : ℝ) (hb : 0 ≤ b) : (normalizedBand b hb).kendallTau = bandTau b

theorem Papers.AnsariRockel2026XiRho.negativeSourceBand_tau (b : ℝ) (hb : 0 < b) : (negativeSourceBand b hb).kendallTau = -bandTau b

Negative source parameters change the sign of Kendall's tau.

theorem Papers.AnsariRockel2026XiRho.unitDiagonalBand_tau : unitDiagonalBand.kendallTau = 1 / 2

The unit-slope copula attaining the global rho-xi gap has tau=1/2.

theorem Papers.AnsariRockel2026XiRho.sourceBand_rank_triple (b : ℝ) (hb : 0 < b) : (sourceBand b hb).chatterjeeXi = bandXi b ∧ (sourceBand b hb).spearmanRho = bandRho b ∧ (sourceBand b hb).kendallTau = bandTau b

Proposition 5 simultaneously, for every positive source parameter.