Finite Čencov-Petz Uniqueness

Source: url:https://bookstore.ams.org/mmono-53 Authors: Adam Benenson Status: verified Main declarations: LeanPool.CencovPetz.MonotoneMetricFamily.eq_smul_fisher_of_continuous Tags: information-geometry, fisher-information, markov-morphisms, finite-simplex MSC: 62B10, 53C21

This project formalizes the finite/discrete Čencov-Petz uniqueness theorem: every continuous monotone metric family on finite probability simplexes is a scalar multiple of the Fisher information metric. The imported declarations are placed under LeanPool.CencovPetz.