← Mathematical handbook

theorem Verification.mtp2_ordered_rectangles {C : ProbabilityTheory.Copula 2} (hC : C.HasMTP2Density) (S T U V : Set ↑unitInterval) (hS : MeasurableSet S) (hT : MeasurableSet T) (hU : MeasurableSet U) (hV : MeasurableSet V) (hST : ∀ a ∈ S, ∀ b ∈ T, a ≤ b) (hUV : ∀ u ∈ U, ∀ v ∈ V, u ≤ v) : C.toMeasure.real {x : Fin 2 → ↑unitInterval | x 0 ∈ S ∧ x 1 ∈ V} * C.toMeasure.real {x : Fin 2 → ↑unitInterval | x 0 ∈ T ∧ x 1 ∈ U} ≤ C.toMeasure.real {x : Fin 2 → ↑unitInterval | x 0 ∈ S ∧ x 1 ∈ U} * C.toMeasure.real {x : Fin 2 → ↑unitInterval | x 0 ∈ T ∧ x 1 ∈ V}

theorem Verification.mtp2_isSI {C : ProbabilityTheory.Copula 2} (hC : C.HasMTP2Density) : C.IsSI

theorem Verification.mtp2_isCI {C : ProbabilityTheory.Copula 2} (hC : C.HasMTP2Density) : C.IsCI