Total variation distance

DefinitionTotal variation distance between finite measures#✓fully proved

For finite measures \(\mu\) and \(\nu\) on a measurable space \(\Omega\), the total variation distance \(d_{TV}(\mu, \nu)\) is the real number \(\sup_B |\mu(B) - \nu(B)|\), where the supremum runs over all measurable sets \(B \subseteq \Omega\) and the masses \(\mu(B)\) and \(\nu(B)\) are taken as real numbers.

noncomputable def totalVariationDist {Ω : Type*} [MeasurableSpace Ω]
    (μ ν : Measure Ω) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : ℝ :=
  ⨆ s : {s : Set Ω // MeasurableSet s}, |(μ s.1).toReal - (ν s.1).toReal|

Sources

• the probability-measure specialization is the Lecture 12 definition. The inline finiteness binders are part of this public interface.

Used by 7

Used bySymmetry of total variation distance · Total variation distance between Dirac measures · Total variation distance vanishes only for equal measures · Total variation distance between probability measures is at most one · Total variation distance is nonnegative · Total variation distance from a measure to itself · Triangle inequality for total variation distance

TheoremTotal variation distance is nonnegative#✓fully proved

For finite measures \(\mu\) and \(\nu\) on a measurable space, the total variation distance satisfies \(0 \le d_{TV}(\mu, \nu)\).

theorem totalVariationDist_nonneg [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    0 ≤ totalVariationDist μ ν

Uses 1 · Used by 1

Statement usesTotal variation distance between finite measures

Used byTotal variation distance from a measure to itself

TheoremTotal variation distance from a measure to itself#✓fully proved

For every finite measure \(\mu\) on a measurable space, the total variation distance \(d_{TV}(\mu, \mu)\) is \(0\).

theorem totalVariationDist_self [IsFiniteMeasure μ] :
    totalVariationDist μ μ = 0

Uses 2 · Used by 2

Statement usesTotal variation distance between finite measures

Proof usesTotal variation distance is nonnegative

Used byTotal variation distance between Dirac measures · Total variation distance vanishes only for equal measures

TheoremSymmetry of total variation distance#✓fully proved

For finite measures \(\mu\) and \(\nu\) on a measurable space, the total variation distances satisfy \(d_{TV}(\mu, \nu) = d_{TV}(\nu, \mu)\).

theorem totalVariationDist_comm [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    totalVariationDist μ ν = totalVariationDist ν μ

Uses 1

Statement usesTotal variation distance between finite measures

TheoremTriangle inequality for total variation distance#✓fully proved

For finite measures \(\mu\), \(\nu\) and \(\rho\) on a measurable space, the total variation distance satisfies \(d_{TV}(\mu, \rho) \le d_{TV}(\mu, \nu) + d_{TV}(\nu, \rho)\).

theorem totalVariationDist_triangle [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    [IsFiniteMeasure ρ] :
    totalVariationDist μ ρ ≤ totalVariationDist μ ν + totalVariationDist ν ρ

Uses 1

Statement usesTotal variation distance between finite measures

TheoremTotal variation distance between probability measures is at most one#✓fully proved

For probability measures \(\mu\) and \(\nu\) on a measurable space, the total variation distance satisfies \(d_{TV}(\mu, \nu) \le 1\).

theorem totalVariationDist_le_one [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
    totalVariationDist μ ν ≤ 1

Uses 1 · Used by 1

Statement usesTotal variation distance between finite measures

Used byTotal variation distance between Dirac measures

TheoremTotal variation distance vanishes only for equal measures#✓fully proved

For finite measures \(\mu\) and \(\nu\) on a measurable space, the total variation distance \(d_{TV}(\mu, \nu)\) is \(0\) if and only if \(\mu = \nu\).

theorem totalVariationDist_eq_zero_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    totalVariationDist μ ν = 0 ↔ μ = ν

Uses 2

Statement usesTotal variation distance between finite measures

Proof usesTotal variation distance from a measure to itself

TheoremTotal variation distance between Dirac measures#✓fully proved

Let \(\Omega\) be a measurable space in which every singleton is measurable, and let \(a, b \in \Omega\). The total variation distance between the Dirac measures \(\delta_a\) and \(\delta_b\) is \(0\) if \(a = b\) and \(1\) if \(a \neq b\).

theorem totalVariationDist_dirac [MeasurableSingletonClass Ω] [DecidableEq Ω] {a b : Ω} :
    totalVariationDist (Measure.dirac a) (Measure.dirac b) =
      if a = b then 0 else 1

Uses 3

Statement usesTotal variation distance between finite measures

Proof usesTotal variation distance between probability measures is at most one · Total variation distance from a measure to itself

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.