Documentation

VCVio.EvalDist.TVDist

Total Variation Distance for SPMFs and Monadic Computations #

This file extends the TV distance from PMF (defined in ToMathlib.Probability.ProbabilityMassFunction.TotalVariation) to:

  1. SPMF.tvDist — on sub-probability mass functions (via toPMF)
  2. tvDist — on any monad with MonadLiftT m SPMF (via evalDist)

SPMF.tvDist #

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

Total variation distance on SPMFs, defined via the underlying PMF (Option α).

Instances For
    source
    @[simp]
    theorem SPMF.tvDist_self {α : Type u_1} (p : SPMF α) :
    p.tvDist p = 0
    source
    theorem SPMF.tvDist_comm {α : Type u_1} (p q : SPMF α) :
    p.tvDist q = q.tvDist p
    source
    theorem SPMF.tvDist_nonneg {α : Type u_1} (p q : SPMF α) :
    0 ≤ p.tvDist q
    source
    theorem SPMF.tvDist_triangle {α : Type u_1} (p q r : SPMF α) :
    p.tvDist r ≤ p.tvDist q + q.tvDist r
    source
    theorem SPMF.tvDist_le_one {α : Type u_1} (p q : SPMF α) :
    p.tvDist q ≤ 1
    source
    @[simp]
    theorem SPMF.tvDist_eq_zero_iff {α : Type u_1} {p q : SPMF α} :
    p.tvDist q = 0 ↔ p.toPMF = q.toPMF
    source
    theorem SPMF.tvDist_map_le {α' β : Type w} (f : α' → β) (p q : SPMF α') :
    (f <$> p).tvDist (f <$> q) ≤ p.tvDist q
    source
    theorem SPMF.tvDist_bind_right_le {α' β : Type w} (f : α' → SPMF β) (p q : SPMF α') :
    (p >>= f).tvDist (q >>= f) ≤ p.tvDist q

    Monadic tvDist #

    source
    noncomputable def tvDist {m : Type u → Type v} [MonadLiftT m SPMF] {α : Type u} (mx my : m α) :
    ℝ

    Total variation distance between two monadic computations, defined via their evaluation distributions.

    Instances For
      source
      @[simp]
      theorem tvDist_self {m : Type u → Type v} [MonadLiftT m SPMF] {α : Type u} (mx : m α) :
      tvDist mx mx = 0
      source
      @[simp]
      theorem tvDist_eq_zero_iff {m : Type u → Type v} [MonadLiftT m SPMF] {α : Type u} (mx my : m α) :
      tvDist mx my = 0 ↔ 𝒟[mx] = 𝒟[my]
      source
      theorem tvDist_comm {m : Type u → Type v} [MonadLiftT m SPMF] {α : Type u} (mx my : m α) :
      tvDist mx my = tvDist my mx
      source
      theorem tvDist_nonneg {m : Type u → Type v} [MonadLiftT m SPMF] {α : Type u} (mx my : m α) :
      0 ≤ tvDist mx my
      source
      theorem tvDist_triangle {m : Type u → Type v} [MonadLiftT m SPMF] {α : Type u} (mx my mz : m α) :
      tvDist mx mz ≤ tvDist mx my + tvDist my mz
      source
      theorem tvDist_le_one {m : Type u → Type v} [MonadLiftT m SPMF] {α : Type u} (mx my : m α) :
      tvDist mx my ≤ 1
      source
      theorem tvDist_map_le {m : Type u → Type v} [Monad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α : Type u} [LawfulMonad m] {β : Type u} (f : α → β) (mx my : m α) :
      tvDist (f <$> mx) (f <$> my) ≤ tvDist mx my
      source
      theorem tvDist_bind_right_le {m : Type u → Type v} [Monad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α : Type u} [LawfulMonad m] {β : Type u} (f : α → m β) (mx my : m α) :
      tvDist (mx >>= f) (my >>= f) ≤ tvDist mx my

      TV distance bounds #

      source
      theorem tvDist_le_probEvent_of_probOutput_eq_of_not {m : Type u → Type v} [Monad m] [MonadLiftT m SPMF] {α : Type u} {mx my : m α} [NeverFail mx] [NeverFail my] (p : α → Prop) (h_eq : ∀ (x : α), ¬p x → Pr[= x | mx] = Pr[= x | my]) (h_event_eq : probEvent mx p = probEvent my p) :
      tvDist mx my ≤ (probEvent mx p).toReal

      Total variation distance is bounded by the probability of an event p whenever the two computations have equal output distribution off p (and equal probability of p).

      TV distance for bind (left) #

      source
      theorem tvDist_bind_left_le {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] {α β : Type u} (mx : m α) (f g : α → m β) :
      tvDist (mx >>= f) (mx >>= g) ≤ ∑' (a : α), Pr[= a | mx].toReal * tvDist (f a) (g a)

      TV distance for bind with a constant bound #

      source
      theorem tvDist_bind_left_le_const {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] [MonadLiftT m SetM] [EvalDistCompatible m] {α β : Type u} (mx : m α) (f g : α → m β) (c : ℝ) (hfg : ∀ a ∈ support mx, tvDist (f a) (g a) ≤ c) :
      tvDist (mx >>= f) (mx >>= g) ≤ c

      Total-variation distance is convex over a shared bind: if tvDist (f a) (g a) ≤ c for every a ∈ support mx, then tvDist (mx >>= f) (mx >>= g) ≤ c. The real-valued root of the const bound, with ℝ≥0∞ companion ofReal_tvDist_bind_left_le_const.

      source
      theorem tvDist_bind_left_le_const' {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] [MonadLiftT m SetM] [EvalDistCompatible m] {α β : Type u} (mx : m α) (f g : α → m β) (c : ℝ) (hfg : ∀ (a : α), tvDist (f a) (g a) ≤ c) :
      tvDist (mx >>= f) (mx >>= g) ≤ c

      Unrestricted companion of tvDist_bind_left_le_const: a uniform per-a bound tvDist (f a) (g a) ≤ c lifts through the shared mx bind.

      source
      theorem ofReal_tvDist_bind_left_le_const {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] [MonadLiftT m SetM] [EvalDistCompatible m] {α β : Type u} (mx : m α) (f g : α → m β) (ε : ENNReal) (hfg : ∀ a ∈ support mx, ENNReal.ofReal (tvDist (f a) (g a)) ≤ ε) :
      ENNReal.ofReal (tvDist (mx >>= f) (mx >>= g)) ≤ ε

      ℝ≥0∞ form of tvDist_bind_left_le_const, matching the quantitative APIs: a per-a bound ENNReal.ofReal (tvDist (f a) (g a)) ≤ ε on the support of mx lifts through the shared bind.

      source
      theorem ofReal_tvDist_bind_left_le_const' {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] [MonadLiftT m SetM] [EvalDistCompatible m] {α β : Type u} (mx : m α) (f g : α → m β) (ε : ENNReal) (hfg : ∀ (a : α), ENNReal.ofReal (tvDist (f a) (g a)) ≤ ε) :
      ENNReal.ofReal (tvDist (mx >>= f) (mx >>= g)) ≤ ε

      Unrestricted companion of ofReal_tvDist_bind_left_le_const.

      TV distance for bind with a bad event #

      source
      theorem tsum_probOutput_toReal_mul_tvDist_le_probEvent {m : Type u → Type v} [Monad m] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] {α β : Type u} (mx : m α) (f g : α → m β) (bad : α → Prop) (h_eq : ∀ (a : α), ¬bad a → 𝒟[f a] = 𝒟[g a]) :
      ∑' (a : α), Pr[= a | mx].toReal * tvDist (f a) (g a) ≤ (probEvent mx bad).toReal

      Bound the weighted TV sum from tvDist_bind_left_le by the probability of a bad event when the two continuations are distributionally equal off that event.

      source
      theorem tvDist_bind_left_event_le {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] {α β : Type u} (mx : m α) (f g : α → m β) (bad : α → Prop) (h_eq : ∀ (a : α), ¬bad a → 𝒟[f a] = 𝒟[g a]) :
      tvDist (mx >>= f) (mx >>= g) ≤ (probEvent mx bad).toReal

      If two continuations are equal off a bad event, binding them over the same base computation changes TV distance by at most the probability of that bad event.

      source
      theorem ofReal_tvDist_bind_left_event_le {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] {α β : Type u} (mx : m α) (f g : α → m β) (bad : α → Prop) (h_eq : ∀ (a : α), ¬bad a → 𝒟[f a] = 𝒟[g a]) :
      ENNReal.ofReal (tvDist (mx >>= f) (mx >>= g)) ≤ probEvent mx bad

      ENNReal form of tvDist_bind_left_event_le, matching the quantitative identical-until-bad APIs.

      source
      theorem tvDist_bind_event_le {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] {α β : Type u} (mx my : m α) (f g : α → m β) (bad : α → Prop) (h_eq : ∀ (a : α), ¬bad a → 𝒟[f a] = 𝒟[g a]) :
      tvDist (mx >>= f) (my >>= g) ≤ (probEvent mx bad).toReal + tvDist mx my

      Bind/event TV bound with different base computations: the base TV distance plus the bad-event probability controls the whole bind.

      source
      theorem ofReal_tvDist_bind_event_le {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] {α β : Type u} (mx my : m α) (f g : α → m β) (bad : α → Prop) (h_eq : ∀ (a : α), ¬bad a → 𝒟[f a] = 𝒟[g a]) :
      ENNReal.ofReal (tvDist (mx >>= f) (my >>= g)) ≤ probEvent mx bad + ENNReal.ofReal (tvDist mx my)

      ENNReal form of tvDist_bind_event_le.

      source
      theorem tvDist_bind_event_right_le {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] {α β : Type u} (mx my : m α) (f g : α → m β) (bad : α → Prop) (h_eq : ∀ (a : α), ¬bad a → 𝒟[f a] = 𝒟[g a]) :
      tvDist (mx >>= f) (my >>= g) ≤ tvDist mx my + (probEvent my bad).toReal

      Bind/event TV bound with different base computations, charging the bad-event probability under the right base computation. This is the symmetric orientation of tvDist_bind_event_le, useful when the bad event is introduced by the simulated side.

      source
      theorem ofReal_tvDist_bind_event_right_le {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] {α β : Type u} (mx my : m α) (f g : α → m β) (bad : α → Prop) (h_eq : ∀ (a : α), ¬bad a → 𝒟[f a] = 𝒟[g a]) :
      ENNReal.ofReal (tvDist (mx >>= f) (my >>= g)) ≤ ENNReal.ofReal (tvDist mx my) + probEvent my bad

      ENNReal form of tvDist_bind_event_right_le.

      source
      theorem abs_probOutput_toReal_sub_le_tvDist {m : Type → Type v} [MonadLiftT m SPMF] (game₁ game₂ : m Bool) :
      |Pr[= true | game₁].toReal - Pr[= true | game₂].toReal| ≤ tvDist game₁ game₂

      For any Bool computation, the difference of Pr[= true] values is bounded by TV distance.