← Copula mathematical handbook

Proposition 2.1 and Corollary 4.2: both remaining pairwise regions

All witnesses are constructed copulas. The tau-beta projection is proved directly, without assuming the still separate three-dimensional theorem.

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.tau_footrule_bounds (C : Copula 2) : 4 / 3 * C.spearmanFootrule - 1 / 3 ≤ C.kendallTau ∧ C.kendallTau ≤ 2 / 3 * C.spearmanFootrule + 1 / 3

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.tau_beta_bounds (C : Copula 2) : (1 + C.blomqvistBeta) ^ 2 / 4 - 1 ≤ C.kendallTau ∧ C.kendallTau ≤ 1 - (1 - C.blomqvistBeta) ^ 2 / 4

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.exact_tau_beta_region (t b : ℝ) : (∃ (C : Copula 2), C.kendallTau = t ∧ C.blomqvistBeta = b) ↔ b ∈ Set.Icc (-1) 1 ∧ (1 + b) ^ 2 / 4 - 1 ≤ t ∧ t ≤ 1 - (1 - b) ^ 2 / 4

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.upperTauSeed_coefficients : (medianWBlocks.reflect {1}).kendallTau = 0 ∧ (medianWBlocks.reflect {1}).spearmanFootrule = -1 / 2 ∧ (medianWBlocks.reflect {1}).blomqvistBeta = -1

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.centered_tau_endpoints (α : ↑unitInterval) : have C := Common.centeredOrdinal countermonotonic α; have D := Common.centeredOrdinal (medianWBlocks.reflect {1}) α; C.spearmanFootrule = 1 - 3 / 2 * ↑α ^ 2 ∧ D.spearmanFootrule = 1 - 3 / 2 * ↑α ^ 2 ∧ C.kendallTau = 1 - 2 * ↑α ^ 2 ∧ D.kendallTau = 1 - ↑α ^ 2 ∧ C.blomqvistBeta = 1 - 2 * ↑α ∧ D.blomqvistBeta = 1 - 2 * ↑α

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.exact_tau_footrule_region (t p : ℝ) : (∃ (C : Copula 2), C.kendallTau = t ∧ C.spearmanFootrule = p) ↔ p ∈ Set.Icc (-1 / 2) 1 ∧ 4 / 3 * p - 1 / 3 ≤ t ∧ t ≤ 2 / 3 * p + 1 / 3