Total variation distance as a supremum over events

Mathlib's total variation distance MeasureTheory.etvDist μ ν between finite measures is the variation of the signed measure μ - ν on the whole space. With this normalization the distance between two probability measures lies in [0, 2]: it is the signed-measure norm ‖μ - ν‖, twice the distance sup_A |μ A - ν A| that some authors use instead.

This file expresses etvDist through measurable events. It is the sum of the largest excess μ A - ν A and the largest excess ν A - μ A, so eventwise bounds

μ A ≤ ν A + c,    ν A ≤ μ A + d    (A measurable)

give etvDist μ ν ≤ c + d. For finite measures of the same total mass the two excesses agree, so etvDist μ ν ≤ 2 * c exactly when every measurable event satisfies μ A ≤ ν A + c. These statements pin down the factor of two relating the two conventions, and turn eventwise estimates into total-variation estimates.

Main declarations

• MeasureTheory.abs_measureReal_sub_le_tvDist: the real masses of a measurable event differ by at most tvDist μ ν;
• MeasureTheory.etvDist_eq_posPart_univ_add_negPart_univ: etvDist μ ν is the total mass of the positive part of the Jordan decomposition of μ - ν plus that of its negative part;
• MeasureTheory.etvDist_eq_iSup_sub_add_iSup_sub: etvDist μ ν is the largest excess of μ over ν on an event plus the largest excess of ν over μ;
• MeasureTheory.etvDist_eq_two_mul_iSup_sub: for finite measures of equal total mass, it is twice the largest excess of μ over ν;
• MeasureTheory.etvDist_le_of_forall_le_add: eventwise bounds in both directions bound the total variation distance;
• MeasureTheory.etvDist_le_two_mul_iff: for finite measures of equal total mass, etvDist μ ν ≤ 2 * c if and only if every measurable event satisfies μ A ≤ ν A + c;
• MeasureTheory.tvDist_dirac_left: the distance from a point mass to a probability measure is twice its mass outside the point.

theorem MeasureTheory.abs_measureReal_sub_le_tvDist {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] {s : Set α} (hs : MeasurableSet s) : |μ.real s - ν.real s| ≤ tvDist μ ν

Total variation bounds the difference of the masses of each measurable event.

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

The total variation distance between finite measures is the total mass of the positive part of the Jordan decomposition of μ - ν plus the total mass of its negative part.

theorem MeasureTheory.etvDist_eq_iSup_sub_add_iSup_sub {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : etvDist μ ν = (⨆ (A : Set α), ⨆ (_ : MeasurableSet A), μ A - ν A) + ⨆ (A : Set α), ⨆ (_ : MeasurableSet A), ν A - μ A

The total variation distance between finite measures is the largest excess μ A - ν A over measurable events plus the largest excess ν A - μ A.

theorem MeasureTheory.etvDist_eq_two_mul_iSup_sub {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} [IsFiniteMeasure μ] (h : μ Set.univ = ν Set.univ) : etvDist μ ν = 2 * ⨆ (A : Set α), ⨆ (_ : MeasurableSet A), μ A - ν A

For a finite measure and a measure of the same total mass (e.g. two probability measures), the total variation distance is twice the largest excess μ A - ν A over measurable events.

theorem MeasureTheory.etvDist_le_of_forall_le_add {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] {c d : ENNReal} (h₁ : ∀ (A : Set α), MeasurableSet A → μ A ≤ ν A + c) (h₂ : ∀ (A : Set α), MeasurableSet A → ν A ≤ μ A + d) : etvDist μ ν ≤ c + d

Total variation from eventwise bounds. If every measurable event has μ-mass at most its ν-mass plus c, and ν-mass at most its μ-mass plus d, then etvDist μ ν ≤ c + d.

theorem MeasureTheory.etvDist_le_two_mul_iff {α : Type u_1} [MeasurableSpace α] {μ ν : Measure α} [IsFiniteMeasure μ] (h : μ Set.univ = ν Set.univ) {c : ENNReal} : etvDist μ ν ≤ 2 * c ↔ ∀ (A : Set α), MeasurableSet A → μ A ≤ ν A + c

Total variation as an eventwise bound. For a finite measure and a measure of the same total mass (e.g. two probability measures), etvDist μ ν ≤ 2 * c if and only if every measurable event has μ-mass at most its ν-mass plus c. In other words, etvDist μ ν is twice the distance sup_A |μ A - ν A|.

@[simp]

theorem MeasureTheory.etvDist_dirac_left {α : Type u_1} [MeasurableSpace α] {ν : Measure α} (x : α) [IsProbabilityMeasure ν] : etvDist (Measure.dirac x) ν = 2 * (1 - ν {x})

The total variation distance from a point mass to a probability measure is twice the probability of missing that point. The factor two is Mathlib's normalization.

@[simp]

theorem MeasureTheory.tvDist_dirac_left {α : Type u_1} [MeasurableSpace α] {ν : Measure α} (x : α) [IsProbabilityMeasure ν] : tvDist (Measure.dirac x) ν = 2 * (1 - ν.real {x})

The real-valued total variation distance from a point mass to a probability measure.