Total variation distance

We define the total variation distance between two finite measures, as the vector total variation distance between the corresponding signed measures.

Note that with this definition, the total variation distance between probability measures takes values in [0, 2]. Some authors prefer to define the total variation distance as half of the value defined here, so that it takes values in [0, 1].

Main definitions

• etvDist μ ν: total variation distance between two finite measures, defined as the value on the whole space of the variation of μ - ν, in which both measures are seen as signed measures. This distance takes values in ℝ≥0∞. If one of the measures is not finite, it is defined to be ∞, and it is finite otherwise (see etvDist_lt_top_iff).
• tvDist μ ν: total variation distance between two finite measures, defined as (etvDist μ ν).toReal. It is equal to 0 if one of the measures is not finite.

Main statements

• tvDist_self, tvDist_eq_zero_iff, tvDist_comm, tvDist_triangle: the total variation distance between finite measures is a distance.

noncomputable def MeasureTheory.etvDist {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ ν : Measure 𝓧) : ENNReal

Total variation distance between two finite measures, with value in ℝ≥0∞. If one of the measures is not finite, it is defined to be ∞.

Equations

• MeasureTheory.etvDist μ ν = if h : MeasureTheory.IsFiniteMeasure μ ∧ MeasureTheory.IsFiniteMeasure ν then MeasureTheory.VectorMeasure.etvDist μ.toSignedMeasure ν.toSignedMeasure else ⊤

noncomputable def MeasureTheory.tvDist {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ ν : Measure 𝓧) : ℝ

Total variation distance between two finite measures, with value in ℝ. If one of the measures is not finite, it is equal to 0.

Equations

• MeasureTheory.tvDist μ ν = (MeasureTheory.etvDist μ ν).toReal

theorem MeasureTheory.etvDist_eq_etvDist_toSignedMeasure {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : etvDist μ ν = VectorMeasure.etvDist μ.toSignedMeasure ν.toSignedMeasure

theorem MeasureTheory.etvDist_of_not_isFiniteMeasure {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} (h : ¬(IsFiniteMeasure μ ∧ IsFiniteMeasure ν)) : etvDist μ ν = ⊤

theorem MeasureTheory.etvDist_of_not_isFiniteMeasure_left {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} (h : ¬IsFiniteMeasure μ) : etvDist μ ν = ⊤

theorem MeasureTheory.etvDist_of_not_isFiniteMeasure_right {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} (h : ¬IsFiniteMeasure ν) : etvDist μ ν = ⊤

theorem MeasureTheory.etvDist_comm {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ ν : Measure 𝓧) : etvDist μ ν = etvDist ν μ

@[simp]

theorem MeasureTheory.etvDist_zero_right {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ : Measure 𝓧) : etvDist μ 0 = μ Set.univ

@[simp]

theorem MeasureTheory.etvDist_zero_left {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (ν : Measure 𝓧) : etvDist 0 ν = ν Set.univ

theorem MeasureTheory.etvDist_triangle {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ ν ξ : Measure 𝓧) : etvDist μ ξ ≤ etvDist μ ν + etvDist ν ξ

theorem MeasureTheory.etvDist_le_add {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} : etvDist μ ν ≤ μ Set.univ + ν Set.univ

theorem MeasureTheory.etvDist_lt_top {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ ν : Measure 𝓧) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : etvDist μ ν < ⊤

@[simp]

theorem MeasureTheory.etvDist_ne_top {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ ν : Measure 𝓧) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : etvDist μ ν ≠ ⊤

theorem MeasureTheory.etvDist_lt_top_iff {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} : etvDist μ ν < ⊤ ↔ IsFiniteMeasure μ ∧ IsFiniteMeasure ν

theorem MeasureTheory.etvDist_ne_top_iff {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} : etvDist μ ν ≠ ⊤ ↔ IsFiniteMeasure μ ∧ IsFiniteMeasure ν

theorem MeasureTheory.etvDist_eq_iSup_finPartition_enorm {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : etvDist μ ν = ⨆ (P : Finpartition ⟨Set.univ, ⋯⟩), ∑ p ∈ P.parts, ‖μ.real ↑p - ν.real ↑p‖ₑ

@[simp]

theorem MeasureTheory.etvDist_self {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ : Measure 𝓧) [IsFiniteMeasure μ] : etvDist μ μ = 0

@[simp]

theorem MeasureTheory.etvDist_eq_zero_iff {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : etvDist μ ν = 0 ↔ μ = ν

theorem MeasureTheory.etvDist_restrict_add_compl {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} {s : Set 𝓧} (hs : MeasurableSet s) : etvDist (μ.restrict s) (ν.restrict s) + etvDist (μ.restrict sᶜ) (ν.restrict sᶜ) = etvDist μ ν

theorem MeasureTheory.etvDist_of_ge {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure ν] (hμν : ν ≤ μ) : etvDist μ ν = μ Set.univ - ν Set.univ

theorem MeasureTheory.etvDist_of_le {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] (hμν : μ ≤ ν) : etvDist μ ν = ν Set.univ - μ Set.univ

@[simp]

theorem MeasureTheory.tvDist_nonneg {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} : 0 ≤ tvDist μ ν

theorem MeasureTheory.tvDist_of_not_isFiniteMeasure {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} (h : ¬(IsFiniteMeasure μ ∧ IsFiniteMeasure ν)) : tvDist μ ν = 0

theorem MeasureTheory.tvDist_of_not_isFiniteMeasure_left {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} (h : ¬IsFiniteMeasure μ) : tvDist μ ν = 0

theorem MeasureTheory.tvDist_of_not_isFiniteMeasure_right {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} (h : ¬IsFiniteMeasure ν) : tvDist μ ν = 0

theorem MeasureTheory.ofReal_tvDist {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ ν : Measure 𝓧) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : ENNReal.ofReal (tvDist μ ν) = etvDist μ ν

theorem MeasureTheory.tvDist_eq_iSup_finPartition_abs {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : tvDist μ ν = ⨆ (P : Finpartition ⟨Set.univ, ⋯⟩), ∑ p ∈ P.parts, |μ.real ↑p - ν.real ↑p|

@[simp]

theorem MeasureTheory.tvDist_self {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ : Measure 𝓧) : tvDist μ μ = 0

@[simp]

theorem MeasureTheory.tvDist_eq_zero_iff {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : tvDist μ ν = 0 ↔ μ = ν

theorem MeasureTheory.tvDist_comm {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ ν : Measure 𝓧) : tvDist μ ν = tvDist ν μ

theorem MeasureTheory.tvDist_triangle {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ ν ξ : Measure 𝓧) [IsFiniteMeasure ν] : tvDist μ ξ ≤ tvDist μ ν + tvDist ν ξ

@[simp]

theorem MeasureTheory.tvDist_zero_right {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (μ : Measure 𝓧) : tvDist μ 0 = μ.real Set.univ

@[simp]

theorem MeasureTheory.tvDist_zero_left {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (ν : Measure 𝓧) : tvDist 0 ν = ν.real Set.univ

theorem MeasureTheory.tvDist_restrict_add_compl {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] [IsFiniteMeasure ν] {s : Set 𝓧} (hs : MeasurableSet s) : tvDist (μ.restrict s) (ν.restrict s) + tvDist (μ.restrict sᶜ) (ν.restrict sᶜ) = tvDist μ ν

theorem MeasureTheory.tvDist_of_ge {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] (hμν : ν ≤ μ) : tvDist μ ν = μ.real Set.univ - ν.real Set.univ

theorem MeasureTheory.tvDist_of_le {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure ν] (hμν : μ ≤ ν) : tvDist μ ν = ν.real Set.univ - μ.real Set.univ

theorem MeasureTheory.tvDist_le_add {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} : tvDist μ ν ≤ μ.real Set.univ + ν.real Set.univ