CencovPetz.MarkovMorphism

Finite/discrete Markov morphisms (row-stochastic matrices) and monotonicity of the Fisher quadratic form.

This is the “general Markov morphism” version of the deterministic sufficient-statistic result in CencovPetz.SufficientStatistic. It provides the main finite-data-processing inequality needed for the Čencov/Chentsov uniqueness story.

Main definitions

• CencovPetz.MarkovMorphism α β: a row-stochastic matrix K : α → β → ℝ together with a mild positivity condition ensuring it maps the open simplex to the open simplex.
• CencovPetz.MarkovMorphism.pushforward: pushforward of a Simplex α along K.
• CencovPetz.MarkovMorphism.tangentPushforward: pushforward of tangent vectors.

Main result

• CencovPetz.fisherBilin_pushforward_le_of_markovMorphism: Fisher monotonicity under a Markov morphism.

structure LeanPool.CencovPetz.MarkovMorphism (α : Type u_3) (β : Type u_4) [Fintype α] [Fintype β] : Type (max u_3 u_4)

A finite Markov morphism α → β, presented as a row-stochastic matrix.

We additionally assume every output coordinate is reachable with positive probability from some input (col_pos). This ensures the pushforward of a strictly positive distribution is again strictly positive, so we stay on the open simplex where the Fisher metric is nondegenerate.

• K : α → β → ℝ

  Transition weights K a b.

• nonneg (a : α) (b : β) : 0 ≤ self.K a b

  Nonnegativity.

• row_sum_eq_one (a : α) : ∑ b : β, self.K a b = 1

  Each row sums to 1.

• col_pos (b : β) : ∃ (a : α), 0 < self.K a b

  Each column has a strictly positive entry (so the open simplex maps to the open simplex).

noncomputable def LeanPool.CencovPetz.MarkovMorphism.deterministic {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (g : α → β) (hg : Function.Surjective g) : MarkovMorphism α β

The deterministic Markov morphism induced by a surjective map g : α → β: K a b = 1 if g a = b, else 0.

Equations

• LeanPool.CencovPetz.MarkovMorphism.deterministic g hg = { K := fun (a : α) (b : β) => if g a = b then 1 else 0, nonneg := ⋯, row_sum_eq_one := ⋯, col_pos := ⋯ }

noncomputable def LeanPool.CencovPetz.MarkovMorphism.pushforward {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (κ : MarkovMorphism α β) (p : Simplex α) : Simplex β

Pushforward of a distribution p along a Markov morphism κ.

Equations

• κ.pushforward p = { p := fun (b : β) => ∑ a : α, p.p a * κ.K a b, pos := ⋯, sum_eq_one := ⋯ }

noncomputable def LeanPool.CencovPetz.MarkovMorphism.tangentPushforward {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (κ : MarkovMorphism α β) (u : ↥(tangentSpace α)) : ↥(tangentSpace β)

Pushforward of a tangent vector along a Markov morphism.

Equations

• κ.tangentPushforward u = ⟨fun (b : β) => ∑ a : α, ↑u a * κ.K a b, ⋯⟩

@[simp]

theorem LeanPool.CencovPetz.MarkovMorphism.pushforward_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (κ : MarkovMorphism α β) (p : Simplex α) (b : β) : (κ.pushforward p).p b = ∑ a : α, p.p a * κ.K a b

@[simp]

theorem LeanPool.CencovPetz.MarkovMorphism.tangentPushforward_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (κ : MarkovMorphism α β) (u : ↥(tangentSpace α)) (b : β) : ↑(κ.tangentPushforward u) b = ∑ a : α, ↑u a * κ.K a b

noncomputable def LeanPool.CencovPetz.MarkovMorphism.tangentPushforwardLinear {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (κ : MarkovMorphism α β) : ↥(tangentSpace α) →ₗ[ℝ] ↥(tangentSpace β)

tangentPushforward packaged as a linear map.

Equations

• κ.tangentPushforwardLinear = { toFun := κ.tangentPushforward, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LeanPool.CencovPetz.MarkovMorphism.tangentPushforwardLinear_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (κ : MarkovMorphism α β) (u : ↥(tangentSpace α)) : κ.tangentPushforwardLinear u = κ.tangentPushforward u

theorem LeanPool.CencovPetz.MarkovMorphism.deterministic_pushforward_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (g : α → β) (hg : Function.Surjective g) (p : Simplex α) (b : β) : ((deterministic g hg).pushforward p).p b = ∑ a : α with g a = b, p.p a

Pushforward along a deterministic morphism is fiberwise summation.

theorem LeanPool.CencovPetz.MarkovMorphism.deterministic_tangentPushforward_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (g : α → β) (hg : Function.Surjective g) (u : ↥(tangentSpace α)) (b : β) : ↑((deterministic g hg).tangentPushforward u) b = ∑ a : α with g a = b, ↑u a

Tangent pushforward along a deterministic morphism is fiberwise summation.

theorem LeanPool.CencovPetz.fisherBilin_pushforward_le_of_markovMorphism {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (κ : MarkovMorphism α β) (p : Simplex α) (u : ↥(tangentSpace α)) : ((fisherBilin (κ.pushforward p)) (κ.tangentPushforward u)) (κ.tangentPushforward u) ≤ ((fisherBilin p) u) u

Fisher monotonicity under a finite Markov morphism.