CencovPetz.Simplex

The strictly positive probability simplex on a finite type, together with its canonical tangent submodule (sum-zero functions) and the classical Fisher information bilinear form.

This is groundwork for the finite/discrete Čencov (Chentsov) uniqueness story.

Main definitions

• CencovPetz.Simplex α: strictly positive distributions p : α → ℝ with ∑ p = 1.
• CencovPetz.tangentSpace α: the submodule {u : α → ℝ | ∑ u = 0}.
• CencovPetz.fisherBilin p: the Fisher bilinear form on tangentSpace α, ∑ uᵢ vᵢ / pᵢ.

Main results

• CencovPetz.fisherBilin_comm: symmetry of the Fisher bilinear form.
• CencovPetz.fisherBilin_pos: positive-definiteness on nonzero tangent vectors.

structure LeanPool.CencovPetz.Simplex (α : Type u_2) [Fintype α] : Type u_2

The strictly positive probability simplex on a finite type α.

• p : α → ℝ

  Coordinate representation p : α → ℝ.

• pos (a : α) : 0 < self.p a

  Strict positivity of each coordinate.

• sum_eq_one : ∑ a : α, self.p a = 1

  Normalization.

theorem LeanPool.CencovPetz.Simplex.ext {α : Type u_1} [Fintype α] {p q : Simplex α} (h : p.p = q.p) : p = q

theorem LeanPool.CencovPetz.Simplex.ext_iff {α : Type u_1} [Fintype α] {p q : Simplex α} : p = q ↔ p.p = q.p

theorem LeanPool.CencovPetz.Simplex.p_ne_zero {α : Type u_1} [Fintype α] (p : Simplex α) (a : α) : p.p a ≠ 0

noncomputable def LeanPool.CencovPetz.sumLinearMap (α : Type u_2) [Fintype α] : (α → ℝ) →ₗ[ℝ] ℝ

The linear functional u ↦ ∑ a, u a on α → ℝ.

Equations

• LeanPool.CencovPetz.sumLinearMap α = { toFun := fun (u : α → ℝ) => ∑ a : α, u a, map_add' := ⋯, map_smul' := ⋯ }

@[reducible, inline]

noncomputable abbrev LeanPool.CencovPetz.tangentSpace (α : Type u_2) [Fintype α] : Submodule ℝ (α → ℝ)

Tangent space to the simplex, modeled as the sum-zero submodule of α → ℝ.

Equations

• LeanPool.CencovPetz.tangentSpace α = (LeanPool.CencovPetz.sumLinearMap α).ker

theorem LeanPool.CencovPetz.tangentSpace.mem_iff (α : Type u_1) [Fintype α] {u : α → ℝ} : u ∈ tangentSpace α ↔ ∑ a : α, u a = 0

noncomputable def LeanPool.CencovPetz.fisherBilin {α : Type u_1} [Fintype α] (p : Simplex α) : LinearMap.BilinForm ℝ ↥(tangentSpace α)

The Fisher bilinear form on the simplex tangent space: ⟪u,v⟫_p = ∑ a, u a * v a / p a.

Equations

• LeanPool.CencovPetz.fisherBilin p = LinearMap.mk₂ ℝ (fun (u v : ↥(LeanPool.CencovPetz.tangentSpace α)) => ∑ a : α, ↑u a * ↑v a / p.p a) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem LeanPool.CencovPetz.fisherBilin.apply {α : Type u_1} [Fintype α] (p : Simplex α) (u v : ↥(tangentSpace α)) : ((fisherBilin p) u) v = ∑ a : α, ↑u a * ↑v a / p.p a

theorem LeanPool.CencovPetz.fisherBilin.comm {α : Type u_1} [Fintype α] (p : Simplex α) (u v : ↥(tangentSpace α)) : ((fisherBilin p) u) v = ((fisherBilin p) v) u

theorem LeanPool.CencovPetz.fisherBilin.pos {α : Type u_1} [Fintype α] (p : Simplex α) (u : ↥(tangentSpace α)) (hu : u ≠ 0) : 0 < ((fisherBilin p) u) u