← Mathematical handbook

theorem Verification.measure_eq_copula_of_interior_rectangles (C : ProbabilityTheory.Copula 2) (ν : MeasureTheory.Measure (Fin 2 → ↑unitInterval)) (hac : ν.AbsolutelyContinuous MeasureTheory.volume) (hrect : ∀ (a b c d : ↑unitInterval), 0 < ↑a → a ≤ b → ↑b < 1 → 0 < ↑c → c ≤ d → ↑d < 1 → ν (Set.univ.pi fun (i : Fin 2) => Set.Ioc (![a, c] i) (![b, d] i)) = C.toMeasure (Set.univ.pi fun (i : Fin 2) => Set.Ioc (![a, c] i) (![b, d] i))) : ν = C.toMeasure

Interior rectangle equality is sufficient, even when a density is unbounded near any side or corner of the unit square.