FintypePMF.uniform: uniform distribution over a nonempty Fintype

Built on FintypePMF.normalize with the all-ones weight vector. Functionally parallels Mathlib.PMF.uniformOfFintype, but lives in the ℝ-valued world needed for the MWU arithmetic.

noncomputable def ProbabilityTheory.FintypePMF.uniform (α : Type u_1) [Fintype α] [Nonempty α] : FintypePMF α

Uniform FintypePMF over a nonempty Fintype.

Equations

• ProbabilityTheory.FintypePMF.uniform α = ProbabilityTheory.FintypePMF.normalize (fun (x : α) => 1) ⋯