← Mathematical handbook

Proposition 2.1: the sharp upper footrule-beta boundary

The diagonal is bounded pointwise by that of a centered W block. Integrating this comparison proves the bound for all copulas, including singular ones.

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.diagonal_le_centralW (C : ProbabilityTheory.Copula 2) (α : ↑unitInterval) (hβ : C.blomqvistBeta = 1 - 2 * ↑α) (t : ↑unitInterval) : C.cdf ![t, t] ≤ (Verification.centralW α).cdf ![t, t]

noncomputable def Papers.OrendayLaresRockel2026TauFootruleBeta.footruleBetaUpper (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ProbabilityTheory.Copula 2

Equations

• Papers.OrendayLaresRockel2026TauFootruleBeta.footruleBetaUpper b hb = Verification.centralW ⟨(1 - b) / 2, ⋯⟩

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.footruleBetaUpper_beta (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (footruleBetaUpper b hb).blomqvistBeta = b

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.footruleBetaUpper_footrule (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (footruleBetaUpper b hb).spearmanFootrule = 1 - 3 / 8 * (1 - b) ^ 2

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.footrule_le_beta_upper (C : ProbabilityTheory.Copula 2) : C.spearmanFootrule ≤ 1 - 3 / 8 * (1 - C.blomqvistBeta) ^ 2

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.maximal_footrule_at_beta (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∃ (D : ProbabilityTheory.Copula 2), D.blomqvistBeta = b ∧ D.spearmanFootrule = 1 - 3 / 8 * (1 - b) ^ 2 ∧ ∀ (C : ProbabilityTheory.Copula 2), C.blomqvistBeta = b → C.spearmanFootrule ≤ D.spearmanFootrule

The upper inequality in equation (8) is attained at every admissible beta.