← Copula mathematical handbook

Theorem 1.1: the exact joint region, with actual attaining copulas

noncomputable def ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.footruleBetaUpperTau (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : Copula 2

Equations

• ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.footruleBetaUpperTau b hb = ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.upperSeed ((1 + b) / 8) ⋯

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.footruleBetaUpperTau_coefficients (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (footruleBetaUpperTau b hb).kendallTau = (1 + b) ^ 2 / 8 ∧ (footruleBetaUpperTau b hb).spearmanFootrule = 3 / 16 * (1 + b) ^ 2 - 1 / 2 ∧ (footruleBetaUpperTau b hb).blomqvistBeta = b

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.upper_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 = 2 / 3 * p + 1 / 3

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.exact_joint_region (t p b : ℝ) : (∃ (C : Copula 2), C.kendallTau = t ∧ 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 ∧ 4 / 3 * p - 1 / 3 ≤ t ∧ t ≤ 2 / 3 * p + 1 / 3