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 β
.
ofFinset
and ofFintype
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.support_map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(p : Pmf α)
:
Pmf.support (Pmf.map f p) = f '' Pmf.support p
theorem
Pmf.mem_support_map_iff
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(p : Pmf α)
(b : β)
:
b ∈ Pmf.support (Pmf.map f p) ↔ ∃ a, a ∈ Pmf.support p ∧ f a = b
@[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.toOuterMeasure_map_apply
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(p : Pmf α)
(s : Set β)
:
↑(Pmf.toOuterMeasure (Pmf.map f p)) s = ↑(Pmf.toOuterMeasure p) (f ⁻¹' s)
@[simp]
theorem
Pmf.toMeasure_map_apply
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(p : Pmf α)
(s : Set β)
[MeasurableSpace α]
[MeasurableSpace β]
(hf : Measurable f)
(hs : MeasurableSet s)
:
↑↑(Pmf.toMeasure (Pmf.map f p)) s = ↑↑(Pmf.toMeasure p) (f ⁻¹' s)
@[simp]
theorem
Pmf.support_seq
{α : Type u_1}
{β : Type u_2}
(q : Pmf (α → β))
(p : Pmf α)
:
Pmf.support (Pmf.seq q p) = ⋃ (f : α → β) (_ : f ∈ Pmf.support q), f '' Pmf.support p
theorem
Pmf.mem_support_seq_iff
{α : Type u_1}
{β : Type u_2}
(q : Pmf (α → β))
(p : Pmf α)
(b : β)
:
b ∈ Pmf.support (Pmf.seq q p) ↔ ∃ f, f ∈ Pmf.support q ∧ b ∈ f '' Pmf.support p
@[simp]
theorem
Pmf.ofFinset_apply
{α : Type u_1}
{f : α → ENNReal}
{s : Finset α}
(h : (Finset.sum s fun a => f a) = 1)
(h' : ∀ (a : α), ¬a ∈ s → f a = 0)
(a : α)
:
↑(Pmf.ofFinset f s h h') a = f a
@[simp]
theorem
Pmf.support_ofFinset
{α : Type u_1}
{f : α → ENNReal}
{s : Finset α}
(h : (Finset.sum s fun a => f a) = 1)
(h' : ∀ (a : α), ¬a ∈ s → f a = 0)
:
Pmf.support (Pmf.ofFinset f s h h') = ↑s ∩ Function.support f
theorem
Pmf.mem_support_ofFinset_iff
{α : Type u_1}
{f : α → ENNReal}
{s : Finset α}
(h : (Finset.sum s fun a => f a) = 1)
(h' : ∀ (a : α), ¬a ∈ s → f a = 0)
(a : α)
:
a ∈ Pmf.support (Pmf.ofFinset f s h h') ↔ a ∈ s ∧ f a ≠ 0
theorem
Pmf.ofFinset_apply_of_not_mem
{α : Type u_1}
{f : α → ENNReal}
{s : Finset α}
(h : (Finset.sum s fun a => f a) = 1)
(h' : ∀ (a : α), ¬a ∈ s → f a = 0)
{a : α}
(ha : ¬a ∈ s)
:
↑(Pmf.ofFinset f s h h') a = 0
@[simp]
theorem
Pmf.toOuterMeasure_ofFinset_apply
{α : Type u_1}
{f : α → ENNReal}
{s : Finset α}
(h : (Finset.sum s fun a => f a) = 1)
(h' : ∀ (a : α), ¬a ∈ s → f a = 0)
(t : Set α)
:
↑(Pmf.toOuterMeasure (Pmf.ofFinset f s h h')) t = ∑' (x : α), Set.indicator t f x
@[simp]
theorem
Pmf.toMeasure_ofFinset_apply
{α : Type u_1}
{f : α → ENNReal}
{s : Finset α}
(h : (Finset.sum s fun a => f a) = 1)
(h' : ∀ (a : α), ¬a ∈ s → f a = 0)
(t : Set α)
[MeasurableSpace α]
(ht : MeasurableSet t)
:
↑↑(Pmf.toMeasure (Pmf.ofFinset f s h h')) t = ∑' (x : α), Set.indicator t f x
def
Pmf.ofFintype
{α : Type u_1}
[Fintype α]
(f : α → ENNReal)
(h : (Finset.sum Finset.univ fun a => f a) = 1)
:
Pmf α
Given a finite type α
and a function f : α → ℝ≥0∞
with sum 1, we get a Pmf
.
Instances For
@[simp]
theorem
Pmf.ofFintype_apply
{α : Type u_1}
[Fintype α]
{f : α → ENNReal}
(h : (Finset.sum Finset.univ fun a => f a) = 1)
(a : α)
:
↑(Pmf.ofFintype f h) a = f a
@[simp]
theorem
Pmf.support_ofFintype
{α : Type u_1}
[Fintype α]
{f : α → ENNReal}
(h : (Finset.sum Finset.univ fun a => f a) = 1)
:
Pmf.support (Pmf.ofFintype f h) = Function.support f
theorem
Pmf.mem_support_ofFintype_iff
{α : Type u_1}
[Fintype α]
{f : α → ENNReal}
(h : (Finset.sum Finset.univ fun a => f a) = 1)
(a : α)
:
a ∈ Pmf.support (Pmf.ofFintype f h) ↔ f a ≠ 0
@[simp]
theorem
Pmf.toOuterMeasure_ofFintype_apply
{α : Type u_1}
[Fintype α]
{f : α → ENNReal}
(h : (Finset.sum Finset.univ fun a => f a) = 1)
(s : Set α)
:
↑(Pmf.toOuterMeasure (Pmf.ofFintype f h)) s = ∑' (x : α), Set.indicator s f x
@[simp]
theorem
Pmf.toMeasure_ofFintype_apply
{α : Type u_1}
[Fintype α]
{f : α → ENNReal}
(h : (Finset.sum Finset.univ fun a => f a) = 1)
(s : Set α)
[MeasurableSpace α]
(hs : MeasurableSet s)
:
↑↑(Pmf.toMeasure (Pmf.ofFintype f h)) s = ∑' (x : α), Set.indicator s f x
@[simp]
theorem
Pmf.support_normalize
{α : Type u_1}
{f : α → ENNReal}
(hf0 : tsum f ≠ 0)
(hf : tsum f ≠ ⊤)
:
Pmf.support (Pmf.normalize f hf0 hf) = Function.support f
theorem
Pmf.mem_support_normalize_iff
{α : Type u_1}
{f : α → ENNReal}
(hf0 : tsum f ≠ 0)
(hf : tsum f ≠ ⊤)
(a : α)
:
a ∈ Pmf.support (Pmf.normalize f hf0 hf) ↔ f a ≠ 0
@[simp]
theorem
Pmf.filter_apply
{α : Type u_1}
{p : Pmf α}
{s : Set α}
(h : ∃ a, a ∈ s ∧ a ∈ Pmf.support p)
(a : α)
:
↑(Pmf.filter p s h) a = Set.indicator s (↑p) a * (∑' (a' : α), Set.indicator s (↑p) a')⁻¹
theorem
Pmf.filter_apply_eq_zero_of_not_mem
{α : Type u_1}
{p : Pmf α}
{s : Set α}
(h : ∃ a, a ∈ s ∧ a ∈ Pmf.support p)
{a : α}
(ha : ¬a ∈ s)
:
↑(Pmf.filter p s h) a = 0
theorem
Pmf.mem_support_filter_iff
{α : Type u_1}
{p : Pmf α}
{s : Set α}
(h : ∃ a, a ∈ s ∧ a ∈ Pmf.support p)
{a : α}
:
a ∈ Pmf.support (Pmf.filter p s h) ↔ a ∈ s ∧ a ∈ Pmf.support p
@[simp]
theorem
Pmf.support_filter
{α : Type u_1}
{p : Pmf α}
{s : Set α}
(h : ∃ a, a ∈ s ∧ a ∈ Pmf.support p)
:
Pmf.support (Pmf.filter p s h) = s ∩ Pmf.support p
theorem
Pmf.filter_apply_eq_zero_iff
{α : Type u_1}
{p : Pmf α}
{s : Set α}
(h : ∃ a, a ∈ s ∧ a ∈ Pmf.support p)
(a : α)
:
↑(Pmf.filter p s h) a = 0 ↔ ¬a ∈ s ∨ ¬a ∈ Pmf.support p
theorem
Pmf.filter_apply_ne_zero_iff
{α : Type u_1}
{p : Pmf α}
{s : Set α}
(h : ∃ a, a ∈ s ∧ a ∈ Pmf.support p)
(a : α)
:
↑(Pmf.filter p s h) a ≠ 0 ↔ a ∈ s ∧ a ∈ Pmf.support p
@[simp]
theorem
Pmf.bernoulli_apply
{p : ENNReal}
(h : p ≤ 1)
(b : Bool)
:
↑(Pmf.bernoulli p h) b = bif b then p else 1 - p
@[simp]
theorem
Pmf.support_bernoulli
{p : ENNReal}
(h : p ≤ 1)
:
Pmf.support (Pmf.bernoulli p h) = {b | bif b then p ≠ 0 else p ≠ 1}
theorem
Pmf.mem_support_bernoulli_iff
{p : ENNReal}
(h : p ≤ 1)
(b : Bool)
:
b ∈ Pmf.support (Pmf.bernoulli p h) ↔ bif b then p ≠ 0 else p ≠ 1