Commit 2026-04-08 09:27 086e717b

feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation (#26160) Add the following lemmas concerning variation of a VectorMeasure:

• norm_measure_le_variation: ‖μ E‖ₑ ≤ variation μ E.
• variation_neg: (-μ).variation = μ.variation.
• variation_zero: (0 : VectorMeasure X V).variation = 0.
• absolutelyContinuous

• depends on: #26156