mathlib documentation

measure_theory.probability_mass_function

source
def pmf (α : Type u) :
Type u

Probability mass functions, i.e. discrete probability measures

Equations
source
@[instance]
def pmf.has_coe_to_fun {α : Type u_1} :
has_coe_to_fun (pmf α)

Equations
source
@[ext]
theorem pmf.ext {α : Type u_1} {p q : pmf α} (a : ∀ (a : α), ⇑p a = ⇑q a) :
p = q

source
theorem pmf.has_sum_coe_one {α : Type u_1} (p : pmf α) :
has_sum ⇑p 1

source
theorem pmf.summable_coe {α : Type u_1} (p : pmf α) :
summable ⇑p

source
@[simp]
theorem pmf.tsum_coe {α : Type u_1} (p : pmf α) :
(∑' (a : α), ⇑p a) = 1

source
def pmf.support {α : Type u_1} (p : pmf α) :
set α

Equations
source
def pmf.pure {α : Type u_1} (a : α) :
pmf α

Equations
source
@[simp]
theorem pmf.pure_apply {α : Type u_1} (a a' : α) :
⇑(pmf.pure a) a' = ite (a' = a) 1 0

source
@[instance]
def pmf.inhabited {α : Type u_1} [inhabited α] :
inhabited (pmf α)

Equations
source
theorem pmf.coe_le_one {α : Type u_1} (p : pmf α) (a : α) :
⇑p a ≤ 1

source
theorem pmf.bind.summable {α : Type u_1} {β : Type u_2} (p : pmf α) (f : α → pmf β) (b : β) :
summable (λ (a : α), (⇑p a) * ⇑(f a) b)

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

Equations
source
@[simp]
theorem pmf.bind_apply {α : Type u_1} {β : Type u_2} (p : pmf α) (f : α → pmf β) (b : β) :
⇑(p.bind f) b = ∑' (a : α), (⇑p a) * ⇑(f a) b

source
theorem pmf.coe_bind_apply {α : Type u_1} {β : Type u_2} (p : pmf α) (f : α → pmf β) (b : β) :
↑(⇑(p.bind f) b) = ∑' (a : α), (↑(⇑p a)) * ↑(⇑(f a) b)

source
@[simp]
theorem pmf.pure_bind {α : Type u_1} {β : Type u_2} (a : α) (f : α → pmf β) :
(pmf.pure a).bind f = f a

source
@[simp]
theorem pmf.bind_pure {α : Type u_1} (p : pmf α) :
p.bind pmf.pure = p

source
@[simp]
theorem pmf.bind_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : pmf α) (f : α → pmf β) (g : β → pmf γ) :
(p.bind f).bind g = p.bind (λ (a : α), (f a).bind g)

source
theorem pmf.bind_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : pmf α) (q : pmf β) (f : α → β → pmf γ) :
p.bind (λ (a : α), q.bind (f a)) = q.bind (λ (b : β), p.bind (λ (a : α), f a b))

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

Equations
source
theorem pmf.bind_pure_comp {α : Type u_1} {β : Type u_2} (f : α → β) (p : pmf α) :
p.bind (pmf.pure ∘ f) = pmf.map f p

source
theorem pmf.map_id {α : Type u_1} (p : pmf α) :
pmf.map id p = p

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

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

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

Equations
source
def pmf.of_multiset {α : Type u_1} (s : multiset α) (hs : s ≠ 0) :
pmf α

Equations
source
def pmf.of_fintype {α : Type u_1} [fintype α] (f : α → ℝ≥0) (h : ∑ (x : α), f x = 1) :
pmf α

Equations
source
def pmf.bernoulli (p : ℝ≥0) (h : p ≤ 1) :
pmf bool

Equations