← Mathematical handbook

Corollary 1.7 and Remark 1.8: the exact mean-variance region

noncomputable def Papers.AnsariRockel2026RhoFootrule.meanDistance (C : ProbabilityTheory.Copula 2) : ℝ

Equations

• Papers.AnsariRockel2026RhoFootrule.meanDistance C = ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂C.toMeasure

noncomputable def Papers.AnsariRockel2026RhoFootrule.distanceVariance (C : ProbabilityTheory.Copula 2) : ℝ

Equations

• Papers.AnsariRockel2026RhoFootrule.distanceVariance C = ∫ (x : Fin 2 → ↑unitInterval), (|↑(x 0) - ↑(x 1)| - Papers.AnsariRockel2026RhoFootrule.meanDistance C) ^ 2 ∂C.toMeasure

noncomputable def Papers.AnsariRockel2026RhoFootrule.maximumVariance (m : ℝ) : ℝ

Equation (23); the nonnegative real power is written as a cube of a square root.

Equations

• Papers.AnsariRockel2026RhoFootrule.maximumVariance m = (1 - √(1 - 2 * m) ^ 3) / 3 - m ^ 2

theorem Papers.AnsariRockel2026RhoFootrule.meanDistance_mem (C : ProbabilityTheory.Copula 2) : meanDistance C ∈ Set.Icc 0 (1 / 2)

The absolute displacement mean has precisely the admissible range [0,1/2].

theorem Papers.AnsariRockel2026RhoFootrule.distanceVariance_eq (C : ProbabilityTheory.Copula 2) : distanceVariance C = (1 - C.spearmanRho) / 6 - meanDistance C ^ 2

The affine conversion between rho and the variance at a fixed mean.

theorem Papers.AnsariRockel2026RhoFootrule.sharp_variance_bounds (C : ProbabilityTheory.Copula 2) : minimumVariance (meanDistance C) ≤ distanceVariance C ∧ distanceVariance C ≤ maximumVariance (meanDistance C)

Corollary 1.7: both sharp variance bounds.

theorem Papers.AnsariRockel2026RhoFootrule.minimumVariance_le_maximumVariance {m : ℝ} (hm : m ∈ Set.Icc 0 (1 / 2)) : minimumVariance m ≤ maximumVariance m

The two boundary variances are ordered throughout the admissible mean range.

theorem Papers.AnsariRockel2026RhoFootrule.exact_mean_variance_region (m v : ℝ) : (∃ (C : ProbabilityTheory.Copula 2), meanDistance C = m ∧ distanceVariance C = v) ↔ m ∈ Set.Icc 0 (1 / 2) ∧ minimumVariance m ≤ v ∧ v ≤ maximumVariance m

Remark 1.8(a): every intermediate variance is attained, and no others are.

theorem Papers.AnsariRockel2026RhoFootrule.maximum_variance_attained {m : ℝ} (hm : m ∈ Set.Icc 0 (1 / 2)) : ∃ (C : ProbabilityTheory.Copula 2), meanDistance C = m ∧ distanceVariance C = maximumVariance m

Corollary 1.7: the upper variance bound is attained for every prescribed mean.