CencovPetz.CencovSplitPoint

Extend the uniform-point scalar-multiple lemma to simplex points that become uniform after a fiberwise split.

This isolates the “rational-point reduction” step in a finite Čencov/Chentsov uniqueness proof: if p has coordinates proportional to a natural multiplicity function m : α → ℕ, then splitting α → Σ a, Fin (m a) sends p to the uniform distribution, and the monotone metric at p is a scalar multiple of Fisher.

Main result

• CencovPetz.MonotoneMetricFamily.eq_smul_fisher_of_isSplitRepresentable

theorem LeanPool.CencovPetz.MonotoneMetricFamily.eq_smul_fisher_of_isSplitRepresentable (G : MonotoneMetricFamily) {α : Type} [Fintype α] [Nonempty α] (p : Simplex α) (hp : p.IsSplitRepresentable) {a0 a1 : α} (ha01 : a0 ≠ a1) (u v : ↥(tangentSpace α)) : ((G.g p) u) v = G.uniformScalar 2 ⋯ * ((fisherBilin p) u) v

If p is split-representable (so it splits to the uniform point), then the metric at p is a scalar multiple of Fisher.

The scalar is the one given by the uniform-point characterization on the split target.

theorem LeanPool.CencovPetz.MonotoneMetricFamily.eq_smul_fisher_of_isRational (G : MonotoneMetricFamily) {α : Type} [Fintype α] [Nonempty α] (p : Simplex α) (hp : p.IsRational) {a0 a1 : α} (ha01 : a0 ≠ a1) (u v : ↥(tangentSpace α)) : ((G.g p) u) v = G.uniformScalar 2 ⋯ * ((fisherBilin p) u) v