Commit 2021-09-13 09:34 d4f8b921

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.