← Mathematical handbook

Remark 1.8(c): the exact universal maximum variance of absolute displacement

theorem Papers.AnsariRockel2026RhoFootrule.maximumVariance_global_bound {m : ℝ} (hm : m ∈ Set.Icc 0 (1 / 2)) : maximumVariance m ≤ 5 * (3 - √5) / 24

The exact global upper bound on the source maximum-variance function.

theorem Papers.AnsariRockel2026RhoFootrule.universal_variance_bounds (C : ProbabilityTheory.Copula 2) : 0 ≤ distanceVariance C ∧ distanceVariance C ≤ 5 * (3 - √5) / 24

Equation (25): the exact universal interval for variance.

noncomputable def Papers.AnsariRockel2026RhoFootrule.maximumVarianceMean : ℝ

The mean corresponding to the source maximizing footrule x0.

Equations

• Papers.AnsariRockel2026RhoFootrule.maximumVarianceMean = (√5 - 1) / 4

theorem Papers.AnsariRockel2026RhoFootrule.maximumVariance_at_maximizer : maximumVariance maximumVarianceMean = 5 * (3 - √5) / 24

Exact evaluation at the golden-ratio contact parameter.

theorem Papers.AnsariRockel2026RhoFootrule.universal_variance_maximum_attained : ∃ (C : ProbabilityTheory.Copula 2), C.spearmanFootrule = (7 - 3 * √5) / 4 ∧ distanceVariance C = 5 * (3 - √5) / 24

Remark 1.8(c): an actual copula attains the bound at x0=(7-3sqrt(5))/4.