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.

Construction of monadic pure and bind is found in probability_mass_function/monad.lean, 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

source
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
source
@[protected, instance]
def pmf.has_coe_to_fun {α : Type u_1} :
has_coe_to_fun (pmf α) (λ (p : pmf α), α → ℝ≥0)
Equations
source
@[protected, 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} (p : pmf α) :
set α

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

Equations
source
@[simp]
theorem pmf.mem_support_iff {α : Type u_1} (p : pmf α) (a : α) :
a ∈ p.support ↔ ⇑p a ≠ 0
source
theorem pmf.apply_eq_zero_iff {α : Type u_1} (p : pmf α) (a : α) :
⇑p a = 0 ↔ a ∉ p.support
source
theorem pmf.coe_le_one {α : Type u_1} (p : pmf α) (a : α) :
⇑p a ≤ 1
source
noncomputable def pmf.to_outer_measure {α : Type u_1} (p : pmf α) :
measure_theory.outer_measure α

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
source
theorem pmf.to_outer_measure_apply {α : Type u_1} (p : pmf α) (s : set α) :
⇑(p.to_outer_measure) s = ∑' (x : α), s.indicator (coe ∘ ⇑p) x
source
theorem pmf.to_outer_measure_apply' {α : Type u_1} (p : pmf α) (s : set α) :
⇑(p.to_outer_measure) s = ↑∑' (x : α), s.indicator ⇑p x
source
@[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)
source
theorem pmf.to_outer_measure_apply_eq_zero_iff {α : Type u_1} (p : pmf α) (s : set α) :
⇑(p.to_outer_measure) s = 0 ↔ disjoint p.support s
source
theorem pmf.to_outer_measure_apply_eq_one_iff {α : Type u_1} (p : pmf α) (s : set α) :
⇑(p.to_outer_measure) s = 1 ↔ p.support ⊆ s
source
@[simp]
theorem pmf.to_outer_measure_apply_inter_support {α : Type u_1} (p : pmf α) (s : set α) :
⇑(p.to_outer_measure) (s ∩ p.support) = ⇑(p.to_outer_measure) s
source
theorem pmf.to_outer_measure_mono {α : Type u_1} (p : pmf α) {s t : set α} (h : s ∩ p.support ⊆ t) :
⇑(p.to_outer_measure) s ≤ ⇑(p.to_outer_measure) t

Slightly stronger than outer_measure.mono having an intersection with p.support

source
theorem pmf.to_outer_measure_apply_eq_of_inter_support_eq {α : Type u_1} (p : pmf α) {s t : set α} (h : s ∩ p.support = t ∩ p.support) :
⇑(p.to_outer_measure) s = ⇑(p.to_outer_measure) t
source
@[simp]
theorem pmf.to_outer_measure_apply_fintype {α : Type u_1} (p : pmf α) (s : set α) [fintype α] :
⇑(p.to_outer_measure) s = ↑∑ (x : α), s.indicator ⇑p x
source
@[simp]
theorem pmf.to_outer_measure_caratheodory {α : Type u_1} (p : pmf α) :
p.to_outer_measure.caratheodory = ⊤
source
noncomputable def pmf.to_measure {α : Type u_1} [measurable_space α] (p : pmf α) :
measure_theory.measure α

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

Equations
source
theorem pmf.to_outer_measure_apply_le_to_measure_apply {α : Type u_1} [measurable_space α] (p : pmf α) (s : set α) :
⇑(p.to_outer_measure) s ≤ ⇑(p.to_measure) s
source
theorem pmf.to_measure_apply_eq_to_outer_measure_apply {α : Type u_1} [measurable_space α] (p : pmf α) (s : set α) (hs : measurable_set s) :
⇑(p.to_measure) s = ⇑(p.to_outer_measure) s
source
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 (coe ∘ ⇑p) x
source
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
source
theorem pmf.to_measure_apply_eq_one_iff {α : Type u_1} [measurable_space α] (p : pmf α) (s : set α) (hs : measurable_set s) :
⇑(p.to_measure) s = 1 ↔ p.support ⊆ s
source
@[simp]
theorem pmf.to_measure_apply_inter_support {α : Type u_1} [measurable_space α] (p : pmf α) (s : set α) (hs : measurable_set s) (hp : measurable_set p.support) :
⇑(p.to_measure) (s ∩ p.support) = ⇑(p.to_measure) s
source
theorem pmf.to_measure_mono {α : Type u_1} [measurable_space α] (p : pmf α) {s t : set α} (hs : measurable_set s) (ht : measurable_set t) (h : s ∩ p.support ⊆ t) :
⇑(p.to_measure) s ≤ ⇑(p.to_measure) t
source
theorem pmf.to_measure_apply_eq_of_inter_support_eq {α : Type u_1} [measurable_space α] (p : pmf α) {s t : set α} (hs : measurable_set s) (ht : measurable_set t) (h : s ∩ p.support = t ∩ p.support) :
⇑(p.to_measure) s = ⇑(p.to_measure) t
source
@[simp]
theorem pmf.to_measure_apply_finset {α : Type u_1} [measurable_space α] (p : pmf α) [measurable_singleton_class α] (s : finset α) :
⇑(p.to_measure) ↑s = ∑ (x : α) in s, ↑(⇑p x)
source
theorem pmf.to_measure_apply_of_finite {α : Type u_1} [measurable_space α] (p : pmf α) (s : set α) [measurable_singleton_class α] (hs : s.finite) :
⇑(p.to_measure) s = ↑∑' (x : α), s.indicator ⇑p x
source
@[simp]
theorem pmf.to_measure_apply_fintype {α : Type u_1} [measurable_space α] (p : pmf α) (s : set α) [measurable_singleton_class α] [fintype α] :
⇑(p.to_measure) s = ↑∑ (x : α), s.indicator ⇑p x
source
@[protected, instance]
def pmf.to_measure.is_probability_measure {α : Type u_1} [measurable_space α] (p : pmf α) :
measure_theory.is_probability_measure p.to_measure

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