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.

Equations

• evalDist mx = (fun {α : Type ?u.8} (x : m α) => HasEvalSPMF.toSPMF.toFun α x) mx

theorem evalDist_def {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {α : Type u} (mx : m α) : evalDist 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.

Equations

• Pr[=x | mx] = (evalDist mx) 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.

Equations

• Pr[p | mx] = (OptionT.run (evalDist mx)).toOuterMeasure (some '' {x : α | p x})

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.

Equations

• Pr[⊥ | mx] = (OptionT.run (evalDist mx)) none

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

Probability that a computation returns a particular output.

Equations

• One or more equations did not get rendered due to their size.

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

Probability that a computation returns a value satisfying a predicate.

Equations

• One or more equations did not get rendered due to their size.

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

Probability that a computation fails to return a value.

Equations

• One or more equations did not get rendered due to their size.

theorem probOutput_def {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) (x : α) : Pr[=x | mx] = (evalDist 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 ↔ (evalDist 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 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'.

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'.

@[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 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.

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.

@[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 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'.

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'.

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

Equations

• decidablePred_probOutput_eq_zero mx = ⋯.mpr inferInstance

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) : Pr[p | mx] = (OptionT.run (evalDist 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) : Pr[p | mx] = ∑' (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) : Pr[p | mx] = ∑ 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] : Pr[p | mx] = ∑' (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] : Pr[p | mx] = ∑ 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) : Pr[p | mx] = ∑' (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] : Pr[p | mx] = ∑ 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} : Pr[p | mx] = 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) → Pr[p | mx] = 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 α] : Pr[p | mx] = 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) → Pr[p | mx] = 0

Alias of the reverse direction of probEvent_eq_zero_iff'.

theorem probEvent_ne_zero_iff {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} : Pr[p | mx] ≠ 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) → Pr[p | mx] ≠ 0

Alias of the reverse direction of probEvent_ne_zero_iff.

theorem probEvent_ne_zero_iff' {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : Pr[p | mx] ≠ 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) → Pr[p | mx] ≠ 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 < Pr[p | mx] ↔ ∃ 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 < Pr[p | mx]

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 < Pr[p | mx] ↔ ∃ 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 < Pr[p | mx]

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) : Pr[p | mx] = ∑' (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] : Pr[p | mx] = ∑' (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] : Pr[p | mx] = ∑ 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] : Pr[p | mx] = ∑ 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) : Pr[p | mx] = Pr[q | mx]

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 : α) : Pr[fun (x_1 : α) => x_1 = x | mx] = Pr[=x | mx]

@[simp]

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

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

def probEventBinding1 : Lean.ParserDescr

Probability that a computation returns a value satisfying a predicate.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem evalDist_cast {α β : Type u} {m : Type u → Type u_1} [Monad m] [HasEvalSPMF m] (h : α = β) (mx : m α) : evalDist (cast ⋯ mx) = cast ⋯ (evalDist 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']) : evalDist mx = evalDist 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 α} : evalDist mx = evalDist 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 α) : evalDist 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 α)) : evalDist 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) : evalDist 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 (evalDist 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 (evalDist 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 α) : evalDist (if p then mx else mx') = if p then evalDist mx else evalDist 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) : Pr[q | if p then mx else mx'] = if p then Pr[q | mx] else Pr[q | mx']

theorem evalDist_eqRec {m : Type u → Type v} [Monad m] {α β : Type u} [HasEvalSPMF m] (h : α = β) (mx : m α) : evalDist (h ▸ mx) = h ▸ evalDist 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) : Pr[q | h ▸ mx] = Pr[fun (x : α) => q (h ▸ x) | mx]

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)] = Pr[p | mx]

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] : Pr[p | mx] ≤ 1

@[simp]

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

@[simp]

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

@[simp]

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

@[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 ≤ Pr[p | mx] ↔ Pr[p | mx] = 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'.

@[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) : Pr[p | mx] * 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 * Pr[p | mx] ≤ 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 α) : Pr[fun (x : α) => False | mx] = 0

@[simp]

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

@[simp]

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

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

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

theorem probFailure_eq_one_iff_probEvent_true {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSPMF m] (mx : m α) : Pr[⊥ | mx] = 1 ↔ Pr[fun (x : α) => True | mx] = 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] : Pr[fun (x : α) => p | mx] = 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 α) : evalDist 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) : Pr[p | mx] ≤ Pr[q | mx]

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) : Pr[p | mx] ≤ Pr[q | mx]

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) : Pr[p | mx] + Pr[fun (x : α) => ¬p x | mx] = 1 - Pr[⊥ | mx]

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

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} : Pr[p | mx] = 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) → Pr[p | mx] = 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} : 1 = Pr[p | mx] ↔ 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 = Pr[p | mx]

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 α] : Pr[p | mx] = 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) → Pr[p | mx] = 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 = Pr[p | mx] ↔ 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 = Pr[p | mx]

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 : evalDist mx = evalDist 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 : evalDist mx = evalDist 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) = Pr[fun (z : α × β) => R z.1 z.2 | mx]