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.

Equations
Instances For
    instance PMF.instFunLike {α : Type u_1} :
    Equations
    • PMF.instFunLike = { coe := fun (p : PMF α) (a : α) => p a, coe_injective' := }
    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
    Instances For
      @[simp]
      theorem PMF.mem_support_iff {α : Type u_1} (p : PMF α) (a : α) :
      @[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 aPMF.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 <

      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
      Instances For
        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_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 α} :
        theorem PMF.toOuterMeasure_apply_eq_zero_iff {α : Type u_1} (p : PMF α) (s : Set α) :
        theorem PMF.toOuterMeasure_apply_eq_one_iff {α : Type u_1} (p : PMF α) (s : Set α) :
        @[simp]
        theorem PMF.toOuterMeasure_apply_inter_support {α : Type u_1} (p : PMF α) (s : Set α) :
        theorem PMF.toOuterMeasure_mono {α : Type u_1} (p : PMF α) {s : Set α} {t : Set α} (h : s PMF.support 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) :
        @[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

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

        Equations
        Instances For
          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
          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
          @[simp]
          theorem PMF.toMeasure_inj {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {p : PMF α} {q : PMF α} :
          @[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

          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
          Instances For

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

            Equations
            • =