Reflecting an actual copula density #
theorem
Verification.reflect_toMeasure_density
{d : ℕ}
(C : ProbabilityTheory.Copula d)
(s : Finset (Fin d))
{f : (Fin d → ↑unitInterval) → ENNReal}
(hf : Measurable f)
(he : C.toMeasure = MeasureTheory.volume.withDensity f)
:
(C.reflect s).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin d → ↑unitInterval) => f (ProbabilityTheory.Copula.reflectPoint s x)