Total variation distance

Main definitions

• FooBar

Main statements

• fooBar_unique

Notation

Implementation details

References

• [F. Bar, Quuxes][bibkey]

Tags

Foobars, barfoos

noncomputable def ProbabilityTheory.tv {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) : ℝ

Total variation distance between two measures.

Equations

• ProbabilityTheory.tv μ ν = (ProbabilityTheory.statInfo μ ν (Bool.boolMeasure 1 1)).toReal

instance ProbabilityTheory.instIsFiniteMeasureBoolBoolMeasureOfNatENNReal : MeasureTheory.IsFiniteMeasure (Bool.boolMeasure 1 1)

Equations

• ProbabilityTheory.instIsFiniteMeasureBoolBoolMeasureOfNatENNReal = ⋯

@[simp]

theorem ProbabilityTheory.tv_zero_left {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {ν : MeasureTheory.Measure 𝒳} : ProbabilityTheory.tv 0 ν = 0

@[simp]

theorem ProbabilityTheory.tv_zero_right {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} : ProbabilityTheory.tv μ 0 = 0

@[simp]

theorem ProbabilityTheory.tv_self {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} : ProbabilityTheory.tv μ μ = 0

theorem ProbabilityTheory.tv_nonneg {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} : 0 ≤ ProbabilityTheory.tv μ ν

theorem ProbabilityTheory.tv_le {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.tv μ ν ≤ min (μ Set.univ).toReal (ν Set.univ).toReal

theorem ProbabilityTheory.tv_comp_le {𝒳 : Type u_1} {𝒳' : Type u_2} {m𝒳 : MeasurableSpace 𝒳} {m𝒳' : MeasurableSpace 𝒳'} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel 𝒳 𝒳') [ProbabilityTheory.IsMarkovKernel κ] : ProbabilityTheory.tv (μ.bind ⇑κ) (ν.bind ⇑κ) ≤ ProbabilityTheory.tv μ ν

Data processing inequality for the total variation.