CencovPetz.SplittingUniform

If a simplex point p has coordinates proportional to a fiber-multiplicity function m : α → ℕ, then the fiberwise splitting Markov morphism α → Σ a, Fin (m a) pushes p forward to the uniform distribution on the split target.

This is one of the standard reduction steps in finite Čencov/Chentsov uniqueness arguments.

Main result

• CencovPetz.MarkovMorphism.split_pushforward_eq_uniform_of_apply_eq_div_card

def LeanPool.CencovPetz.Simplex.IsSplitRepresentable {α : Type u} [Fintype α] (p : Simplex α) : Prop

A simplex point whose coordinates are proportional to a natural multiplicity function.

Such points become uniform after applying the fiberwise splitting Markov morphism α → Σ a, Fin (m a). This is the standard “rational-point” reduction step in finite Čencov/Chentsov arguments.

Equations

• p.IsSplitRepresentable = ∃ (m : α → ℕ), (∀ (a : α), 0 < m a) ∧ ∀ (a : α), p.p a = ↑(m a) / ↑(Fintype.card (LeanPool.CencovPetz.MarkovMorphism.SplitTarget m))

theorem LeanPool.CencovPetz.MarkovMorphism.split_pushforward_eq_uniform_of_apply_eq_div_card {α : Type u} [Fintype α] [Nonempty α] (m : α → ℕ) (hm : ∀ (a : α), 0 < m a) (p : Simplex α) (hp : ∀ (a : α), p.p a = ↑(m a) / ↑(Fintype.card (SplitTarget m))) : (split m hm).pushforward p = Simplex.uniform