mathlib documentation

measure_theory.probability_mass_function.constructions

Specific Constructions of Probability Mass Functions #

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. of_multiset, uniform_of_finset, and uniform_of_fintype construct probability mass functions from the corresponding object, with proportional weighting for each element of the object.

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.

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.

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
@[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 α) :
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 α) :
theorem pmf.map_id {α : Type u_1} (p : pmf α) :
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 : α) :
noncomputable def pmf.seq {α : Type u_1} {β : Type u_2} (q : pmf (α → β)) (p : pmf α) :
pmf β

The monadic sequencing operation for pmf.

Equations
@[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
def pmf.of_finset {α : Type u_1} (f : α → ℝ≥0) (s : finset α) (h : ∑ (a : α) in s, f a = 1) (h' : ∀ (a : α), a sf 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
@[simp]
theorem pmf.of_finset_apply {α : Type u_1} {f : α → ℝ≥0} {s : finset α} (h : ∑ (a : α) in s, f a = 1) (h' : ∀ (a : α), a sf a = 0) (a : α) :
(pmf.of_finset f s h h') a = f a
@[simp]
theorem pmf.support_of_finset {α : Type u_1} {f : α → ℝ≥0} {s : finset α} (h : ∑ (a : α) in s, f a = 1) (h' : ∀ (a : α), a sf a = 0) :
theorem pmf.mem_support_of_finset_iff {α : Type u_1} {f : α → ℝ≥0} {s : finset α} (h : ∑ (a : α) in s, f a = 1) (h' : ∀ (a : α), a sf 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 : α → ℝ≥0} {s : finset α} (h : ∑ (a : α) in s, f a = 1) (h' : ∀ (a : α), a sf a = 0) {a : α} (ha : a s) :
(pmf.of_finset f s h h') a = 0
def pmf.of_fintype {α : Type u_1} [fintype α] (f : α → ℝ≥0) (h : ∑ (a : α), f a = 1) :
pmf α

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

Equations
@[simp]
theorem pmf.of_fintype_apply {α : Type u_1} [fintype α] {f : α → ℝ≥0} (h : ∑ (a : α), f a = 1) (a : α) :
(pmf.of_fintype f h) a = f a
@[simp]
theorem pmf.support_of_fintype {α : Type u_1} [fintype α] {f : α → ℝ≥0} (h : ∑ (a : α), f a = 1) :
theorem pmf.mem_support_of_fintype_iff {α : Type u_1} [fintype α] {f : α → ℝ≥0} (h : ∑ (a : α), f a = 1) (a : α) :
noncomputable def pmf.of_multiset {α : Type u_1} (s : multiset α) (hs : s 0) :
pmf α

Given a non-empty multiset s we construct the pmf which sends a to the fraction of elements in s that are a.

Equations
@[simp]
theorem pmf.of_multiset_apply {α : Type u_1} {s : multiset α} (hs : s 0) (a : α) :
@[simp]
theorem pmf.support_of_multiset {α : Type u_1} {s : multiset α} (hs : s 0) :
theorem pmf.mem_support_of_multiset_iff {α : Type u_1} {s : multiset α} (hs : s 0) (a : α) :
theorem pmf.of_multiset_apply_of_not_mem {α : Type u_1} {s : multiset α} (hs : s 0) {a : α} (ha : a s) :
noncomputable def pmf.uniform_of_finset {α : Type u_1} (s : finset α) (hs : s.nonempty) :
pmf α

Uniform distribution taking the same non-zero probability on the nonempty finset s

Equations
@[simp]
theorem pmf.uniform_of_finset_apply {α : Type u_1} {s : finset α} (hs : s.nonempty) (a : α) :
theorem pmf.uniform_of_finset_apply_of_mem {α : Type u_1} {s : finset α} (hs : s.nonempty) {a : α} (ha : a s) :
theorem pmf.uniform_of_finset_apply_of_not_mem {α : Type u_1} {s : finset α} (hs : s.nonempty) {a : α} (ha : a s) :
@[simp]
theorem pmf.support_uniform_of_finset {α : Type u_1} {s : finset α} (hs : s.nonempty) :
theorem pmf.mem_support_uniform_of_finset_iff {α : Type u_1} {s : finset α} (hs : s.nonempty) (a : α) :
noncomputable def pmf.uniform_of_fintype (α : Type u_1) [fintype α] [nonempty α] :
pmf α

The uniform pmf taking the same uniform value on all of the fintype α

Equations
@[simp]
theorem pmf.uniform_of_fintype_apply {α : Type u_1} [fintype α] [nonempty α] (a : α) :
@[simp]
theorem pmf.mem_support_uniform_of_fintype_iff {α : Type u_1} [fintype α] [nonempty α] (a : α) :
noncomputable def pmf.normalize {α : Type u_1} (f : α → ℝ≥0) (hf0 : tsum f 0) :
pmf α

Given a f with non-zero sum, we get a pmf by normalizing f by it's tsum

Equations
@[simp]
theorem pmf.normalize_apply {α : Type u_1} {f : α → ℝ≥0} (hf0 : tsum f 0) (a : α) :
(pmf.normalize f hf0) a = (f a) * (∑' (x : α), f x)⁻¹
@[simp]
theorem pmf.support_normalize {α : Type u_1} {f : α → ℝ≥0} (hf0 : tsum f 0) :
theorem pmf.mem_support_normalize_iff {α : Type u_1} {f : α → ℝ≥0} (hf0 : tsum f 0) (a : α) :
a (pmf.normalize f hf0).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
@[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
@[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.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
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 : ℝ≥0) (h : p 1) :

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

Equations
@[simp]
theorem pmf.bernoulli_apply {p : ℝ≥0} (h : p 1) (b : bool) :
(pmf.bernoulli p h) b = cond b p (1 - p)
@[simp]
theorem pmf.support_bernoulli {p : ℝ≥0} (h : p 1) :
(pmf.bernoulli p h).support = {b : bool | cond b (p 0) (p 1)}
theorem pmf.mem_support_bernoulli_iff {p : ℝ≥0} (h : p 1) (b : bool) :
b (pmf.bernoulli p h).support cond b (p 0) (p 1)
@[protected]
theorem pmf.bind_on_support.summable {α : Type u_1} {β : Type u_2} (p : pmf α) (f : Π (a : α), a p.supportpmf β) (b : β) :
summable (λ (a : α), (p a) * dite (p a = 0) (λ (h : p a = 0), 0) (λ (h : ¬p a = 0), (f a h) b))
noncomputable def pmf.bind_on_support {α : 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.bind_on_support (λ a _, f a), see bind_on_support_eq_bind

Equations
@[simp]
theorem pmf.bind_on_support_apply {α : Type u_1} {β : Type u_2} {p : pmf α} (f : Π (a : α), a p.supportpmf β) (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.supportpmf β) :
(p.bind_on_support f).support = {b : β | ∃ (a : α) (h : a p.support), b (f a h).support}
theorem pmf.mem_support_bind_on_support_iff {α : Type u_1} {β : Type u_2} {p : pmf α} (f : Π (a : α), a p.supportpmf β) (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.coe_bind_on_support_apply {α : Type u_1} {β : Type u_2} {p : pmf α} (f : Π (a : α), a p.supportpmf β) (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))
theorem pmf.bind_on_support_eq_zero_iff {α : Type u_1} {β : Type u_2} {p : pmf α} (f : Π (a : α), a p.supportpmf β) (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).supportpmf β) :
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.supportpmf β) (g : Π (b : β), b (p.bind_on_support f).supportpmf γ) :
(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.supportpmf γ) :
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))