CencovPetz.RationalPoint

Common-denominator (“rational”) points of the finite open simplex.

The classical finite Čencov/Chentsov argument typically proves the scalar-multiple claim first at the uniform point, then extends it to a dense family of points with rational coordinates by a fiberwise splitting construction.

This file packages the notion of a common-denominator point and relates it to Simplex.IsSplitRepresentable.

Main definitions

• CencovPetz.Simplex.IsRational: p(a) = m(a) / (∑ m) for some m : α → ℕ with strictly positive coordinates.

Main results

• CencovPetz.Simplex.IsRational.isSplitRepresentable

theorem LeanPool.CencovPetz.MarkovMorphism.card_splitTarget {α : Type u} [Fintype α] (m : α → ℕ) : Fintype.card (SplitTarget m) = ∑ a : α, m a

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

A simplex point whose coordinates have a finite common-denominator representation p(a) = m(a) / (∑ m) for some strictly positive m : α → ℕ.

Equations

• p.IsRational = ∃ (m : α → ℕ), (∀ (a : α), 0 < m a) ∧ ∀ (a : α), p.p a = ↑(m a) / ↑(∑ a : α, m a)

theorem LeanPool.CencovPetz.Simplex.IsRational.isSplitRepresentable {α : Type u} [Fintype α] {p : Simplex α} (hp : p.IsRational) : p.IsSplitRepresentable