← Mathematical handbook

theorem Verification.integral_plackett_section {θ : ℝ} (hθ : 0 < θ) (hne : θ ≠ 1) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), (plackett θ hθ).cdf ![u, v] = ↑v - ↑v ^ 2 / 2 - ↑v * (1 - ↑v) * (θ * Real.log θ - θ + 1) / (θ - 1) ^ 2

theorem Verification.integral_plackett_cdf {θ : ℝ} (hθ : 0 < θ) (hne : θ ≠ 1) : ∫ (x : Fin 2 → ↑unitInterval), (plackett θ hθ).cdf x = 1 / 3 - (θ * Real.log θ - θ + 1) / (6 * (θ - 1) ^ 2)

theorem Verification.plackett_spearmanRho {θ : ℝ} (hθ : 0 < θ) (hne : θ ≠ 1) : (plackett θ hθ).spearmanRho = (θ + 1) / (θ - 1) - 2 * θ * Real.log θ / (θ - 1) ^ 2

Spearman rho obtained by integration of the actual Plackett CDF.

theorem Verification.plackett_spearmanRho_one : (plackett 1 ⋯).spearmanRho = 0

theorem Verification.plackett_printed_rho_false : (plackett 2 ⋯).spearmanRho ≠ (2 + 1) / (2 - 1) - 2 * (2 * 2 / (2 - 1) ^ 2) * Real.log 2

The doubled logarithmic term printed in arXiv v3 Table 6 fails already at theta=2.