Commit 2022-01-31 09:46 7468d8dd

feat(measure_theory/integral/lebesgue): weaken assumptions for with_density lemmas (#11711) We state more precise versions of some lemmas about the measure μ.with_density f, making it possible to remove some assumptions down the road. For instance, the lemma

  integrable g (μ.with_density f) ↔ integrable (λ x, g x * (f x).to_real) μ

currently requires the measurability of g, while we can completely remove it with the new lemmas. We also make lintegral irreducible.