← Copula mathematical handbook

Proposition 2.1: the sharp upper footrule-beta boundary

The diagonal is bounded pointwise by that of a centered W block. Integrating this comparison proves the bound for all copulas, including singular ones.

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.diagonal_le_centralW (C : Copula 2) (α : ↑unitInterval) (hβ : C.blomqvistBeta = 1 - 2 * ↑α) (t : ↑unitInterval) : C.cdf ![t, t] ≤ (Common.centralW α).cdf ![t, t]

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

Equations

• ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.footruleBetaUpper b hb = ProbabilityTheory.Copula.RankRegion.Common.centralW ⟨(1 - b) / 2, ⋯⟩

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.footruleBetaUpper_beta (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (footruleBetaUpper b hb).blomqvistBeta = b

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.footruleBetaUpper_footrule (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (footruleBetaUpper b hb).spearmanFootrule = 1 - 3 / 8 * (1 - b) ^ 2

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.footrule_le_beta_upper (C : Copula 2) : C.spearmanFootrule ≤ 1 - 3 / 8 * (1 - C.blomqvistBeta) ^ 2

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.maximal_footrule_at_beta (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∃ (D : Copula 2), D.blomqvistBeta = b ∧ D.spearmanFootrule = 1 - 3 / 8 * (1 - b) ^ 2 ∧ ∀ (C : Copula 2), C.blomqvistBeta = b → C.spearmanFootrule ≤ D.spearmanFootrule

The upper inequality in equation (8) is attained at every admissible beta.