Jordan decomposition of a difference of measures, eventwise

The positive part of the Jordan decomposition of a signed measure s has total mass equal to the largest value of s on a set, and its negative part the largest value of -s. For a difference μ - ν of two finite measures these are the largest excess μ A - ν A and the largest excess ν A - μ A over measurable events A. For two finite measures of the same total mass the two parts have equal mass.

These masses compute Mathlib's total variation distance etvDist μ ν through measurable events; see TauCeti.MeasureTheory.Measure.TotalVariation.Basic.

Main declarations

• MeasureTheory.SignedMeasure.toJordanDecomposition_posPart_univ_eq_iSup and MeasureTheory.SignedMeasure.toJordanDecomposition_negPart_univ_eq_iSup: the masses of the positive and negative parts as suprema of s and -s;
• MeasureTheory.Measure.toJordanDecomposition_toSignedMeasure_sub_posPart_univ_eq_iSup and MeasureTheory.Measure.toJordanDecomposition_toSignedMeasure_sub_negPart_univ_eq_iSup: the same masses for μ - ν, as largest excesses over measurable events;
• MeasureTheory.Measure.toJordanDecomposition_toSignedMeasure_sub_posPart_univ_eq_negPart_univ: for finite measures of equal total mass the two parts have equal mass.

theorem MeasureTheory.SignedMeasure.toJordanDecomposition_posPart_univ_eq_iSup {α : Type u_1} [MeasurableSpace α] (s : SignedMeasure α) : s.toJordanDecomposition.posPart Set.univ = ⨆ (A : Set α), ENNReal.ofReal (s A)

The positive part of the Jordan decomposition of s has total mass the supremum of s over all sets (s vanishes on non-measurable sets, so they do not contribute).

theorem MeasureTheory.SignedMeasure.toJordanDecomposition_negPart_univ_eq_iSup {α : Type u_1} [MeasurableSpace α] (s : SignedMeasure α) : s.toJordanDecomposition.negPart Set.univ = ⨆ (A : Set α), ENNReal.ofReal (-s A)

The negative part of the Jordan decomposition of s has total mass the supremum of -s over all sets.

theorem MeasureTheory.Measure.toJordanDecomposition_toSignedMeasure_sub_posPart_univ_eq_iSup {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition.posPart Set.univ = ⨆ (A : Set α), ⨆ (_ : MeasurableSet A), μ A - ν A

The positive part of the Jordan decomposition of μ - ν has total mass the largest excess μ A - ν A over measurable events.

theorem MeasureTheory.Measure.toJordanDecomposition_toSignedMeasure_sub_negPart_univ_eq_iSup {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition.negPart Set.univ = ⨆ (A : Set α), ⨆ (_ : MeasurableSet A), ν A - μ A

The negative part of the Jordan decomposition of μ - ν has total mass the largest excess ν A - μ A over measurable events.

theorem MeasureTheory.Measure.toJordanDecomposition_toSignedMeasure_sub_posPart_univ_eq_negPart_univ {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : μ Set.univ = ν Set.univ) : (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition.posPart Set.univ = (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition.negPart Set.univ

For finite measures of equal total mass, the positive and negative parts of the Jordan decomposition of μ - ν have equal total mass.