Documentation

Complexity.Languages.Probabilistic.Notation

Probability notation for Boolean experiments #

Pr[e] is the probability, as a real number, that the Boolean experiment e returns true. The experiment is either a program e : ProbComp Bool, for which Pr[e] is (ProbComp.eval e true).toReal, or a distribution e : PMF Bool, for which it is (e true).toReal. The notation adds no constant: Pr[e] elaborates to exactly these terms, so every lemma about ENNReal.toReal, PMF and ProbComp.eval applies to it, and the program form is the distribution form at ProbComp.eval e. The elaborator tries ProbComp Bool first, so a do block or a chain of binds is read as a program, and falls back to PMF Bool.

Probabilities are real numbers so that advantages and biases are signed differences, as in |Pr[real] - Pr[ideal]| or Pr[game] - 1 / 2. Nonnegativity is ENNReal.toReal_nonneg.

Events are final returns. The probability that a sample of μ : PMF α lies in a set s is Pr[(fun x => decide (x ∈ s)) <$> μ], and the probability of an outcome a is Pr[(· == a) <$> μ]; these are (μ.toOuterMeasure s).toReal and (μ a).toReal. A Boolean game, a set event and a single outcome therefore share one form.

The notation is scoped: open Cslib.Probability enables it, as does open Probability inside the namespace Cslib. It then also prints both forms back as Pr[e].

Main definitions #

Main results #

source
def Cslib.Probability.probabilityTrue :
Lean.ParserDescr

Pr[e] is the probability, as a real number, that the Boolean experiment e returns true: (ProbComp.eval e true).toReal for a program e : ProbComp Bool, and (e true).toReal for a distribution e : PMF Bool.

Instances For
    source
    def Cslib.Probability.elabProbabilityTrue :
    Lean.Elab.Term.TermElab

    Elaborate Pr[e] as (ProbComp.eval e true).toReal, with e elaborated as a ProbComp Bool; if that fails, as (e true).toReal with e : PMF Bool.

    Instances For
      source
      def Cslib.Probability.delabProbabilityTrue :
      Lean.PrettyPrinter.Delaborator.Delab

      Print (ProbComp.eval e true).toReal as Pr[e], and (μ true).toReal for μ : PMF Bool as Pr[μ]. Unlike an unexpander, it checks that the argument is a PMF Bool.

      Instances For
        source
        theorem Cslib.Probability.PMF.toReal_apply_le_one {α : Type u_1} (μ : PMF α) (a : α) :
        (μ a).toReal ≤ 1

        A probability is at most one; in particular Pr[e] ≤ 1 for every Boolean experiment.

        source
        theorem Cslib.Probability.PMF.probability_map_decide_mem {α : Type} (μ : PMF α) (s : Set α) [DecidablePred fun (x : α) => x ∈ s] :
        (((fun (x : α) => decide (x ∈ s)) <$> μ) true).toReal = (μ.toOuterMeasure s).toReal

        The probability that a sample lies in a set is the probability that testing membership returns true.

        source
        theorem Cslib.Probability.PMF.probability_map_beq {α : Type} [BEq α] [LawfulBEq α] (μ : PMF α) (a : α) :
        (((fun (x : α) => x == a) <$> μ) true).toReal = (μ a).toReal

        The probability of an outcome is the probability that comparing with it returns true.

        source
        theorem Cslib.ProbComp.probability_pure (b : Bool) :
        ((pure b).eval true).toReal = if b = true then 1 else 0

        A program that returns b succeeds with probability one if b is true and zero otherwise.

        source
        theorem Cslib.ProbComp.probability_bind {α : Type} [Fintype α] (source : ProbComp α) (next : α → ProbComp Bool) :
        ((source >>= next).eval true).toReal = ∑ a : α, (source.eval a).toReal * ((next a).eval true).toReal

        After a finite random choice, the probability of success is the average of the probabilities of success of the continuations.

        source
        theorem Cslib.ProbComp.probability_map_decide_mem {α : Type} (program : ProbComp α) (s : Set α) [DecidablePred fun (x : α) => x ∈ s] :
        (((fun (x : α) => decide (x ∈ s)) <$> program).eval true).toReal = (program.eval.toOuterMeasure s).toReal

        The probability that a program's output lies in a set is the probability that testing membership returns true.

        source
        theorem Cslib.ProbComp.probability_map_beq {α : Type} [BEq α] [LawfulBEq α] (program : ProbComp α) (a : α) :
        (((fun (x : α) => x == a) <$> program).eval true).toReal = (program.eval a).toReal

        The probability of an output is the probability that comparing with it returns true.