mathlib3 documentation

probability.probability_mass_function.basic

Probability mass functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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. Conversely, given a probability measure μ on a measurable space α with all singleton sets measurable, μ.to_pmf constructs a pmf on α, setting the probability mass of a point x to be the measure of the singleton set {x}.

Tags #

probability mass function, discrete probability measure

def pmf (α : 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}

Instances for pmf

@[protected, instance]

def pmf.fun_like {α : Type u_1} :

fun_like (pmf α) α (λ (p : α), ennreal)

Equations

pmf.fun_like = {coe := λ (p : pmf α) (a : α), p.val a, coe_injective' := _}

@[protected, ext]

theorem pmf.ext {α : Type u_1} {p q : pmf α} (h : ∀ (x : α), ⇑p x = ⇑q x) :

p = q

theorem pmf.ext_iff {α : Type u_1} {p q : pmf α} :

p = q ↔ ∀ (x : α), ⇑p x = ⇑q x

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

@[simp]

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

∑' (a : α), ⇑p a = 1

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

∑' (a : α), ⇑p a ≠ ⊤

theorem pmf.tsum_coe_indicator_ne_top {α : Type u_1} (p : pmf α) (s : set α) :

∑' (a : α), s.indicator ⇑p a ≠ ⊤

@[simp]

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

def pmf.support {α : Type u_1} (p : pmf α) :

set α

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

Equations

p.support = function.support ⇑p

@[simp]

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

a ∈ p.support ↔ ⇑p a ≠ 0

@[simp]

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

p.support.nonempty

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

⇑p a = 0 ↔ a ∉ p.support

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

0 < ⇑p a ↔ a ∈ p.support

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

⇑p a = 1 ↔ p.support = {a}

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

⇑p a ≤ 1

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

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

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

p.to_outer_measure = measure_theory.outer_measure.sum (λ (x : α), ⇑p x • measure_theory.outer_measure.dirac 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_caratheodory {α : Type u_1} (p : pmf α) :

p.to_outer_measure.caratheodory = ⊤

@[simp]

theorem pmf.to_outer_measure_apply_finset {α : Type u_1} (p : pmf α) (s : finset α) :

⇑(p.to_outer_measure) ↑s = s.sum (λ (x : α), ⇑p x)

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

⇑(p.to_outer_measure) {a} = ⇑p a

theorem pmf.to_outer_measure_injective {α : Type u_1} :

function.injective pmf.to_outer_measure

@[simp]

theorem pmf.to_outer_measure_inj {α : Type u_1} {p q : pmf α} :

p.to_outer_measure = q.to_outer_measure ↔ p = q

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

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

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

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

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

@[simp]

theorem pmf.to_outer_measure_apply_fintype {α : Type u_1} (p : pmf α) (s : set α) [fintype α] :

⇑(p.to_outer_measure) s = finset.univ.sum (λ (x : α), s.indicator ⇑p x)

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

p.to_measure = p.to_outer_measure.to_measure _

Instances for pmf.to_measure

pmf.to_measure.is_probability_measure

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

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

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

theorem pmf.to_measure_apply_singleton {α : Type u_1} [measurable_space α] (p : pmf α) (a : α) (h : measurable_set {a}) :

⇑(p.to_measure) {a} = ⇑p a

theorem pmf.to_measure_apply_eq_zero_iff {α : Type u_1} [measurable_space α] (p : pmf α) (s : set α) (hs : measurable_set s) :

⇑(p.to_measure) s = 0 ↔ disjoint p.support s

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

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

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

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

theorem pmf.to_measure_injective {α : Type u_1} [measurable_space α] [measurable_singleton_class α] :

function.injective pmf.to_measure

@[simp]

theorem pmf.to_measure_inj {α : Type u_1} [measurable_space α] [measurable_singleton_class α] {p q : pmf α} :

p.to_measure = q.to_measure ↔ p = q

@[simp]

theorem pmf.to_measure_apply_finset {α : Type u_1} [measurable_space α] (p : pmf α) [measurable_singleton_class α] (s : finset α) :

⇑(p.to_measure) ↑s = s.sum (λ (x : α), ⇑p x)

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

@[simp]

theorem pmf.to_measure_apply_fintype {α : Type u_1} [measurable_space α] (p : pmf α) (s : set α) [measurable_singleton_class α] [fintype α] :

⇑(p.to_measure) s = finset.univ.sum (λ (x : α), s.indicator ⇑p x)

def measure_theory.measure.to_pmf {α : Type u_1} [countable α] [measurable_space α] [measurable_singleton_class α] (μ : measure_theory.measure α) [h : measure_theory.is_probability_measure μ] :

pmf α

Given that α is a countable, measurable space with all singleton sets measurable, we can convert any probability measure into a pmf, where the mass of a point is the measure of the singleton set under the original measure.

Equations

μ.to_pmf = ⟨λ (x : α), ⇑μ {x}, _⟩

theorem measure_theory.measure.to_pmf_apply {α : Type u_1} [countable α] [measurable_space α] [measurable_singleton_class α] (μ : measure_theory.measure α) [measure_theory.is_probability_measure μ] (x : α) :

⇑(μ.to_pmf) x = ⇑μ {x}

@[simp]

theorem measure_theory.measure.to_pmf_to_measure {α : Type u_1} [countable α] [measurable_space α] [measurable_singleton_class α] (μ : measure_theory.measure α) [measure_theory.is_probability_measure μ] :

μ.to_pmf.to_measure = μ

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

@[simp]

theorem pmf.to_measure_to_pmf {α : Type u_1} [countable α] [measurable_space α] [measurable_singleton_class α] (p : pmf α) :

p.to_measure.to_pmf = p

theorem pmf.to_measure_eq_iff_eq_to_pmf {α : Type u_1} [countable α] [measurable_space α] [measurable_singleton_class α] (p : pmf α) (μ : measure_theory.measure α) [measure_theory.is_probability_measure μ] :

p.to_measure = μ ↔ p = μ.to_pmf

theorem pmf.to_pmf_eq_iff_to_measure_eq {α : Type u_1} [countable α] [measurable_space α] [measurable_singleton_class α] (p : pmf α) (μ : measure_theory.measure α) [measure_theory.is_probability_measure μ] :

μ.to_pmf = p ↔ μ = p.to_measure