mathlib

eb5c5ed5 - feat(measure_theory/integral/set_integral): Bochner integral with respect to a measure with density (#12123)

feat(measure_theory/integral/set_integral): Bochner integral with respect to a measure with density (#12123) This PR shows that `∫ a, g a ∂(μ.with_density (λ x, f x)) = ∫ a, f a • g a ∂μ`. (This fact is already available for the Lebesgue integral, not for the Bochner integral.)