# Documentation

Mathlib.Probability.ProbabilityMassFunction.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 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) :

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

Instances For
instance Pmf.funLike {α : Type u_1} :
FunLike (Pmf α) α fun x => ENNReal
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.

Instances For
@[simp]
theorem Pmf.mem_support_iff {α : Type u_1} (p : Pmf α) (a : α) :
a p a 0
@[simp]
theorem Pmf.support_nonempty {α : Type u_1} (p : Pmf α) :
@[simp]
theorem Pmf.support_countable {α : Type u_1} (p : Pmf α) :
theorem Pmf.apply_eq_zero_iff {α : Type u_1} (p : Pmf α) (a : α) :
p a = 0 ¬a
theorem Pmf.apply_pos_iff {α : Type u_1} (p : Pmf α) (a : α) :
0 < p a a
theorem Pmf.apply_eq_one_iff {α : Type u_1} (p : Pmf α) (a : α) :
p a = 1 = {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 α) :

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

Instances For
theorem Pmf.toOuterMeasure_apply {α : Type u_1} (p : Pmf α) (s : Set α) :
↑() s = ∑' (x : α), Set.indicator s (p) x
@[simp]
theorem Pmf.toOuterMeasure_caratheodory {α : Type u_1} (p : Pmf α) :
@[simp]
theorem Pmf.toOuterMeasure_apply_finset {α : Type u_1} (p : Pmf α) (s : ) :
↑() s = Finset.sum s fun x => p x
theorem Pmf.toOuterMeasure_apply_singleton {α : Type u_1} (p : Pmf α) (a : α) :
↑() {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 α} :
p = q
theorem Pmf.toOuterMeasure_apply_eq_zero_iff {α : Type u_1} (p : Pmf α) (s : Set α) :
↑() s = 0 Disjoint () s
theorem Pmf.toOuterMeasure_apply_eq_one_iff {α : Type u_1} (p : Pmf α) (s : Set α) :
↑() s = 1 s
@[simp]
theorem Pmf.toOuterMeasure_apply_inter_support {α : Type u_1} (p : Pmf α) (s : Set α) :
↑() (s ) = ↑() s
theorem Pmf.toOuterMeasure_mono {α : Type u_1} (p : Pmf α) {s : Set α} {t : Set α} (h : s t) :
↑() s ↑() 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 = t ) :
↑() s = ↑() t
@[simp]
theorem Pmf.toOuterMeasure_apply_fintype {α : Type u_1} (p : Pmf α) (s : Set α) [] :
↑() s = Finset.sum Finset.univ fun x => Set.indicator s (p) x
def Pmf.toMeasure {α : Type u_1} [] (p : Pmf α) :

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

Instances For
theorem Pmf.toOuterMeasure_apply_le_toMeasure_apply {α : Type u_1} [] (p : Pmf α) (s : Set α) :
↑() s ↑() s
theorem Pmf.toMeasure_apply_eq_toOuterMeasure_apply {α : Type u_1} [] (p : Pmf α) (s : Set α) (hs : ) :
↑() s = ↑() s
theorem Pmf.toMeasure_apply {α : Type u_1} [] (p : Pmf α) (s : Set α) (hs : ) :
↑() s = ∑' (x : α), Set.indicator s (p) x
theorem Pmf.toMeasure_apply_singleton {α : Type u_1} [] (p : Pmf α) (a : α) (h : ) :
↑() {a} = p a
theorem Pmf.toMeasure_apply_eq_zero_iff {α : Type u_1} [] (p : Pmf α) (s : Set α) (hs : ) :
↑() s = 0 Disjoint () s
theorem Pmf.toMeasure_apply_eq_one_iff {α : Type u_1} [] (p : Pmf α) (s : Set α) (hs : ) :
↑() s = 1 s
@[simp]
theorem Pmf.toMeasure_apply_inter_support {α : Type u_1} [] (p : Pmf α) (s : Set α) (hs : ) (hp : ) :
↑() (s ) = ↑() s
@[simp]
theorem Pmf.restrict_toMeasure_support {α : Type u_1} [] (p : Pmf α) :
theorem Pmf.toMeasure_mono {α : Type u_1} [] (p : Pmf α) {s : Set α} {t : Set α} (hs : ) (ht : ) (h : s t) :
↑() s ↑() t
theorem Pmf.toMeasure_apply_eq_of_inter_support_eq {α : Type u_1} [] (p : Pmf α) {s : Set α} {t : Set α} (hs : ) (ht : ) (h : s = t ) :
↑() s = ↑() t
theorem Pmf.toMeasure_injective {α : Type u_1} [] :
Function.Injective Pmf.toMeasure
@[simp]
theorem Pmf.toMeasure_inj {α : Type u_1} [] {p : Pmf α} {q : Pmf α} :
p = q
@[simp]
theorem Pmf.toMeasure_apply_finset {α : Type u_1} [] (p : Pmf α) (s : ) :
↑() s = Finset.sum s fun x => p x
theorem Pmf.toMeasure_apply_of_finite {α : Type u_1} [] (p : Pmf α) (s : Set α) (hs : ) :
↑() s = ∑' (x : α), Set.indicator s (p) x
@[simp]
theorem Pmf.toMeasure_apply_fintype {α : Type u_1} [] (p : Pmf α) (s : Set α) [] :
↑() s = Finset.sum Finset.univ fun x => Set.indicator s (p) x
def MeasureTheory.Measure.toPmf {α : Type u_1} [] [] (μ : ) :
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.

Instances For
theorem MeasureTheory.Measure.toPmf_apply {α : Type u_1} [] [] (μ : ) (x : α) :
= μ {x}
@[simp]
theorem MeasureTheory.Measure.toPmf_toMeasure {α : Type u_1} [] [] (μ : ) :
instance Pmf.toMeasure.isProbabilityMeasure {α : Type u_1} [] (p : Pmf α) :

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

@[simp]
theorem Pmf.toMeasure_toPmf {α : Type u_1} [] [] (p : Pmf α) :
theorem Pmf.toMeasure_eq_iff_eq_toPmf {α : Type u_1} [] [] (p : Pmf α) (μ : ) :
theorem Pmf.toPmf_eq_iff_toMeasure_eq {α : Type u_1} [] [] (p : Pmf α) (μ : ) :