CencovPetz.Uniform

Minimal facts about the uniform distribution on a finite type.

Mathlib already provides uniform distributions as probability measures / PMFs. This file keeps a lightweight α → ℝ “density” version that is sometimes convenient in finite-dimensional calculations.

Main definitions

• uniformDistribution: the constant function 1 / |α|.
• IsUniform: predicate asserting a function is uniform.

@[reducible, inline]

noncomputable abbrev LeanPool.CencovPetz.uniformDistribution {α : Type u} [Fintype α] : α → ℝ

Uniform distribution over a finite type α, defined as 1 / |α| for all elements.

Equations

• LeanPool.CencovPetz.uniformDistribution = Function.const α (1 / ↑(Fintype.card α))

def LeanPool.CencovPetz.IsUniform {α : Type u} [Fintype α] (p : α → ℝ) : Prop

Predicate asserting that a function agrees with uniformDistribution.

Equations

• LeanPool.CencovPetz.IsUniform p = ∀ (a : α), p a = LeanPool.CencovPetz.uniformDistribution a

theorem LeanPool.CencovPetz.uniformDistribution_sum_one {α : Type u} [Fintype α] [Nonempty α] : ∑ a : α, uniformDistribution a = 1

The uniform distribution sums to 1.