← Mathematical handbook

The converse ordinal-sum theorem

At each interior diagonal fixed point a copula is the ordinal sum of its two rescaled restrictions. The pair of components is unique for that fixed split. This is the binary form of Nelsen's Theorem 3.2.1; the split itself need not be unique.

theorem ProbabilityTheory.Copula.ordinalSum_components (C : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) (ha : C.diagonal a = ↑a) : (C.lowerOrdinalComponent a ha0 ha).ordinalSum (C.upperOrdinalComponent a ha1 ha) a = C

@[simp]

theorem ProbabilityTheory.Copula.lowerOrdinalComponent_ordinalSum (C D : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) : (C.ordinalSum D a).lowerOrdinalComponent a ha0 ⋯ = C

@[simp]

theorem ProbabilityTheory.Copula.upperOrdinalComponent_ordinalSum (C D : Copula 2) (a : ↑unitInterval) (ha1 : a < 1) : (C.ordinalSum D a).upperOrdinalComponent a ha1 ⋯ = D

@[simp]

theorem ProbabilityTheory.Copula.lowerOrdinalComponent_one (C : Copula 2) : C.lowerOrdinalComponent 1 ⋯ ⋯ = C

@[simp]

theorem ProbabilityTheory.Copula.upperOrdinalComponent_zero (C : Copula 2) : C.upperOrdinalComponent 0 ⋯ ⋯ = C

theorem ProbabilityTheory.Copula.diagonal_eq_iff_exists_ordinalSum (C : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : C.diagonal a = ↑a ↔ ∃ (D : Copula 2) (E : Copula 2), D.ordinalSum E a = C

A prescribed interior point is an ordinal-sum split exactly when the diagonal is fixed there.

theorem ProbabilityTheory.Copula.diagonal_eq_iff_existsUnique_ordinalSum (C : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : C.diagonal a = ↑a ↔ ∃! p : Copula 2 × Copula 2, p.1.ordinalSum p.2 a = C

For a fixed interior split, the two components are uniquely determined.

theorem ProbabilityTheory.Copula.exists_ordinalSum_iff_exists_diagonal_fixedPoint (C : Copula 2) : (∃ (a : ↑unitInterval) (D : Copula 2) (E : Copula 2), 0 < a ∧ a < 1 ∧ D.ordinalSum E a = C) ↔ ∃ (a : ↑unitInterval), 0 < a ∧ a < 1 ∧ C.diagonal a = ↑a

The binary ordinal-sum characterization, Nelsen, second edition, Theorem 3.2.1.

theorem ProbabilityTheory.Copula.IsNQD.not_exists_ordinalSum {C : Copula 2} (h : C.IsNQD) : ¬∃ (a : ↑unitInterval) (D : Copula 2) (E : Copula 2), 0 < a ∧ a < 1 ∧ D.ordinalSum E a = C