← Copula mathematical handbook

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 ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.joint_region_outer_bound (C : 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 ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.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 : Copula 2), C.spearmanFootrule = p ∧ C.blomqvistBeta = b ∧ C.kendallTau = 4 / 3 * p - 1 / 3