CencovPetz.SplittingInvariance #
For a monotone metric family (Čencov setting), fiberwise splitting maps α → Σ a, Fin (m a) are
isometries: they have a deterministic left inverse (merge), so monotonicity holds in both
directions.
theorem
LeanPool.CencovPetz.MonotoneMetricFamily.comp_eq_of_split
{α : Type u}
[Fintype α]
(G : MonotoneMetricFamily)
(m : α → ℕ)
(hm : ∀ (a : α), 0 < m a)
(p : Simplex α)
:
(G.g ((MarkovMorphism.split m hm).pushforward p)).comp (MarkovMorphism.split m hm).tangentPushforwardLinear
(MarkovMorphism.split m hm).tangentPushforwardLinear = G.g p
theorem
LeanPool.CencovPetz.MonotoneMetricFamily.eq_of_split
{α : Type u}
[Fintype α]
(G : MonotoneMetricFamily)
(m : α → ℕ)
(hm : ∀ (a : α), 0 < m a)
(p : Simplex α)
(u v : ↥(tangentSpace α))
:
((G.g ((MarkovMorphism.split m hm).pushforward p)) ((MarkovMorphism.split m hm).tangentPushforward u))
((MarkovMorphism.split m hm).tangentPushforward v) = ((G.g p) u) v