Documentation

Mathlib.Probability.ProbabilityMassFunction.Monad

Monad Operations for Probability Mass Functions #

This file constructs two operations on Pmf that give it a monad structure. pure a is the distribution where a single value a has probability 1. bind pa pb : Pmf β is the distribution given by sampling a : α from pa : Pmf α, and then sampling from pb a : Pmf β to get a final result b : β.

bindOnSupport generalizes bind to allow binding to a partial function, so that the second argument only needs to be defined on the support of the first argument.

def Pmf.pure {α : Type u_1} (a : α) :
Pmf α

The pure Pmf is the Pmf where all the mass lies in one point. The value of pure a is 1 at a and 0 elsewhere.

Instances For
    @[simp]
    theorem Pmf.pure_apply {α : Type u_1} (a : α) (a' : α) :
    ↑(Pmf.pure a) a' = if a' = a then 1 else 0
    @[simp]
    theorem Pmf.support_pure {α : Type u_1} (a : α) :
    theorem Pmf.mem_support_pure_iff {α : Type u_1} (a : α) (a' : α) :
    theorem Pmf.pure_apply_self {α : Type u_1} (a : α) :
    ↑(Pmf.pure a) a = 1
    theorem Pmf.pure_apply_of_ne {α : Type u_1} (a : α) (a' : α) (h : a' a) :
    ↑(Pmf.pure a) a' = 0
    instance Pmf.instInhabitedPmf {α : Type u_1} [Inhabited α] :
    @[simp]
    theorem Pmf.toOuterMeasure_pure_apply {α : Type u_1} (a : α) (s : Set α) :
    ↑(Pmf.toOuterMeasure (Pmf.pure a)) s = if a s then 1 else 0
    @[simp]
    theorem Pmf.toMeasure_pure_apply {α : Type u_1} (a : α) (s : Set α) [MeasurableSpace α] (hs : MeasurableSet s) :
    ↑(Pmf.toMeasure (Pmf.pure a)) s = if a s then 1 else 0

    The measure of a set under pure a is 1 for sets containing a and 0 otherwise.

    def Pmf.bind {α : Type u_1} {β : Type u_2} (p : Pmf α) (f : αPmf β) :
    Pmf β

    The monadic bind operation for Pmf.

    Instances For
      @[simp]
      theorem Pmf.bind_apply {α : Type u_1} {β : Type u_2} (p : Pmf α) (f : αPmf β) (b : β) :
      ↑(Pmf.bind p f) b = ∑' (a : α), p a * ↑(f a) b
      @[simp]
      theorem Pmf.support_bind {α : Type u_1} {β : Type u_2} (p : Pmf α) (f : αPmf β) :
      Pmf.support (Pmf.bind p f) = ⋃ (a : α) (_ : a Pmf.support p), Pmf.support (f a)
      theorem Pmf.mem_support_bind_iff {α : Type u_1} {β : Type u_2} (p : Pmf α) (f : αPmf β) (b : β) :
      @[simp]
      theorem Pmf.pure_bind {α : Type u_1} {β : Type u_2} (a : α) (f : αPmf β) :
      Pmf.bind (Pmf.pure a) f = f a
      @[simp]
      theorem Pmf.bind_pure {α : Type u_1} (p : Pmf α) :
      Pmf.bind p Pmf.pure = p
      @[simp]
      theorem Pmf.bind_const {α : Type u_1} {β : Type u_2} (p : Pmf α) (q : Pmf β) :
      (Pmf.bind p fun x => q) = q
      @[simp]
      theorem Pmf.bind_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : Pmf α) (f : αPmf β) (g : βPmf γ) :
      Pmf.bind (Pmf.bind p f) g = Pmf.bind p fun a => Pmf.bind (f a) g
      theorem Pmf.bind_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : Pmf α) (q : Pmf β) (f : αβPmf γ) :
      (Pmf.bind p fun a => Pmf.bind q (f a)) = Pmf.bind q fun b => Pmf.bind p fun a => f a b
      @[simp]
      theorem Pmf.toOuterMeasure_bind_apply {α : Type u_1} {β : Type u_2} (p : Pmf α) (f : αPmf β) (s : Set β) :
      ↑(Pmf.toOuterMeasure (Pmf.bind p f)) s = ∑' (a : α), p a * ↑(Pmf.toOuterMeasure (f a)) s
      @[simp]
      theorem Pmf.toMeasure_bind_apply {α : Type u_1} {β : Type u_2} (p : Pmf α) (f : αPmf β) (s : Set β) [MeasurableSpace β] (hs : MeasurableSet s) :
      ↑(Pmf.toMeasure (Pmf.bind p f)) s = ∑' (a : α), p a * ↑(Pmf.toMeasure (f a)) s

      The measure of a set under p.bind f is the sum over a : α of the probability of a under p times the measure of the set under f a.

      def Pmf.bindOnSupport {α : Type u_1} {β : Type u_2} (p : Pmf α) (f : (a : α) → a Pmf.support pPmf β) :
      Pmf β

      Generalized version of bind allowing f to only be defined on the support of p. p.bind f is equivalent to p.bindOnSupport (fun a _ ↦ f a), see bindOnSupport_eq_bind.

      Instances For
        @[simp]
        theorem Pmf.bindOnSupport_apply {α : Type u_1} {β : Type u_2} {p : Pmf α} (f : (a : α) → a Pmf.support pPmf β) (b : β) :
        ↑(Pmf.bindOnSupport p f) b = ∑' (a : α), p a * if h : p a = 0 then 0 else ↑(f a h) b
        @[simp]
        theorem Pmf.support_bindOnSupport {α : Type u_1} {β : Type u_2} {p : Pmf α} (f : (a : α) → a Pmf.support pPmf β) :
        Pmf.support (Pmf.bindOnSupport p f) = ⋃ (a : α) (h : a Pmf.support p), Pmf.support (f a h)
        theorem Pmf.mem_support_bindOnSupport_iff {α : Type u_1} {β : Type u_2} {p : Pmf α} (f : (a : α) → a Pmf.support pPmf β) (b : β) :
        b Pmf.support (Pmf.bindOnSupport p f) a h, b Pmf.support (f a h)
        @[simp]
        theorem Pmf.bindOnSupport_eq_bind {α : Type u_1} {β : Type u_2} (p : Pmf α) (f : αPmf β) :
        (Pmf.bindOnSupport p fun a x => f a) = Pmf.bind p f

        bindOnSupport reduces to bind if f doesn't depend on the additional hypothesis.

        theorem Pmf.bindOnSupport_eq_zero_iff {α : Type u_1} {β : Type u_2} {p : Pmf α} (f : (a : α) → a Pmf.support pPmf β) (b : β) :
        ↑(Pmf.bindOnSupport p f) b = 0 ∀ (a : α) (ha : p a 0), ↑(f a ha) b = 0
        @[simp]
        theorem Pmf.pure_bindOnSupport {α : Type u_1} {β : Type u_2} (a : α) (f : (a' : α) → a' Pmf.support (Pmf.pure a)Pmf β) :
        theorem Pmf.bindOnSupport_pure {α : Type u_1} (p : Pmf α) :
        (Pmf.bindOnSupport p fun a x => Pmf.pure a) = p
        @[simp]
        theorem Pmf.bindOnSupport_bindOnSupport {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : Pmf α) (f : (a : α) → a Pmf.support pPmf β) (g : (b : β) → b Pmf.support (Pmf.bindOnSupport p f)Pmf γ) :
        Pmf.bindOnSupport (Pmf.bindOnSupport p f) g = Pmf.bindOnSupport p fun a ha => Pmf.bindOnSupport (f a ha) fun b hb => g b (_ : b Pmf.support (Pmf.bindOnSupport p f))
        theorem Pmf.bindOnSupport_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : Pmf α) (q : Pmf β) (f : (a : α) → a Pmf.support p(b : β) → b Pmf.support qPmf γ) :
        (Pmf.bindOnSupport p fun a ha => Pmf.bindOnSupport q (f a ha)) = Pmf.bindOnSupport q fun b hb => Pmf.bindOnSupport p fun a ha => f a ha b hb
        @[simp]
        theorem Pmf.toOuterMeasure_bindOnSupport_apply {α : Type u_1} {β : Type u_2} {p : Pmf α} (f : (a : α) → a Pmf.support pPmf β) (s : Set β) :
        ↑(Pmf.toOuterMeasure (Pmf.bindOnSupport p f)) s = ∑' (a : α), p a * if h : p a = 0 then 0 else ↑(Pmf.toOuterMeasure (f a h)) s
        @[simp]
        theorem Pmf.toMeasure_bindOnSupport_apply {α : Type u_1} {β : Type u_2} {p : Pmf α} (f : (a : α) → a Pmf.support pPmf β) (s : Set β) [MeasurableSpace β] (hs : MeasurableSet s) :
        ↑(Pmf.toMeasure (Pmf.bindOnSupport p f)) s = ∑' (a : α), p a * if h : p a = 0 then 0 else ↑(Pmf.toMeasure (f a h)) s

        The measure of a set under p.bindOnSupport f is the sum over a : α of the probability of a under p times the measure of the set under f a _. The additional if statement is needed since f is only a partial function.