CencovPetz.UniformScalarMultiple #
At the uniform point on a finite simplex, a monotone metric family's bilinear form is a scalar multiple of the Fisher bilinear form.
This is an algebraic step in the finite Čencov/Chentsov uniqueness proof: permutation invariance
plus the dij relations imply that (at the uniform point) the metric is determined by a single
scalar.
theorem
LeanPool.CencovPetz.TangentFin.Bilin.B_eq_smul_fisherBilin_uniform
{n : ℕ}
(G : MonotoneMetricFamily)
[Nonempty (Fin n)]
(i0 i1 : Fin n)
(hi01 : i0 ≠ i1)
:
B G = (((B G) (Basis.dij i0 i1)) (Basis.dij i0 i1) / (2 * ↑(Fintype.card (Fin n)))) • fisherBilin Simplex.uniform