← Copula mathematical handbook

Block probabilities and support of ordinal sums

The two coordinates belong to the same block almost surely. The lower block has probability a and the upper block has probability 1-a. The statements include both degenerate splits.

theorem ProbabilityTheory.Copula.ae_ordinalSum_mem_blocks (C D : Copula 2) (a : ↑unitInterval) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂(C.ordinalSum D a).toMeasure, (∀ (i : Fin 2), x i ≤ a) ∨ ∀ (i : Fin 2), a ≤ x i

theorem ProbabilityTheory.Copula.measureReal_ordinalSum_lower_block (C D : Copula 2) (a : ↑unitInterval) : (C.ordinalSum D a).toMeasure.real {x : Fin 2 → ↑unitInterval | ∀ (i : Fin 2), x i ≤ a} = ↑a

theorem ProbabilityTheory.Copula.measureReal_ordinalSum_upper_block (C D : Copula 2) (a : ↑unitInterval) : (C.ordinalSum D a).toMeasure.real {x : Fin 2 → ↑unitInterval | ∀ (i : Fin 2), a ≤ x i} = 1 - ↑a

theorem ProbabilityTheory.Copula.measure_ordinalSum_cross_blocks (C D : Copula 2) (a : ↑unitInterval) : (C.ordinalSum D a).toMeasure {x : Fin 2 → ↑unitInterval | x 0 < a ∧ a < x 1 ∨ x 1 < a ∧ a < x 0} = 0

theorem ProbabilityTheory.Copula.ae_ordinalSum_same_side (C D : Copula 2) (a : ↑unitInterval) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂(C.ordinalSum D a).toMeasure, x 0 ≤ a ↔ x 1 ≤ a