Properties of the total variation distance

We prove properties of the total variation distance, in particular alternative formulas for it.

Main statements

• tvDist_eq_integral_abs_rnDeriv_add_singularPart: the total variation distance satisfies the formula tvDist μ ν = ∫ x, |1 - (μ.rnDeriv ν x).toReal| ∂ν + (μ.singularPart ν).real Set.univ.

theorem MeasureTheory.etvDist_of_mutuallySingular {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} (hμν : μ.MutuallySingular ν) : etvDist μ ν = μ Set.univ + ν Set.univ

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

theorem MeasureTheory.IsHahnDecomposition.etvDist_eq {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] [IsFiniteMeasure ν] {s : Set 𝓧} (h : IsHahnDecomposition μ ν s) : etvDist μ ν = ν s - μ s + (μ sᶜ - ν sᶜ)

theorem MeasureTheory.IsHahnDecomposition.tvDist_eq {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] [IsFiniteMeasure ν] {s : Set 𝓧} (h : IsHahnDecomposition μ ν s) : tvDist μ ν = ν.real s - μ.real s + (μ.real sᶜ - ν.real sᶜ)

theorem MeasureTheory.tvDist_withDensity_self_eq_integral {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : Measure 𝓧} [IsFiniteMeasure μ] {f : 𝓧 → ENNReal} (hf : Integrable f μ) : tvDist (μ.withDensity f) μ = ∫ (x : 𝓧), |1 - (f x).toReal| ∂μ

theorem MeasureTheory.etvDist_withDensity_self_eq_lintegral {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : Measure 𝓧} [IsFiniteMeasure μ] {f : 𝓧 → ENNReal} (hf : Integrable f μ) : etvDist (μ.withDensity f) μ = ∫⁻ (x : 𝓧), ‖1 - (f x).toReal‖ₑ ∂μ

theorem MeasureTheory.tvDist_eq_integral_abs_rnDeriv_of_ac {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) : tvDist μ ν = ∫ (x : 𝓧), |1 - (μ.rnDeriv ν x).toReal| ∂ν

theorem MeasureTheory.etvDist_eq_lintegral_enorm_rnDeriv_of_ac {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) : etvDist μ ν = ∫⁻ (x : 𝓧), ‖1 - (μ.rnDeriv ν x).toReal‖ₑ ∂ν

theorem MeasureTheory.tvDist_add_of_ac_of_mutuallySingular {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] [IsFiniteMeasure ν] {μ' : Measure 𝓧} [IsFiniteMeasure μ'] (hμν : μ.AbsolutelyContinuous ν) (hμ'ν : μ'.MutuallySingular ν) : tvDist (μ + μ') ν = tvDist μ ν + μ'.real Set.univ

theorem MeasureTheory.etvDist_add_of_ac_of_mutuallySingular {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] [IsFiniteMeasure ν] {μ' : Measure 𝓧} [IsFiniteMeasure μ'] (hμν : μ.AbsolutelyContinuous ν) (hμ'ν : μ'.MutuallySingular ν) : etvDist (μ + μ') ν = etvDist μ ν + μ' Set.univ

theorem MeasureTheory.tvDist_eq_integral_abs_rnDeriv_add_singularPart {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : tvDist μ ν = ∫ (x : 𝓧), |1 - (μ.rnDeriv ν x).toReal| ∂ν + (μ.singularPart ν).real Set.univ

theorem MeasureTheory.etvDist_eq_lintegral_enorm_rnDeriv_add_singularPart {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : etvDist μ ν = ∫⁻ (x : 𝓧), ‖1 - (μ.rnDeriv ν x).toReal‖ₑ ∂ν + (μ.singularPart ν) Set.univ