CencovPetz.MonotoneMetric

An interface for monotone Riemannian metrics on the finite open probability simplex (Čencov/Chentsov setting), together with basic consequences.

We model a metric as a family of bilinear forms on the canonical tangent space tangentSpace α = {u : α → ℝ | ∑ u = 0}. A monotone metric family is one that is contractive under Markov morphisms (CencovPetz.MarkovMorphism).

This file does not prove the full Čencov uniqueness theorem; it sets up the infrastructure needed for that proof.

Main definitions

• CencovPetz.MonotoneMetricFamily: assigns a pointwise metric to each finite type, and is monotone under Markov morphisms.
• CencovPetz.fisherMetricFamily: the Fisher metric family, as a monotone metric family.

Main results

structure LeanPool.CencovPetz.MonotoneMetricFamily : Type (u + 1)

A finite monotone metric family on open simplices.

g p is a bilinear form on the canonical tangent space at p, and monotone asserts the data-processing inequality under Markov morphisms.

• g {α : Type u} [Fintype α] : Simplex α → LinearMap.BilinForm ℝ ↥(tangentSpace α)

  The bilinear form at p : Simplex α.

• symm {α : Type u} [Fintype α] (p : Simplex α) (u v : ↥(tangentSpace α)) : ((self.g p) u) v = ((self.g p) v) u

  Symmetry of the bilinear form.

• pos {α : Type u} [Fintype α] (p : Simplex α) (u : ↥(tangentSpace α)) : u ≠ 0 → 0 < ((self.g p) u) u

  Positive definiteness on tangent vectors.

• monotone {α β : Type u} [Fintype α] [Fintype β] (κ : MarkovMorphism α β) (p : Simplex α) (u : ↥(tangentSpace α)) : ((self.g (κ.pushforward p)) (κ.tangentPushforward u)) (κ.tangentPushforward u) ≤ ((self.g p) u) u

  Monotonicity under Markov morphisms.

noncomputable def LeanPool.CencovPetz.fisherMetricFamily : MonotoneMetricFamily

The Fisher metric family is a monotone metric family.

Equations

• LeanPool.CencovPetz.fisherMetricFamily = { g := fun {α : Type ?u.1} (x : Fintype α) => LeanPool.CencovPetz.fisherBilin, symm := ⋯, pos := ⋯, monotone := ⋯ }