← Mathematical handbook

Kendall tau of the corrected Raftery family

The identified copula density turns Kendall's integral into a Lebesgue integral. Symmetry reduces it to one triangle, where exact power integration gives the Table 6 formula on the full parameter interval, including both endpoints.

theorem Verification.integral_raftery_cdf_density_triangle {a : ℝ} (ha : 1 < a) (v : ↑unitInterval) (hv : 0 < ↑v) : ∫ (u : ↑unitInterval) in Set.Iic v, (rafteryPower a ha).cdf ![u, v] * rafteryDensity a ↑u ↑v = (a * (a - 1) / ((2 * a - 1) * (a + 1)) - (a - 1) / (2 * (2 * a - 1) ^ 2)) * ↑v + (a ^ 2 / ((2 * a - 1) * (a + 1)) - 1 / (2 * (2 * a - 1) ^ 2)) * ↑v ^ (2 * a) + a / (2 * (2 * a - 1) ^ 2) * ↑v ^ (4 * a - 1)

theorem Verification.rafteryPower_kendallTau {a : ℝ} (ha : 1 < a) : (rafteryPower a ha).kendallTau = 2 * (a - 1) / (2 * a + 1)

theorem Verification.raftery_kendallTau (δ : ↑unitInterval) : (raftery δ).kendallTau = 2 * ↑δ / (3 - ↑δ)