Typeclasses for Denotational Monad Semantics

This file defines typeclasses HasEvalSPMF and HasEvalPMF for assigning denotational probability semantics to monadic computations. We also introduce functions probOutput, probEvent, and probFailure with associated notation.

-- dtumad: document various probability notation definitions here

class HasEvalSPMF (m : Type u → Type v) [Monad m] extends HasEvalSet m : Type (max (u + 1) v)

The monad m can be evaluated to get a sub-distribution of outputs. Should not be implemented manually if a HasEvalPMF instance already exists.

• toSet : m →ᵐ SetM
• toSPMF : m →ᵐ SPMF
• support_eq {α : Type u} (mx : m α) : support mx = ((fun {α : Type u} (x : m α) => toSPMF.toFun α x) mx).support

def evalDist {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {α : Type u} (mx : m α) : SPMF α

The resulting distribution of running the monadic computation mx. dtumad: I think we should eventually just deprecate this, just say toSPMF.

def «term𝒟[_]» : Lean.ParserDescr

Evaluation distribution notation for any monad with HasEvalSPMF. For monads with HasEvalPMF, this uses the inherited HasEvalSPMF semantics.

theorem evalDist_def {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {α : Type u} (mx : m α) : 𝒟[mx] = (fun {α : Type u} (x : m α) => HasEvalSPMF.toSPMF.toFun α x) mx

def probOutput {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : ENNReal

Probability that a computation mx returns the value x.

noncomputable def probEvent {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (p : α → Prop) : ENNReal

Probability that a computation mx outputs a value satisfying p.

def probFailure {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : ENNReal

Probability that a computation mx will fail to return a value.

def «termPr[=_|_]» : Lean.ParserDescr

Probability that a computation returns a particular output.

def probEventNotation : Lean.ParserDescr

Probability that a computation returns a value satisfying a predicate.

def «termPr[⊥|_]» : Lean.ParserDescr

Probability that a computation fails to return a value.

theorem probOutput_def {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : Pr[= x | mx] = 𝒟[mx] x

theorem mem_support_iff {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : x ∈ support mx ↔ Pr[= x | mx] ≠ 0

theorem mem_support_iff_evalDist_apply_ne_zero {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : x ∈ support mx ↔ 𝒟[mx] x ≠ 0

theorem mem_finSupport_iff {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] [DecidableEq α] [HasEvalFinset m] (mx : m α) (x : α) : x ∈ finSupport mx ↔ Pr[= x | mx] ≠ 0

theorem probOutput_ne_zero_of_mem_support {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {x : α} (h : x ∈ support mx) : Pr[= x | mx] ≠ 0

theorem probOutput_eq_zero_of_not_mem_support {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {x : α} (h : x ∉ support mx) : Pr[= x | mx] = 0

@[simp]

theorem probOutput_eq_zero_iff {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : Pr[= x | mx] = 0 ↔ x ∉ support mx

theorem not_mem_support_of_probOutput_eq_zero {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : Pr[= x | mx] = 0 → x ∉ support mx

Alias of the forward direction of probOutput_eq_zero_iff.

theorem probOutput_eq_zero {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : x ∉ support mx → Pr[= x | mx] = 0

Alias of the reverse direction of probOutput_eq_zero_iff.

@[simp]

theorem zero_eq_probOutput_iff {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : 0 = Pr[= x | mx] ↔ x ∉ support mx

theorem zero_eq_probOutput {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : x ∉ support mx → 0 = Pr[= x | mx]

Alias of the reverse direction of zero_eq_probOutput_iff.

@[simp]

theorem probOutput_eq_zero_iff' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : Pr[= x | mx] = 0 ↔ x ∉ finSupport mx

theorem probOutput_eq_zero' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : x ∉ finSupport mx → Pr[= x | mx] = 0

Alias of the reverse direction of probOutput_eq_zero_iff'.

theorem not_mem_fin_support_of_probOutput_eq_zero {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : Pr[= x | mx] = 0 → x ∉ finSupport mx

Alias of the forward direction of probOutput_eq_zero_iff'.

@[simp]

theorem zero_eq_probOutput_iff' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : 0 = Pr[= x | mx] ↔ x ∉ finSupport mx

theorem zero_eq_probOutput' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : x ∉ finSupport mx → 0 = Pr[= x | mx]

Alias of the reverse direction of zero_eq_probOutput_iff'.

@[simp]

theorem probOutput_pos_iff {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : 0 < Pr[= x | mx] ↔ x ∈ support mx

theorem mem_support_of_probOutput_pos {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : 0 < Pr[= x | mx] → x ∈ support mx

Alias of the forward direction of probOutput_pos_iff.

theorem probOutput_pos {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : x ∈ support mx → 0 < Pr[= x | mx]

Alias of the reverse direction of probOutput_pos_iff.

@[simp]

theorem probOutput_pos_iff' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : 0 < Pr[= x | mx] ↔ x ∈ finSupport mx

theorem probOutput_pos' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : x ∈ finSupport mx → 0 < Pr[= x | mx]

Alias of the reverse direction of probOutput_pos_iff'.

theorem mem_finSupport_of_probOutput_pos {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : 0 < Pr[= x | mx] → x ∈ finSupport mx

Alias of the forward direction of probOutput_pos_iff'.

@[implicit_reducible]

instance decidablePred_probOutput_eq_zero {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] [hm : HasEvalSet.Decidable m] (mx : m α) : DecidablePred fun (x : α) => Pr[= x | mx] = 0

theorem probOutput_ne_zero {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) (h : x ∈ support mx) : Pr[= x | mx] ≠ 0

theorem probOutput_ne_zero' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] (h : x ∈ finSupport mx) : Pr[= x | mx] ≠ 0

@[simp]

theorem support_probOutput {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : Function.support (probOutput mx) = support mx

theorem probEvent_def {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (p : α → Prop) : probEvent mx p = (OptionT.run 𝒟[mx]).toOuterMeasure (some '' {x : α | p x})

theorem probEvent_eq_tsum_indicator {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (p : α → Prop) : probEvent mx p = ∑' (x : α), {x : α | p x}.indicator (fun (x : α) => Pr[= x | mx]) x

theorem probEvent_eq_sum_fintype_indicator {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] [Fintype α] (mx : m α) (p : α → Prop) : probEvent mx p = ∑ x : α, {x : α | p x}.indicator (fun (x : α) => Pr[= x | mx]) x

theorem probEvent_eq_tsum_ite {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (p : α → Prop) [DecidablePred p] : probEvent mx p = ∑' (x : α), if p x then Pr[= x | mx] else 0

theorem probEvent_eq_sum_fintype_ite {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] [Fintype α] (mx : m α) (p : α → Prop) [DecidablePred p] : probEvent mx p = ∑ x : α, if p x then Pr[= x | mx] else 0

theorem probEvent_eq_tsum_subtype {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (p : α → Prop) : probEvent mx p = ∑' (x : ↑{x : α | p x}), Pr[= ↑x | mx]

theorem probEvent_eq_sum_filter_univ {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] [Fintype α] (mx : m α) (p : α → Prop) [DecidablePred p] : probEvent mx p = ∑ x : α with p x, Pr[= x | mx]

@[simp]

theorem probEvent_eq_zero_iff {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} : probEvent mx p = 0 ↔ ∀ x ∈ support mx, ¬p x

theorem probEvent_eq_zero {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} : (∀ x ∈ support mx, ¬p x) → probEvent mx p = 0

Alias of the reverse direction of probEvent_eq_zero_iff.

@[simp]

theorem probEvent_eq_zero_iff' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : probEvent mx p = 0 ↔ ∀ x ∈ finSupport mx, ¬p x

theorem probEvent_eq_zero' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : (∀ x ∈ finSupport mx, ¬p x) → probEvent mx p = 0

Alias of the reverse direction of probEvent_eq_zero_iff'.

@[simp]

theorem probEvent_ne_zero_iff {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} : probEvent mx p ≠ 0 ↔ ∃ x ∈ support mx, p x

theorem probEvent_ne_zero {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} : (∃ x ∈ support mx, p x) → probEvent mx p ≠ 0

Alias of the reverse direction of probEvent_ne_zero_iff.

@[simp]

theorem probEvent_ne_zero_iff' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : probEvent mx p ≠ 0 ↔ ∃ x ∈ finSupport mx, p x

theorem probEvent_ne_zero' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : (∃ x ∈ finSupport mx, p x) → probEvent mx p ≠ 0

Alias of the reverse direction of probEvent_ne_zero_iff'.

@[simp]

theorem probEvent_pos_iff {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} : 0 < probEvent mx p ↔ ∃ x ∈ support mx, p x

theorem probEvent_pos {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} : (∃ x ∈ support mx, p x) → 0 < probEvent mx p

Alias of the reverse direction of probEvent_pos_iff.

@[simp]

theorem probEvent_pos_iff' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : 0 < probEvent mx p ↔ ∃ x ∈ finSupport mx, p x

theorem probEvent_pos' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : (∃ x ∈ finSupport mx, p x) → 0 < probEvent mx p

Alias of the reverse direction of probEvent_pos_iff'.

theorem probEvent_eq_tsum_subtype_mem_support {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (p : α → Prop) : probEvent mx p = ∑' (x : ↑{x : α | x ∈ support mx ∧ p x}), Pr[= ↑x | mx]

theorem probEvent_eq_tsum_subtype_support_ite {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (p : α → Prop) [DecidablePred p] : probEvent mx p = ∑' (x : ↑(support mx)), if p ↑x then Pr[= ↑x | mx] else 0

theorem probEvent_eq_sum_filter_finSupport {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] [HasEvalFinset m] [DecidableEq α] (mx : m α) (p : α → Prop) [DecidablePred p] : probEvent mx p = ∑ x ∈ finSupport mx with p x, Pr[= x | mx]

theorem probEvent_eq_sum_finSupport_ite {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] [HasEvalFinset m] [DecidableEq α] (mx : m α) (p : α → Prop) [DecidablePred p] : probEvent mx p = ∑ x ∈ finSupport mx, if p x then Pr[= x | mx] else 0

theorem probEvent_ext {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p q : α → Prop} (h : ∀ x ∈ support mx, p x ↔ q x) : probEvent mx p = probEvent mx q

If two events are equivalent on the support of mx then they have the same output chance.

@[simp]

theorem probEvent_eq_eq_probOutput {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : (probEvent mx fun (x_1 : α) => x_1 = x) = Pr[= x | mx]

@[simp]

theorem probEvent_eq_eq_probOutput' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : (probEvent mx fun (x_1 : α) => x = x_1) = Pr[= x | mx]

theorem probFailure_def {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : Pr[⊥ | mx] = (OptionT.run 𝒟[mx]) none

def probEventBinding1 : Lean.ParserDescr

Probability that a computation returns a value satisfying a predicate.

def probEventBinding2 : Lean.ParserDescr

Probability that a computation returns a value satisfying a predicate. See probOutput_true_eq_probEvent for relation to the above definitions.

@[simp]

theorem evalDist_cast {α β : Type u} {m : Type u → Type u_1} [Monad m] [HasEvalSPMF m] (h : α = β) (mx : m α) : 𝒟[cast ⋯ mx] = cast ⋯ 𝒟[mx]

theorem evalDist_ext {α : Type u} {m : Type u → Type u_1} {n : Type u → Type u_2} [Monad m] [HasEvalSPMF m] [Monad n] [HasEvalSPMF n] {mx : m α} {mx' : n α} (h : ∀ (x : α), Pr[= x | mx] = Pr[= x | mx']) : 𝒟[mx] = 𝒟[mx']

theorem evalDist_ext_iff {α : Type u} {m : Type u → Type u_1} {n : Type u → Type u_2} [Monad m] [HasEvalSPMF m] [Monad n] [HasEvalSPMF n] {mx : m α} {mx' : n α} : 𝒟[mx] = 𝒟[mx'] ↔ ∀ (x : α), Pr[= x | mx] = Pr[= x | mx']

@[simp]

theorem evalDist_eq_liftM_iff {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (p : PMF α) : 𝒟[mx] = liftM p ↔ ∀ (x : α), Pr[= x | mx] = p x

@[simp]

theorem evalDist_eq_mk_iff {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (p : PMF (Option α)) : 𝒟[mx] = SPMF.mk p ↔ ∀ (x : α), Pr[= x | mx] = p (some x)

theorem evalDist_eq_liftM {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : PMF α} (h : ∀ (x : α), Pr[= x | mx] = p x) : 𝒟[mx] = liftM p

@[simp]

theorem evalDist_apply_eq_zero_iff {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : Option α) : (OptionT.run 𝒟[mx]) x = 0 ↔ Option.rec (Pr[⊥ | mx] = 0) (fun (x : α) => x ∉ support mx) x

@[simp]

theorem evalDist_apply_eq_zero_iff' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] [HasEvalFinset m] [DecidableEq α] (mx : m α) (x : Option α) : (OptionT.run 𝒟[mx]) x = 0 ↔ Option.rec (Pr[⊥ | mx] = 0) (fun (x : α) => x ∉ finSupport mx) x

@[simp]

theorem evalDist_ite {m : Type u → Type v} [Monad m] {α : Type u} (p : Prop) [Decidable p] [HasEvalSPMF m] (mx mx' : m α) : 𝒟[if p then mx else mx'] = if p then 𝒟[mx] else 𝒟[mx']

@[simp]

theorem probOutput_ite {m : Type u → Type v} [Monad m] {α : Type u} (p : Prop) [Decidable p] [HasEvalSPMF m] (x : α) (mx mx' : m α) : Pr[= x | if p then mx else mx'] = if p then Pr[= x | mx] else Pr[= x | mx']

@[simp]

theorem probFailure_ite {m : Type u → Type v} [Monad m] {α : Type u} (p : Prop) [Decidable p] [HasEvalSPMF m] (mx mx' : m α) : Pr[⊥ | if p then mx else mx'] = if p then Pr[⊥ | mx] else Pr[⊥ | mx']

@[simp]

theorem probEvent_ite {m : Type u → Type v} [Monad m] {α : Type u} (p : Prop) [Decidable p] [HasEvalSPMF m] (mx mx' : m α) (q : α → Prop) : probEvent (if p then mx else mx') q = if p then probEvent mx q else probEvent mx' q

theorem evalDist_eqRec {m : Type u → Type v} [Monad m] {α β : Type u} [HasEvalSPMF m] (h : α = β) (mx : m α) : 𝒟[h ▸ mx] = h ▸ 𝒟[mx]

theorem probOutput_eqRec {m : Type u → Type v} [Monad m] {α β : Type u} [HasEvalSPMF m] (h : α = β) (mx : m α) (y : β) : Pr[= y | h ▸ mx] = Pr[= ⋯ ▸ y | mx]

@[simp]

theorem probFailure_eqRec {m : Type u → Type v} [Monad m] {α β : Type u} [HasEvalSPMF m] (h : α = β) (mx : m α) : Pr[⊥ | h ▸ mx] = Pr[⊥ | mx]

theorem probEvent_eqRec {m : Type u → Type v} [Monad m] {α β : Type u} [HasEvalSPMF m] (h : α = β) (mx : m α) (q : β → Prop) : probEvent (h ▸ mx) q = probEvent mx fun (x : α) => q (h ▸ x)

theorem probOutput_true_eq_probEvent {α : Type} {m : Type → Type u} [Monad m] [HasEvalSPMF m] (mx : m α) (p : α → Prop) : Pr[= True | do let x ← mx pure (p x)] = probEvent mx p

Connection between the two different probability notations.

@[simp]

theorem tsum_probOutput_add_probFailure {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : ∑' (x : α), Pr[= x | mx] + Pr[⊥ | mx] = 1

@[simp]

theorem probFailure_add_tsum_probOutput {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : Pr[⊥ | mx] + ∑' (x : α), Pr[= x | mx] = 1

@[simp]

theorem probOutput_le_one {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {x : α} [HasEvalSPMF m] : Pr[= x | mx] ≤ 1

@[simp]

theorem probOutput_ne_top {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {x : α} [HasEvalSPMF m] : Pr[= x | mx] ≠ ⊤

@[simp]

theorem probOutput_lt_top {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {x : α} [HasEvalSPMF m] : Pr[= x | mx] < ⊤

@[simp]

theorem not_one_lt_probOutput {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {x : α} [HasEvalSPMF m] : ¬1 < Pr[= x | mx]

@[simp]

theorem tsum_probOutput_le_one {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} [HasEvalSPMF m] : ∑' (x : α), Pr[= x | mx] ≤ 1

@[simp]

theorem tsum_probOutput_ne_top {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} [HasEvalSPMF m] : ∑' (x : α), Pr[= x | mx] ≠ ⊤

@[simp]

theorem probEvent_le_one {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {p : α → Prop} [HasEvalSPMF m] : probEvent mx p ≤ 1

@[simp]

theorem probEvent_ne_top {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {p : α → Prop} [HasEvalSPMF m] : probEvent mx p ≠ ⊤

@[simp]

theorem probEvent_lt_top {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {p : α → Prop} [HasEvalSPMF m] : probEvent mx p < ⊤

@[simp]

theorem not_one_lt_probEvent {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {p : α → Prop} [HasEvalSPMF m] : ¬1 < probEvent mx p

@[simp]

theorem probFailure_le_one {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} [HasEvalSPMF m] : Pr[⊥ | mx] ≤ 1

@[simp]

theorem probFailure_ne_top {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} [HasEvalSPMF m] : Pr[⊥ | mx] ≠ ⊤

@[simp]

theorem probFailure_lt_top {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} [HasEvalSPMF m] : Pr[⊥ | mx] < ⊤

@[simp]

theorem not_one_lt_probFailure {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} [HasEvalSPMF m] : ¬1 < Pr[⊥ | mx]

@[simp]

theorem one_le_probOutput_iff {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {x : α} [HasEvalSPMF m] : 1 ≤ Pr[= x | mx] ↔ Pr[= x | mx] = 1

@[simp]

theorem one_le_probEvent_iff {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {p : α → Prop} [HasEvalSPMF m] : 1 ≤ probEvent mx p ↔ probEvent mx p = 1

@[simp]

theorem one_le_probFailure_iff {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} [HasEvalSPMF m] : 1 ≤ Pr[⊥ | mx] ↔ Pr[⊥ | mx] = 1

@[simp]

theorem probOutput_eq_one_iff {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {x : α} [HasEvalSPMF m] : Pr[= x | mx] = 1 ↔ Pr[⊥ | mx] = 0 ∧ support mx = {x}

theorem probOutput_eq_one {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {x : α} [HasEvalSPMF m] : Pr[⊥ | mx] = 0 ∧ support mx = {x} → Pr[= x | mx] = 1

Alias of the reverse direction of probOutput_eq_one_iff.

@[simp]

theorem one_eq_probOutput_iff {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {x : α} [HasEvalSPMF m] : 1 = Pr[= x | mx] ↔ Pr[⊥ | mx] = 0 ∧ support mx = {x}

theorem one_eq_probOutput {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {x : α} [HasEvalSPMF m] : Pr[⊥ | mx] = 0 ∧ support mx = {x} → 1 = Pr[= x | mx]

Alias of the reverse direction of one_eq_probOutput_iff.

@[simp]

theorem probOutput_eq_one_iff' {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {x : α} [HasEvalSPMF m] [HasEvalFinset m] [DecidableEq α] : Pr[= x | mx] = 1 ↔ Pr[⊥ | mx] = 0 ∧ finSupport mx = {x}

theorem probOutput_eq_one' {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {x : α} [HasEvalSPMF m] [HasEvalFinset m] [DecidableEq α] : Pr[⊥ | mx] = 0 ∧ finSupport mx = {x} → Pr[= x | mx] = 1

Alias of the reverse direction of probOutput_eq_one_iff'.

@[simp]

theorem one_eq_probOutput_iff' {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {x : α} [HasEvalSPMF m] [HasEvalFinset m] [DecidableEq α] : 1 = Pr[= x | mx] ↔ Pr[⊥ | mx] = 0 ∧ finSupport mx = {x}

theorem one_eq_probOutput' {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {x : α} [HasEvalSPMF m] [HasEvalFinset m] [DecidableEq α] : Pr[⊥ | mx] = 0 ∧ finSupport mx = {x} → 1 = Pr[= x | mx]

Alias of the reverse direction of one_eq_probOutput_iff'.

theorem probOutput_eq_one_of_support_subset_singleton {m : Type u → Type v} [Monad m] {α : Type u} {mx : m α} {x : α} [HasEvalSPMF m] (hnf : Pr[⊥ | mx] = 0) (huniq : ∀ y ∈ support mx, y = x) : Pr[= x | mx] = 1

If a non-failing computation can only return x, then it returns x with probability one.

@[simp]

theorem probFailure_mul_le {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (r : ENNReal) : Pr[⊥ | mx] * r ≤ r

@[simp]

theorem mul_probFailure_le {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (r : ENNReal) : r * Pr[⊥ | mx] ≤ r

@[simp]

theorem probOutput_mul_le {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (r : ENNReal) (x : α) : Pr[= x | mx] * r ≤ r

@[simp]

theorem mul_probOutput_le {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (r : ENNReal) (x : α) : r * Pr[= x | mx] ≤ r

@[simp]

theorem probEvent_mul_le {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (r : ENNReal) (p : α → Prop) : probEvent mx p * r ≤ r

@[simp]

theorem mul_probEvent_le {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (r : ENNReal) (p : α → Prop) : r * probEvent mx p ≤ r

@[simp]

theorem tsum_probOutput_eq_sub {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : ∑' (x : α), Pr[= x | mx] = 1 - Pr[⊥ | mx]

theorem tsum_probOutput_eq_one' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} (h : Pr[⊥ | mx] = 0) : ∑' (x : α), Pr[= x | mx] = 1

@[simp]

theorem tsum_support_probOutput_eq_sub {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : ∑' (x : ↑(support mx)), Pr[= ↑x | mx] = 1 - Pr[⊥ | mx]

theorem tsum_support_probOutput_eq_one' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} (h : Pr[⊥ | mx] = 0) : ∑' (x : ↑(support mx)), Pr[= ↑x | mx] = 1

@[simp]

theorem sum_probOutput_eq_sub {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] [Fintype α] (mx : m α) : ∑ x : α, Pr[= x | mx] = 1 - Pr[⊥ | mx]

theorem sum_probOutput_eq_one {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] [Fintype α] {mx : m α} (h : Pr[⊥ | mx] = 0) : ∑ x : α, Pr[= x | mx] = 1

@[simp]

theorem sum_finSupport_probOutput_eq_sub {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] [HasEvalFinset m] [DecidableEq α] (mx : m α) : ∑ x ∈ finSupport mx, Pr[= x | mx] = 1 - Pr[⊥ | mx]

theorem sum_finSupport_probOutput_eq_one {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] [HasEvalFinset m] [DecidableEq α] {mx : m α} (h : Pr[⊥ | mx] = 0) : ∑ x ∈ finSupport mx, Pr[= x | mx] = 1

theorem probFailure_eq_sub_tsum {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : Pr[⊥ | mx] = 1 - ∑' (x : α), Pr[= x | mx]

theorem probFailure_eq_sub_sum {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] [Fintype α] (mx : m α) : Pr[⊥ | mx] = 1 - ∑ x : α, Pr[= x | mx]

@[simp]

theorem probEvent_False {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : (probEvent mx fun (x : α) => False) = 0

@[simp]

theorem probEvent_false {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : (probEvent mx fun (x : α) => false = true) = 0

@[simp]

theorem probEvent_True_eq_sub {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : (probEvent mx fun (x : α) => True) = 1 - Pr[⊥ | mx]

theorem probEvent_true_eq_sub {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : (probEvent mx fun (x : α) => true = true) = 1 - Pr[⊥ | mx]

theorem probFailure_eq_sub_probEvent {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : Pr[⊥ | mx] = 1 - probEvent mx fun (x : α) => True

theorem probFailure_eq_one_iff_probEvent_true {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : Pr[⊥ | mx] = 1 ↔ (probEvent mx fun (x : α) => True) = 0

@[simp]

theorem probFailure_eq_one_iff {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : Pr[⊥ | mx] = 1 ↔ support mx = ∅

theorem probFailure_eq_one {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} (h : support mx = ∅) : Pr[⊥ | mx] = 1

@[simp]

theorem probEvent_const {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (p : Prop) [Decidable p] : (probEvent mx fun (x : α) => p) = if p then 1 - Pr[⊥ | mx] else 0

class HasEvalPMF (m : Type u → Type v) [Monad m] extends HasEvalSPMF m : Type (max (u + 1) v)

The monad m can be evaluated to get a distribution of outputs.

• toSet : m →ᵐ SetM
• toSPMF : m →ᵐ SPMF
• support_eq {α : Type u} (mx : m α) : support mx = ((fun {α : Type u} (x : m α) => toSPMF.toFun α x) mx).support
• toPMF : m →ᵐ PMF
• toSPMF_eq {α : Type u} (mx : m α) : (fun {α : Type u} (x : m α) => HasEvalSPMF.toSPMF.toFun α x) mx = liftM ((fun {α : Type u} (x : m α) => toPMF.toFun α x) mx)

theorem HasEvalPMF.evalDist_of_hasEvalPMF_def {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalPMF m] (mx : m α) : 𝒟[mx] = liftM ((fun {α : Type u} (x : m α) => toPMF.toFun α x) mx)

@[simp]

theorem HasEvalPMF.probFailure_eq_zero {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalPMF m] (mx : m α) : Pr[⊥ | mx] = 0

The evalDist arising from a HasEvalPMF instance never fails.

theorem HasEvalPMF.tsum_probOutput_eq_one {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalPMF m] (mx : m α) : ∑' (x : α), Pr[= x | mx] = 1

theorem HasEvalPMF.tsum_support_probOutput_eq_one {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalPMF m] (mx : m α) : ∑' (x : ↑(support mx)), Pr[= ↑x | mx] = 1

theorem HasEvalPMF.sum_probOutput_eq_one {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalPMF m] [Fintype α] (mx : m α) : ∑ x : α, Pr[= x | mx] = 1

theorem HasEvalPMF.sum_finSupport_probOutput_eq_one {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalPMF m] [HasEvalFinset m] [DecidableEq α] (mx : m α) : ∑ x ∈ finSupport mx, Pr[= x | mx] = 1

theorem HasEvalPMF.finSupport_nonempty {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalPMF m] [HasEvalFinset m] [DecidableEq α] (mx : m α) : (finSupport mx).Nonempty

theorem HasEvalPMF.probOutput_eq_inv_finSupport_card {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalPMF m] [HasEvalFinset m] [DecidableEq α] {mx : m α} {c : ENNReal} (hconst : ∀ x ∈ support mx, Pr[= x | mx] = c) : c = 1 / ↑(finSupport mx).card

theorem probEvent_mono {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p q : α → Prop} (h : ∀ x ∈ support mx, p x → q x) : probEvent mx p ≤ probEvent mx q

If p implies q on the support of a computation then it is more likely to happen.

theorem probEvent_mono' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p q : α → Prop} [HasEvalFinset m] [DecidableEq α] (h : ∀ x ∈ finSupport mx, p x → q x) : probEvent mx p ≤ probEvent mx q

If p implies q on the finSupport of a computation then it is more likely to happen.

theorem probEvent_compl {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (p : α → Prop) : (probEvent mx p + probEvent mx fun (x : α) => ¬p x) = 1 - Pr[⊥ | mx]

theorem probEvent_or_le {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (p q : α → Prop) : (probEvent mx fun (x : α) => p x ∨ q x) ≤ probEvent mx p + probEvent mx q

Union bound: the probability of p ∨ q is at most the sum of probabilities.

@[simp]

theorem probEvent_eq_one_iff {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} : probEvent mx p = 1 ↔ Pr[⊥ | mx] = 0 ∧ ∀ x ∈ support mx, p x

theorem probEvent_eq_one {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} : (Pr[⊥ | mx] = 0 ∧ ∀ x ∈ support mx, p x) → probEvent mx p = 1

Alias of the reverse direction of probEvent_eq_one_iff.

theorem probOutput_eq_one_iff_forall {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : Pr[= x | mx] = 1 ↔ Pr[⊥ | mx] = 0 ∧ ∀ y ∈ support mx, y = x

Pointwise variant of probOutput_eq_one_iff: Pr[= x | mx] = 1 iff the support is a subset of {x} (phrased as a forall over the support) and the computation never fails.

More usable than probOutput_eq_one_iff when the caller wants to iterate over arbitrary support elements rather than prove a set equality.

@[simp]

theorem one_eq_probEvent_iff {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} : 1 = probEvent mx p ↔ Pr[⊥ | mx] = 0 ∧ ∀ x ∈ support mx, p x

theorem one_eq_probEvent {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} : (Pr[⊥ | mx] = 0 ∧ ∀ x ∈ support mx, p x) → 1 = probEvent mx p

Alias of the reverse direction of one_eq_probEvent_iff.

@[simp]

theorem probEvent_eq_one_iff' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : probEvent mx p = 1 ↔ Pr[⊥ | mx] = 0 ∧ ∀ x ∈ finSupport mx, p x

theorem probEvent_eq_one' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : (Pr[⊥ | mx] = 0 ∧ ∀ x ∈ finSupport mx, p x) → probEvent mx p = 1

Alias of the reverse direction of probEvent_eq_one_iff'.

@[simp]

theorem one_eq_probEvent_iff' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : 1 = probEvent mx p ↔ Pr[⊥ | mx] = 0 ∧ ∀ x ∈ finSupport mx, p x

theorem one_eq_probEvent' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : (Pr[⊥ | mx] = 0 ∧ ∀ x ∈ finSupport mx, p x) → 1 = probEvent mx p

Alias of the reverse direction of one_eq_probEvent_iff'.

@[simp]

theorem function_support_probOutput {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} : (Function.support fun (x : α) => Pr[= x | mx]) = support mx

theorem mem_support_iff_of_evalDist_eq {α : Type u} {m : Type u → Type u_1} {n : Type u → Type u_2} [Monad m] [HasEvalSPMF m] [Monad n] [HasEvalSPMF n] {mx : m α} {mx' : n α} (h : 𝒟[mx] = 𝒟[mx']) (x : α) : x ∈ support mx ↔ x ∈ support mx'

theorem mem_finSupport_iff_of_evalDist_eq {α : Type u} {m : Type u → Type u_1} {n : Type u → Type u_2} [Monad m] [HasEvalSPMF m] [Monad n] [HasEvalSPMF n] [HasEvalFinset m] [HasEvalFinset n] [DecidableEq α] {mx : m α} {mx' : n α} (h : 𝒟[mx] = 𝒟[mx']) (x : α) : x ∈ finSupport mx ↔ x ∈ finSupport mx'

theorem indicator_objective_eq_probEvent {m : Type u → Type v} [Monad m] {α β : Type u} [HasEvalSPMF m] (mx : m (α × β)) (R : α → β → Prop) : (∑' (z : α × β), Pr[= z | mx] * if R z.1 z.2 then 1 else 0) = probEvent mx fun (z : α × β) => R z.1 z.2