Documentation

Cslib.Probability.StatisticalDistance

Statistical Distance of Finite Probability Mass Functions #

For PMFs p and q on a finite type, their statistical distance is

(1 / 2) * ∑ a, |p a - q a|.

This is [BS23], Definition 3.5. The probabilities are converted from ℝ≥0∞, Mathlib's codomain for a PMF, to ℝ before taking the finite sum.

Statistical distance is packaged as a scoped MetricSpace instance on PMF α, so it is spelled dist p q and the general metric API applies: dist_nonneg, dist_self, dist_comm, dist_triangle, dist_eq_zero, and so on. Open Cslib.Probability.PMF (or open scoped Cslib.Probability.PMF) to activate the instance; it is scoped so that this library does not install a global metric on Mathlib's PMF type.

Besides the metric structure, this file proves that applying the same transformation — deterministic or randomized — to two PMFs cannot increase their statistical distance; [BS23], Theorem 3.13 is the deterministic case.

Main definitions #

Main results #

References #

source
@[instance_reducible]
noncomputable def Cslib.Probability.PMF.instMetricSpace {α : Type u} [Fintype α] :
MetricSpace (PMF α)

Statistical distance makes the PMFs on a finite type a metric space ([BS23], Definition 3.5).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Cslib.Probability.PMF.dist_eq {α : Type u} [Fintype α] (p q : PMF α) :
    dist p q = (∑ a : α, |(p a).toReal - (q a).toReal|) / 2

    The distance between two PMFs on a finite type is their statistical distance ([BS23], Definition 3.5).

    source
    theorem Cslib.Probability.PMF.dist_le_one {α : Type u} [Fintype α] (p q : PMF α) :
    dist p q ≤ 1

    Statistical distance is at most one.

    source
    theorem Cslib.Probability.PMF.dist_eq_one_of_disjoint_support {α : Type u} [Fintype α] {p q : PMF α} (h : Disjoint p.support q.support) :
    dist p q = 1

    PMFs with disjoint supports are at the maximum statistical distance.

    source
    theorem Cslib.Probability.PMF.dist_bind_le {α : Type u} {β : Type v} [Fintype α] [Fintype β] (p q : PMF α) (kernel : α → PMF β) :
    dist (p.bind kernel) (q.bind kernel) ≤ dist p q

    Applying the same randomized kernel to two PMFs cannot increase their statistical distance.

    source
    theorem Cslib.Probability.PMF.dist_map_le {α : Type u} {β : Type v} [Fintype α] [Fintype β] (p q : PMF α) (f : α → β) :
    dist (PMF.map f p) (PMF.map f q) ≤ dist p q

    Deterministic postprocessing cannot increase statistical distance ([BS23], Theorem 3.13).

    source
    def Cslib.Probability.PMF.StatisticallyClose {α : Type u} [Fintype α] (p q : PMF α) (ε : NNReal) :
    Prop

    Two PMFs are ε-statistically close when their statistical distance is at most ε. The ℝ≥0 parameter rules out meaningless negative bounds.

    Equations
    Instances For
      source
      theorem Cslib.Probability.PMF.StatisticallyClose.refl {α : Type u} [Fintype α] (p : PMF α) :
      StatisticallyClose p p 0

      Every PMF is statistically close to itself with zero error.

      source
      theorem Cslib.Probability.PMF.StatisticallyClose.symm {α : Type u} [Fintype α] {p q : PMF α} {ε : NNReal} (h : StatisticallyClose p q ε) :
      StatisticallyClose q p ε

      Statistical closeness is symmetric.

      source
      theorem Cslib.Probability.PMF.StatisticallyClose.mono {α : Type u} [Fintype α] {p q : PMF α} :
      Monotone (StatisticallyClose p q)

      A statistical-closeness bound remains valid when its error is enlarged.

      source
      theorem Cslib.Probability.PMF.StatisticallyClose.trans {α : Type u} [Fintype α] {p q r : PMF α} {ε δ : NNReal} (hpq : StatisticallyClose p q ε) (hqr : StatisticallyClose q r δ) :
      StatisticallyClose p r (ε + δ)

      Closeness bounds chain through an intermediate distribution, adding the errors.

      source
      theorem Cslib.Probability.PMF.StatisticallyClose.bind {α : Type u} {β : Type v} [Fintype α] [Fintype β] {p q : PMF α} {ε : NNReal} (h : StatisticallyClose p q ε) (kernel : α → PMF β) :
      StatisticallyClose (p.bind kernel) (q.bind kernel) ε

      A shared randomized postprocessing kernel preserves statistical closeness.

      source
      theorem Cslib.Probability.PMF.StatisticallyClose.map {α : Type u} {β : Type v} [Fintype α] [Fintype β] {p q : PMF α} {ε : NNReal} (h : StatisticallyClose p q ε) (f : α → β) :
      StatisticallyClose (PMF.map f p) (PMF.map f q) ε

      Deterministic postprocessing preserves statistical closeness.

      source
      @[simp]
      theorem Cslib.Probability.PMF.statisticallyClose_zero_iff {α : Type u} [Fintype α] (p q : PMF α) :
      StatisticallyClose p q 0 ↔ p = q

      Statistical closeness with zero error is equality.