CencovPetz.Replication

Replication Markov morphisms α → α × Fin m that split each outcome into m copies uniformly.

noncomputable def LeanPool.CencovPetz.MarkovMorphism.replicate {α : Type u} [Fintype α] (m : ℕ) (hm : 0 < m) : MarkovMorphism α (α × Fin m)

Replication Markov morphism α → α × Fin m: each input a is sent uniformly to the m outputs (a,i).

This is a standard “splitting” map used in finite Čencov uniqueness proofs.

Equations

• LeanPool.CencovPetz.MarkovMorphism.replicate m hm = { K := fun (a : α) (b : α × Fin m) => if a = b.1 then 1 / ↑m else 0, nonneg := ⋯, row_sum_eq_one := ⋯, col_pos := ⋯ }

theorem LeanPool.CencovPetz.MarkovMorphism.replicate_pushforward_apply {α : Type u} [Fintype α] (m : ℕ) (hm : 0 < m) (p : Simplex α) (a : α) (i : Fin m) : ((replicate m hm).pushforward p).p (a, i) = p.p a / ↑m

theorem LeanPool.CencovPetz.MarkovMorphism.replicate_pushforward_uniform {α : Type u} [Fintype α] [Nonempty α] (m : ℕ) (hm : 0 < m) : (replicate m hm).pushforward Simplex.uniform = Simplex.uniform

theorem LeanPool.CencovPetz.MarkovMorphism.replicate_tangentPushforward_apply {α : Type u} [Fintype α] (m : ℕ) (hm : 0 < m) (u : ↥(tangentSpace α)) (a : α) (i : Fin m) : ↑((replicate m hm).tangentPushforward u) (a, i) = ↑u a / ↑m

noncomputable def LeanPool.CencovPetz.MarkovMorphism.coarsen {α : Type u} [Fintype α] (m : ℕ) (hm : 0 < m) : MarkovMorphism (α × Fin m) α

Coarsening map α × Fin m → α that forgets the replica index.

Equations

• LeanPool.CencovPetz.MarkovMorphism.coarsen m hm = LeanPool.CencovPetz.MarkovMorphism.deterministic Prod.fst ⋯

theorem LeanPool.CencovPetz.MarkovMorphism.coarsen_pushforward_replicate {α : Type u} [Fintype α] (m : ℕ) (hm : 0 < m) (p : Simplex α) : (coarsen m hm).pushforward ((replicate m hm).pushforward p) = p

theorem LeanPool.CencovPetz.MarkovMorphism.coarsen_tangentPushforward_replicate {α : Type u} [Fintype α] (m : ℕ) (hm : 0 < m) (u : ↥(tangentSpace α)) : (coarsen m hm).tangentPushforward ((replicate m hm).tangentPushforward u) = u