theorem
Verification.copula_density_of_interior_derivatives
(C : ProbabilityTheory.Copula 2)
(f F P : ℝ → ℝ → ℝ)
(hfn : ∀ (u v : ↑unitInterval), 0 ≤ f ↑u ↑v)
(hfc : ∀ (u v : ℝ), u ∈ Set.Ioo 0 1 → v ∈ Set.Ioo 0 1 → ContinuousAt (Function.uncurry f) (u, v))
(hPc : ∀ (u v : ℝ), u ∈ Set.Ioo 0 1 → v ∈ Set.Ioo 0 1 → ContinuousAt (fun (x : ℝ) => P x v) u)
(hF : ∀ (u v : ℝ), u ∈ Set.Ioo 0 1 → v ∈ Set.Ioo 0 1 → HasDerivAt (fun (x : ℝ) => F x v) (P u v) u)
(hP : ∀ (u v : ℝ), u ∈ Set.Ioo 0 1 → v ∈ Set.Ioo 0 1 → HasDerivAt (P u) (f u v) v)
(hCDF : ∀ (u v : ↑unitInterval), 0 < ↑u → ↑u < 1 → 0 < ↑v → ↑v < 1 → F ↑u ↑v = C.cdf ![u, v])
:
C.toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (f ↑(x 0) ↑(x 1))
Identify an interior mixed derivative with a copula density. The density may be unbounded near the boundary and may be assigned arbitrary nonnegative values there. All differentiability and continuity assumptions are interior.