mathlib docs: measure_theory.probability_mass

source

def pmf :

Type u → Type u

Probability mass functions, i.e. discrete probability measures

Equations

pmf α = {f // has_sum f 1}

source

@[instance]

def pmf.has_coe_to_fun {α : Type u_1} :

has_coe_to_fun (pmf α)

Equations

pmf.has_coe_to_fun = {F := λ (p : pmf α), α → nnreal, coe := λ (p : pmf α) (a : α), p.val a}

source

@[ext]

theorem pmf.ext {α : Type u_1} {p q : pmf α} :

(∀ (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} :

pmf α → set α

Equations

p.support = {a : α | p.val a ≠ 0}

source

def pmf.pure {α : Type u_1} :

α → pmf α

Equations

pmf.pure a = ⟨λ (a' : α), ite (a' = a) 1 0, _⟩

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

pmf.inhabited = {default := pmf.pure (inhabited.default α)}

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} :

pmf α → (α → pmf β) → pmf β

Equations

p.bind f = ⟨λ (b : β), ∑' (a : α), ⇑p a * ⇑(f a) b, _⟩

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} :

(α → β) → pmf α → pmf β

Equations

pmf.map f p = p.bind (pmf.pure ∘ f)

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} :

pmf (α → β) → pmf α → pmf β

Equations

f.seq p = f.bind (λ (m : α → β), p.bind (λ (a : α), pmf.pure (m a)))

source

def pmf.of_multiset {α : Type u_1} (s : multiset α) :

s ≠ 0 → pmf α

Equations

pmf.of_multiset s hs = ⟨λ (a : α), ↑(multiset.count a s) / ↑(s.card), _⟩

source

def pmf.of_fintype {α : Type u_1} [fintype α] (f : α → nnreal) :

finset.univ.sum (λ (x : α), f x) = 1 → pmf α

Equations

pmf.of_fintype f h = ⟨f, _⟩

source

def pmf.bernoulli (p : nnreal) :

p ≤ 1 → pmf bool

Equations

pmf.bernoulli p h = pmf.of_fintype (λ (b : bool), cond b p (1 - p)) _

mathlib documentation

measure_theory.probability_mass_function

General documentation

Additional documentation

Library

mathlib documentation

measure_theory.​probability_mass_function

General documentation

Additional documentation

Library

measure_theory.probability_mass_function