CencovPetz.Splitting

Fiberwise splitting (dependent replication) Markov morphisms in the finite/discrete setting.

Given a finite type α and a multiplicity function m : α → ℕ with 0 < m a for all a, we define:

• a split Markov morphism α → Σ a, Fin (m a) sending a to the uniform distribution on its fiber, and
• a merge (coarsening) Markov morphism Σ a, Fin (m a) → α forgetting the fiber index.

These are left inverses on simplex points and tangent vectors, and are standard tools in finite Čencov/Chentsov uniqueness proofs.

@[reducible, inline]

abbrev LeanPool.CencovPetz.MarkovMorphism.SplitTarget {α : Type u} (m : α → ℕ) : Type u

The target type for a fiberwise split: Σ a, Fin (m a).

Equations

• LeanPool.CencovPetz.MarkovMorphism.SplitTarget m = ((a : α) × Fin (m a))

noncomputable def LeanPool.CencovPetz.MarkovMorphism.split {α : Type u} [Fintype α] (m : α → ℕ) (hm : ∀ (a : α), 0 < m a) : MarkovMorphism α (SplitTarget m)

Fiberwise split: send a to the uniform distribution on the fiber Fin (m a).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.CencovPetz.MarkovMorphism.merge {α : Type u} [Fintype α] (m : α → ℕ) (hm : ∀ (a : α), 0 < m a) : MarkovMorphism (SplitTarget m) α

Fiberwise merge: forget the fiber index.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.CencovPetz.MarkovMorphism.split_pushforward_apply {α : Type u} [Fintype α] (m : α → ℕ) (hm : ∀ (a : α), 0 < m a) (p : Simplex α) (a : α) (i : Fin (m a)) : ((split m hm).pushforward p).p ⟨a, i⟩ = p.p a / ↑(m a)

theorem LeanPool.CencovPetz.MarkovMorphism.split_tangentPushforward_apply {α : Type u} [Fintype α] (m : α → ℕ) (hm : ∀ (a : α), 0 < m a) (u : ↥(tangentSpace α)) (a : α) (i : Fin (m a)) : ↑((split m hm).tangentPushforward u) ⟨a, i⟩ = ↑u a / ↑(m a)

theorem LeanPool.CencovPetz.MarkovMorphism.merge_pushforward_split {α : Type u} [Fintype α] (m : α → ℕ) (hm : ∀ (a : α), 0 < m a) (p : Simplex α) : (merge m hm).pushforward ((split m hm).pushforward p) = p

theorem LeanPool.CencovPetz.MarkovMorphism.merge_tangentPushforward_split {α : Type u} [Fintype α] (m : α → ℕ) (hm : ∀ (a : α), 0 < m a) (u : ↥(tangentSpace α)) : (merge m hm).tangentPushforward ((split m hm).tangentPushforward u) = u