Commit 2026-02-10 17:28 e0118614
View on Github →feat(MeasureTheory.VectorMeasure): add a definition of total variation for VectorMeasure (#26156)
This PR adds variation for any VectorMeasure using a supremum definition. Currently mathlib has TotalVariation defined for a signed measure using the Hahn-Jordan decomposition, but this doesn't generalise.
Motivation: generally this is an important concept but specifically as a step for proving RMK in the complex case which in turn is a step to prove the spectral theorem.
This PR was migrated from #25442. PR divided into smaller pieces, this is just the definition without additional lemmas. PRs adding further results related to variation are: