CencovPetz.LeftInverseIsometry

For a monotone metric family (Čencov setting), any Markov morphism that admits a left inverse on:

• simplex points (pushforward), and
• tangent vectors (tangentPushforward)

is an isometry for the metric family.

This is the abstract lemma behind permutation invariance and replication invariance.

theorem LeanPool.CencovPetz.MonotoneMetricFamily.comp_eq_of_left_inverse (G : MonotoneMetricFamily) {α β : Type u} [Fintype α] [Fintype β] (κ : MarkovMorphism α β) (κ' : MarkovMorphism β α) (p : Simplex α) (hp : κ'.pushforward (κ.pushforward p) = p) (ht : ∀ (u : ↥(tangentSpace α)), κ'.tangentPushforward (κ.tangentPushforward u) = u) : (G.g (κ.pushforward p)).comp κ.tangentPushforwardLinear κ.tangentPushforwardLinear = G.g p

theorem LeanPool.CencovPetz.MonotoneMetricFamily.eq_of_left_inverse (G : MonotoneMetricFamily) {α β : Type u} [Fintype α] [Fintype β] (κ : MarkovMorphism α β) (κ' : MarkovMorphism β α) (p : Simplex α) (hp : κ'.pushforward (κ.pushforward p) = p) (ht : ∀ (u : ↥(tangentSpace α)), κ'.tangentPushforward (κ.tangentPushforward u) = u) (u v : ↥(tangentSpace α)) : ((G.g (κ.pushforward p)) (κ.tangentPushforward u)) (κ.tangentPushforward v) = ((G.g p) u) v