mathlib3

7468d8dd - feat(measure_theory/integral/lebesgue): weaken assumptions for with_density lemmas (#11711)

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 ```lean 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.