CencovPetz.SufficientStatistic

Deterministic “sufficient statistics” in the finite/discrete setting, and monotonicity of the Fisher quadratic form under such maps.

In classical information geometry (Čencov/Chentsov), a key input is that the Fisher metric is monotone under sufficient statistics. For a finite type α of outcomes and a surjection g : α → β, the pushforward distribution is obtained by summing over fibers:

q(b) = ∑_{a : g a = b} p(a).

The corresponding tangent vector pushforward is the same fiberwise sum, and the Fisher inequality reduces to Titu's lemma / Engel form of Cauchy–Schwarz on each fiber.

Main definitions

• CencovPetz.Simplex.pushforward: pushforward of a strictly positive distribution along a surjective map, by summing over fibers.
• CencovPetz.tangentPushforward: pushforward of a tangent vector along a map, by summing over fibers.

Main results

• CencovPetz.fisherBilin_pushforward_le: Fisher quadratic form monotonicity under a surjective map (finite sufficient statistic).

noncomputable def LeanPool.CencovPetz.Simplex.pushforward {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (g : α → β) (hg : Function.Surjective g) (p : Simplex α) : Simplex β

Pushforward of a strictly positive distribution along a surjective map, by summing over fibers.

Equations

• LeanPool.CencovPetz.Simplex.pushforward g hg p = { p := fun (b : β) => ∑ a : α with g a = b, p.p a, pos := ⋯, sum_eq_one := ⋯ }

@[simp]

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

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

Pushforward of a tangent vector along a map, by summing over fibers.

Equations

• LeanPool.CencovPetz.tangentPushforward g u = ⟨fun (b : β) => ∑ a : α with g a = b, ↑u a, ⋯⟩

@[simp]

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

theorem LeanPool.CencovPetz.fisherBilin_pushforward_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (g : α → β) (hg : Function.Surjective g) (p : Simplex α) (u : ↥(tangentSpace α)) : ((fisherBilin (Simplex.pushforward g hg p)) (tangentPushforward g u)) (tangentPushforward g u) ≤ ((fisherBilin p) u) u

Monotonicity of the Fisher quadratic form under a surjective map (finite sufficient statistic).