← Copula mathematical handbook

Consequences of diagonal cuts

The decomposition theorem transfers fixed-split rank bounds to any copula with a diagonal fixed point. At the median this gives a structural characterization of maximal Blomqvist beta and sharp bounds on three other rank coefficients. Component diagonals retain the remaining cuts.

theorem ProbabilityTheory.Copula.diagonal_lowerOrdinalComponent (C : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha : C.diagonal a = ↑a) (t : ↑unitInterval) : (C.lowerOrdinalComponent a ha0 ha).diagonal t = C.diagonal (OrdinalSum.lowerEmbed a t) / ↑a

theorem ProbabilityTheory.Copula.diagonal_upperOrdinalComponent (C : Copula 2) (a : ↑unitInterval) (ha1 : a < 1) (ha : C.diagonal a = ↑a) (t : ↑unitInterval) : (C.upperOrdinalComponent a ha1 ha).diagonal t = (C.diagonal (OrdinalSum.upperEmbed a t) - ↑a) / (1 - ↑a)

theorem ProbabilityTheory.Copula.diagonal_lowerOrdinalComponent_eq_iff (C : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha : C.diagonal a = ↑a) (t : ↑unitInterval) : (C.lowerOrdinalComponent a ha0 ha).diagonal t = ↑t ↔ C.diagonal (OrdinalSum.lowerEmbed a t) = ↑(OrdinalSum.lowerEmbed a t)

theorem ProbabilityTheory.Copula.diagonal_upperOrdinalComponent_eq_iff (C : Copula 2) (a : ↑unitInterval) (ha1 : a < 1) (ha : C.diagonal a = ↑a) (t : ↑unitInterval) : (C.upperOrdinalComponent a ha1 ha).diagonal t = ↑t ↔ C.diagonal (OrdinalSum.upperEmbed a t) = ↑(OrdinalSum.upperEmbed a t)

theorem ProbabilityTheory.Copula.kendallTau_lower_bound_of_diagonal_eq (C : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) (ha : C.diagonal a = ↑a) : 4 * ↑a * (1 - ↑a) - 1 ≤ C.kendallTau

theorem ProbabilityTheory.Copula.spearmanRho_lower_bound_of_diagonal_eq (C : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) (ha : C.diagonal a = ↑a) : 6 * ↑a * (1 - ↑a) - 1 ≤ C.spearmanRho

theorem ProbabilityTheory.Copula.spearmanFootrule_lower_bound_of_diagonal_eq (C : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) (ha : C.diagonal a = ↑a) : 3 * ↑a * (1 - ↑a) - 1 / 2 ≤ C.spearmanFootrule

theorem ProbabilityTheory.Copula.blomqvistBeta_eq_one_iff_exists_ordinalSum (C : Copula 2) : C.blomqvistBeta = 1 ↔ ∃ (D : Copula 2) (E : Copula 2), D.ordinalSum E unitHalf = C

theorem ProbabilityTheory.Copula.blomqvistBeta_eq_one_iff_existsUnique_ordinalSum (C : Copula 2) : C.blomqvistBeta = 1 ↔ ∃! p : Copula 2 × Copula 2, p.1.ordinalSum p.2 unitHalf = C

theorem ProbabilityTheory.Copula.kendallTau_nonneg_of_blomqvistBeta_eq_one (C : Copula 2) (h : C.blomqvistBeta = 1) : 0 ≤ C.kendallTau

theorem ProbabilityTheory.Copula.half_le_spearmanRho_of_blomqvistBeta_eq_one (C : Copula 2) (h : C.blomqvistBeta = 1) : 1 / 2 ≤ C.spearmanRho

theorem ProbabilityTheory.Copula.quarter_le_spearmanFootrule_of_blomqvistBeta_eq_one (C : Copula 2) (h : C.blomqvistBeta = 1) : 1 / 4 ≤ C.spearmanFootrule

theorem ProbabilityTheory.Copula.blomqvistBeta_eq_neg_one_iff_exists_reflected_ordinalSum (C : Copula 2) : C.blomqvistBeta = -1 ↔ ∃ (D : Copula 2) (E : Copula 2), (D.ordinalSum E unitHalf).reflect {1} = C

theorem ProbabilityTheory.Copula.kendallTau_nonpos_of_blomqvistBeta_eq_neg_one (C : Copula 2) (h : C.blomqvistBeta = -1) : C.kendallTau ≤ 0

theorem ProbabilityTheory.Copula.spearmanRho_le_neg_half_of_blomqvistBeta_eq_neg_one (C : Copula 2) (h : C.blomqvistBeta = -1) : C.spearmanRho ≤ -1 / 2