CencovPetz.UniformSimplex

Package the uniform distribution on a finite type as a point of the open simplex.

noncomputable def LeanPool.CencovPetz.Simplex.uniform {α : Type u_1} [Fintype α] [Nonempty α] : Simplex α

The uniform point of the open simplex.

Equations

• LeanPool.CencovPetz.Simplex.uniform = { p := LeanPool.CencovPetz.uniformDistribution, pos := ⋯, sum_eq_one := ⋯ }

@[simp]

theorem LeanPool.CencovPetz.Simplex.uniform_apply {α : Type u_1} [Fintype α] [Nonempty α] (a : α) : uniform.p a = 1 / ↑(Fintype.card α)