Discrete uniform distribution

DefinitionUniform distribution on a finite set#✓fully proved

For a nonempty finite subset \(s\) of a type \(\alpha\), the uniform distribution on \(s\) is the probability mass function on \(\alpha\) that gives mass \(1/|s|\) to each element of \(s\) and mass \(0\) to every other element of \(\alpha\).

noncomputable def uniformFinset (s : Finset α) (hs : s.Nonempty) : PMF α := by
  classical
  refine ofFinset (fun a => if a ∈ s then (s.card : ℝ≥0∞)⁻¹ else 0) s ?_ ?_
  · simp only [Finset.sum_ite_mem, Finset.inter_self, Finset.sum_const, nsmul_eq_mul]
    have h : (s.card : ℝ≥0∞) ≠ 0 := by
      simpa only [Ne, Nat.cast_eq_zero, Finset.card_eq_zero] using
        Finset.nonempty_iff_ne_empty.1 hs
    exact ENNReal.mul_inv_cancel h (ENNReal.natCast_ne_top s.card)
  · exact fun a ha => by simp only [ha, ite_false]

Used by 1

Used byUniform distribution on the whole finite type

DefinitionUniform distribution on a finite type#✓fully proved

For a nonempty finite type \(\alpha\), the uniform distribution on \(\alpha\) is the probability mass function on \(\alpha\) that gives mass \(1/|\alpha|\) to every element of \(\alpha\).

noncomputable def uniformFintype (α : Type*) [Fintype α] [Nonempty α] : PMF α :=
  ofFintype (fun _ => (Fintype.card α : ℝ≥0∞)⁻¹) (by
    simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
    have h : (Fintype.card α : ℝ≥0∞) ≠ 0 := by
      simpa only [Ne, Nat.cast_eq_zero] using (Fintype.card_ne_zero (α := α))
    exact ENNReal.mul_inv_cancel h (ENNReal.natCast_ne_top (Fintype.card α)))

Used by 11

Used byAllele frequencies are conserved · Mendel's law of segregation · Allele transmission law of a parental genotype · Average formula for the expected time over random orderings · Expected number of hires under a random permutation · Haar measure on the dyadic integers · Probability of an event under the uniform distribution · Outer measure of an event under the uniform distribution · Uniform distribution on the whole finite type · Extended expectation under the uniform distribution · Expectation under the uniform distribution

TheoremUniform distribution on the whole finite type#✓fully proved

For a nonempty finite type \(\alpha\), the uniform distribution on the finite set of all elements of \(\alpha\) equals the uniform distribution on \(\alpha\).

@[simp] theorem uniformFinset_univ :
    uniformFinset (Finset.univ : Finset α) Finset.univ_nonempty = uniformFintype α

Uses 2

Statement usesUniform distribution on a finite set · Uniform distribution on a finite type

TheoremOuter measure of an event under the uniform distribution#✓fully proved

Let \(\alpha\) be a nonempty finite type. For every subset \(s \subseteq \alpha\), the outer measure associated to the uniform distribution on \(\alpha\) assigns to \(s\) the value \(|s| / |\alpha|\), computed in the extended nonnegative reals.

theorem toOuterMeasure_uniformFintype_apply (s : Set α) [Fintype s] :
    (uniformFintype α).toOuterMeasure s =
      (Fintype.card s : ℝ≥0∞) / (Fintype.card α : ℝ≥0∞)

Uses 1 · Used by 1

Statement usesUniform distribution on a finite type

Used byProbability of an event under the uniform distribution

TheoremProbability of an event under the uniform distribution#✓fully proved

Let \(\alpha\) be a nonempty finite type carrying a σ-algebra. For every measurable set \(s \subseteq \alpha\), the probability measure associated to the uniform distribution on \(\alpha\) gives \(s\) the measure \(|s| / |\alpha|\), computed in the extended nonnegative reals.

theorem toMeasure_uniformFintype_apply (s : Set α) [MeasurableSpace α]
    (hs : MeasurableSet s) [Fintype s] :
    (uniformFintype α).toMeasure s =
      (Fintype.card s : ℝ≥0∞) / (Fintype.card α : ℝ≥0∞)

Uses 2

Statement usesUniform distribution on a finite type

Proof usesOuter measure of an event under the uniform distribution

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.