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 ProbabilityMassFunction/Monad.lean, other constructions of PMFs are found in ProbabilityMassFunction/Constructions.lean.

Given p : PMF α, PMF.toOuterMeasure constructs an OuterMeasure 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.toMeasure. PMF.toMeasure.isProbabilityMeasure shows this associated measure is a probability measure. Conversely, given a probability measure μ on a measurable space α with all singleton sets measurable, μ.toPMF 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) : 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 : α → ENNReal // HasSum f 1 }

instance PMF.instFunLike {α : Type u_1} : FunLike (PMF α) α ENNReal

Equations

• One or more equations did not get rendered due to their size.

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

theorem PMF.ext_iff {α : Type u_1} {p : PMF α} {q : PMF α} : p = q ↔ ∀ (x : α), p x = q x

theorem PMF.hasSum_coe_one {α : Type u_1} (p : PMF α) : HasSum (⇑p) 1

@[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 : α), Set.indicator s (⇑p) a ≠ ⊤

@[simp]

theorem PMF.coe_ne_zero {α : Type u_1} (p : PMF α) : ⇑p ≠ 0

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

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

Equations

• PMF.support p = Function.support ⇑p

@[simp]

theorem PMF.mem_support_iff {α : Type u_1} (p : PMF α) (a : α) : a ∈ PMF.support p ↔ p a ≠ 0

@[simp]

theorem PMF.support_nonempty {α : Type u_1} (p : PMF α) : Set.Nonempty (PMF.support p)

@[simp]

theorem PMF.support_countable {α : Type u_1} (p : PMF α) : Set.Countable (PMF.support p)

theorem PMF.apply_eq_zero_iff {α : Type u_1} (p : PMF α) (a : α) : p a = 0 ↔ a ∉ PMF.support p

theorem PMF.apply_pos_iff {α : Type u_1} (p : PMF α) (a : α) : 0 < p a ↔ a ∈ PMF.support p

theorem PMF.apply_eq_one_iff {α : Type u_1} (p : PMF α) (a : α) : p a = 1 ↔ PMF.support p = {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 : α) : p a ≠ ⊤

theorem PMF.apply_lt_top {α : Type u_1} (p : PMF α) (a : α) : p a < ⊤

def PMF.toOuterMeasure {α : Type u_1} (p : PMF α) : MeasureTheory.OuterMeasure α

Construct an OuterMeasure from a PMF, by assigning measure to each set s : Set α equal to the sum of p x for each x ∈ α.

Equations

• PMF.toOuterMeasure p = MeasureTheory.OuterMeasure.sum fun (x : α) => p x • MeasureTheory.OuterMeasure.dirac x

theorem PMF.toOuterMeasure_apply {α : Type u_1} (p : PMF α) (s : Set α) : ↑(PMF.toOuterMeasure p) s = ∑' (x : α), Set.indicator s (⇑p) x

@[simp]

theorem PMF.toOuterMeasure_caratheodory {α : Type u_1} (p : PMF α) : MeasureTheory.OuterMeasure.caratheodory (PMF.toOuterMeasure p) = ⊤

@[simp]

theorem PMF.toOuterMeasure_apply_finset {α : Type u_1} (p : PMF α) (s : Finset α) : ↑(PMF.toOuterMeasure p) ↑s = Finset.sum s fun (x : α) => p x

theorem PMF.toOuterMeasure_apply_singleton {α : Type u_1} (p : PMF α) (a : α) : ↑(PMF.toOuterMeasure p) {a} = p a

theorem PMF.toOuterMeasure_injective {α : Type u_1} : Function.Injective PMF.toOuterMeasure

@[simp]

theorem PMF.toOuterMeasure_inj {α : Type u_1} {p : PMF α} {q : PMF α} : PMF.toOuterMeasure p = PMF.toOuterMeasure q ↔ p = q

theorem PMF.toOuterMeasure_apply_eq_zero_iff {α : Type u_1} (p : PMF α) (s : Set α) : ↑(PMF.toOuterMeasure p) s = 0 ↔ Disjoint (PMF.support p) s

theorem PMF.toOuterMeasure_apply_eq_one_iff {α : Type u_1} (p : PMF α) (s : Set α) : ↑(PMF.toOuterMeasure p) s = 1 ↔ PMF.support p ⊆ s

@[simp]

theorem PMF.toOuterMeasure_apply_inter_support {α : Type u_1} (p : PMF α) (s : Set α) : ↑(PMF.toOuterMeasure p) (s ∩ PMF.support p) = ↑(PMF.toOuterMeasure p) s

theorem PMF.toOuterMeasure_mono {α : Type u_1} (p : PMF α) {s : Set α} {t : Set α} (h : s ∩ PMF.support p ⊆ t) : ↑(PMF.toOuterMeasure p) s ≤ ↑(PMF.toOuterMeasure p) t

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

theorem PMF.toOuterMeasure_apply_eq_of_inter_support_eq {α : Type u_1} (p : PMF α) {s : Set α} {t : Set α} (h : s ∩ PMF.support p = t ∩ PMF.support p) : ↑(PMF.toOuterMeasure p) s = ↑(PMF.toOuterMeasure p) t

@[simp]

theorem PMF.toOuterMeasure_apply_fintype {α : Type u_1} (p : PMF α) (s : Set α) [Fintype α] : ↑(PMF.toOuterMeasure p) s = Finset.sum Finset.univ fun (x : α) => Set.indicator s (⇑p) x

def PMF.toMeasure {α : Type u_1} [MeasurableSpace α] (p : PMF α) : MeasureTheory.Measure α

Since every set is Carathéodory-measurable under PMF.toOuterMeasure, we can further extend this OuterMeasure to a Measure on α.

Equations

• PMF.toMeasure p = MeasureTheory.OuterMeasure.toMeasure (PMF.toOuterMeasure p) (_ : inst ≤ MeasureTheory.OuterMeasure.caratheodory (PMF.toOuterMeasure p))

theorem PMF.toOuterMeasure_apply_le_toMeasure_apply {α : Type u_1} [MeasurableSpace α] (p : PMF α) (s : Set α) : ↑(PMF.toOuterMeasure p) s ≤ ↑↑(PMF.toMeasure p) s

theorem PMF.toMeasure_apply_eq_toOuterMeasure_apply {α : Type u_1} [MeasurableSpace α] (p : PMF α) (s : Set α) (hs : MeasurableSet s) : ↑↑(PMF.toMeasure p) s = ↑(PMF.toOuterMeasure p) s

theorem PMF.toMeasure_apply {α : Type u_1} [MeasurableSpace α] (p : PMF α) (s : Set α) (hs : MeasurableSet s) : ↑↑(PMF.toMeasure p) s = ∑' (x : α), Set.indicator s (⇑p) x

theorem PMF.toMeasure_apply_singleton {α : Type u_1} [MeasurableSpace α] (p : PMF α) (a : α) (h : MeasurableSet {a}) : ↑↑(PMF.toMeasure p) {a} = p a

theorem PMF.toMeasure_apply_eq_zero_iff {α : Type u_1} [MeasurableSpace α] (p : PMF α) (s : Set α) (hs : MeasurableSet s) : ↑↑(PMF.toMeasure p) s = 0 ↔ Disjoint (PMF.support p) s

theorem PMF.toMeasure_apply_eq_one_iff {α : Type u_1} [MeasurableSpace α] (p : PMF α) (s : Set α) (hs : MeasurableSet s) : ↑↑(PMF.toMeasure p) s = 1 ↔ PMF.support p ⊆ s

@[simp]

theorem PMF.toMeasure_apply_inter_support {α : Type u_1} [MeasurableSpace α] (p : PMF α) (s : Set α) (hs : MeasurableSet s) (hp : MeasurableSet (PMF.support p)) : ↑↑(PMF.toMeasure p) (s ∩ PMF.support p) = ↑↑(PMF.toMeasure p) s

@[simp]

theorem PMF.restrict_toMeasure_support {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (p : PMF α) : MeasureTheory.Measure.restrict (PMF.toMeasure p) (PMF.support p) = PMF.toMeasure p

theorem PMF.toMeasure_mono {α : Type u_1} [MeasurableSpace α] (p : PMF α) {s : Set α} {t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (h : s ∩ PMF.support p ⊆ t) : ↑↑(PMF.toMeasure p) s ≤ ↑↑(PMF.toMeasure p) t

theorem PMF.toMeasure_apply_eq_of_inter_support_eq {α : Type u_1} [MeasurableSpace α] (p : PMF α) {s : Set α} {t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (h : s ∩ PMF.support p = t ∩ PMF.support p) : ↑↑(PMF.toMeasure p) s = ↑↑(PMF.toMeasure p) t

theorem PMF.toMeasure_injective {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] : Function.Injective PMF.toMeasure

@[simp]

theorem PMF.toMeasure_inj {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {p : PMF α} {q : PMF α} : PMF.toMeasure p = PMF.toMeasure q ↔ p = q

@[simp]

theorem PMF.toMeasure_apply_finset {α : Type u_1} [MeasurableSpace α] (p : PMF α) [MeasurableSingletonClass α] (s : Finset α) : ↑↑(PMF.toMeasure p) ↑s = Finset.sum s fun (x : α) => p x

theorem PMF.toMeasure_apply_of_finite {α : Type u_1} [MeasurableSpace α] (p : PMF α) (s : Set α) [MeasurableSingletonClass α] (hs : Set.Finite s) : ↑↑(PMF.toMeasure p) s = ∑' (x : α), Set.indicator s (⇑p) x

@[simp]

theorem PMF.toMeasure_apply_fintype {α : Type u_1} [MeasurableSpace α] (p : PMF α) (s : Set α) [MeasurableSingletonClass α] [Fintype α] : ↑↑(PMF.toMeasure p) s = Finset.sum Finset.univ fun (x : α) => Set.indicator s (⇑p) x

def MeasureTheory.Measure.toPMF {α : Type u_1} [Countable α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α) [h : MeasureTheory.IsProbabilityMeasure μ] : 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

• MeasureTheory.Measure.toPMF μ = { val := fun (x : α) => ↑↑μ {x}, property := (_ : HasSum (fun (x : α) => ↑↑μ {x}) 1) }

theorem MeasureTheory.Measure.toPMF_apply {α : Type u_1} [Countable α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (x : α) : (MeasureTheory.Measure.toPMF μ) x = ↑↑μ {x}

@[simp]

theorem MeasureTheory.Measure.toPMF_toMeasure {α : Type u_1} [Countable α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : PMF.toMeasure (MeasureTheory.Measure.toPMF μ) = μ

instance PMF.toMeasure.isProbabilityMeasure {α : Type u_1} [MeasurableSpace α] (p : PMF α) : MeasureTheory.IsProbabilityMeasure (PMF.toMeasure p)

The measure associated to a PMF by toMeasure is a probability measure.

Equations

• (_ : MeasureTheory.IsProbabilityMeasure (PMF.toMeasure p)) = (_ : MeasureTheory.IsProbabilityMeasure (PMF.toMeasure p))

@[simp]

theorem PMF.toMeasure_toPMF {α : Type u_1} [Countable α] [MeasurableSpace α] [MeasurableSingletonClass α] (p : PMF α) : MeasureTheory.Measure.toPMF (PMF.toMeasure p) = p

theorem PMF.toMeasure_eq_iff_eq_toPMF {α : Type u_1} [Countable α] [MeasurableSpace α] [MeasurableSingletonClass α] (p : PMF α) (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : PMF.toMeasure p = μ ↔ p = MeasureTheory.Measure.toPMF μ

theorem PMF.toPMF_eq_iff_toMeasure_eq {α : Type u_1} [Countable α] [MeasurableSpace α] [MeasurableSingletonClass α] (p : PMF α) (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.Measure.toPMF μ = p ↔ μ = PMF.toMeasure p