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.

Equations
Instances For
    theorem PMF.monad_map_eq_map {α : Type u} {β : Type u} (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 α) :
    (PMF.map f p).support = f '' p.support
    theorem PMF.mem_support_map_iff {α : Type u_1} {β : Type u_2} (f : αβ) (p : PMF α) (b : β) :
    b (PMF.map f p).support ap.support, f a = b
    theorem PMF.bind_pure_comp {α : Type u_1} {β : Type u_2} (f : αβ) (p : PMF α) :
    p.bind (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 (p.bind q) = p.bind 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.map f p).bind q = p.bind (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 β) :
    (PMF.map f p).toOuterMeasure s = p.toOuterMeasure (f ⁻¹' s)
    @[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.map f p).toMeasure s = p.toMeasure (f ⁻¹' s)
    def PMF.seq {α : Type u_1} {β : Type u_2} (q : PMF (αβ)) (p : PMF α) :
    PMF β

    The monadic sequencing operation for PMF.

    Equations
    • q.seq p = q.bind fun (m : αβ) => p.bind fun (a : α) => PMF.pure (m a)
    Instances For
      theorem PMF.monad_seq_eq_seq {α : Type u} {β : Type u} (q : PMF (αβ)) (p : PMF α) :
      (Seq.seq q fun (x : Unit) => p) = q.seq p
      @[simp]
      theorem PMF.seq_apply {α : Type u_1} {β : Type u_2} (q : PMF (αβ)) (p : PMF α) (b : β) :
      (q.seq 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 α) :
      (q.seq p).support = fq.support, f '' p.support
      theorem PMF.mem_support_seq_iff {α : Type u_1} {β : Type u_2} (q : PMF (αβ)) (p : PMF α) (b : β) :
      b (q.seq p).support fq.support, b f '' p.support
      def PMF.ofFinset {α : Type u_1} (f : αENNReal) (s : Finset α) (h : as, f a = 1) (h' : as, f 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.

      Equations
      Instances For
        @[simp]
        theorem PMF.ofFinset_apply {α : Type u_1} {f : αENNReal} {s : Finset α} (h : as, f a = 1) (h' : as, f 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 : as, f a = 1) (h' : as, f a = 0) :
        (PMF.ofFinset f s h h').support = s Function.support f
        theorem PMF.mem_support_ofFinset_iff {α : Type u_1} {f : αENNReal} {s : Finset α} (h : as, f a = 1) (h' : as, f a = 0) (a : α) :
        a (PMF.ofFinset f s h h').support a s f a 0
        theorem PMF.ofFinset_apply_of_not_mem {α : Type u_1} {f : αENNReal} {s : Finset α} (h : as, f a = 1) (h' : as, f a = 0) {a : α} (ha : as) :
        (PMF.ofFinset f s h h') a = 0
        @[simp]
        theorem PMF.toOuterMeasure_ofFinset_apply {α : Type u_1} {f : αENNReal} {s : Finset α} (h : as, f a = 1) (h' : as, f a = 0) (t : Set α) :
        (PMF.ofFinset f s h h').toOuterMeasure t = ∑' (x : α), t.indicator f x
        @[simp]
        theorem PMF.toMeasure_ofFinset_apply {α : Type u_1} {f : αENNReal} {s : Finset α} (h : as, f a = 1) (h' : as, f a = 0) (t : Set α) [MeasurableSpace α] (ht : MeasurableSet t) :
        (PMF.ofFinset f s h h').toMeasure t = ∑' (x : α), t.indicator f x
        def PMF.ofFintype {α : Type u_1} [Fintype α] (f : αENNReal) (h : a : α, f a = 1) :
        PMF α

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

        Equations
        Instances For
          @[simp]
          theorem PMF.ofFintype_apply {α : Type u_1} [Fintype α] {f : αENNReal} (h : a : α, f a = 1) (a : α) :
          (PMF.ofFintype f h) a = f a
          @[simp]
          theorem PMF.support_ofFintype {α : Type u_1} [Fintype α] {f : αENNReal} (h : a : α, f a = 1) :
          theorem PMF.mem_support_ofFintype_iff {α : Type u_1} [Fintype α] {f : αENNReal} (h : a : α, f a = 1) (a : α) :
          a (PMF.ofFintype f h).support f a 0
          @[simp]
          theorem PMF.toOuterMeasure_ofFintype_apply {α : Type u_1} [Fintype α] {f : αENNReal} (h : a : α, f a = 1) (s : Set α) :
          (PMF.ofFintype f h).toOuterMeasure s = ∑' (x : α), s.indicator f x
          @[simp]
          theorem PMF.toMeasure_ofFintype_apply {α : Type u_1} [Fintype α] {f : αENNReal} (h : a : α, f a = 1) (s : Set α) [MeasurableSpace α] (hs : MeasurableSet s) :
          (PMF.ofFintype f h).toMeasure s = ∑' (x : α), s.indicator 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.

          Equations
          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 ) :
            (PMF.normalize f hf0 hf).support = Function.support f
            theorem PMF.mem_support_normalize_iff {α : Type u_1} {f : αENNReal} (hf0 : tsum f 0) (hf : tsum f ) (a : α) :
            a (PMF.normalize f hf0 hf).support f a 0
            def PMF.filter {α : Type u_1} (p : PMF α) (s : Set α) (h : as, a p.support) :
            PMF α

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

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

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

              Equations
              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.bernoulli p h).support = {b : Bool | bif b then p 0 else p 1}
                theorem PMF.mem_support_bernoulli_iff {p : ENNReal} (h : p 1) (b : Bool) :
                b (PMF.bernoulli p h).support bif b then p 0 else p 1