Uniform Probability Mass Functions

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

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

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

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

@[simp]

theorem Pmf.uniformOfFinset_apply {α : Type u_1} {s : Finset α} (hs : Finset.Nonempty s) (a : α) : ↑(Pmf.uniformOfFinset s hs) a = if a ∈ s then (↑(Finset.card s))⁻¹ else 0

theorem Pmf.uniformOfFinset_apply_of_mem {α : Type u_1} {s : Finset α} (hs : Finset.Nonempty s) {a : α} (ha : a ∈ s) : ↑(Pmf.uniformOfFinset s hs) a = (↑(Finset.card s))⁻¹

theorem Pmf.uniformOfFinset_apply_of_not_mem {α : Type u_1} {s : Finset α} (hs : Finset.Nonempty s) {a : α} (ha : ¬a ∈ s) : ↑(Pmf.uniformOfFinset s hs) a = 0

@[simp]

theorem Pmf.support_uniformOfFinset {α : Type u_1} {s : Finset α} (hs : Finset.Nonempty s) : Pmf.support (Pmf.uniformOfFinset s hs) = ↑s

theorem Pmf.mem_support_uniformOfFinset_iff {α : Type u_1} {s : Finset α} (hs : Finset.Nonempty s) (a : α) : a ∈ Pmf.support (Pmf.uniformOfFinset s hs) ↔ a ∈ s

@[simp]

theorem Pmf.toOuterMeasure_uniformOfFinset_apply {α : Type u_1} {s : Finset α} (hs : Finset.Nonempty s) (t : Set α) : ↑(Pmf.toOuterMeasure (Pmf.uniformOfFinset s hs)) t = ↑(Finset.card (Finset.filter (fun x => x ∈ t) s)) / ↑(Finset.card s)

@[simp]

theorem Pmf.toMeasure_uniformOfFinset_apply {α : Type u_1} {s : Finset α} (hs : Finset.Nonempty s) (t : Set α) [MeasurableSpace α] (ht : MeasurableSet t) : ↑↑(Pmf.toMeasure (Pmf.uniformOfFinset s hs)) t = ↑(Finset.card (Finset.filter (fun x => x ∈ t) s)) / ↑(Finset.card s)

def Pmf.uniformOfFintype (α : Type u_4) [Fintype α] [Nonempty α] : Pmf α

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

@[simp]

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

@[simp]

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

theorem Pmf.mem_support_uniformOfFintype {α : Type u_1} [Fintype α] [Nonempty α] (a : α) : a ∈ Pmf.support (Pmf.uniformOfFintype α)

theorem Pmf.toOuterMeasure_uniformOfFintype_apply {α : Type u_1} [Fintype α] [Nonempty α] (s : Set α) : ↑(Pmf.toOuterMeasure (Pmf.uniformOfFintype α)) s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)

theorem Pmf.toMeasure_uniformOfFintype_apply {α : Type u_1} [Fintype α] [Nonempty α] (s : Set α) [MeasurableSpace α] (hs : MeasurableSet s) : ↑↑(Pmf.toMeasure (Pmf.uniformOfFintype α)) 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.

@[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.support (Pmf.ofMultiset s hs) = ↑(Multiset.toFinset s)

theorem Pmf.mem_support_ofMultiset_iff {α : Type u_1} {s : Multiset α} (hs : s ≠ 0) (a : α) : a ∈ Pmf.support (Pmf.ofMultiset s hs) ↔ a ∈ Multiset.toFinset s

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.toOuterMeasure (Pmf.ofMultiset s hs)) 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.toMeasure (Pmf.ofMultiset s hs)) t = (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s))) / ↑(↑Multiset.card s)