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.
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.support_of_finset
{α : Type u_1}
{f : α → nnreal}
{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
@[simp]
theorem
pmf.to_outer_measure_of_finset_apply
{α : Type u_1}
{f : α → nnreal}
{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 : α → nnreal}
{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 : α → nnreal)
(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 : α → nnreal}
(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 : α → nnreal}
(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 : α → nnreal}
(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 : α → nnreal}
(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 : α → nnreal}
(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
@[simp]
theorem
pmf.normalize_apply
{α : Type u_1}
{f : α → nnreal}
(hf0 : tsum f ≠ 0)
(a : α) :
⇑(pmf.normalize f hf0) a = f a * (∑' (x : α), f x)⁻¹
@[simp]
theorem
pmf.support_normalize
{α : Type u_1}
{f : α → nnreal}
(hf0 : tsum f ≠ 0) :
(pmf.normalize f hf0).support = function.support f
theorem
pmf.mem_support_normalize_iff
{α : Type u_1}
{f : α → nnreal}
(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 : nnreal}
(h : p ≤ 1)
(b : bool) :
⇑(pmf.bernoulli p h) b = cond b p (1 - p)