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

• IsUniform X s ℙ μ : A random variable X has uniform distribution on s under ℙ if the push-forward measure agrees with the rescaled restricted measure μ.

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

TODO

• Refactor the PMF definitions to come from a uniformMeasure on a Finset/Fintype/Multiset.

def MeasureTheory.pdf.IsUniform {E : Type u_1} [MeasurableSpace E] {Ω : Type u_2} : {x : MeasurableSpace Ω} → (Ω → E) → Set E → MeasureTheory.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

• MeasureTheory.pdf.IsUniform X s ℙ μ = (MeasureTheory.Measure.map X ℙ = ProbabilityTheory.cond μ s)

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.toMeasurable_iff {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 (MeasureTheory.toMeasurable μ s) ℙ μ ↔ MeasureTheory.pdf.IsUniform X s ℙ μ

theorem MeasureTheory.pdf.IsUniform.toMeasurable {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.pdf.IsUniform X (MeasureTheory.toMeasurable μ s) ℙ μ

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 s → MeasureTheory.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 s → MeasureTheory.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 s → MeasureTheory.pdf.IsUniform X s ℙ MeasureTheory.volume → MeasureTheory.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.

theorem MeasureTheory.pdf.IsUniform.cond {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {s : Set E} : MeasureTheory.pdf.IsUniform id s (ProbabilityTheory.cond μ s) μ

def MeasureTheory.pdf.uniformPDF {E : Type u_1} [MeasurableSpace E] (s : Set E) (x : E) (μ : autoParam (MeasureTheory.Measure E) _auto✝) : ENNReal

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

• MeasureTheory.pdf.uniformPDF s x μ = s.indicator ((μ s)⁻¹ • 1) x

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 s → MeasureTheory.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

• PMF.uniformOfFinset s hs = PMF.ofFinset (fun (a : α) => if a ∈ s then (↑s.card)⁻¹ else 0) s ⋯ ⋯

@[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 : a ∉ s) : (PMF.uniformOfFinset s hs) a = 0

@[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_2) [Fintype α] [Nonempty α] : PMF α

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

Equations

• PMF.uniformOfFintype α = PMF.uniformOfFinset Finset.univ ⋯

@[simp]

theorem PMF.uniformOfFintype_apply {α : Type u_1} [Fintype α] [Nonempty α] (a : α) : (PMF.uniformOfFintype α) a = (↑(Fintype.card α))⁻¹

@[simp]

theorem PMF.support_uniformOfFintype (α : Type u_2) [Fintype α] [Nonempty α] : (PMF.uniformOfFintype α).support = ⊤

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

• PMF.ofMultiset s hs = ⟨fun (a : α) => ↑(Multiset.count a s) / ↑(Multiset.card s), ⋯⟩

@[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 : a ∉ s) : (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)