CencovPetz.UniformScalarConstant #
Show that the uniform-point scalar from UniformScalarMultiple is independent of the simplex
dimension.
At the uniform point on Fin n, UniformScalarMultiple proves G = cₙ · Fisher. This file shows
cₙ is actually a single constant c (independent of n ≥ 2), using replication isometries.
This is a key step toward a genuinely unique finite Čencov/Chentsov statement, rather than a pointwise scalar multiple with a scalar depending on the point.
Main results #
noncomputable def
LeanPool.CencovPetz.MonotoneMetricFamily.uniformScalar
(G : MonotoneMetricFamily)
(n : ℕ)
(hn : 2 ≤ n)
:
The scalar relating a monotone metric family to Fisher at the uniform simplex
of dimension n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LeanPool.CencovPetz.MonotoneMetricFamily.uniformScalar_eq_of_mul
(G : MonotoneMetricFamily)
{n m : ℕ}
(hn : 2 ≤ n)
(hm : 0 < m)
:
theorem
LeanPool.CencovPetz.MonotoneMetricFamily.uniformScalar_eq_uniformScalar_two
(G : MonotoneMetricFamily)
{n : ℕ}
(hn : 2 ≤ n)
: