← Mathematical handbook

theorem Verification.density_rectangle_integral (C : ProbabilityTheory.Copula 2) (f : (Fin 2 → ↑unitInterval) → ℝ) (hf : Measurable f) (hd : C.toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (f x)) (S T : Set ↑unitInterval) (hS : MeasurableSet S) (hT : MeasurableSet T) : C.toMeasure {x : Fin 2 → ↑unitInterval | x 0 ∈ S ∧ x 1 ∈ T} = ∫⁻ (a : ↑unitInterval) in S, ∫⁻ (b : ↑unitInterval) in T, ENNReal.ofReal (f ![a, b])

theorem Verification.measureReal_coordinate_rectangle (C : ProbabilityTheory.Copula 2) (a b c d : ↑unitInterval) (hab : a ≤ b) (hcd : c ≤ d) : C.toMeasure.real {x : Fin 2 → ↑unitInterval | x 0 ∈ Set.Ioc a b ∧ x 1 ∈ Set.Ioc c d} = C.cdf ![b, d] - C.cdf ![a, d] - C.cdf ![b, c] + C.cdf ![a, c]