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

Type u

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

Equations

pmf α = {f // has_sum f 1}

@[protected, instance]

def pmf.has_coe_to_fun {α : Type u_1} :

has_coe_to_fun (pmf α)

Equations

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

@[protected, 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} (p : pmf α) :

set α

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

Equations

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

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

pmf.pure a = ⟨λ (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

@[protected, instance]

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

inhabited (pmf α)

Equations

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

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

⇑p a ≤ 1

@[protected]

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

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

@[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.bind pmf.pure = 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))

@[protected]

theorem pmf.bind_on_support.summable {α : Type u_1} {β : Type u_2} (p : pmf α) (f : Π (a : α), a ∈ p.support → pmf β) (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.support → pmf β) :

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

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_apply {α : Type u_1} {β : Type u_2} (p : pmf α) (f : Π (a : α), a ∈ p.support → pmf β) (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.support → pmf β) (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.support → pmf β) (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.support → pmf β) (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).support → pmf β) :

(pmf.pure a).bind_on_support 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.support → pmf β) (g : Π (b : β), b ∈ (p.bind_on_support f).support → pmf γ) :

(p.bind_on_support f).bind_on_support 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.support → pmf γ) :

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

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

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

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

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

pmf.map id p = p

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 : α → β) :

pmf.map 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

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

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

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

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

pmf.of_fintype f h = ⟨f, _⟩

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

pmf.normalize f hf0 = ⟨λ (a : α), (f a) * (∑' (x : α), f x)⁻¹, _⟩

theorem pmf.normalize_apply {α : Type u_1} {f : α → ℝ≥0} (hf0 : tsum f ≠ 0) (a : α) :

⇑(pmf.normalize f 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

p.filter s h = pmf.normalize (s.indicator ⇑p) _

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

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