← Copula mathematical handbook

Median concordance and nonunique extremal coefficients

Beta is extremal exactly when the midpoint CDF attains its corresponding bound. Its negative extreme is also equivalent to minimal footrule and the lower Fréchet diagonal. Explicit ordinal sums show that neither extreme of beta, nor the lower extreme of footrule, determines a unique copula.

theorem ProbabilityTheory.Copula.blomqvistBeta_eq_one_iff (C : Copula 2) : C.blomqvistBeta = 1 ↔ C.cdf ![unitHalf, unitHalf] = 1 / 2

theorem ProbabilityTheory.Copula.blomqvistBeta_eq_neg_one_iff (C : Copula 2) : C.blomqvistBeta = -1 ↔ C.cdf ![unitHalf, unitHalf] = 0

theorem ProbabilityTheory.Copula.diagonal_eq_lower_iff_blomqvistBeta_eq_neg_one (C : Copula 2) : (∀ (t : ↑unitInterval), C.diagonal t = max 0 (2 * ↑t - 1)) ↔ C.blomqvistBeta = -1

theorem ProbabilityTheory.Copula.spearmanFootrule_eq_neg_half_iff_blomqvistBeta_eq_neg_one (C : Copula 2) : C.spearmanFootrule = -1 / 2 ↔ C.blomqvistBeta = -1

theorem ProbabilityTheory.Copula.neg_half_lt_spearmanFootrule_iff (C : Copula 2) : -1 / 2 < C.spearmanFootrule ↔ C.blomqvistBeta ≠ -1

theorem ProbabilityTheory.Copula.blomqvistBeta_ordinalSum_half (C D : Copula 2) : (C.ordinalSum D unitHalf).blomqvistBeta = 1

theorem ProbabilityTheory.Copula.blomqvistBeta_reflect_ordinalSum_half (C D : Copula 2) : ((C.ordinalSum D unitHalf).reflect {1}).blomqvistBeta = -1

theorem ProbabilityTheory.Copula.spearmanFootrule_reflect_ordinalSum_half (C D : Copula 2) : ((C.ordinalSum D unitHalf).reflect {1}).spearmanFootrule = -1 / 2

theorem ProbabilityTheory.Copula.ordinalSum_independence_half_ne_comonotonic : (independence 2).ordinalSum (independence 2) unitHalf ≠ comonotonic 2

theorem ProbabilityTheory.Copula.exists_blomqvistBeta_eq_one_ne_comonotonic : ∃ (C : Copula 2), C.blomqvistBeta = 1 ∧ C ≠ comonotonic 2

Maximal median concordance does not characterize comonotonicity.

theorem ProbabilityTheory.Copula.exists_blomqvistBeta_eq_neg_one_ne_countermonotonic : ∃ (C : Copula 2), C.blomqvistBeta = -1 ∧ C ≠ countermonotonic

Minimal median concordance does not characterize countermonotonicity.

theorem ProbabilityTheory.Copula.exists_spearmanFootrule_eq_neg_half_ne_countermonotonic : ∃ (C : Copula 2), C.spearmanFootrule = -1 / 2 ∧ C ≠ countermonotonic

Minimal footrule does not characterize countermonotonicity.