mathlib documentation

measure_theory.probability_mass_function

Probability mass functions

This file is about probability mass functions or discrete probability measures: a function α → ℝ≥0 such that the values have (infinite) sum 1.

This file features the monadic structure of pmf and the Bernoulli distribution

Implementation Notes

This file is not yet connected to the measure_theory library in any way. At some point we need to define a measure from a pmf and prove the appropriate lemmas about that.

Tags

probability mass function, discrete probability measure, bernoulli distribution

def pmf  :
Type uType u

A probability mass function, or discrete probability measures is a function α → ℝ≥0 such that the values have (infinite) sum 1.

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

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

theorem pmf.has_sum_coe_one {α : Type u_1} (p : pmf α) :

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

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

def pmf.support {α : Type u_1} :
pmf αset α

The support of a pmf is the set where it is nonzero.

Equations
def pmf.pure {α : Type u_1} :
α → pmf α

The pure pmf is the pmf where all the mass lies in one point. The value of pure a is 1 at a and 0 elsewhere.

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

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

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

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

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

The monadic bind operation for pmf.

Equations
@[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

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)

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

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

@[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)

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))

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

The functorial action of a function on a pmf.

Equations
theorem pmf.bind_pure_comp {α : Type u_1} {β : Type u_2} (f : α → β) (p : pmf α) :

theorem pmf.map_id {α : Type u_1} (p : pmf α) :

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

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

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

The monadic sequencing operation for pmf.

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

Given a non-empty multiset s we construct the pmf which sends a to the fraction of elements in s that are a.

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

Given a finite type α and a function f : α → ℝ≥0 with sum 1, we get a pmf.

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

A pmf which assigns probability p to tt and 1 - p to ff.

Equations