← Mathematical handbook

Remark 2.2: asymptotic sharpness for actual finite permutations

theorem Papers.AnsariRockel2026RhoFootrule.ranking_moment_limits (C : ProbabilityTheory.Copula 2) : ∃ (π : (n : ℕ) → Equiv.Perm (Fin (n + 1))), Filter.Tendsto (fun (n : ℕ) => rankingDistance n (π n) / (↑n + 1) ^ 2) Filter.atTop (nhds (meanDistance C)) ∧ Filter.Tendsto (fun (n : ℕ) => rankingSquare n (π n) / (↑n + 1) ^ 3) Filter.atTop (nhds ((1 - C.spearmanRho) / 6))

Both normalized ranking moments approach those of any prescribed copula.

theorem Papers.AnsariRockel2026RhoFootrule.ranking_lower_asymptotic_sharp {m : ℝ} (hm : m ∈ Set.Icc 0 (1 / 2)) : ∃ (π : (n : ℕ) → Equiv.Perm (Fin (n + 1))), Filter.Tendsto (fun (n : ℕ) => rankingDistance n (π n) / (↑n + 1) ^ 2) Filter.atTop (nhds m) ∧ Filter.Tendsto (fun (n : ℕ) => rankingSquare n (π n) / (↑n + 1) ^ 3) Filter.atTop (nhds (m ^ 2 + minimumVariance m))

At every admissible mean, finite rankings approach the sharp lower moment boundary.

theorem Papers.AnsariRockel2026RhoFootrule.ranking_upper_asymptotic_sharp {m : ℝ} (hm : m ∈ Set.Icc 0 (1 / 2)) : ∃ (π : (n : ℕ) → Equiv.Perm (Fin (n + 1))), Filter.Tendsto (fun (n : ℕ) => rankingDistance n (π n) / (↑n + 1) ^ 2) Filter.atTop (nhds m) ∧ Filter.Tendsto (fun (n : ℕ) => rankingSquare n (π n) / (↑n + 1) ^ 3) Filter.atTop (nhds ((1 - √(1 - 2 * m) ^ 3) / 3))

At every admissible mean, finite rankings approach the sharp upper moment boundary.