CencovPetz.PermutationInvariance

Bridge deterministic sufficient statistics and deterministic Markov morphisms, and derive permutation/equivalence invariance consequences for monotone metric families in the finite Čencov/Chentsov setting.

Main results

• CencovPetz.MarkovMorphism.deterministic_pushforward_eq_simplex_pushforward: deterministic Markov pushforward agrees with the fiberwise-sum pushforward from SufficientStatistic.
• CencovPetz.MonotoneMetricFamily.comp_eq_of_equiv: any monotone metric family is invariant under equivalences (permutations) of finite types.

theorem LeanPool.CencovPetz.MarkovMorphism.deterministic_pushforward_eq_simplex_pushforward {α β : Type u} [Fintype α] [Fintype β] [DecidableEq β] (g : α → β) (hg : Function.Surjective g) (p : Simplex α) : (deterministic g hg).pushforward p = Simplex.pushforward g hg p

theorem LeanPool.CencovPetz.MarkovMorphism.deterministic_tangentPushforward_eq_tangentPushforward {α β : Type u} [Fintype α] [Fintype β] [DecidableEq β] (g : α → β) (hg : Function.Surjective g) (u : ↥(tangentSpace α)) : (deterministic g hg).tangentPushforward u = CencovPetz.tangentPushforward g u

theorem LeanPool.CencovPetz.MarkovMorphism.deterministic_pushforward_apply_of_equiv {α β : Type u} [Fintype α] [Fintype β] (e : α ≃ β) (p : Simplex α) (b : β) : ((deterministic ⇑e ⋯).pushforward p).p b = p.p (e.symm b)

theorem LeanPool.CencovPetz.MarkovMorphism.deterministic_tangentPushforward_apply_of_equiv {α β : Type u} [Fintype α] [Fintype β] (e : α ≃ β) (u : ↥(tangentSpace α)) (b : β) : ↑((deterministic ⇑e ⋯).tangentPushforward u) b = ↑u (e.symm b)

theorem LeanPool.CencovPetz.MarkovMorphism.deterministic_pushforward_comp_symm {α β : Type u} [Fintype α] [Fintype β] (e : α ≃ β) (p : Simplex α) : (deterministic ⇑e.symm ⋯).pushforward ((deterministic ⇑e ⋯).pushforward p) = p

theorem LeanPool.CencovPetz.MarkovMorphism.deterministic_tangentPushforward_comp_symm {α β : Type u} [Fintype α] [Fintype β] (e : α ≃ β) (u : ↥(tangentSpace α)) : (deterministic ⇑e.symm ⋯).tangentPushforward ((deterministic ⇑e ⋯).tangentPushforward u) = u

theorem LeanPool.CencovPetz.MonotoneMetricFamily.comp_eq_of_equiv {α β : Type u} [Fintype α] [Fintype β] (G : MonotoneMetricFamily) (e : α ≃ β) (p : Simplex α) : (G.g ((MarkovMorphism.deterministic ⇑e ⋯).pushforward p)).comp (MarkovMorphism.deterministic ⇑e ⋯).tangentPushforwardLinear (MarkovMorphism.deterministic ⇑e ⋯).tangentPushforwardLinear = G.g p

theorem LeanPool.CencovPetz.MonotoneMetricFamily.eq_of_equiv {α β : Type u} [Fintype α] [Fintype β] (G : MonotoneMetricFamily) (e : α ≃ β) (p : Simplex α) (u v : ↥(tangentSpace α)) : ((G.g ((MarkovMorphism.deterministic ⇑e ⋯).pushforward p)) ((MarkovMorphism.deterministic ⇑e ⋯).tangentPushforward u)) ((MarkovMorphism.deterministic ⇑e ⋯).tangentPushforward v) = ((G.g p) u) v