Fisher–Rao metric on the open simplex (mirror of Physlib PR #1652)

Category: 1-Mathlib (CSD-free; a verbatim mirror of a Physlib file, to be deleted when the PR merges).

Provenance. This file mirrors the metric half of QuantumInfo/ForMathlib/FisherRao.lean from Physlib pull request #1652 (leanprover-community/physlib, branch naype888-cloud:nava-fisher-rao-cramer-rao, commit 5e6f0837630b, 2026-09-15), by Eduardo Nava-Hernandez. The declarations are copied unchanged, under the same namespace FisherRao, so that a theorem stated against them here is the same theorem in Physlib with one import line changed. The only edits are the module-system header (module, public import, @[expose] public section) and docstrings on the three fields of OpenSimplex, both of which this repository's lints require. The Cramér–Rao half of the source file (expect, variance, cramerRao) is not needed by the bridge and is not mirrored. The bridge this file serves is recorded in this repository's completed-work ledger (specs/future-work.md, KG-4).

Delete this file and import Physlib when the PR merges. Until then csd-lean4 does not depend on Physlib, and must not depend on an unmerged branch.

Main definitions

• FisherRao.OpenSimplex — a point on the open probability simplex
• FisherRao.OpenSimplex.fisherRaoInner — the Fisher–Rao inner product gₚ(u,v) = Σᵢ uᵢvᵢ/pᵢ
• FisherRao.fisherInfo — classical Fisher information I(θ) for a parametric family

References

• C. R. Rao, Information and the accuracy attainable in the estimation of statistical parameters, Bull. Calcutta Math. Soc. 37, 81–91 (1945)
• H. Cramér, Mathematical Methods of Statistics, Princeton (1946)

Open probability simplex

structure FisherRao.OpenSimplex (α : Type u_2) [Fintype α] : Type u_2

A point on the open probability simplex: strictly positive weights summing to 1.

• val : α → ℝ

  The weights.

• pos (i : α) : 0 < self.val i

  Every weight is strictly positive.

• sum_one : ∑ i : α, self.val i = 1

  The weights sum to one.

theorem FisherRao.OpenSimplex.val_ne_zero {α : Type u_1} [Fintype α] (p : OpenSimplex α) (i : α) : p.val i ≠ 0

theorem FisherRao.OpenSimplex.val_nonneg {α : Type u_1} [Fintype α] (p : OpenSimplex α) (i : α) : 0 ≤ p.val i

Fisher–Rao inner product

noncomputable def FisherRao.OpenSimplex.fisherRaoInner {α : Type u_1} [Fintype α] (p : OpenSimplex α) (u v : α → ℝ) : ℝ

The Fisher–Rao inner product at p ∈ Δ°(α): gₚ(u, v) = Σᵢ uᵢ vᵢ / pᵢ.

Equations

• p.fisherRaoInner u v = ∑ i : α, u i * v i / p.val i

noncomputable def FisherRao.OpenSimplex.fisherRaoSq {α : Type u_1} [Fintype α] (p : OpenSimplex α) (u : α → ℝ) : ℝ

The Fisher–Rao quadratic form.

Equations

• p.fisherRaoSq u = p.fisherRaoInner u u

theorem FisherRao.OpenSimplex.fisherRaoSq_nonneg {α : Type u_1} [Fintype α] (p : OpenSimplex α) (u : α → ℝ) : 0 ≤ p.fisherRaoSq u

theorem FisherRao.OpenSimplex.fisherRaoSq_eq_zero_iff {α : Type u_1} [Fintype α] (p : OpenSimplex α) (u : α → ℝ) : p.fisherRaoSq u = 0 ↔ u = 0

theorem FisherRao.OpenSimplex.fisherRaoInner_comm {α : Type u_1} [Fintype α] (p : OpenSimplex α) (u v : α → ℝ) : p.fisherRaoInner u v = p.fisherRaoInner v u

Cauchy–Schwarz for the Fisher–Rao inner product

theorem FisherRao.OpenSimplex.fisherRao_cauchy_schwarz {α : Type u_1} [Fintype α] (p : OpenSimplex α) (u v : α → ℝ) : p.fisherRaoInner u v ^ 2 ≤ p.fisherRaoSq u * p.fisherRaoSq v

Cauchy–Schwarz for the Fisher–Rao inner product: gₚ(u, v)² ≤ gₚ(u, u) · gₚ(v, v).

Classical Fisher information

noncomputable def FisherRao.fisherInfo {α : Type u_1} [Fintype α] (p dp : α → ℝ) : ℝ

Classical Fisher information for a 1-parameter discrete family θ ↦ p(·|θ), defined as I(θ) = Σᵢ (∂pᵢ/∂θ)² / pᵢ(θ).

Equations

• FisherRao.fisherInfo p dp = ∑ i : α, dp i ^ 2 / p i

theorem FisherRao.fisherInfo_nonneg {α : Type u_1} [Fintype α] (p dp : α → ℝ) (hpos : ∀ (i : α), 0 < p i) : 0 ≤ fisherInfo p dp

theorem FisherRao.fisherInfo_eq_fisherRaoSq {α : Type u_1} [Fintype α] (q : OpenSimplex α) (dp : α → ℝ) : fisherInfo q.val dp = q.fisherRaoSq dp

Fisher information equals the Fisher–Rao squared norm of the derivative vector.