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 #
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 eq_smul_fisher_of_isSplitRepresentable._proof_1 * ((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 eq_smul_fisher_of_isSplitRepresentable._proof_1 * ((fisherBilin p) u) v