# mathlibdocumentation

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 u) :
Type 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 α) :
1
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} (p : pmf α) :
set α

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

Equations
@[simp]
theorem pmf.mem_support_iff {α : Type u_1} (p : pmf α) (a : α) :
a p.support p a 0
def pmf.pure {α : Type u_1} (a : α) :
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
• = λ (a' : α), ite (a' = a) 1 0, _⟩
@[simp]
theorem pmf.pure_apply {α : Type u_1} (a a' : α) :
(pmf.pure a) a' = ite (a' = a) 1 0
theorem pmf.mem_support_pure_iff {α : Type u_1} (a a' : α) :
a' (pmf.pure a).support a' = a
@[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} (p : pmf α) (f : α → 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 α) :
= p
@[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))
theorem pmf.bind_on_support.summable {α : Type u_1} {β : Type u_2} (p : pmf α) (f : Π (a : α), a p.supportpmf β) (b : β) :
summable (λ (a : α), (p a) * dite (p a = 0) (λ (h : p a = 0), 0) (λ (h : ¬p a = 0), (f a h) b))
def pmf.bind_on_support {α : Type u_1} {β : Type u_2} (p : pmf α) (f : Π (a : α), a p.supportpmf β) :
pmf β

Generalized version of bind allowing f to only be defined on the support of p. p.bind f is equivalent to p.bind_on_support (λ a _, f a), see bind_on_support_eq_bind

Equations
@[simp]
theorem pmf.bind_on_support_apply {α : Type u_1} {β : Type u_2} (p : pmf α) (f : Π (a : α), a p.supportpmf β) (b : β) :
(p.bind_on_support f) b = ∑' (a : α), (p a) * dite (p a = 0) (λ (h : p a = 0), 0) (λ (h : ¬p a = 0), (f a h) b)
@[simp]
theorem pmf.bind_on_support_eq_bind {α : Type u_1} {β : Type u_2} (p : pmf α) (f : α → pmf β) :
p.bind_on_support (λ (a : α) (_x : a p.support), f a) = p.bind f

bind_on_support reduces to bind if f doesn't depend on the additional hypothesis

theorem pmf.coe_bind_on_support_apply {α : Type u_1} {β : Type u_2} (p : pmf α) (f : Π (a : α), a p.supportpmf β) (b : β) :
((p.bind_on_support f) b) = ∑' (a : α), ((p a)) * dite (p a = 0) (λ (h : p a = 0), 0) (λ (h : ¬p a = 0), ((f a h) b))
@[simp]
theorem pmf.mem_support_bind_on_support_iff {α : Type u_1} {β : Type u_2} (p : pmf α) (f : Π (a : α), a p.supportpmf β) (b : β) :
b (p.bind_on_support f).support ∃ (a : α) (ha : p a 0), b (f a ha).support
theorem pmf.bind_on_support_eq_zero_iff {α : Type u_1} {β : Type u_2} (p : pmf α) (f : Π (a : α), a p.supportpmf β) (b : β) :
(p.bind_on_support f) b = 0 ∀ (a : α) (ha : p a 0), (f a ha) b = 0
@[simp]
theorem pmf.pure_bind_on_support {α : Type u_1} {β : Type u_2} (a : α) (f : Π (a' : α), a' (pmf.pure a).supportpmf β) :
f = f a _
theorem pmf.bind_on_support_pure {α : Type u_1} (p : pmf α) :
p.bind_on_support (λ (a : α) (_x : a p.support), pmf.pure a) = p
@[simp]
theorem pmf.bind_on_support_bind_on_support {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : pmf α) (f : Π (a : α), a p.supportpmf β) (g : Π (b : β), b (p.bind_on_support f).supportpmf γ) :
g = p.bind_on_support (λ (a : α) (ha : a p.support), (f a ha).bind_on_support (λ (b : β) (hb : b (f a ha).support), g b _))
theorem pmf.bind_on_support_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : pmf α) (q : pmf β) (f : Π (a : α), a p.supportΠ (b : β), b q.supportpmf γ) :
p.bind_on_support (λ (a : α) (ha : a p.support), q.bind_on_support (f a ha)) = q.bind_on_support (λ (b : β) (hb : b q.support), p.bind_on_support (λ (a : α) (ha : a p.support), f a ha b hb))
def pmf.map {α : Type u_1} {β : Type u_2} (f : α → β) (p : 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 α) :
p.bind (pmf.pure f) = p
theorem pmf.map_id {α : Type u_1} (p : pmf α) :
= p
theorem pmf.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : pmf α) (f : α → β) (g : β → γ) :
(pmf.map f p) = pmf.map (g f) p
theorem pmf.pure_map {α : Type u_1} {β : Type u_2} (a : α) (f : α → β) :
(pmf.pure a) = pmf.pure (f a)
def pmf.seq {α : Type u_1} {β : Type u_2} (f : pmf (α → β)) (p : pmf α) :
pmf β

The monadic sequencing operation for pmf.

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

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) (h : ∑ (x : α), f x = 1) :
pmf α

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

Equations
def pmf.normalize {α : Type u_1} (f : α → ℝ≥0) (hf0 : tsum f 0) :
pmf α

Given a f with non-zero sum, we get a pmf by normalizing f by its tsum

Equations
• hf0 = λ (a : α), (f a) * (∑' (x : α), f x)⁻¹, _⟩
theorem pmf.normalize_apply {α : Type u_1} {f : α → ℝ≥0} (hf0 : tsum f 0) (a : α) :
hf0) a = (f a) * (∑' (x : α), f x)⁻¹
def pmf.filter {α : Type u_1} (p : pmf α) (s : set α) (h : ∃ (a : α) (H : a s), p a 0) :
pmf α

Create new pmf by filtering on a set with non-zero measure and normalizing

Equations
theorem pmf.filter_apply {α : Type u_1} (p : pmf α) {s : set α} (h : ∃ (a : α) (H : a s), p a 0) {a : α} :
(p.filter s h) a = (s.indicator p a) * (∑' (x : α), s.indicator p x)⁻¹
theorem pmf.filter_apply_eq_zero_of_not_mem {α : Type u_1} (p : pmf α) {s : set α} (h : ∃ (a : α) (H : a s), p a 0) {a : α} (ha : a s) :
(p.filter s h) a = 0
theorem pmf.filter_apply_eq_zero_iff {α : Type u_1} (p : pmf α) {s : set α} (h : ∃ (a : α) (H : a s), p a 0) (a : α) :
(p.filter s h) a = 0 a p.support s
theorem pmf.filter_apply_ne_zero_iff {α : Type u_1} (p : pmf α) {s : set α} (h : ∃ (a : α) (H : a s), p a 0) (a : α) :
(p.filter s h) a 0 a p.support s
def pmf.bernoulli (p : ℝ≥0) (h : p 1) :

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

Equations