← Mathematical handbook

The lower footrule-beta boundary and the complete pairwise region

The lower seed of Proposition 3.2 is constructed by reflection of a centered ordinal sum. No shuffle formula or assumed coefficient values are required.

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.diagonal_beta_lower (C : ProbabilityTheory.Copula 2) (t : ↑unitInterval) : ProbabilityTheory.Copula.countermonotonic.cdf ![t, t] + 2 * Verification.medianTent ((C.blomqvistBeta + 1) / 4) ↑t ≤ C.cdf ![t, t]

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

noncomputable def Papers.OrendayLaresRockel2026TauFootruleBeta.medianWBlocks : ProbabilityTheory.Copula 2

Equations

• Papers.OrendayLaresRockel2026TauFootruleBeta.medianWBlocks = ProbabilityTheory.Copula.countermonotonic.ordinalSum ProbabilityTheory.Copula.countermonotonic ProbabilityTheory.Copula.unitHalf

noncomputable def Papers.OrendayLaresRockel2026TauFootruleBeta.lowerSeed (α : ↑unitInterval) : ProbabilityTheory.Copula 2

Equations

• Papers.OrendayLaresRockel2026TauFootruleBeta.lowerSeed α = (Verification.centeredOrdinal (Papers.OrendayLaresRockel2026TauFootruleBeta.medianWBlocks.reflect {1}) α).reflect {1}

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.lowerSeed_coefficients (α : ↑unitInterval) : (lowerSeed α).kendallTau = ↑α ^ 2 - 1 ∧ (lowerSeed α).spearmanFootrule = 3 / 4 * ↑α ^ 2 - 1 / 2 ∧ (lowerSeed α).blomqvistBeta = 2 * ↑α - 1

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

Equations

• Papers.OrendayLaresRockel2026TauFootruleBeta.footruleBetaLower b hb = Papers.OrendayLaresRockel2026TauFootruleBeta.lowerSeed ⟨(1 + b) / 2, ⋯⟩

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.footruleBetaLower_coefficients (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (footruleBetaLower b hb).kendallTau = (1 + b) ^ 2 / 4 - 1 ∧ (footruleBetaLower b hb).spearmanFootrule = 3 / 16 * (1 + b) ^ 2 - 1 / 2 ∧ (footruleBetaLower b hb).blomqvistBeta = b

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

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.exact_footrule_beta_region (p b : ℝ) : (∃ (C : ProbabilityTheory.Copula 2), C.spearmanFootrule = p ∧ C.blomqvistBeta = b) ↔ b ∈ Set.Icc (-1) 1 ∧ 3 / 16 * (1 + b) ^ 2 - 1 / 2 ≤ p ∧ p ≤ 1 - 3 / 8 * (1 - b) ^ 2