CencovPetz.CencovFinite

The finite/discrete Čencov (Chentsov) uniqueness theorem under continuity hypotheses.

In the purely algebraic part of the argument, one proves the scalar-multiple identity on:

1. the uniform point;
2. all common-denominator (“rational”) points via splitting.

This file provides the final topological step: since rational points are dense and Fisher is continuous, any continuous monotone metric family coincides everywhere with a fixed scalar multiple of Fisher.

Main result

• CencovPetz.MonotoneMetricFamily.eq_smul_fisher_of_continuous

theorem LeanPool.CencovPetz.MonotoneMetricFamily.eq_smul_fisher_of_continuous (G : MonotoneMetricFamily) {α : Type} [Fintype α] [Nonempty α] {a0 a1 : α} (ha01 : a0 ≠ a1) (hG : ∀ (u v : ↥(tangentSpace α)), Continuous fun (p : Simplex α) => ((G.g p) u) v) (p : Simplex α) (u v : ↥(tangentSpace α)) : ((G.g p) u) v = G.uniformScalar 2 ⋯ * ((fisherBilin p) u) v