Total variation distance of vector measures

We define the total variation distance between two vector measures μ, ν as (μ - ν).variation Set.univ.

Main definitions

• VectorMeasure.etvDist μ ν: total variation distance between two vector measures, defined as the value on the universal set of the variation of μ - ν.

Main statements

• etvDist_self, etvDist_eq_zero_iff, etvDist_comm, etvDist_triangle: the total variation distance between vector measures is a distance.

noncomputable def MeasureTheory.VectorMeasure.etvDist {𝓧 : Type u_1} {M : Type u_2} {m𝓧 : MeasurableSpace 𝓧} [NormedAddCommGroup M] (μ ν : VectorMeasure 𝓧 M) : ENNReal

Total variation distance between two vector measures, with value in ℝ≥0∞.

Equations

• μ.etvDist ν = (μ - ν).variation Set.univ

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

@[simp]

theorem MeasureTheory.VectorMeasure.etvDist_self {𝓧 : Type u_1} {M : Type u_2} {m𝓧 : MeasurableSpace 𝓧} [NormedAddCommGroup M] (μ : VectorMeasure 𝓧 M) : μ.etvDist μ = 0

@[simp]

theorem MeasureTheory.VectorMeasure.etvDist_eq_zero_iff {𝓧 : Type u_1} {M : Type u_2} {m𝓧 : MeasurableSpace 𝓧} [NormedAddCommGroup M] (μ ν : VectorMeasure 𝓧 M) : μ.etvDist ν = 0 ↔ μ = ν

theorem MeasureTheory.VectorMeasure.etvDist_comm {𝓧 : Type u_1} {M : Type u_2} {m𝓧 : MeasurableSpace 𝓧} [NormedAddCommGroup M] (μ ν : VectorMeasure 𝓧 M) : μ.etvDist ν = ν.etvDist μ

theorem MeasureTheory.VectorMeasure.etvDist_triangle {𝓧 : Type u_1} {M : Type u_2} {m𝓧 : MeasurableSpace 𝓧} [NormedAddCommGroup M] (μ ν ξ : VectorMeasure 𝓧 M) : μ.etvDist ξ ≤ μ.etvDist ν + ν.etvDist ξ

@[simp]

theorem MeasureTheory.VectorMeasure.etvDist_zero_right {𝓧 : Type u_1} {M : Type u_2} {m𝓧 : MeasurableSpace 𝓧} [NormedAddCommGroup M] (μ : VectorMeasure 𝓧 M) : μ.etvDist 0 = μ.variation Set.univ

@[simp]

theorem MeasureTheory.VectorMeasure.etvDist_zero_left {𝓧 : Type u_1} {M : Type u_2} {m𝓧 : MeasurableSpace 𝓧} [NormedAddCommGroup M] (ν : VectorMeasure 𝓧 M) : etvDist 0 ν = ν.variation Set.univ

theorem MeasureTheory.VectorMeasure.etvDist_eq_etvDist_sub_zero {𝓧 : Type u_1} {M : Type u_2} {m𝓧 : MeasurableSpace 𝓧} [NormedAddCommGroup M] {μ ν : VectorMeasure 𝓧 M} : μ.etvDist ν = (μ - ν).etvDist 0

theorem MeasureTheory.VectorMeasure.etvDist_restrict_add_compl {𝓧 : Type u_1} {M : Type u_2} {m𝓧 : MeasurableSpace 𝓧} [NormedAddCommGroup M] {μ ν : VectorMeasure 𝓧 M} {s : Set 𝓧} (hs : MeasurableSet s) : (μ.restrict s).etvDist (ν.restrict s) + (μ.restrict sᶜ).etvDist (ν.restrict sᶜ) = μ.etvDist ν