mathlib3 documentation

probability.probability_mass_function.constructions

Specific Constructions of Probability Mass Functions #

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

This file gives a number of different pmf constructions for common probability distributions.

map and seq allow pushing a pmf α along a function f : α → β (or distribution of functions f : pmf (α → β)) to get a pmf β

of_finset and of_fintype simplify the construction of a pmf α from a function f : α → ℝ≥0∞, by allowing the "sum equals 1" constraint to be in terms of finset.sum instead of tsum.

normalize constructs a pmf α by normalizing a function f : α → ℝ≥0∞ by its sum, and filter uses this to filter the support of a pmf and re-normalize the new distribution.

bernoulli represents the bernoulli distribution on bool

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

pmf β

The functorial action of a function on a pmf.

Equations

pmf.map f p = p.bind (pmf.pure ∘ f)

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

f <$> p = pmf.map f p

@[simp]

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

⇑(pmf.map f p) b = ∑' (a : α), ite (b = f a) (⇑p a) 0

@[simp]

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

(pmf.map f p).support = f '' p.support

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

b ∈ (pmf.map f p).support ↔ ∃ (a : α) (H : a ∈ p.support), f a = b

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

p.bind (pmf.pure ∘ f) = pmf.map f p

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

pmf.map id p = p

theorem pmf.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (p : pmf α) (g : β → γ) :

pmf.map g (pmf.map f p) = pmf.map (g ∘ f) p

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

pmf.map f (pmf.pure a) = pmf.pure (f a)

theorem pmf.map_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : pmf α) (q : α → pmf β) (f : β → γ) :

pmf.map f (p.bind q) = p.bind (λ (a : α), pmf.map f (q a))

@[simp]

theorem pmf.bind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : pmf α) (f : α → β) (q : β → pmf γ) :

(pmf.map f p).bind q = p.bind (q ∘ f)

@[simp]

theorem pmf.map_const {α : Type u_1} {β : Type u_2} (p : pmf α) (b : β) :

pmf.map (function.const α b) p = pmf.pure b

@[simp]

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

⇑((pmf.map f p).to_outer_measure) s = ⇑(p.to_outer_measure) (f ⁻¹' s)

@[simp]

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

⇑((pmf.map f p).to_measure) s = ⇑(p.to_measure) (f ⁻¹' s)

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

pmf β

The monadic sequencing operation for pmf.

Equations

q.seq p = q.bind (λ (m : α → β), p.bind (λ (a : α), pmf.pure (m a)))

theorem pmf.monad_seq_eq_seq {α β : Type u_1} (q : pmf (α → β)) (p : pmf α) :

q <*> p = q.seq p

@[simp]

theorem pmf.seq_apply {α : Type u_1} {β : Type u_2} (q : pmf (α → β)) (p : pmf α) (b : β) :

⇑(q.seq p) b = ∑' (f : α → β) (a : α), ite (b = f a) (⇑q f * ⇑p a) 0

@[simp]

theorem pmf.support_seq {α : Type u_1} {β : Type u_2} (q : pmf (α → β)) (p : pmf α) :

(q.seq p).support = ⋃ (f : α → β) (H : f ∈ q.support), f '' p.support

theorem pmf.mem_support_seq_iff {α : Type u_1} {β : Type u_2} (q : pmf (α → β)) (p : pmf α) (b : β) :

b ∈ (q.seq p).support ↔ ∃ (f : α → β) (H : f ∈ q.support), b ∈ f '' p.support

@[protected, instance]

def pmf.is_lawful_functor :

is_lawful_functor pmf

@[protected, instance]

def pmf.is_lawful_monad :

is_lawful_monad pmf

def pmf.of_finset {α : Type u_1} (f : α → ennreal) (s : finset α) (h : s.sum (λ (a : α), f a) = 1) (h' : ∀ (a : α), a ∉ s → f a = 0) :

pmf α

Given a finset s and a function f : α → ℝ≥0∞ with sum 1 on s, such that f a = 0 for a ∉ s, we get a pmf

Equations

pmf.of_finset f s h h' = ⟨f, _⟩

@[simp]

theorem pmf.of_finset_apply {α : Type u_1} {f : α → ennreal} {s : finset α} (h : s.sum (λ (a : α), f a) = 1) (h' : ∀ (a : α), a ∉ s → f a = 0) (a : α) :

⇑(pmf.of_finset f s h h') a = f a

@[simp]

theorem pmf.support_of_finset {α : Type u_1} {f : α → ennreal} {s : finset α} (h : s.sum (λ (a : α), f a) = 1) (h' : ∀ (a : α), a ∉ s → f a = 0) :

(pmf.of_finset f s h h').support = ↑s ∩ function.support f

theorem pmf.mem_support_of_finset_iff {α : Type u_1} {f : α → ennreal} {s : finset α} (h : s.sum (λ (a : α), f a) = 1) (h' : ∀ (a : α), a ∉ s → f a = 0) (a : α) :

a ∈ (pmf.of_finset f s h h').support ↔ a ∈ s ∧ f a ≠ 0

theorem pmf.of_finset_apply_of_not_mem {α : Type u_1} {f : α → ennreal} {s : finset α} (h : s.sum (λ (a : α), f a) = 1) (h' : ∀ (a : α), a ∉ s → f a = 0) {a : α} (ha : a ∉ s) :

⇑(pmf.of_finset f s h h') a = 0

@[simp]

theorem pmf.to_outer_measure_of_finset_apply {α : Type u_1} {f : α → ennreal} {s : finset α} (h : s.sum (λ (a : α), f a) = 1) (h' : ∀ (a : α), a ∉ s → f a = 0) (t : set α) :

⇑((pmf.of_finset f s h h').to_outer_measure) t = ∑' (x : α), t.indicator f x

@[simp]

theorem pmf.to_measure_of_finset_apply {α : Type u_1} {f : α → ennreal} {s : finset α} (h : s.sum (λ (a : α), f a) = 1) (h' : ∀ (a : α), a ∉ s → f a = 0) (t : set α) [measurable_space α] (ht : measurable_set t) :

⇑((pmf.of_finset f s h h').to_measure) t = ∑' (x : α), t.indicator f x

def pmf.of_fintype {α : Type u_1} [fintype α] (f : α → ennreal) (h : finset.univ.sum (λ (a : α), f a) = 1) :

pmf α

Given a finite type α and a function f : α → ℝ≥0∞ with sum 1, we get a pmf.

Equations

pmf.of_fintype f h = pmf.of_finset f finset.univ h _

@[simp]

theorem pmf.of_fintype_apply {α : Type u_1} [fintype α] {f : α → ennreal} (h : finset.univ.sum (λ (a : α), f a) = 1) (a : α) :

⇑(pmf.of_fintype f h) a = f a

@[simp]

theorem pmf.support_of_fintype {α : Type u_1} [fintype α] {f : α → ennreal} (h : finset.univ.sum (λ (a : α), f a) = 1) :

(pmf.of_fintype f h).support = function.support f

theorem pmf.mem_support_of_fintype_iff {α : Type u_1} [fintype α] {f : α → ennreal} (h : finset.univ.sum (λ (a : α), f a) = 1) (a : α) :

a ∈ (pmf.of_fintype f h).support ↔ f a ≠ 0

@[simp]

theorem pmf.to_outer_measure_of_fintype_apply {α : Type u_1} [fintype α] {f : α → ennreal} (h : finset.univ.sum (λ (a : α), f a) = 1) (s : set α) :

⇑((pmf.of_fintype f h).to_outer_measure) s = ∑' (x : α), s.indicator f x

@[simp]

theorem pmf.to_measure_of_fintype_apply {α : Type u_1} [fintype α] {f : α → ennreal} (h : finset.univ.sum (λ (a : α), f a) = 1) (s : set α) [measurable_space α] (hs : measurable_set s) :

⇑((pmf.of_fintype f h).to_measure) s = ∑' (x : α), s.indicator f x

noncomputable def pmf.normalize {α : Type u_1} (f : α → ennreal) (hf0 : tsum f ≠ 0) (hf : tsum f ≠ ⊤) :

pmf α

Given a f with non-zero and non-infinite sum, get a pmf by normalizing f by its tsum

Equations

pmf.normalize f hf0 hf = ⟨λ (a : α), f a * (∑' (x : α), f x)⁻¹, _⟩

@[simp]

theorem pmf.normalize_apply {α : Type u_1} {f : α → ennreal} (hf0 : tsum f ≠ 0) (hf : tsum f ≠ ⊤) (a : α) :

⇑(pmf.normalize f hf0 hf) a = f a * (∑' (x : α), f x)⁻¹

@[simp]

theorem pmf.support_normalize {α : Type u_1} {f : α → ennreal} (hf0 : tsum f ≠ 0) (hf : tsum f ≠ ⊤) :

(pmf.normalize f hf0 hf).support = function.support f

theorem pmf.mem_support_normalize_iff {α : Type u_1} {f : α → ennreal} (hf0 : tsum f ≠ 0) (hf : tsum f ≠ ⊤) (a : α) :

a ∈ (pmf.normalize f hf0 hf).support ↔ f a ≠ 0

noncomputable def pmf.filter {α : Type u_1} (p : pmf α) (s : set α) (h : ∃ (a : α) (H : a ∈ s), a ∈ p.support) :

pmf α

Create new pmf by filtering on a set with non-zero measure and normalizing

Equations

p.filter s h = pmf.normalize (s.indicator ⇑p) _ _

@[simp]

theorem pmf.filter_apply {α : Type u_1} {p : pmf α} {s : set α} (h : ∃ (a : α) (H : a ∈ s), a ∈ p.support) (a : α) :

⇑(p.filter s h) a = s.indicator ⇑p a * (∑' (a' : α), s.indicator ⇑p a')⁻¹

theorem pmf.filter_apply_eq_zero_of_not_mem {α : Type u_1} {p : pmf α} {s : set α} (h : ∃ (a : α) (H : a ∈ s), a ∈ p.support) {a : α} (ha : a ∉ s) :

⇑(p.filter s h) a = 0

theorem pmf.mem_support_filter_iff {α : Type u_1} {p : pmf α} {s : set α} (h : ∃ (a : α) (H : a ∈ s), a ∈ p.support) {a : α} :

a ∈ (p.filter s h).support ↔ a ∈ s ∧ a ∈ p.support

@[simp]

theorem pmf.support_filter {α : Type u_1} {p : pmf α} {s : set α} (h : ∃ (a : α) (H : a ∈ s), a ∈ p.support) :

(p.filter s h).support = s ∩ p.support

theorem pmf.filter_apply_eq_zero_iff {α : Type u_1} {p : pmf α} {s : set α} (h : ∃ (a : α) (H : a ∈ s), a ∈ p.support) (a : α) :

⇑(p.filter s h) a = 0 ↔ a ∉ s ∨ a ∉ p.support

theorem pmf.filter_apply_ne_zero_iff {α : Type u_1} {p : pmf α} {s : set α} (h : ∃ (a : α) (H : a ∈ s), a ∈ p.support) (a : α) :

⇑(p.filter s h) a ≠ 0 ↔ a ∈ s ∧ a ∈ p.support

noncomputable def pmf.bernoulli (p : ennreal) (h : p ≤ 1) :

A pmf which assigns probability p to tt and 1 - p to ff.

Equations

pmf.bernoulli p h = pmf.of_fintype (λ (b : bool), cond b p (1 - p)) _

@[simp]

theorem pmf.bernoulli_apply {p : ennreal} (h : p ≤ 1) (b : bool) :

⇑(pmf.bernoulli p h) b = cond b p (1 - p)

@[simp]

theorem pmf.support_bernoulli {p : ennreal} (h : p ≤ 1) :

(pmf.bernoulli p h).support = {b : bool | cond b (p ≠ 0) (p ≠ 1)}

theorem pmf.mem_support_bernoulli_iff {p : ennreal} (h : p ≤ 1) (b : bool) :

b ∈ (pmf.bernoulli p h).support ↔ cond b (p ≠ 0) (p ≠ 1)