[Merged by Bors] - feat(MeasureTheory/VectorMeasure): add integral of a vector-valued function against a vector measure#28499

yoh-tanimoto wants to merge 138 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

yoh-tanimoto:yoh-tanimoto-vectormeasure-integralyoh-tanimoto/mathlib4:yoh-tanimoto-vectormeasure-integralCopy head branch name to clipboard