Total variation for complex measures (and vector measures)

Stream: mathlib4

[Oliver Butterley]

As far as I can see we don't yet have total variation for complex measures, only for signed measures. docs#MeasureTheory.SignedMeasure.totalVariation (Right now it would be useful for proving the complex version of RMK and generally it would be useful.)

In the case of signed measures it can and is defined using the decomposition, s.toJordanDecomposition.posPart + s.toJordanDecomposition.negPart but the general case has to be defined as a supremum. What makes sense for defining total variation for vector valued measures since it doesn't directly generalize? Define VectorMeasure.totalVariation as the standard supremum and then show the equivalence to SignedMeasure.totalVariation when restricted to signed measures?

[Yoh Tanimoto]

as far as I see, totalVariation in the current definition has not been used in many place, except in the definin file MeasureTheory.SignedMeasure.totalVariation and MeasureTheory.SignedMeasure.singularPart_totalVariation. It seems more natural to me that totalVariation is defiend for any normed-space-valued measure, and proven to be equalt to the current definition for SignedMeasure.

[Oliver Butterley]

Seems good. Let's work along these lines and it will surely become rather clearer when we have something complete.