← Copula mathematical handbook

Rank coefficients determined by power diagonals

Spearman's footrule and Blomqvist's beta depend only on the diagonal. Thus their closed forms hold for every power-diagonal copula, in particular every bivariate extreme-value copula, including singular ones.

theorem ProbabilityTheory.Copula.HasPowerDiagonal.spearmanFootrule {C : Copula 2} {κ : ℝ} (h : C.HasPowerDiagonal κ) : C.spearmanFootrule = 6 / (κ + 1) - 2

theorem ProbabilityTheory.Copula.HasPowerDiagonal.blomqvistBeta {C : Copula 2} {κ : ℝ} (h : C.HasPowerDiagonal κ) : C.blomqvistBeta = 2 ^ (2 - κ) - 1

theorem ProbabilityTheory.Copula.IsExtremeValue.spearmanFootrule {C : Copula 2} (h : C.IsExtremeValue) : C.spearmanFootrule = 6 / (C.extremalCoefficient + 1) - 2

theorem ProbabilityTheory.Copula.IsExtremeValue.blomqvistBeta {C : Copula 2} (h : C.IsExtremeValue) : C.blomqvistBeta = 2 ^ (2 - C.extremalCoefficient) - 1

theorem ProbabilityTheory.Copula.spearmanFootrule_marshallOlkin (α β : ↑unitInterval) : (marshallOlkin α β).spearmanFootrule = 6 / (3 - min ↑α ↑β) - 2

theorem ProbabilityTheory.Copula.blomqvistBeta_marshallOlkin (α β : ↑unitInterval) : (marshallOlkin α β).blomqvistBeta = 2 ^ min ↑α ↑β - 1

theorem ProbabilityTheory.Copula.spearmanFootrule_cuadrasAuge (α : ↑unitInterval) : (cuadrasAuge α).spearmanFootrule = 6 / (3 - ↑α) - 2

theorem ProbabilityTheory.Copula.blomqvistBeta_cuadrasAuge (α : ↑unitInterval) : (cuadrasAuge α).blomqvistBeta = 2 ^ ↑α - 1

theorem ProbabilityTheory.Copula.spearmanFootrule_gumbel (θ : ℝ) (hθ : 1 ≤ θ) : (gumbel θ hθ).spearmanFootrule = 6 / (2 ^ θ⁻¹ + 1) - 2

theorem ProbabilityTheory.Copula.blomqvistBeta_gumbel (θ : ℝ) (hθ : 1 ≤ θ) : (gumbel θ hθ).blomqvistBeta = 2 ^ (2 - 2 ^ θ⁻¹) - 1

theorem ProbabilityTheory.Copula.spearmanFootrule_tawn (θ : ℝ) (hθ : 1 ≤ θ) (α β : ↑unitInterval) : (tawn θ hθ α β).spearmanFootrule = 6 / (3 - ↑α - ↑β + (↑α ^ θ + ↑β ^ θ) ^ θ⁻¹) - 2

theorem ProbabilityTheory.Copula.blomqvistBeta_tawn (θ : ℝ) (hθ : 1 ≤ θ) (α β : ↑unitInterval) : (tawn θ hθ α β).blomqvistBeta = 2 ^ (↑α + ↑β - (↑α ^ θ + ↑β ^ θ) ^ θ⁻¹) - 1