# Monad Operations for Probability Mass Functions #

This file constructs two operations on PMF that give it a monad structure. pure a is the distribution where a single value a has probability 1. bind pa pb : PMF β is the distribution given by sampling a : α from pa : PMF α, and then sampling from pb a : PMF β to get a final result b : β.

bindOnSupport generalizes bind to allow binding to a partial function, so that the second argument only needs to be defined on the support of the first argument.

def PMF.pure {α : Type u_1} (a : α) :
PMF α

The pure PMF is the PMF where all the mass lies in one point. The value of pure a is 1 at a and 0 elsewhere.

Equations
• = fun (a' : α) => if a' = a then 1 else 0,
Instances For
@[simp]
theorem PMF.pure_apply {α : Type u_1} (a : α) (a' : α) :
() a' = if a' = a then 1 else 0
@[simp]
theorem PMF.support_pure {α : Type u_1} (a : α) :
().support = {a}
theorem PMF.mem_support_pure_iff {α : Type u_1} (a : α) (a' : α) :
a' ().support a' = a
theorem PMF.pure_apply_self {α : Type u_1} (a : α) :
() a = 1
theorem PMF.pure_apply_of_ne {α : Type u_1} (a : α) (a' : α) (h : a' a) :
() a' = 0
instance PMF.instInhabited {α : Type u_1} [] :
Equations
• PMF.instInhabited = { default := PMF.pure default }
@[simp]
theorem PMF.toOuterMeasure_pure_apply {α : Type u_1} (a : α) (s : Set α) :
().toOuterMeasure s = if a s then 1 else 0
@[simp]
theorem PMF.toMeasure_pure_apply {α : Type u_1} (a : α) (s : Set α) [] (hs : ) :
().toMeasure s = if a s then 1 else 0

The measure of a set under pure a is 1 for sets containing a and 0 otherwise.

theorem PMF.toMeasure_pure {α : Type u_1} (a : α) [] :
().toMeasure =
@[simp]
theorem PMF.toPMF_dirac {α : Type u_1} (a : α) [] [] [h : ] :
.toPMF =
def PMF.bind {α : Type u_1} {β : Type u_2} (p : PMF α) (f : αPMF β) :
PMF β

The monadic bind operation for PMF.

Equations
• p.bind f = fun (b : β) => ∑' (a : α), p a * (f a) b,
Instances For
@[simp]
theorem PMF.bind_apply {α : Type u_1} {β : Type u_2} (p : PMF α) (f : αPMF β) (b : β) :
(p.bind f) b = ∑' (a : α), p a * (f a) b
@[simp]
theorem PMF.support_bind {α : Type u_1} {β : Type u_2} (p : PMF α) (f : αPMF β) :
(p.bind f).support = ap.support, (f a).support
theorem PMF.mem_support_bind_iff {α : Type u_1} {β : Type u_2} (p : PMF α) (f : αPMF β) (b : β) :
b (p.bind f).support ap.support, b (f a).support
@[simp]
theorem PMF.pure_bind {α : Type u_1} {β : Type u_2} (a : α) (f : αPMF β) :
().bind f = f a
@[simp]
theorem PMF.bind_pure {α : Type u_1} (p : PMF α) :
p.bind PMF.pure = p
@[simp]
theorem PMF.bind_const {α : Type u_1} {β : Type u_2} (p : PMF α) (q : PMF β) :
(p.bind fun (x : α) => q) = q
@[simp]
theorem PMF.bind_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : PMF α) (f : αPMF β) (g : βPMF γ) :
(p.bind f).bind g = p.bind fun (a : α) => (f a).bind g
theorem PMF.bind_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : PMF α) (q : PMF β) (f : αβPMF γ) :
(p.bind fun (a : α) => q.bind (f a)) = q.bind fun (b : β) => p.bind fun (a : α) => f a b
@[simp]
theorem PMF.toOuterMeasure_bind_apply {α : Type u_1} {β : Type u_2} (p : PMF α) (f : αPMF β) (s : Set β) :
(p.bind f).toOuterMeasure s = ∑' (a : α), p a * (f a).toOuterMeasure s
@[simp]
theorem PMF.toMeasure_bind_apply {α : Type u_1} {β : Type u_2} (p : PMF α) (f : αPMF β) (s : Set β) [] (hs : ) :
(p.bind f).toMeasure s = ∑' (a : α), p a * (f a).toMeasure s

The measure of a set under p.bind f is the sum over a : α of the probability of a under p times the measure of the set under f a.

Equations
def PMF.bindOnSupport {α : Type u_1} {β : Type u_2} (p : PMF α) (f : (a : α) → a p.supportPMF β) :
PMF β

Generalized version of bind allowing f to only be defined on the support of p. p.bind f is equivalent to p.bindOnSupport (fun a _ ↦ f a), see bindOnSupport_eq_bind.

Equations
• p.bindOnSupport f = fun (b : β) => ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) b,
Instances For
@[simp]
theorem PMF.bindOnSupport_apply {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a p.supportPMF β) (b : β) :
(p.bindOnSupport f) b = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) b
@[simp]
theorem PMF.support_bindOnSupport {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a p.supportPMF β) :
(p.bindOnSupport f).support = ⋃ (a : α), ⋃ (h : a p.support), (f a h).support
theorem PMF.mem_support_bindOnSupport_iff {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a p.supportPMF β) (b : β) :
b (p.bindOnSupport f).support ∃ (a : α) (h : a p.support), b (f a h).support
@[simp]
theorem PMF.bindOnSupport_eq_bind {α : Type u_1} {β : Type u_2} (p : PMF α) (f : αPMF β) :
(p.bindOnSupport fun (a : α) (x : a p.support) => f a) = p.bind f

bindOnSupport reduces to bind if f doesn't depend on the additional hypothesis.

theorem PMF.bindOnSupport_eq_zero_iff {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a p.supportPMF β) (b : β) :
(p.bindOnSupport f) b = 0 ∀ (a : α) (ha : p a 0), (f a ha) b = 0
@[simp]
theorem PMF.pure_bindOnSupport {α : Type u_1} {β : Type u_2} (a : α) (f : (a' : α) → a' ().supportPMF β) :
().bindOnSupport f = f a
theorem PMF.bindOnSupport_pure {α : Type u_1} (p : PMF α) :
(p.bindOnSupport fun (a : α) (x : a p.support) => ) = p
@[simp]
theorem PMF.bindOnSupport_bindOnSupport {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : PMF α) (f : (a : α) → a p.supportPMF β) (g : (b : β) → b (p.bindOnSupport f).supportPMF γ) :
(p.bindOnSupport f).bindOnSupport g = p.bindOnSupport fun (a : α) (ha : a p.support) => (f a ha).bindOnSupport fun (b : β) (hb : b (f a ha).support) => g b
theorem PMF.bindOnSupport_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : PMF α) (q : PMF β) (f : (a : α) → a p.support(b : β) → b q.supportPMF γ) :
(p.bindOnSupport fun (a : α) (ha : a p.support) => q.bindOnSupport (f a ha)) = q.bindOnSupport fun (b : β) (hb : b q.support) => p.bindOnSupport fun (a : α) (ha : a p.support) => f a ha b hb
@[simp]
theorem PMF.toOuterMeasure_bindOnSupport_apply {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a p.supportPMF β) (s : Set β) :
(p.bindOnSupport f).toOuterMeasure s = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h).toOuterMeasure s
@[simp]
theorem PMF.toMeasure_bindOnSupport_apply {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a p.supportPMF β) (s : Set β) [] (hs : ) :
(p.bindOnSupport f).toMeasure s = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h).toMeasure s

The measure of a set under p.bindOnSupport f is the sum over a : α of the probability of a under p times the measure of the set under f a _. The additional if statement is needed since f is only a partial function.