CencovPetz.FisherContinuity #
Continuity of the finite Fisher bilinear form as a function of the simplex point.
This is a small topological lemma used to extend the finite Čencov/Chentsov identity from a dense family of rational points to all simplex points under continuity hypotheses on a monotone metric family.
Main result #
theorem
LeanPool.CencovPetz.Simplex.continuous_fisherBilin_apply
{α : Type u_1}
[Fintype α]
(u v : ↥(tangentSpace α))
:
Continuous fun (p : Simplex α) => ((fisherBilin p) u) v