theorem
Verification.measure_eq_copula_of_positive_rectangles
(C : ProbabilityTheory.Copula 2)
(ν : MeasureTheory.Measure (Fin 2 → ↑unitInterval))
(hac : ν.AbsolutelyContinuous MeasureTheory.volume)
(hrect :
∀ (a b c d : ↑unitInterval),
0 < ↑a →
a ≤ b →
0 < ↑c →
c ≤ d →
ν (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)))
:
Equality on rectangles bounded away from the axes identifies an absolutely continuous measure with a copula measure. No global density bound is required.