mathlib3 documentation

probability.probability_mass_function.uniform

Uniform Probability Mass Functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

pmf.uniform_of_finset gives each element in the set equal probability, with 0 probability for elements not in the set.

pmf.uniform_of_fintype gives all elements equal probability, equal to the inverse of the size of the fintype.

pmf.of_multiset 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

source
noncomputable def pmf.uniform_of_finset {α : Type u_1} (s : finset α) (hs : s.nonempty) :
pmf α

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

Equations
source
@[simp]
theorem pmf.uniform_of_finset_apply {α : Type u_1} {s : finset α} (hs : s.nonempty) (a : α) :
⇑(pmf.uniform_of_finset s hs) a = ite (a ∈ s) (↑(s.card))⁻¹ 0
source
theorem pmf.uniform_of_finset_apply_of_mem {α : Type u_1} {s : finset α} (hs : s.nonempty) {a : α} (ha : a ∈ s) :
⇑(pmf.uniform_of_finset s hs) a = (↑(s.card))⁻¹
source
theorem pmf.uniform_of_finset_apply_of_not_mem {α : Type u_1} {s : finset α} (hs : s.nonempty) {a : α} (ha : a ∉ s) :
⇑(pmf.uniform_of_finset s hs) a = 0
source
@[simp]
theorem pmf.support_uniform_of_finset {α : Type u_1} {s : finset α} (hs : s.nonempty) :
(pmf.uniform_of_finset s hs).support = ↑s
source
theorem pmf.mem_support_uniform_of_finset_iff {α : Type u_1} {s : finset α} (hs : s.nonempty) (a : α) :
a ∈ (pmf.uniform_of_finset s hs).support ↔ a ∈ s
source
@[simp]
theorem pmf.to_outer_measure_uniform_of_finset_apply {α : Type u_1} {s : finset α} (hs : s.nonempty) (t : set α) :
⇑((pmf.uniform_of_finset s hs).to_outer_measure) t = ↑((finset.filter (λ (_x : α), _x ∈ t) s).card) / ↑(s.card)
source
@[simp]
theorem pmf.to_measure_uniform_of_finset_apply {α : Type u_1} {s : finset α} (hs : s.nonempty) (t : set α) [measurable_space α] (ht : measurable_set t) :
⇑((pmf.uniform_of_finset s hs).to_measure) t = ↑((finset.filter (λ (_x : α), _x ∈ t) s).card) / ↑(s.card)
source
noncomputable def pmf.uniform_of_fintype (α : Type u_1) [fintype α] [nonempty α] :
pmf α

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

Equations
source
@[simp]
theorem pmf.uniform_of_fintype_apply {α : Type u_1} [fintype α] [nonempty α] (a : α) :
⇑(pmf.uniform_of_fintype α) a = (↑(fintype.card α))⁻¹
source
@[simp]
theorem pmf.support_uniform_of_fintype (α : Type u_1) [fintype α] [nonempty α] :
(pmf.uniform_of_fintype α).support = ⊤
source
theorem pmf.mem_support_uniform_of_fintype {α : Type u_1} [fintype α] [nonempty α] (a : α) :
a ∈ (pmf.uniform_of_fintype α).support
source
theorem pmf.to_outer_measure_uniform_of_fintype_apply {α : Type u_1} [fintype α] [nonempty α] (s : set α) :
⇑((pmf.uniform_of_fintype α).to_outer_measure) s = ↑(fintype.card ↥s) / ↑(fintype.card α)
source
theorem pmf.to_measure_uniform_of_fintype_apply {α : Type u_1} [fintype α] [nonempty α] (s : set α) [measurable_space α] (hs : measurable_set s) :
⇑((pmf.uniform_of_fintype α).to_measure) s = ↑(fintype.card ↥s) / ↑(fintype.card α)
source
noncomputable def pmf.of_multiset {α : 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
source
@[simp]
theorem pmf.of_multiset_apply {α : Type u_1} {s : multiset α} (hs : s ≠ 0) (a : α) :
⇑(pmf.of_multiset s hs) a = ↑(multiset.count a s) / ↑(⇑multiset.card s)
source
@[simp]
theorem pmf.support_of_multiset {α : Type u_1} {s : multiset α} (hs : s ≠ 0) :
(pmf.of_multiset s hs).support = ↑(s.to_finset)
source
theorem pmf.mem_support_of_multiset_iff {α : Type u_1} {s : multiset α} (hs : s ≠ 0) (a : α) :
a ∈ (pmf.of_multiset s hs).support ↔ a ∈ s.to_finset
source
theorem pmf.of_multiset_apply_of_not_mem {α : Type u_1} {s : multiset α} (hs : s ≠ 0) {a : α} (ha : a ∉ s) :
⇑(pmf.of_multiset s hs) a = 0
source
@[simp]
theorem pmf.to_outer_measure_of_multiset_apply {α : Type u_1} {s : multiset α} (hs : s ≠ 0) (t : set α) :
⇑((pmf.of_multiset s hs).to_outer_measure) t = (∑' (x : α), ↑(multiset.count x (multiset.filter (λ (_x : α), _x ∈ t) s))) / ↑(⇑multiset.card s)
source
@[simp]
theorem pmf.to_measure_of_multiset_apply {α : Type u_1} {s : multiset α} (hs : s ≠ 0) (t : set α) [measurable_space α] (ht : measurable_set t) :
⇑((pmf.of_multiset s hs).to_measure) t = (∑' (x : α), ↑(multiset.count x (multiset.filter (λ (_x : α), _x ∈ t) s))) / ↑(⇑multiset.card s)