CencovPetz.ReplicationInvariance #
For a monotone metric family (Čencov setting), replication maps α → α × Fin m are isometries:
they have a deterministic left inverse (coarsening), so monotonicity holds in both directions.
theorem
LeanPool.CencovPetz.MonotoneMetricFamily.comp_eq_of_replicate
{α : Type u}
[Fintype α]
(G : MonotoneMetricFamily)
(m : ℕ)
(hm : 0 < m)
(p : Simplex α)
:
(G.g ((MarkovMorphism.replicate m hm).pushforward p)).comp (MarkovMorphism.replicate m hm).tangentPushforwardLinear
(MarkovMorphism.replicate m hm).tangentPushforwardLinear = G.g p
theorem
LeanPool.CencovPetz.MonotoneMetricFamily.eq_of_replicate
{α : Type u}
[Fintype α]
(G : MonotoneMetricFamily)
(m : ℕ)
(hm : 0 < m)
(p : Simplex α)
(u v : ↥(tangentSpace α))
:
((G.g ((MarkovMorphism.replicate m hm).pushforward p)) ((MarkovMorphism.replicate m hm).tangentPushforward u))
((MarkovMorphism.replicate m hm).tangentPushforward v) = ((G.g p) u) v