Documentation

VCVio.EvalDist.Monad.Basic

Evaluation Distributions of Computations with Bind #

File for lemmas about evalDist and support involving the monadic pure and bind.

source
@[simp]
theorem support_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] (x : α) :
support (pure x) = {x}
source
theorem mem_support_pure_iff {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] (x y : α) :
x ∈ support (pure y) ↔ x = y
source
theorem mem_support_pure_iff' {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] (x y : α) :
x ∈ support (pure y) ↔ y = x
source
@[simp]
theorem finSupport_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] (x : α) :
finSupport (pure x) = {x}
source
theorem mem_finSupport_pure_iff {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] (x y : α) :
x ∈ finSupport (pure y) ↔ x = y
source
theorem mem_finSupport_pure_iff' {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] (x y : α) :
x ∈ finSupport (pure y) ↔ y = x
source
@[simp]
theorem evalDist_pure {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {α : Type u} (x : α) :
evalDist (pure x) = pure x
source
@[simp]
theorem evalDist_comp_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] :
evalDist ∘ pure = pure
source
@[simp]
theorem evalDist_comp_pure' {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (f : α → β) :
evalDist ∘ pure ∘ f = pure ∘ f
source
@[simp]
theorem probOutput_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [DecidableEq α] (x y : α) :
Pr[=x | pure y] = if x = y then 1 else 0
source
@[simp]
theorem probOutput_pure_self {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (x : α) :
Pr[=x | pure x] = 1
source
theorem probOutput_pure_eq_indicator {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (x y : α) :
Pr[=x | pure y] = {y}.indicator (Function.const α 1) x

Fallback when we don't have decidable equality.

source
@[simp]
theorem probEvent_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (x : α) (p : α → Prop) [DecidablePred p] :
Pr[p | pure x] = if p x then 1 else 0
source
theorem probEvent_pure_eq_indicator {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (x : α) (p : α → Prop) :
Pr[p | pure x] = {x : α | p x}.indicator (Function.const α 1) x

Fallback when we don't have decidable equality.

source
@[simp]
theorem probFailure_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (x : α) :
Pr[⊥ | pure x] = 0
source
@[simp]
theorem tsum_probOutput_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (x : α) :
∑' (y : α), Pr[=y | pure x] = 1
source
@[simp]
theorem tsum_probOutput_pure' {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (x : α) :
∑' (y : α), Pr[=x | pure y] = 1
source
@[simp]
theorem sum_probOutput_pure {α : Type u} {m : Type u → Type v} [Monad m] [Fintype α] [HasEvalSPMF m] (x : α) :
∑ y : α, Pr[=y | pure x] = 1
source
@[simp]
theorem sum_probOutput_pure' {α : Type u} {m : Type u → Type v} [Monad m] [Fintype α] [HasEvalSPMF m] (x : α) :
∑ y : α, Pr[=x | pure y] = 1
source
@[simp]
theorem support_bind {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] (mx : m α) (my : α → m β) :
support (mx >>= my) = ⋃ x ∈ support mx, support (my x)
source
theorem mem_support_bind_iff {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] (mx : m α) (my : α → m β) (y : β) :
y ∈ support (mx >>= my) ↔ ∃ x ∈ support mx, y ∈ support (my x)
source
@[simp]
theorem finSupport_bind {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] [DecidableEq β] (mx : m α) (my : α → m β) :
finSupport (mx >>= my) = (finSupport mx).biUnion fun (x : α) => finSupport (my x)
source
theorem mem_finSupport_bind_iff {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] [DecidableEq β] (mx : m α) (my : α → m β) (y : β) :
y ∈ finSupport (mx >>= my) ↔ ∃ x ∈ finSupport mx, y ∈ finSupport (my x)
source
@[simp]
theorem evalDist_bind {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) :
evalDist (mx >>= my) = do let x ← evalDist mx evalDist (my x)
source
theorem evalDist_bind_of_support_eq_empty {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) (h : support mx = ∅) :
evalDist (mx >>= my) = failure
source
theorem probOutput_bind_eq_tsum {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) (y : β) :
Pr[=y | mx >>= my] = ∑' (x : α), Pr[=x | mx] * Pr[=y | my x]
source
theorem probEvent_bind_eq_tsum {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) (q : β → Prop) :
Pr[q | mx >>= my] = ∑' (x : α), Pr[=x | mx] * Pr[q | my x]
source
theorem probFailure_bind_eq_add_tsum {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) :
Pr[⊥ | mx >>= my] = Pr[⊥ | mx] + ∑' (x : α), Pr[=x | mx] * Pr[⊥ | my x]
source
theorem probFailure_bind_eq_add_tsum_support {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) :
Pr[⊥ | mx >>= my] = Pr[⊥ | mx] + ∑' (x : ↑(support mx)), Pr[=↑x | mx] * Pr[⊥ | my ↑x]
source
@[simp]
theorem probFailure_bind_eq_zero_iff {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) :
Pr[⊥ | mx >>= my] = 0 ↔ Pr[⊥ | mx] = 0 ∧ ∀ x ∈ support mx, Pr[⊥ | my x] = 0
source
theorem probOutput_bind_eq_tsum_subtype {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) (y : β) :
Pr[=y | mx >>= my] = ∑' (x : ↑(support mx)), Pr[=↑x | mx] * Pr[=y | my ↑x]

Version of probOutput_bind_eq_tsum that sums only over the subtype given by the support of the first computation. This can be useful to avoid looking at edge cases that can't actually happen in practice after the first computation. A common example is if the first computation does some error handling to avoids returning malformed outputs.

source
theorem probEvent_bind_eq_tsum_subtype {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) (q : β → Prop) :
Pr[q | mx >>= my] = ∑' (x : ↑(support mx)), Pr[=↑x | mx] * Pr[q | my ↑x]
source
theorem probOutput_bind_eq_sum_finSupport {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [HasEvalFinset m] (mx : m α) (my : α → m β) [DecidableEq α] (y : β) :
Pr[=y | mx >>= my] = ∑ x ∈ finSupport mx, Pr[=x | mx] * Pr[=y | my x]
source
theorem probEvent_bind_eq_sum_finSupport {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [HasEvalFinset m] (mx : m α) (my : α → m β) [DecidableEq α] (q : β → Prop) :
Pr[q | mx >>= my] = ∑ x ∈ finSupport mx, Pr[=x | mx] * Pr[q | my x]
source
@[simp]
theorem support_bind_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] (mx : m α) (my : m β) :
(support do let _ ← mx my) = {y : β | y ∈ support my ∧ (support mx).Nonempty}
source
@[simp]
theorem finSupport_bind_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [HasEvalFinset m] [DecidableEq β] [DecidableEq α] (mx : m α) (my : m β) :
(finSupport do let _ ← mx my) = if (finSupport mx).Nonempty then finSupport my else ∅
source
theorem probOutput_bind_of_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) {my : α → m β} {y : β} {r : ENNReal} (h : ∀ x ∈ support mx, Pr[=y | my x] = r) :
Pr[=y | mx >>= my] = (1 - Pr[⊥ | mx]) * r
source
@[simp]
theorem probOutput_bind_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : m β) (y : β) :
Pr[=y | do let _ ← mx my] = (1 - Pr[⊥ | mx]) * Pr[=y | my]
source
theorem probEvent_bind_of_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) {my : α → m β} {p : β → Prop} {r : ENNReal} (h : ∀ x ∈ support mx, Pr[p | my x] = r) :
Pr[p | mx >>= my] = (1 - Pr[⊥ | mx]) * r
source
@[simp]
theorem probEvent_bind_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : m β) (p : β → Prop) :
Pr[p | do let _ ← mx my] = (1 - Pr[⊥ | mx]) * Pr[p | my]
source
theorem probFailure_bind_of_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {my : α → m β} {r : ENNReal} (h : ∀ x ∈ support mx, Pr[⊥ | my x] = r) :
Pr[⊥ | mx >>= my] = Pr[⊥ | mx] + r * (1 - Pr[⊥ | mx])

Write the probability of mx >>= my failing given that my has constant failure chance over the possible outputs in support mx as a fixed expression without any sums.

source
theorem probFailure_bind_of_const' {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {my : α → m β} {r : ENNReal} (hr : r ≠ ⊤) (h : ∀ x ∈ support mx, Pr[⊥ | my x] = r) :
Pr[⊥ | mx >>= my] = Pr[⊥ | mx] + r - Pr[⊥ | mx] * r
source
@[simp]
theorem probFailure_bind_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : m β) :
Pr[⊥ | do let _ ← mx my] = Pr[⊥ | mx] + Pr[⊥ | my] - Pr[⊥ | mx] * Pr[⊥ | my]
source
theorem probFailure_bind_eq_sub_mul {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) (r : ENNReal) (hr : r ≠ ⊤) (h : ∀ x ∈ support mx, Pr[⊥ | my x] = r) :
Pr[⊥ | mx >>= my] = 1 - (1 - Pr[⊥ | mx]) * (1 - r)
source
theorem probFailure_bind_le_of_forall {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {s : ENNReal} (h' : Pr[⊥ | mx] ≤ s) (my : α → m β) {r : ENNReal} (hr : ∀ x ∈ support mx, Pr[⊥ | my x] ≤ r) :
Pr[⊥ | mx >>= my] ≤ s + (1 - s) * r
source
theorem probFailure_bind_le_of_forall' {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {s : ENNReal} (h' : Pr[⊥ | mx] = s) (my : α → m β) {r : ENNReal} (hr : ∀ x ∈ support mx, Pr[⊥ | my x] ≤ r) :
Pr[⊥ | mx >>= my] ≤ s + r

Version of probFailure_bind_le_of_forall with the 1 - s factor ommited for convenience.

source
theorem probFailure_bind_le_of_le_of_probFailure_eq_zero {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} (h' : Pr[⊥ | mx] = 0) {my : α → m β} {r : ENNReal} (hr : ∀ x ∈ support mx, Pr[⊥ | my x] ≤ r) :
Pr[⊥ | mx >>= my] ≤ r

Version of probFailure_bind_le_of_forall when mx never fails.

source
theorem probFailure_bind_of_probFailure_eq_zero {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} (h' : Pr[⊥ | mx] = 0) {my : α → m β} :
Pr[⊥ | mx >>= my] = ∑' (x : α), Pr[=x | mx] * Pr[⊥ | my x]