← Copula mathematical handbook

Bounds at fixed Blomqvist beta

The beta–footrule inequalities of Kokol Bukovšek et al. (2021), Theorem 11, and the beta–gamma inequalities, as collected in Proposition 2.2 of Kokol Bukovšek–Mojškerc (2026). Boundary witnesses and the four exact-region theorems are provided in Copula.Rank.Region.Beta.

theorem ProbabilityTheory.Copula.integral_unit_tent {h : ℝ} (h0 : 0 ≤ h) (h1 : h ≤ 1 / 2) : ∫ (u : ↑unitInterval), max 0 (h - |↑u - 1 / 2|) = h ^ 2

Area of a symmetric tent of height at most one half.

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

theorem ProbabilityTheory.Copula.beta_le_spearmanFootrule (C : Copula 2) : 3 / 16 * (1 + C.blomqvistBeta) ^ 2 - 1 / 2 ≤ C.spearmanFootrule

theorem ProbabilityTheory.Copula.giniGamma_le_beta (C : Copula 2) : C.giniGamma ≤ 1 - 3 / 8 * (1 - C.blomqvistBeta) ^ 2

theorem ProbabilityTheory.Copula.beta_le_giniGamma (C : Copula 2) : 3 / 8 * (1 + C.blomqvistBeta) ^ 2 - 1 ≤ C.giniGamma

theorem ProbabilityTheory.Copula.beta_le_kendallTau (C : Copula 2) : 1 / 4 * (1 + C.blomqvistBeta) ^ 2 - 1 ≤ C.kendallTau

theorem ProbabilityTheory.Copula.kendallTau_le_beta (C : Copula 2) : C.kendallTau ≤ 1 - 1 / 4 * (1 - C.blomqvistBeta) ^ 2