Total Variation Distance for PMFs

This file defines total variation distance on probability mass functions and provides a MetricSpace instance for PMF α.

We follow the Mathlib convention of providing both an ℝ≥0∞-valued version (etvDist) and an ℝ-valued version (tvDist), connected by tvDist = etvDist.toReal.

Main definitions

• PMF.etvDist p q : ℝ≥0∞ — extended TV distance on PMFs
• PMF.tvDist p q : ℝ — TV distance on PMFs
• PMF.instMetricSpace — MetricSpace instance on PMF α via TV distance

Main results

• PMF.tvDist_self, PMF.tvDist_comm, PMF.tvDist_nonneg
• PMF.tvDist_triangle — triangle inequality
• PMF.tvDist_le_one — TV distance is bounded by 1
• PMF.tvDist_eq_zero_iff — TV distance is zero iff the PMFs are equal
• PMF.etvDist_option_punit — closed form for binary distributions
• PMF.etvDist_map_le / PMF.tvDist_map_le — data processing inequality for deterministic maps
• PMF.etvDist_bind_right_le / PMF.tvDist_bind_right_le — data processing inequality for Markov kernels (post-processing)

noncomputable def PMF.etvDist {α : Type u_1} (p q : PMF α) : ENNReal

Extended total variation distance on PMFs, valued in ℝ≥0∞. Defined as (1/2) * ∑' x, |p(x) - q(x)| using ℝ≥0∞-valued absolute difference.

noncomputable def PMF.tvDist {α : Type u_1} (p q : PMF α) : ℝ

Total variation distance on PMFs.

theorem PMF.tvDist_def {α : Type u_1} (p q : PMF α) : p.tvDist q = (p.etvDist q).toReal

@[simp]

theorem PMF.etvDist_self {α : Type u_1} (p : PMF α) : p.etvDist p = 0

theorem PMF.etvDist_comm {α : Type u_1} (p q : PMF α) : p.etvDist q = q.etvDist p

theorem PMF.etvDist_triangle {α : Type u_1} (p q r : PMF α) : p.etvDist r ≤ p.etvDist q + q.etvDist r

theorem PMF.etvDist_le_one {α : Type u_1} (p q : PMF α) : p.etvDist q ≤ 1

theorem PMF.etvDist_ne_top {α : Type u_1} (p q : PMF α) : p.etvDist q ≠ ⊤

@[simp]

theorem PMF.etvDist_eq_zero_iff {α : Type u_1} {p q : PMF α} : p.etvDist q = 0 ↔ p = q

@[simp]

theorem PMF.tvDist_self {α : Type u_1} (p : PMF α) : p.tvDist p = 0

theorem PMF.tvDist_comm {α : Type u_1} (p q : PMF α) : p.tvDist q = q.tvDist p

theorem PMF.tvDist_nonneg {α : Type u_1} (p q : PMF α) : 0 ≤ p.tvDist q

theorem PMF.tvDist_triangle {α : Type u_1} (p q r : PMF α) : p.tvDist r ≤ p.tvDist q + q.tvDist r

theorem PMF.tvDist_le_one {α : Type u_1} (p q : PMF α) : p.tvDist q ≤ 1

@[simp]

theorem PMF.tvDist_eq_zero_iff {α : Type u_1} {p q : PMF α} : p.tvDist q = 0 ↔ p = q

Data processing inequality

theorem PMF.map_apply_eq {α' β : Type u₀} [DecidableEq β] (f : α' → β) (p : PMF α') (y : β) : (f <$> p) y = ∑' (x : α'), if f x = y then p x else 0

theorem PMF.etvDist_map_le {α' β : Type u₀} (f : α' → β) (p q : PMF α') : (f <$> p).etvDist (f <$> q) ≤ p.etvDist q

theorem PMF.tvDist_map_le {α' β : Type u₀} (f : α' → β) (p q : PMF α') : (f <$> p).tvDist (f <$> q) ≤ p.tvDist q

theorem PMF.etvDist_bind_right_le {α' β : Type u₀} (f : α' → PMF β) (p q : PMF α') : (p.bind f).etvDist (q.bind f) ≤ p.etvDist q

theorem PMF.tvDist_bind_right_le {α' β : Type u₀} (f : α' → PMF β) (p q : PMF α') : (p.bind f).tvDist (q.bind f) ≤ p.tvDist q

@[implicit_reducible]

noncomputable instance PMF.instMetricSpace {α : Type u_1} : MetricSpace (PMF α)

@[simp]

theorem PMF.dist_eq_tvDist {α : Type u_1} (p q : PMF α) : dist p q = p.tvDist q

@[simp]

theorem PMF.edist_eq_etvDist {α : Type u_1} (p q : PMF α) : edist p q = p.etvDist q

theorem PMF.pmf_none_eq (p : PMF (Option PUnit.{1})) : p none = 1 - p (some ())

theorem PMF.etvDist_option_punit (p q : PMF (Option PUnit.{1})) : p.etvDist q = (p (some ())).absDiff (q (some ()))

theorem PMF.tvDist_option_punit (p q : PMF (Option PUnit.{1})) : p.tvDist q = |(p (some ())).toReal - (q (some ())).toReal|