The necessary joint bounds and the entire lower tau face #
At every admissible (footrule,beta) pair, a centered lower seed attains the lower tau bound simultaneously. The upper tau face is a separate obligation.
theorem
Papers.OrendayLaresRockel2026TauFootruleBeta.joint_region_outer_bound
(C : ProbabilityTheory.Copula 2)
:
C.blomqvistBeta ∈ Set.Icc (-1) 1 ∧ 3 / 16 * (1 + C.blomqvistBeta) ^ 2 - 1 / 2 ≤ C.spearmanFootrule ∧ C.spearmanFootrule ≤ 1 - 3 / 8 * (1 - C.blomqvistBeta) ^ 2 ∧ 4 / 3 * C.spearmanFootrule - 1 / 3 ≤ C.kendallTau ∧ C.kendallTau ≤ 2 / 3 * C.spearmanFootrule + 1 / 3
theorem
Papers.OrendayLaresRockel2026TauFootruleBeta.lower_joint_face_attained
(p b : ℝ)
(hb : b ∈ Set.Icc (-1) 1)
(hpL : 3 / 16 * (1 + b) ^ 2 - 1 / 2 ≤ p)
(hpU : p ≤ 1 - 3 / 8 * (1 - b) ^ 2)
:
∃ (C : ProbabilityTheory.Copula 2), C.spearmanFootrule = p ∧ C.blomqvistBeta = b ∧ C.kendallTau = 4 / 3 * p - 1 / 3