← Mathematical handbook

Theorem 2.1: the sharp uniform-marginal correction for finite rankings

A ranking of positive size is represented by a permutation of Fin (n+1). The associated straight shuffle preserves each point's displacement within a strip.

noncomputable def Papers.AnsariRockel2026RhoFootrule.rankingDistance (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : ℝ

The source unnormalized footrule distance Dπ.

Equations

• Papers.AnsariRockel2026RhoFootrule.rankingDistance n π = ∑ i : Fin (n + 1), |↑↑(π i) - ↑↑i|

noncomputable def Papers.AnsariRockel2026RhoFootrule.rankingSquare (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : ℝ

The source unnormalized squared distance Sπ.

Equations

• Papers.AnsariRockel2026RhoFootrule.rankingSquare n π = ∑ i : Fin (n + 1), (↑↑(π i) - ↑↑i) ^ 2

theorem Papers.AnsariRockel2026RhoFootrule.ranking_mean (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : meanDistance (Verification.PermutationShuffle.copula n π) = rankingDistance n π / (↑n + 1) ^ 2

Exact finite-to-population normalization of the first absolute moment.

theorem Papers.AnsariRockel2026RhoFootrule.ranking_second_moment (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 ∂(Verification.PermutationShuffle.copula n π).toMeasure = rankingSquare n π / (↑n + 1) ^ 3

Exact finite-to-population normalization of the second moment.

theorem Papers.AnsariRockel2026RhoFootrule.finite_ranking_bounds (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : have m := rankingDistance n π / (↑n + 1) ^ 2; have q := rankingSquare n π / (↑n + 1) ^ 3; m ^ 2 + minimumVariance m ≤ q ∧ q ≤ (1 - √(1 - 2 * m) ^ 3) / 3

Theorem 2.1: both corrected finite-ranking inequalities, with their exact scaling.

theorem Papers.AnsariRockel2026RhoFootrule.finite_ranking_cauchy_correction (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : rankingDistance n π ^ 2 / (↑n + 1) + (↑n + 1) ^ 3 * minimumVariance (rankingDistance n π / (↑n + 1) ^ 2) ≤ rankingSquare n π

Remark 2.2: the unnormalized strengthening of Cauchy--Schwarz.