← Copula mathematical handbook

Order, recovery and symmetry of ordinal sums

theorem ProbabilityTheory.Copula.LowerOrthantLE.ordinalSum {C D E F : Copula 2} (h : C.LowerOrthantLE E) (k : D.LowerOrthantLE F) (a : ↑unitInterval) : (C.ordinalSum D a).LowerOrthantLE (E.ordinalSum F a)

theorem ProbabilityTheory.Copula.lowerOrthantLE_ordinalSum_iff (C D E F : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : (C.ordinalSum D a).LowerOrthantLE (E.ordinalSum F a) ↔ C.LowerOrthantLE E ∧ D.LowerOrthantLE F

Each positive-length component can be compared by restricting to its own block.

theorem ProbabilityTheory.Copula.ordinalSum_eq_iff (C D E F : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : C.ordinalSum D a = E.ordinalSum F a ↔ C = E ∧ D = F

theorem ProbabilityTheory.Copula.transpose_ordinalSum (C D : Copula 2) (a : ↑unitInterval) : (C.ordinalSum D a).transpose = C.transpose.ordinalSum D.transpose a

theorem ProbabilityTheory.Copula.IsExchangeable.ordinalSum {C D : Copula 2} (hC : C.IsExchangeable) (hD : D.IsExchangeable) (a : ↑unitInterval) : (C.ordinalSum D a).IsExchangeable

theorem ProbabilityTheory.Copula.isExchangeable_ordinalSum_iff (C D : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : (C.ordinalSum D a).IsExchangeable ↔ C.IsExchangeable ∧ D.IsExchangeable

@[simp]

theorem ProbabilityTheory.Copula.diagonal_ordinalSum_split (C D : Copula 2) (a : ↑unitInterval) : (C.ordinalSum D a).diagonal a = ↑a

theorem ProbabilityTheory.Copula.diagonal_ordinalSum_lower (C D : Copula 2) (a t : ↑unitInterval) (ht : t ≤ a) : (C.ordinalSum D a).diagonal t = ↑a * C.diagonal (OrdinalSum.lowerCoord a t)

theorem ProbabilityTheory.Copula.diagonal_ordinalSum_upper (C D : Copula 2) (a t : ↑unitInterval) (ht : a ≤ t) : (C.ordinalSum D a).diagonal t = ↑a + (1 - ↑a) * D.diagonal (OrdinalSum.upperCoord a t)

theorem ProbabilityTheory.Copula.ordinalSum_ne_independence (C D : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : C.ordinalSum D a ≠ independence 2

A nontrivial ordinal sum can never be independence.

theorem ProbabilityTheory.Copula.not_isNQD_ordinalSum (C D : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : ¬(C.ordinalSum D a).IsNQD

@[simp]

theorem ProbabilityTheory.Copula.ordinalSum_comonotonic (a : ↑unitInterval) : (comonotonic 2).ordinalSum (comonotonic 2) a = comonotonic 2

theorem ProbabilityTheory.Copula.ordinalSum_eq_comonotonic_iff (C D : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : C.ordinalSum D a = comonotonic 2 ↔ C = comonotonic 2 ∧ D = comonotonic 2