Commit 2023-11-14 12:32 21b59396

feat: generalize some lemmas using withDensity_apply' (#8383) @sgouezel added a version of withDensity_apply that does not require measurability of the set if the measure is s-finite. This PR uses that result in other files of the library. For results about rnDeriv, I put a prime on the version that assumes measurability of the set and no prime on the version for s-finite measures, as the second one should be the main use case.