mathlib3

d4f8b921 - feat(measure_theory/measure/with_density_vector_measure): define vector measures by an integral over a function (#9008)

feat(measure_theory/measure/with_density_vector_measure): define vector measures by an integral over a function (#9008) This PR defined the vector measure corresponding to mapping the set `s` to the integral `∫ x in s, f x ∂μ` given some measure `μ` and some integrable function `f`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>