Documentation

Mathlib.Probability.Distributions.Uniform

Uniform distributions and probability mass functions #

This file defines two related notions of uniform distributions, which will be unified in the future.

Uniform distributions #

Defines the uniform distribution for any set with finite measure.

Main definitions #

Uniform probability mass functions #

This file defines a number of uniform PMF distributions from various inputs, uniformly drawing from the corresponding object.

Main definitions #

PMF.uniformOfFinset gives each element in the set equal probability, with 0 probability for elements not in the set.

PMF.uniformOfFintype gives all elements equal probability, equal to the inverse of the size of the Fintype.

PMF.ofMultiset draws randomly from the given Multiset, treating duplicate values as distinct. Each probability is given by the count of the element divided by the size of the Multiset

To Do: #

def MeasureTheory.pdf.IsUniform {E : Type u_1} [MeasurableSpace E] {Ω : Type u_2} :
{x : MeasurableSpace Ω} → (ΩE)Set EMeasureTheory.Measure ΩautoParam (MeasureTheory.Measure E) _auto✝Prop

A random variable X has uniform distribution on s if its push-forward measure is (μ s)⁻¹ • μ.restrict s.

Equations
Instances For
    theorem MeasureTheory.pdf.IsUniform.aemeasurable {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} :
    ∀ {x : MeasurableSpace Ω} { : MeasureTheory.Measure Ω} {X : ΩE} {s : Set E}, μ s 0μ s MeasureTheory.pdf.IsUniform X s μAEMeasurable X
    theorem MeasureTheory.pdf.IsUniform.absolutelyContinuous {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} :
    ∀ {x : MeasurableSpace Ω} { : MeasureTheory.Measure Ω} {X : ΩE} {s : Set E}, MeasureTheory.pdf.IsUniform X s μ(MeasureTheory.Measure.map X ).AbsolutelyContinuous μ
    theorem MeasureTheory.pdf.IsUniform.measure_preimage {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} :
    ∀ {x : MeasurableSpace Ω} { : MeasureTheory.Measure Ω} {X : ΩE} {s : Set E}, μ s 0μ s MeasureTheory.pdf.IsUniform X s μ∀ {A : Set E}, MeasurableSet A (X ⁻¹' A) = μ (s A) / μ s
    theorem MeasureTheory.pdf.IsUniform.isProbabilityMeasure {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} :
    ∀ {x : MeasurableSpace Ω} { : MeasureTheory.Measure Ω} {X : ΩE} {s : Set E}, μ s 0μ s MeasureTheory.pdf.IsUniform X s μMeasureTheory.IsProbabilityMeasure
    theorem MeasureTheory.pdf.IsUniform.hasPDF {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} :
    ∀ {x : MeasurableSpace Ω} { : MeasureTheory.Measure Ω} {X : ΩE} {s : Set E}, μ s 0μ s MeasureTheory.pdf.IsUniform X s μMeasureTheory.HasPDF X μ
    theorem MeasureTheory.pdf.IsUniform.pdf_eq_zero_of_measure_eq_zero_or_top {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} :
    ∀ {x : MeasurableSpace Ω} { : MeasureTheory.Measure Ω} {X : ΩE} {s : Set E}, MeasureTheory.pdf.IsUniform X s μμ s = 0 μ s = MeasureTheory.pdf X μ =ᵐ[μ] 0
    theorem MeasureTheory.pdf.IsUniform.pdf_eq {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} :
    ∀ {x : MeasurableSpace Ω} { : MeasureTheory.Measure Ω} {X : ΩE} {s : Set E}, MeasurableSet sMeasureTheory.pdf.IsUniform X s μMeasureTheory.pdf X μ =ᵐ[μ] s.indicator ((μ s)⁻¹ 1)
    theorem MeasureTheory.pdf.IsUniform.pdf_toReal_ae_eq {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} :
    ∀ {x : MeasurableSpace Ω} { : MeasureTheory.Measure Ω} {X : ΩE} {s : Set E}, MeasurableSet sMeasureTheory.pdf.IsUniform X s μ(fun (x_1 : E) => (MeasureTheory.pdf X μ x_1).toReal) =ᵐ[μ] fun (x : E) => (s.indicator ((μ s)⁻¹ 1) x).toReal
    theorem MeasureTheory.pdf.IsUniform.mul_pdf_integrable {Ω : Type u_2} :
    ∀ {x : MeasurableSpace Ω} { : MeasureTheory.Measure Ω} {X : Ω} {s : Set }, IsCompact sMeasureTheory.pdf.IsUniform X s MeasureTheory.volumeMeasureTheory.Integrable (fun (x_1 : ) => x_1 * (MeasureTheory.pdf X MeasureTheory.volume x_1).toReal) MeasureTheory.volume
    theorem MeasureTheory.pdf.IsUniform.integral_eq {Ω : Type u_2} :
    ∀ {x : MeasurableSpace Ω} { : MeasureTheory.Measure Ω} {X : Ω} {s : Set }, MeasureTheory.pdf.IsUniform X s MeasureTheory.volume∫ (x : Ω), X x = (MeasureTheory.volume s)⁻¹.toReal * ∫ (x : ) in s, x

    A real uniform random variable X with support s has expectation (λ s)⁻¹ * ∫ x in s, x ∂λ where λ is the Lebesgue measure.

    The density of the uniform measure on a set with respect to itself. This allows us to abstract away the choice of random variable and probability space.

    Equations
    Instances For
      theorem MeasureTheory.pdf.uniformPDF_eq_pdf {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} :
      ∀ {x : MeasurableSpace Ω} { : MeasureTheory.Measure Ω} {X : ΩE} {s : Set E}, MeasurableSet sMeasureTheory.pdf.IsUniform X s μ(fun (x : E) => MeasureTheory.pdf.uniformPDF s x μ) =ᵐ[μ] MeasureTheory.pdf X μ

      Check that indeed any uniform random variable has the uniformPDF.

      theorem MeasureTheory.pdf.uniformPDF_ite {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} {x : E} :
      MeasureTheory.pdf.uniformPDF s x μ = if x s then (μ s)⁻¹ else 0

      Alternative way of writing the uniformPDF.

      def PMF.uniformOfFinset {α : Type u_1} (s : Finset α) (hs : s.Nonempty) :
      PMF α

      Uniform distribution taking the same non-zero probability on the nonempty finset s

      Equations
      Instances For
        @[simp]
        theorem PMF.uniformOfFinset_apply {α : Type u_1} {s : Finset α} (hs : s.Nonempty) (a : α) :
        (PMF.uniformOfFinset s hs) a = if a s then (s.card)⁻¹ else 0
        theorem PMF.uniformOfFinset_apply_of_mem {α : Type u_1} {s : Finset α} (hs : s.Nonempty) {a : α} (ha : a s) :
        (PMF.uniformOfFinset s hs) a = (s.card)⁻¹
        theorem PMF.uniformOfFinset_apply_of_not_mem {α : Type u_1} {s : Finset α} (hs : s.Nonempty) {a : α} (ha : as) :
        @[simp]
        theorem PMF.support_uniformOfFinset {α : Type u_1} {s : Finset α} (hs : s.Nonempty) :
        (PMF.uniformOfFinset s hs).support = s
        theorem PMF.mem_support_uniformOfFinset_iff {α : Type u_1} {s : Finset α} (hs : s.Nonempty) (a : α) :
        a (PMF.uniformOfFinset s hs).support a s
        @[simp]
        theorem PMF.toOuterMeasure_uniformOfFinset_apply {α : Type u_1} {s : Finset α} (hs : s.Nonempty) (t : Set α) :
        (PMF.uniformOfFinset s hs).toOuterMeasure t = (Finset.filter (fun (x : α) => x t) s).card / s.card
        @[simp]
        theorem PMF.toMeasure_uniformOfFinset_apply {α : Type u_1} {s : Finset α} (hs : s.Nonempty) (t : Set α) [MeasurableSpace α] (ht : MeasurableSet t) :
        (PMF.uniformOfFinset s hs).toMeasure t = (Finset.filter (fun (x : α) => x t) s).card / s.card
        def PMF.uniformOfFintype (α : Type u_4) [Fintype α] [Nonempty α] :
        PMF α

        The uniform pmf taking the same uniform value on all of the fintype α

        Equations
        Instances For
          @[simp]
          theorem PMF.uniformOfFintype_apply {α : Type u_1} [Fintype α] [Nonempty α] (a : α) :
          @[simp]
          theorem PMF.support_uniformOfFintype (α : Type u_4) [Fintype α] [Nonempty α] :
          theorem PMF.mem_support_uniformOfFintype {α : Type u_1} [Fintype α] [Nonempty α] (a : α) :
          a (PMF.uniformOfFintype α).support
          theorem PMF.toOuterMeasure_uniformOfFintype_apply {α : Type u_1} [Fintype α] [Nonempty α] (s : Set α) :
          (PMF.uniformOfFintype α).toOuterMeasure s = (Fintype.card s) / (Fintype.card α)
          theorem PMF.toMeasure_uniformOfFintype_apply {α : Type u_1} [Fintype α] [Nonempty α] (s : Set α) [MeasurableSpace α] (hs : MeasurableSet s) :
          (PMF.uniformOfFintype α).toMeasure s = (Fintype.card s) / (Fintype.card α)
          def PMF.ofMultiset {α : Type u_1} (s : Multiset α) (hs : s 0) :
          PMF α

          Given a non-empty multiset s we construct the PMF which sends a to the fraction of elements in s that are a.

          Equations
          Instances For
            @[simp]
            theorem PMF.ofMultiset_apply {α : Type u_1} {s : Multiset α} (hs : s 0) (a : α) :
            (PMF.ofMultiset s hs) a = (Multiset.count a s) / (Multiset.card s)
            @[simp]
            theorem PMF.support_ofMultiset {α : Type u_1} {s : Multiset α} (hs : s 0) :
            (PMF.ofMultiset s hs).support = s.toFinset
            theorem PMF.mem_support_ofMultiset_iff {α : Type u_1} {s : Multiset α} (hs : s 0) (a : α) :
            a (PMF.ofMultiset s hs).support a s.toFinset
            theorem PMF.ofMultiset_apply_of_not_mem {α : Type u_1} {s : Multiset α} (hs : s 0) {a : α} (ha : as) :
            (PMF.ofMultiset s hs) a = 0
            @[simp]
            theorem PMF.toOuterMeasure_ofMultiset_apply {α : Type u_1} {s : Multiset α} (hs : s 0) (t : Set α) :
            (PMF.ofMultiset s hs).toOuterMeasure t = (∑' (x : α), (Multiset.count x (Multiset.filter (fun (x : α) => x t) s))) / (Multiset.card s)
            @[simp]
            theorem PMF.toMeasure_ofMultiset_apply {α : Type u_1} {s : Multiset α} (hs : s 0) (t : Set α) [MeasurableSpace α] (ht : MeasurableSet t) :
            (PMF.ofMultiset s hs).toMeasure t = (∑' (x : α), (Multiset.count x (Multiset.filter (fun (x : α) => x t) s))) / (Multiset.card s)