Documentation

VCVio.EvalDist.Bool

Evaluation Distributions on Boolean-Valued Computations #

Specialization lemmas for HasEvalSPMF computations returning Bool.

source
@[simp]
theorem probOutput_true_add_false {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] (mx : m Bool) :
Pr[=true | mx] + Pr[=false | mx] = 1 - Pr[⊥ | mx]
source
@[simp]
theorem probOutput_false_add_true {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] (mx : m Bool) :
Pr[=false | mx] + Pr[=true | mx] = 1 - Pr[⊥ | mx]
source
theorem probOutput_true_eq_sub {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] (mx : m Bool) :
Pr[=true | mx] = 1 - Pr[⊥ | mx] - Pr[=false | mx]
source
theorem probOutput_false_eq_sub {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] (mx : m Bool) :
Pr[=false | mx] = 1 - Pr[⊥ | mx] - Pr[=true | mx]
source
@[simp]
theorem probOutput_not_map {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m Bool) :
Pr[=true | (fun (x : Bool) => !x) <$> mx] = Pr[=false | mx]
source
@[simp]
theorem probOutput_not_map' {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m Bool) :
Pr[=false | (fun (x : Bool) => !x) <$> mx] = Pr[=true | mx]
source
@[simp]
theorem probOutput_true_add_false_of_neverFail {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] {mx : m Bool} [NeverFail mx] :
Pr[=true | mx] + Pr[=false | mx] = 1
source
@[simp]
theorem probEvent_true_eq_probOutput {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] (mx : m Bool) :
Pr[fun (x : Bool) => x = true | mx] = Pr[=true | mx]
source
@[simp]
theorem probEvent_not_eq_probOutput {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] (mx : m Bool) :
Pr[fun (x : Bool) => x = false | mx] = Pr[=false | mx]