Documentation

Mathlib.Probability.ProbabilityMassFunction.Constructions

Specific Constructions of Probability Mass Functions #

This file gives a number of different Pmf constructions for common probability distributions.

map and seq allow pushing a Pmf α along a function f : α → β (or distribution of functions f : Pmf (α → β)) to get a Pmf β.

ofFinset and ofFintype simplify the construction of a Pmf α from a function f : α → ℝ≥0∞, by allowing the "sum equals 1" constraint to be in terms of Finset.sum instead of tsum.

normalize constructs a Pmf α by normalizing a function f : α → ℝ≥0∞ by its sum, and filter uses this to filter the support of a Pmf and re-normalize the new distribution.

bernoulli represents the bernoulli distribution on Bool.

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

The functorial action of a function on a Pmf.

Instances For
    theorem Pmf.monad_map_eq_map {α : Type u_4} {β : Type u_4} (f : αβ) (p : Pmf α) :
    f <$> p = Pmf.map f p
    @[simp]
    theorem Pmf.map_apply {α : Type u_1} {β : Type u_2} (f : αβ) (p : Pmf α) (b : β) :
    ↑(Pmf.map f p) b = ∑' (a : α), if b = f a then p a else 0
    @[simp]
    theorem Pmf.support_map {α : Type u_1} {β : Type u_2} (f : αβ) (p : Pmf α) :
    theorem Pmf.mem_support_map_iff {α : Type u_1} {β : Type u_2} (f : αβ) (p : Pmf α) (b : β) :
    b Pmf.support (Pmf.map f p) a, a Pmf.support p f a = b
    theorem Pmf.bind_pure_comp {α : Type u_1} {β : Type u_2} (f : αβ) (p : Pmf α) :
    Pmf.bind p (Pmf.pure f) = Pmf.map f p
    theorem Pmf.map_id {α : Type u_1} (p : Pmf α) :
    Pmf.map id p = p
    theorem Pmf.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (p : Pmf α) (g : βγ) :
    Pmf.map g (Pmf.map f p) = Pmf.map (g f) p
    theorem Pmf.pure_map {α : Type u_1} {β : Type u_2} (f : αβ) (a : α) :
    theorem Pmf.map_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : Pmf α) (q : αPmf β) (f : βγ) :
    Pmf.map f (Pmf.bind p q) = Pmf.bind p fun a => Pmf.map f (q a)
    @[simp]
    theorem Pmf.bind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : Pmf α) (f : αβ) (q : βPmf γ) :
    Pmf.bind (Pmf.map f p) q = Pmf.bind p (q f)
    @[simp]
    theorem Pmf.map_const {α : Type u_1} {β : Type u_2} (p : Pmf α) (b : β) :
    @[simp]
    theorem Pmf.toOuterMeasure_map_apply {α : Type u_1} {β : Type u_2} (f : αβ) (p : Pmf α) (s : Set β) :
    @[simp]
    theorem Pmf.toMeasure_map_apply {α : Type u_1} {β : Type u_2} (f : αβ) (p : Pmf α) (s : Set β) [MeasurableSpace α] [MeasurableSpace β] (hf : Measurable f) (hs : MeasurableSet s) :
    ↑(Pmf.toMeasure (Pmf.map f p)) s = ↑(Pmf.toMeasure p) (f ⁻¹' s)
    def Pmf.seq {α : Type u_1} {β : Type u_2} (q : Pmf (αβ)) (p : Pmf α) :
    Pmf β

    The monadic sequencing operation for Pmf.

    Instances For
      theorem Pmf.monad_seq_eq_seq {α : Type u_4} {β : Type u_4} (q : Pmf (αβ)) (p : Pmf α) :
      (Seq.seq q fun x => p) = Pmf.seq q p
      @[simp]
      theorem Pmf.seq_apply {α : Type u_1} {β : Type u_2} (q : Pmf (αβ)) (p : Pmf α) (b : β) :
      ↑(Pmf.seq q p) b = ∑' (f : αβ) (a : α), if b = f a then q f * p a else 0
      @[simp]
      theorem Pmf.support_seq {α : Type u_1} {β : Type u_2} (q : Pmf (αβ)) (p : Pmf α) :
      Pmf.support (Pmf.seq q p) = ⋃ (f : αβ) (_ : f Pmf.support q), f '' Pmf.support p
      theorem Pmf.mem_support_seq_iff {α : Type u_1} {β : Type u_2} (q : Pmf (αβ)) (p : Pmf α) (b : β) :
      def Pmf.ofFinset {α : Type u_1} (f : αENNReal) (s : Finset α) (h : (Finset.sum s fun a => f a) = 1) (h' : ∀ (a : α), ¬a sf a = 0) :
      Pmf α

      Given a finset s and a function f : α → ℝ≥0∞ with sum 1 on s, such that f a = 0 for a ∉ s, we get a Pmf.

      Instances For
        @[simp]
        theorem Pmf.ofFinset_apply {α : Type u_1} {f : αENNReal} {s : Finset α} (h : (Finset.sum s fun a => f a) = 1) (h' : ∀ (a : α), ¬a sf a = 0) (a : α) :
        ↑(Pmf.ofFinset f s h h') a = f a
        @[simp]
        theorem Pmf.support_ofFinset {α : Type u_1} {f : αENNReal} {s : Finset α} (h : (Finset.sum s fun a => f a) = 1) (h' : ∀ (a : α), ¬a sf a = 0) :
        theorem Pmf.mem_support_ofFinset_iff {α : Type u_1} {f : αENNReal} {s : Finset α} (h : (Finset.sum s fun a => f a) = 1) (h' : ∀ (a : α), ¬a sf a = 0) (a : α) :
        a Pmf.support (Pmf.ofFinset f s h h') a s f a 0
        theorem Pmf.ofFinset_apply_of_not_mem {α : Type u_1} {f : αENNReal} {s : Finset α} (h : (Finset.sum s fun a => f a) = 1) (h' : ∀ (a : α), ¬a sf a = 0) {a : α} (ha : ¬a s) :
        ↑(Pmf.ofFinset f s h h') a = 0
        @[simp]
        theorem Pmf.toOuterMeasure_ofFinset_apply {α : Type u_1} {f : αENNReal} {s : Finset α} (h : (Finset.sum s fun a => f a) = 1) (h' : ∀ (a : α), ¬a sf a = 0) (t : Set α) :
        ↑(Pmf.toOuterMeasure (Pmf.ofFinset f s h h')) t = ∑' (x : α), Set.indicator t f x
        @[simp]
        theorem Pmf.toMeasure_ofFinset_apply {α : Type u_1} {f : αENNReal} {s : Finset α} (h : (Finset.sum s fun a => f a) = 1) (h' : ∀ (a : α), ¬a sf a = 0) (t : Set α) [MeasurableSpace α] (ht : MeasurableSet t) :
        ↑(Pmf.toMeasure (Pmf.ofFinset f s h h')) t = ∑' (x : α), Set.indicator t f x
        def Pmf.ofFintype {α : Type u_1} [Fintype α] (f : αENNReal) (h : (Finset.sum Finset.univ fun a => f a) = 1) :
        Pmf α

        Given a finite type α and a function f : α → ℝ≥0∞ with sum 1, we get a Pmf.

        Instances For
          @[simp]
          theorem Pmf.ofFintype_apply {α : Type u_1} [Fintype α] {f : αENNReal} (h : (Finset.sum Finset.univ fun a => f a) = 1) (a : α) :
          ↑(Pmf.ofFintype f h) a = f a
          @[simp]
          theorem Pmf.support_ofFintype {α : Type u_1} [Fintype α] {f : αENNReal} (h : (Finset.sum Finset.univ fun a => f a) = 1) :
          theorem Pmf.mem_support_ofFintype_iff {α : Type u_1} [Fintype α] {f : αENNReal} (h : (Finset.sum Finset.univ fun a => f a) = 1) (a : α) :
          @[simp]
          theorem Pmf.toOuterMeasure_ofFintype_apply {α : Type u_1} [Fintype α] {f : αENNReal} (h : (Finset.sum Finset.univ fun a => f a) = 1) (s : Set α) :
          ↑(Pmf.toOuterMeasure (Pmf.ofFintype f h)) s = ∑' (x : α), Set.indicator s f x
          @[simp]
          theorem Pmf.toMeasure_ofFintype_apply {α : Type u_1} [Fintype α] {f : αENNReal} (h : (Finset.sum Finset.univ fun a => f a) = 1) (s : Set α) [MeasurableSpace α] (hs : MeasurableSet s) :
          ↑(Pmf.toMeasure (Pmf.ofFintype f h)) s = ∑' (x : α), Set.indicator s f x
          def Pmf.normalize {α : Type u_1} (f : αENNReal) (hf0 : tsum f 0) (hf : tsum f ) :
          Pmf α

          Given an f with non-zero and non-infinite sum, get a Pmf by normalizing f by its tsum.

          Instances For
            @[simp]
            theorem Pmf.normalize_apply {α : Type u_1} {f : αENNReal} (hf0 : tsum f 0) (hf : tsum f ) (a : α) :
            ↑(Pmf.normalize f hf0 hf) a = f a * (∑' (x : α), f x)⁻¹
            @[simp]
            theorem Pmf.support_normalize {α : Type u_1} {f : αENNReal} (hf0 : tsum f 0) (hf : tsum f ) :
            theorem Pmf.mem_support_normalize_iff {α : Type u_1} {f : αENNReal} (hf0 : tsum f 0) (hf : tsum f ) (a : α) :
            a Pmf.support (Pmf.normalize f hf0 hf) f a 0
            def Pmf.filter {α : Type u_1} (p : Pmf α) (s : Set α) (h : a, a s a Pmf.support p) :
            Pmf α

            Create new Pmf by filtering on a set with non-zero measure and normalizing.

            Instances For
              @[simp]
              theorem Pmf.filter_apply {α : Type u_1} {p : Pmf α} {s : Set α} (h : a, a s a Pmf.support p) (a : α) :
              ↑(Pmf.filter p s h) a = Set.indicator s (p) a * (∑' (a' : α), Set.indicator s (p) a')⁻¹
              theorem Pmf.filter_apply_eq_zero_of_not_mem {α : Type u_1} {p : Pmf α} {s : Set α} (h : a, a s a Pmf.support p) {a : α} (ha : ¬a s) :
              ↑(Pmf.filter p s h) a = 0
              theorem Pmf.mem_support_filter_iff {α : Type u_1} {p : Pmf α} {s : Set α} (h : a, a s a Pmf.support p) {a : α} :
              @[simp]
              theorem Pmf.support_filter {α : Type u_1} {p : Pmf α} {s : Set α} (h : a, a s a Pmf.support p) :
              theorem Pmf.filter_apply_eq_zero_iff {α : Type u_1} {p : Pmf α} {s : Set α} (h : a, a s a Pmf.support p) (a : α) :
              ↑(Pmf.filter p s h) a = 0 ¬a s ¬a Pmf.support p
              theorem Pmf.filter_apply_ne_zero_iff {α : Type u_1} {p : Pmf α} {s : Set α} (h : a, a s a Pmf.support p) (a : α) :
              ↑(Pmf.filter p s h) a 0 a s a Pmf.support p
              def Pmf.bernoulli (p : ENNReal) (h : p 1) :

              A Pmf which assigns probability p to true and 1 - p to false.

              Instances For
                @[simp]
                theorem Pmf.bernoulli_apply {p : ENNReal} (h : p 1) (b : Bool) :
                ↑(Pmf.bernoulli p h) b = bif b then p else 1 - p
                @[simp]
                theorem Pmf.support_bernoulli {p : ENNReal} (h : p 1) :
                Pmf.support (Pmf.bernoulli p h) = {b | bif b then p 0 else p 1}
                theorem Pmf.mem_support_bernoulli_iff {p : ENNReal} (h : p 1) (b : Bool) :
                b Pmf.support (Pmf.bernoulli p h) bif b then p 0 else p 1