[Merged by Bors] - feat: more API for the variation of vector measures#39616

sgouezel wants to merge 12 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

sgouezel:SG_variationsgouezel/mathlib4:SG_variationCopy head branch name to clipboard