← Mathematical handbook

Classical coefficient formulas for Fréchet and Mardia copulas

Together with Rank.Frechet and Rank.FrechetChatterjee, these formulas cover all six supported coefficients on the entire parameter domains. The tau formulas agree with Table 6 of Ansari and Rockel, Dependence properties of bivariate copula families.

theorem ProbabilityTheory.Copula.kendallTau_frechet (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (frechet a b ha hb hab).kendallTau = (a - b) * (a + b + 2) / 3

theorem ProbabilityTheory.Copula.kendallTau_mardia (θ : ℝ) (hθ : |θ| ≤ 1) : (mardia θ hθ).kendallTau = θ ^ 3 * (θ ^ 2 + 2) / 3

theorem ProbabilityTheory.Copula.spearmanFootrule_frechet (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (frechet a b ha hb hab).spearmanFootrule = a - b / 2

theorem ProbabilityTheory.Copula.giniGamma_frechet (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (frechet a b ha hb hab).giniGamma = a - b

theorem ProbabilityTheory.Copula.blomqvistBeta_frechet (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (frechet a b ha hb hab).blomqvistBeta = a - b

theorem ProbabilityTheory.Copula.spearmanFootrule_mardia (θ : ℝ) (hθ : |θ| ≤ 1) : (mardia θ hθ).spearmanFootrule = θ ^ 2 * (1 + 3 * θ) / 4

theorem ProbabilityTheory.Copula.giniGamma_mardia (θ : ℝ) (hθ : |θ| ≤ 1) : (mardia θ hθ).giniGamma = θ ^ 3

theorem ProbabilityTheory.Copula.blomqvistBeta_mardia (θ : ℝ) (hθ : |θ| ≤ 1) : (mardia θ hθ).blomqvistBeta = θ ^ 3

theorem ProbabilityTheory.Copula.kendallTau_frechet_eq_zero_iff (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (frechet a b ha hb hab).kendallTau = 0 ↔ a = b

theorem ProbabilityTheory.Copula.kendallTau_mardia_eq_zero_iff (θ : ℝ) (hθ : |θ| ≤ 1) : (mardia θ hθ).kendallTau = 0 ↔ θ = 0