mathlib documentation

measure_theory.probability_mass_function.basic

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, other constructions of pmfs are found in probability_mass_function/constructions.lean

Given p : pmf α, pmf.to_outer_measure constructs an outer_measure on α, by assigning each set the sum of the probabilities of each of its elements. Under this outer measure, every set is Carathéodory-measurable, so we can further extend this to a measure on α, see pmf.to_measure. pmf.to_measure.is_probability_measure shows this associated measure is a probability measure.

Tags #

probability mass function, discrete probability measure

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
@[protected, instance]
def pmf.has_coe_to_fun {α : Type u_1} :
has_coe_to_fun (pmf α) (λ (p : pmf α), α → ℝ≥0)
Equations
@[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
@[simp]
theorem pmf.mem_support_iff {α : Type u_1} (p : pmf α) (a : α) :
a p.support p a 0
theorem pmf.apply_eq_zero_iff {α : Type u_1} (p : pmf α) (a : α) :
p a = 0 a p.support
theorem pmf.coe_le_one {α : Type u_1} (p : pmf α) (a : α) :
p a 1
noncomputable 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
@[simp]
theorem pmf.pure_apply {α : Type u_1} (a a' : α) :
(pmf.pure a) a' = ite (a' = a) 1 0
@[simp]
theorem pmf.support_pure {α : Type u_1} (a : α) :
theorem pmf.mem_support_pure_iff {α : Type u_1} (a a' : α) :
a' (pmf.pure a).support a' = a
@[protected, instance]
noncomputable def pmf.inhabited {α : Type u_1} [inhabited α] :
Equations
@[protected]
theorem pmf.bind.summable {α : Type u_1} {β : Type u_2} (p : pmf α) (f : α → pmf β) (b : β) :
summable (λ (a : α), (p a) * (f a) b)
noncomputable 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
@[simp]
theorem pmf.support_bind {α : Type u_1} {β : Type u_2} (p : pmf α) (f : α → pmf β) :
(p.bind f).support = {b : β | ∃ (a : α) (H : a p.support), b (f a).support}
theorem pmf.mem_support_bind_iff {α : Type u_1} {β : Type u_2} (p : pmf α) (f : α → pmf β) (b : β) :
b (p.bind f).support ∃ (a : α) (H : a p.support), b (f a).support
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))
@[protected, instance]
noncomputable def pmf.monad  :
Equations
noncomputable def pmf.to_outer_measure {α : Type u_1} (p : pmf α) :

Construct an outer_measure from a pmf, by assigning measure to each set s : set α equal to the sum of p x for for each x ∈ α

Equations
theorem pmf.to_outer_measure_apply {α : Type u_1} (p : pmf α) (s : set α) :
(p.to_outer_measure) s = ∑' (x : α), s.indicator (λ (x : α), (p x)) x
theorem pmf.to_outer_measure_apply' {α : Type u_1} (p : pmf α) (s : set α) :
(p.to_outer_measure) s = ∑' (x : α), s.indicator p x
@[simp]
theorem pmf.to_outer_measure_apply_finset {α : Type u_1} (p : pmf α) (s : finset α) :
(p.to_outer_measure) s = ∑ (x : α) in s, (p x)
@[simp]
theorem pmf.to_outer_measure_apply_fintype {α : Type u_1} [fintype α] (p : pmf α) (s : set α) :
(p.to_outer_measure) s = ∑ (x : α), s.indicator (λ (x : α), (p x)) x
theorem pmf.to_outer_measure_apply_eq_zero_iff {α : Type u_1} (p : pmf α) (s : set α) :
@[simp]
noncomputable def pmf.to_measure {α : Type u_1} [measurable_space α] (p : pmf α) :

Since every set is Carathéodory-measurable under pmf.to_outer_measure, we can further extend this outer_measure to a measure on α

Equations
theorem pmf.to_measure_apply_eq_to_outer_measure_apply {α : Type u_1} [measurable_space α] (p : pmf α) (s : set α) (hs : measurable_set s) :
theorem pmf.to_measure_apply {α : Type u_1} [measurable_space α] (p : pmf α) (s : set α) (hs : measurable_set s) :
(p.to_measure) s = ∑' (x : α), s.indicator (λ (x : α), (p x)) x
theorem pmf.to_measure_apply' {α : Type u_1} [measurable_space α] (p : pmf α) (s : set α) (hs : measurable_set s) :
(p.to_measure) s = ∑' (x : α), s.indicator p x
@[simp]
theorem pmf.to_measure_apply_finset {α : Type u_1} [measurable_space α] [measurable_singleton_class α] (p : pmf α) (s : finset α) :
(p.to_measure) s = ∑ (x : α) in s, (p x)
theorem pmf.to_measure_apply_of_finite {α : Type u_1} [measurable_space α] [measurable_singleton_class α] (p : pmf α) (s : set α) (hs : s.finite) :
(p.to_measure) s = ∑' (x : α), s.indicator (λ (x : α), (p x)) x
@[simp]
theorem pmf.to_measure_apply_fintype {α : Type u_1} [measurable_space α] [measurable_singleton_class α] [fintype α] (p : pmf α) (s : set α) :
(p.to_measure) s = ∑ (x : α), s.indicator (λ (x : α), (p x)) x
@[protected, instance]

The measure associated to a pmf by to_measure is a probability measure