Total Variation Distance

This file defines total variation distance between probability measures and relates it to the usual finite sum formula on finite measurable spaces.

noncomputable def CommunicationComplexity.signedMeasureDiff {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) : MeasureTheory.SignedMeasure Ω

The signed difference between two probability measures.

Equations

• CommunicationComplexity.signedMeasureDiff μ ν = (↑μ).toSignedMeasure - (↑ν).toSignedMeasure

noncomputable def CommunicationComplexity.tvDistance {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) : ℝ

Total variation distance between probability measures, defined using the total variation of the signed measure μ - ν.

Equations

• CommunicationComplexity.tvDistance μ ν = 1 / 2 * (CommunicationComplexity.signedMeasureDiff μ ν).totalVariation.real Set.univ

noncomputable def CommunicationComplexity.tvDistanceSup {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) : ℝ

Total variation distance between probability measures, defined as the supremum over measurable events.

Equations

• CommunicationComplexity.tvDistanceSup μ ν = sSup (Set.range fun (S : { S : Set Ω // MeasurableSet S }) => |(↑μ).real ↑S - (↑ν).real ↑S|)

theorem CommunicationComplexity.TVDistance.tvDistance_eq_tvDistanceSup {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) : tvDistance μ ν = tvDistanceSup μ ν

The total-variation-mass definition agrees with the supremum-over-events definition.

theorem CommunicationComplexity.TVDistance.abs_measureReal_sub_le_tvDistance {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) (S : { S : Set Ω // MeasurableSet S }) : |(↑μ).real ↑S - (↑ν).real ↑S| ≤ tvDistance μ ν

The total variation distance bounds the probability gap of every measurable event.

theorem CommunicationComplexity.TVDistance.tvDistance_nonneg {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) : 0 ≤ tvDistance μ ν

Total variation distance is nonnegative.

theorem CommunicationComplexity.TVDistance.tvDistanceSup_eq_half_sum {Ω : Type u_1} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) : tvDistanceSup μ ν = 1 / 2 * ∑ ω : Ω, |(↑μ).real {ω} - (↑ν).real {ω}|

On a finite measurable space, total variation distance is half the ℓ¹ distance between the singleton masses.

theorem CommunicationComplexity.TVDistance.tvDistance_eq_half_sum {Ω : Type u_1} [MeasurableSpace Ω] [FiniteMeasureSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) : tvDistance μ ν = 1 / 2 * ∑ ω : Ω, |(↑μ).real {ω} - (↑ν).real {ω}|

On a finite measurable space, total variation distance is half the ℓ¹ distance between the singleton masses.

theorem CommunicationComplexity.TVDistance.tvDistance_bool_eq_abs_true (μ ν : MeasureTheory.ProbabilityMeasure Bool) : tvDistance μ ν = |(↑μ).real {true} - (↑ν).real {true}|

On Bool, total variation distance is the absolute singleton-mass gap at true.

noncomputable def CommunicationComplexity.TVDistance.probabilityMeasureProd {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) : MeasureTheory.ProbabilityMeasure (α × β)

Product of two probability measures, bundled as a probability measure.

Equations

• CommunicationComplexity.TVDistance.probabilityMeasureProd μ ν = ⟨(↑μ).prod ↑ν, ⋯⟩

theorem CommunicationComplexity.TVDistance.tvDistance_prod_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [FiniteMeasureSpace α] [FiniteMeasureSpace β] (μ₁ ν₁ : MeasureTheory.ProbabilityMeasure α) (μ₂ ν₂ : MeasureTheory.ProbabilityMeasure β) : tvDistance (probabilityMeasureProd μ₁ μ₂) (probabilityMeasureProd ν₁ ν₂) ≤ tvDistance μ₁ ν₁ + tvDistance μ₂ ν₂

The total variation distance between product distributions is bounded by the sum of the total variation distances between their marginals.