Documentation

VCVio.EvalDist.RenyiDivergence

Rényi Divergence for SPMFs and Monadic Computations #

This file extends the Rényi divergence from PMF (defined in ToMathlib.Probability.ProbabilityMassFunction.RenyiDivergence) to:

  1. SPMF.renyiDiv — on sub-probability mass functions (via toPMF)
  2. renyiDiv — on any monad with HasEvalSPMF (via evalDist)

This mirrors the structure of VCVio.EvalDist.TVDist, which performs the same lift for total variation distance.

Application #

The monadic renyiDiv is used to state sampler quality bounds:

renyiDiv a (concreteSamplerZ μ σ') (idealSamplerZ μ σ') ≤ 1 + ε

where concreteSamplerZ uses FPR arithmetic and idealSamplerZ samples from the exact discrete Gaussian. The probability preservation theorem then translates this into a security loss factor in the Falcon EUF-CMA proof.

SPMF.renyiDiv #

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

Rényi MGF on SPMFs, defined via the underlying PMF (Option α).

Instances For
    source
    noncomputable def SPMF.renyiDiv {α : Type u_1} (a : ℝ) (p q : SPMF α) :
    ENNReal

    Multiplicative Rényi divergence on SPMFs, defined via the underlying PMF (Option α).

    Instances For
      source
      noncomputable def SPMF.maxDiv {α : Type u_1} (p q : SPMF α) :
      ENNReal

      Max-divergence on SPMFs.

      Instances For
        source
        @[simp]
        theorem SPMF.renyiDiv_self {α : Type u_1} (a : ℝ) (p : SPMF α) :
        SPMF.renyiDiv a p p = 1
        source
        theorem SPMF.renyiDiv_map_le (a : ℝ) (ha : 1 < a) {α' β : Type w} (f : α' → β) (p q : SPMF α') :
        SPMF.renyiDiv a (f <$> p) (f <$> q) ≤ SPMF.renyiDiv a p q
        source
        theorem SPMF.renyiDiv_bind_right_le (a : ℝ) (ha : 1 < a) {α' β : Type w} (f : α' → SPMF β) (p q : SPMF α') :
        SPMF.renyiDiv a (p >>= f) (q >>= f) ≤ SPMF.renyiDiv a p q

        Monadic renyiDiv #

        source
        noncomputable def renyiDiv {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {α : Type u} (a : ℝ) (mx my : m α) :
        ENNReal

        Rényi divergence between two monadic computations, defined via their evaluation distributions.

        Instances For
          source
          @[simp]
          theorem renyiDiv_self {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {α : Type u} (a : ℝ) (mx : m α) :
          renyiDiv a mx mx = 1
          source
          theorem renyiDiv_map_le {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {α : Type u} [LawfulMonad m] {β : Type u} (a : ℝ) (ha : 1 < a) (f : α → β) (mx my : m α) :
          renyiDiv a (f <$> mx) (f <$> my) ≤ renyiDiv a mx my
          source
          theorem renyiDiv_bind_right_le {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {α : Type u} [LawfulMonad m] {β : Type u} (a : ℝ) (ha : 1 < a) (f : α → m β) (mx my : m α) :
          renyiDiv a (mx >>= f) (my >>= f) ≤ renyiDiv a mx my

          Rényi to Probability Bounds #

          source
          theorem probOutput_le_of_renyiDiv {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {α : Type u} (a : ℝ) (ha : 1 < a) (mx my : m α) (R : ENNReal) (hR : renyiDiv a mx my ≤ R) (x : α) :
          Pr[= x | mx] ^ (a / (a - 1)) / R ≤ Pr[= x | my]

          If the Rényi divergence between two computations is at most R, then for any output x, Pr[= x | my] ≥ Pr[= x | mx]^{a/(a-1)} / R.