Equivalence of variation definitions for signed measures

For a SignedMeasure, two definitions of variation are available:

• the supremum-based VectorMeasure.variation,
• the Hahn–Jordan-based SignedMeasure.totalVariation.

In this file the two notions are shown to coincide.

Main results

• MeasureTheory.SignedMeasure.totalVariation_eq_variation: μ.totalVariation = μ.variation.

theorem MeasureTheory.SignedMeasure.norm_le_totalVariation {X : Type u_1} {mX : MeasurableSpace X} (s : SignedMeasure X) (i : Set X) : ‖s i‖ ≤ s.totalVariation.real i

The pointwise bound ‖s i‖ ≤ s.totalVariation.real i for any signed measure.

theorem MeasureTheory.SignedMeasure.eNorm_le_totalVariation {X : Type u_1} {mX : MeasurableSpace X} (s : SignedMeasure X) (i : Set X) : ‖s i‖ₑ ≤ s.totalVariation i

The pointwise bound ‖s i‖ₑ ≤ s.totalVariation i for any signed measure.

@[deprecated MeasureTheory.SignedMeasure.eNorm_le_totalVariation (since := "2026-11-06")]

theorem MeasureTheory.SignedMeasure.enorm_le_totalVariation {X : Type u_1} {mX : MeasurableSpace X} (s : SignedMeasure X) (i : Set X) : ‖s i‖ₑ ≤ s.totalVariation i

Alias of MeasureTheory.SignedMeasure.eNorm_le_totalVariation.

---

The pointwise bound ‖s i‖ₑ ≤ s.totalVariation i for any signed measure.

theorem MeasureTheory.SignedMeasure.totalVariation_eq_variation {X : Type u_1} {mX : MeasurableSpace X} (μ : SignedMeasure X) : μ.totalVariation = VectorMeasure.variation μ

The Hahn–Jordan-based totalVariation agrees with the supremum-based variation.