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.
@[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)
@[simp]
theorem
pmf.of_finset_apply
{α : Type u_1}
{f : α → ℝ≥0}
{s : finset α}
(h : ∑ (a : α) in s, 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 : α → ℝ≥0}
{s : finset α}
(h : ∑ (a : α) in s, f a = 1)
(h' : ∀ (a : α), a ∉ s → f a = 0) :
(pmf.of_finset f s h h').support = ↑s ∩ function.support f
@[simp]
theorem
pmf.to_outer_measure_of_finset_apply
{α : Type u_1}
{f : α → ℝ≥0}
{s : finset α}
(h : ∑ (a : α) in s, 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 : α → ℝ≥0}
{s : finset α}
(h : ∑ (a : α) in s, 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
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 : α → ℝ≥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) :
(pmf.of_fintype f h).support = function.support f
theorem
pmf.mem_support_of_fintype_iff
{α : Type u_1}
[fintype α]
{f : α → ℝ≥0}
(h : ∑ (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 : α → ℝ≥0}
(h : ∑ (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 : α → ℝ≥0}
(h : ∑ (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
Given a non-empty multiset s we construct the pmf which sends a to the fraction of
elements in s that are a.
Equations
- pmf.of_multiset s hs = ⟨λ (a : α), ↑(multiset.count a s) / ↑(⇑multiset.card s), _⟩
@[simp]
theorem
pmf.of_multiset_apply
{α : Type u_1}
{s : multiset α}
(hs : s ≠ 0)
(a : α) :
⇑(pmf.of_multiset s hs) a = ↑(multiset.count a s) / ↑(⇑multiset.card s)
@[simp]
theorem
pmf.support_of_multiset
{α : Type u_1}
{s : multiset α}
(hs : s ≠ 0) :
(pmf.of_multiset s hs).support = ↑(s.to_finset)
theorem
pmf.of_multiset_apply_of_not_mem
{α : Type u_1}
{s : multiset α}
(hs : s ≠ 0)
{a : α}
(ha : a ∉ s) :
⇑(pmf.of_multiset s hs) a = 0
@[simp]
theorem
pmf.to_outer_measure_of_multiset_apply
{α : Type u_1}
{s : multiset α}
(hs : s ≠ 0)
(t : set α) :
⇑((pmf.of_multiset s hs).to_outer_measure) t = (∑' (x : α), ↑(multiset.count x (multiset.filter (λ (_x : α), _x ∈ t) s))) / ↑(⇑multiset.card s)
@[simp]
theorem
pmf.to_measure_of_multiset_apply
{α : Type u_1}
{s : multiset α}
(hs : s ≠ 0)
(t : set α)
[measurable_space α]
(ht : measurable_set t) :
⇑((pmf.of_multiset s hs).to_measure) t = (∑' (x : α), ↑(multiset.count x (multiset.filter (λ (_x : α), _x ∈ t) s))) / ↑(⇑multiset.card s)
Uniform distribution taking the same non-zero probability on the nonempty finset s
Equations
- pmf.uniform_of_finset s hs = pmf.of_finset (λ (a : α), ite (a ∈ s) (↑(s.card))⁻¹ 0) s _ _
theorem
pmf.uniform_of_finset_apply_of_not_mem
{α : Type u_1}
{s : finset α}
(hs : s.nonempty)
{a : α}
(ha : a ∉ s) :
⇑(pmf.uniform_of_finset s hs) a = 0
@[simp]
theorem
pmf.support_uniform_of_finset
{α : Type u_1}
{s : finset α}
(hs : s.nonempty) :
(pmf.uniform_of_finset s hs).support = ↑s
theorem
pmf.mem_support_uniform_of_finset_iff
{α : Type u_1}
{s : finset α}
(hs : s.nonempty)
(a : α) :
a ∈ (pmf.uniform_of_finset s hs).support ↔ a ∈ s
@[simp]
theorem
pmf.to_outer_measure_uniform_of_finset_apply
{α : Type u_1}
{s : finset α}
(hs : s.nonempty)
(t : set α) :
⇑((pmf.uniform_of_finset s hs).to_outer_measure) t = ↑((finset.filter (λ (_x : α), _x ∈ t) s).card) / ↑(s.card)
@[simp]
theorem
pmf.to_measure_uniform_of_finset_apply
{α : Type u_1}
{s : finset α}
(hs : s.nonempty)
(t : set α)
[measurable_space α]
(ht : measurable_set t) :
⇑((pmf.uniform_of_finset s hs).to_measure) t = ↑((finset.filter (λ (_x : α), _x ∈ t) s).card) / ↑(s.card)
The uniform pmf taking the same uniform value on all of the fintype α
@[simp]
theorem
pmf.uniform_of_fintype_apply
{α : Type u_1}
[fintype α]
[nonempty α]
(a : α) :
⇑(pmf.uniform_of_fintype α) a = (↑(fintype.card α))⁻¹
@[simp]
theorem
pmf.mem_support_uniform_of_fintype
{α : Type u_1}
[fintype α]
[nonempty α]
(a : α) :
a ∈ (pmf.uniform_of_fintype α).support
theorem
pmf.to_outer_measure_uniform_of_fintype_apply
{α : Type u_1}
[fintype α]
[nonempty α]
(s : set α) :
⇑((pmf.uniform_of_fintype α).to_outer_measure) s = ↑(fintype.card ↥s) / ↑(fintype.card α)
theorem
pmf.to_measure_uniform_of_fintype_apply
{α : Type u_1}
[fintype α]
[nonempty α]
(s : set α)
[measurable_space α]
(hs : measurable_set s) :
⇑((pmf.uniform_of_fintype α).to_measure) s = ↑(fintype.card ↥s) / ↑(fintype.card α)
@[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) :
(pmf.normalize f hf0).support = function.support f
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
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 : ℝ≥0}
(h : p ≤ 1)
(b : bool) :
⇑(pmf.bernoulli p h) b = cond b p (1 - p)