Commit 2023-11-08 21:29 0821e8fd
View on Github →feat: SigmaFinite instances for Measure.withDensity (#8271)
If a measure μ is sigma-finite, then μ.withDensity f is sigma-finite for any a.e.-measurable and a.e. finite function f.
feat: SigmaFinite instances for Measure.withDensity (#8271)
If a measure μ is sigma-finite, then μ.withDensity f is sigma-finite for any a.e.-measurable and a.e. finite function f.