mathlib3 documentation

probability.probability_mass_function.monad

Monad Operations for Probability Mass Functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : β.

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

noncomputable 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

pmf.pure a = ⟨λ (a' : α), ite (a' = a) 1 0, _⟩

@[simp]

theorem pmf.pure_apply {α : Type u_1} (a a' : α) :

⇑(pmf.pure a) a' = ite (a' = a) 1 0

@[simp]

theorem pmf.support_pure {α : Type u_1} (a : α) :

(pmf.pure a).support = {a}

theorem pmf.mem_support_pure_iff {α : Type u_1} (a a' : α) :

a' ∈ (pmf.pure a).support ↔ a' = a

@[simp]

theorem pmf.pure_apply_self {α : Type u_1} (a : α) :

⇑(pmf.pure a) a = 1

theorem pmf.pure_apply_of_ne {α : Type u_1} (a a' : α) (h : a' ≠ a) :

⇑(pmf.pure a) a' = 0

@[protected, instance]

noncomputable def pmf.inhabited {α : Type u_1} [inhabited α] :

inhabited (pmf α)

Equations

pmf.inhabited = {default := pmf.pure inhabited.default}

@[simp]

theorem pmf.to_outer_measure_pure_apply {α : Type u_1} (a : α) (s : set α) :

⇑((pmf.pure a).to_outer_measure) s = ite (a ∈ s) 1 0

@[simp]

theorem pmf.to_measure_pure_apply {α : Type u_1} (a : α) (s : set α) [measurable_space α] (hs : measurable_set s) :

⇑((pmf.pure a).to_measure) s = ite (a ∈ s) 1 0

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

theorem pmf.to_measure_pure {α : Type u_1} (a : α) [measurable_space α] :

(pmf.pure a).to_measure = measure_theory.measure.dirac a

@[simp]

theorem pmf.to_pmf_dirac {α : Type u_1} (a : α) [measurable_space α] [countable α] [h : measurable_singleton_class α] :

(measure_theory.measure.dirac a).to_pmf = pmf.pure a

noncomputable def pmf.bind {α : Type u_1} {β : Type u_2} (p : pmf α) (f : α → pmf β) :

pmf β

The monadic bind operation for pmf.

Equations

p.bind f = ⟨λ (b : β), ∑' (a : α), ⇑p a * ⇑(f a) b, _⟩

@[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 = ⋃ (a : α) (H : a ∈ p.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 ↔ ∃ (a : α) (H : a ∈ p.support), b ∈ (f a).support

@[simp]

theorem pmf.pure_bind {α : Type u_1} {β : Type u_2} (a : α) (f : α → pmf β) :

(pmf.pure a).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 (λ (_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 (λ (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 (λ (a : α), q.bind (f a)) = q.bind (λ (b : β), p.bind (λ (a : α), f a b))

@[simp]

theorem pmf.to_outer_measure_bind_apply {α : Type u_1} {β : Type u_2} (p : pmf α) (f : α → pmf β) (s : set β) :

⇑((p.bind f).to_outer_measure) s = ∑' (a : α), ⇑p a * ⇑((f a).to_outer_measure) s

@[simp]

theorem pmf.to_measure_bind_apply {α : Type u_1} {β : Type u_2} (p : pmf α) (f : α → pmf β) (s : set β) [measurable_space β] (hs : measurable_set s) :

⇑((p.bind f).to_measure) s = ∑' (a : α), ⇑p a * ⇑((f a).to_measure) 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

@[protected, instance]

noncomputable def pmf.monad :

Equations

pmf.monad = monad.mk

noncomputable def pmf.bind_on_support {α : Type u_1} {β : Type u_2} (p : pmf α) (f : Π (a : α), a ∈ p.support → pmf β) :

pmf β

Generalized version of bind allowing f to only be defined on the support of p. p.bind f is equivalent to p.bind_on_support (λ a _, f a), see bind_on_support_eq_bind

Equations

p.bind_on_support f = ⟨λ (b : β), ∑' (a : α), ⇑p a * dite (⇑p a = 0) (λ (h : ⇑p a = 0), 0) (λ (h : ¬⇑p a = 0), ⇑(f a h) b), _⟩

@[simp]

theorem pmf.bind_on_support_apply {α : Type u_1} {β : Type u_2} {p : pmf α} (f : Π (a : α), a ∈ p.support → pmf β) (b : β) :

⇑(p.bind_on_support f) b = ∑' (a : α), ⇑p a * dite (⇑p a = 0) (λ (h : ⇑p a = 0), 0) (λ (h : ¬⇑p a = 0), ⇑(f a h) b)

@[simp]

theorem pmf.support_bind_on_support {α : Type u_1} {β : Type u_2} {p : pmf α} (f : Π (a : α), a ∈ p.support → pmf β) :

(p.bind_on_support f).support = ⋃ (a : α) (h : a ∈ p.support), (f a h).support

theorem pmf.mem_support_bind_on_support_iff {α : Type u_1} {β : Type u_2} {p : pmf α} (f : Π (a : α), a ∈ p.support → pmf β) (b : β) :

b ∈ (p.bind_on_support f).support ↔ ∃ (a : α) (h : a ∈ p.support), b ∈ (f a h).support

@[simp]

theorem pmf.bind_on_support_eq_bind {α : Type u_1} {β : Type u_2} (p : pmf α) (f : α → pmf β) :

p.bind_on_support (λ (a : α) (_x : a ∈ p.support), f a) = p.bind f

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

theorem pmf.bind_on_support_eq_zero_iff {α : Type u_1} {β : Type u_2} {p : pmf α} (f : Π (a : α), a ∈ p.support → pmf β) (b : β) :

⇑(p.bind_on_support f) b = 0 ↔ ∀ (a : α) (ha : ⇑p a ≠ 0), ⇑(f a ha) b = 0

@[simp]

theorem pmf.pure_bind_on_support {α : Type u_1} {β : Type u_2} (a : α) (f : Π (a' : α), a' ∈ (pmf.pure a).support → pmf β) :

(pmf.pure a).bind_on_support f = f a _

theorem pmf.bind_on_support_pure {α : Type u_1} (p : pmf α) :

p.bind_on_support (λ (a : α) (_x : a ∈ p.support), pmf.pure a) = p

@[simp]

theorem pmf.bind_on_support_bind_on_support {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : pmf α) (f : Π (a : α), a ∈ p.support → pmf β) (g : Π (b : β), b ∈ (p.bind_on_support f).support → pmf γ) :

(p.bind_on_support f).bind_on_support g = p.bind_on_support (λ (a : α) (ha : a ∈ p.support), (f a ha).bind_on_support (λ (b : β) (hb : b ∈ (f a ha).support), g b _))

theorem pmf.bind_on_support_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : pmf α) (q : pmf β) (f : Π (a : α), a ∈ p.support → Π (b : β), b ∈ q.support → pmf γ) :

p.bind_on_support (λ (a : α) (ha : a ∈ p.support), q.bind_on_support (f a ha)) = q.bind_on_support (λ (b : β) (hb : b ∈ q.support), p.bind_on_support (λ (a : α) (ha : a ∈ p.support), f a ha b hb))

@[simp]

theorem pmf.to_outer_measure_bind_on_support_apply {α : Type u_1} {β : Type u_2} {p : pmf α} (f : Π (a : α), a ∈ p.support → pmf β) (s : set β) :

⇑((p.bind_on_support f).to_outer_measure) s = ∑' (a : α), ⇑p a * dite (⇑p a = 0) (λ (h : ⇑p a = 0), 0) (λ (h : ¬⇑p a = 0), ⇑((f a h).to_outer_measure) s)

@[simp]

theorem pmf.to_measure_bind_on_support_apply {α : Type u_1} {β : Type u_2} {p : pmf α} (f : Π (a : α), a ∈ p.support → pmf β) (s : set β) [measurable_space β] (hs : measurable_set s) :

⇑((p.bind_on_support f).to_measure) s = ∑' (a : α), ⇑p a * dite (⇑p a = 0) (λ (h : ⇑p a = 0), 0) (λ (h : ¬⇑p a = 0), ⇑((f a h).to_measure) s)

The measure of a set under p.bind_on_support 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