The Born map is an isometry from the torus-horizontal directions to Fisher–Rao

Category: 1-Mathlib (CSD-free; finite-dimensional inner-product algebra on EuclideanSpace ℂ ι and the open simplex of FisherRao.lean).

A unit vector ψ : ℂ^ι has Born weights pᵢ = ‖ψᵢ‖², a point of the open probability simplex when no coordinate vanishes. Moving ψ in a direction u moves the weights by dpᵢ = 2 Re(ψ̄ᵢ uᵢ), and the Fisher–Rao inner product of two such displacements is

`Σᵢ dpᵢ dp'ᵢ / pᵢ`.

Write u as uᵢ = aᵢ ψᵢ coordinate by coordinate. When every aᵢ is real (the direction is torus-horizontal: it changes moduli, not phases), dpᵢ = 2 aᵢ pᵢ and the sum collapses to 4 Σᵢ ūᵢ vᵢ = 4 ⟪u, v⟫. That is an identity between vectors, and it reads as a statement about the state space once u is also tangent to the unit sphere at ψ (⟪ψ, u⟫ = 0): then 4 Re ⟪u, v⟫ is the Fubini–Study inner product of the two directions, in the normalisation where the state space of a qubit is the unit round sphere and the Fubini–Study metric is the quantum Fisher information of a pure-state family (the Bengtsson–Życzkowski normalisation is a quarter of it). The radial direction u = ψ is torus-horizontal but not tangent, and moves no state; the projective form of everything here (BraunsteinCaves.lean, horizontalLift) projects that component off before anything is said.

Along a general direction the phases also move and Fisher–Rao only sees the moduli; the resulting inequality, Braunstein–Caves for the computational-basis measurement, is BraunsteinCaves.lean.

Main declarations

• FisherRao.bornWeight ψ i = ‖ψ i‖ ^ 2, FisherRao.bornSimplex — the Born weights as a point of OpenSimplex ι for a unit vector with no vanishing coordinate.
• FisherRao.bornDeriv ψ u i = 2 Re(ψ̄ᵢ uᵢ) and hasFDerivAt_bornWeight — it is the differential of ψ ↦ ‖ψ i‖ ^ 2; sum_bornDeriv — the displacement sums to 2 Re ⟪ψ, u⟫, so it is tangent to the simplex whenever u is tangent to the unit sphere.
• FisherRao.IsTorusHorizontal ψ u — every ψ̄ᵢ uᵢ is real (orthogonal to the torus orbit; not the same as the projective horizontal lift of BraunsteinCaves.lean, which also projects off ψ).
• ★ fisherRaoInner_bornDeriv — for torus-horizontal u and any v, fisherRaoInner (bornSimplex ψ) (bornDeriv ψ u) (bornDeriv ψ v) = 4 * Re ⟪u, v⟫; fisherRaoSq_bornDeriv — the quadratic form of a torus-horizontal displacement is 4 ‖u‖².

The constant

The right-hand side 4 * Re ⟪u, v⟫ is the Fubini–Study metric of the projective space in the normalisation of Projectivization.fsMetric (Geometry/Manifold/Instances/ProjectiveSpaceFubiniStudyRiemannian.lean, where the Gram matrix at a chart origin is 4 • 1), evaluated on horizontal lifts. In that normalisation the Fubini–Study metric of a pure-state family is its quantum Fisher information, 4 (‖u‖² − ‖⟪ψ, u⟫‖²) for unit ψ (BraunsteinCaves.lean, fsInnerHom_self_of_norm_eq_one). In the normalisation ‖u‖² − ‖⟪ψ, u⟫‖² of Bengtsson–Życzkowski, which Empirical/Metrology/QuantumFisher.lean's vector-level fsMetric uses, the bridge constant is 4 and the quantum Fisher information is 4 g_FS. No constant is assumed here; the 4 is the derivative of ‖·‖².

References

• S. L. Braunstein, C. M. Caves, Statistical distance and the geometry of quantum states, Phys. Rev. Lett. 72, 3439 (1994).
• I. Bengtsson, K. Życzkowski, Geometry of Quantum States, 2nd ed., §§4.4, 14.2.
• Physlib PR #1652 (FisherRao.lean, mirrored in this directory).

Provenance

Built 2026-09-16 for Physlib PR #1652; split 2026-09-18 (the homogeneous coordinates and the Braunstein–Caves inequality moved to BraunsteinCaves.lean, so that each file is one Physlib-sized pull request); recorded in this repository's completed-work ledger (specs/future-work.md, KG-4) and claims ledger (CL-076).

The Born weights of a vector, coordinate by coordinate

noncomputable def FisherRao.bornWeight {ι : Type u_1} (ψ : EuclideanSpace ℂ ι) (i : ι) : ℝ

The Born weight of the i-th coordinate: ‖ψ i‖ ^ 2.

Equations

• FisherRao.bornWeight ψ i = ‖ψ.ofLp i‖ ^ 2

theorem FisherRao.bornWeight_def {ι : Type u_1} (ψ : EuclideanSpace ℂ ι) (i : ι) : bornWeight ψ i = ‖ψ.ofLp i‖ ^ 2

bornWeight, unfolded: the definitional equation.

theorem FisherRao.bornWeight_nonneg {ι : Type u_1} (ψ : EuclideanSpace ℂ ι) (i : ι) : 0 ≤ bornWeight ψ i

theorem FisherRao.bornWeight_pos {ι : Type u_1} (ψ : EuclideanSpace ℂ ι) {i : ι} (h : ψ.ofLp i ≠ 0) : 0 < bornWeight ψ i

The differential of the Born map

def FisherRao.bornDeriv {ι : Type u_1} (ψ u : EuclideanSpace ℂ ι) (i : ι) : ℝ

The displacement of the i-th Born weight along u: 2 Re(ψ̄ᵢ uᵢ).

Equations

• FisherRao.bornDeriv ψ u i = 2 * ((starRingEnd ((fun (x : ι) => ℂ) i)) (ψ.ofLp i) * u.ofLp i).re

theorem FisherRao.bornDeriv_def {ι : Type u_1} (ψ u : EuclideanSpace ℂ ι) (i : ι) : bornDeriv ψ u i = 2 * ((starRingEnd ((fun (x : ι) => ℂ) i)) (ψ.ofLp i) * u.ofLp i).re

bornDeriv, unfolded: the definitional equation.

Horizontal directions

def FisherRao.IsTorusHorizontal {ι : Type u_1} (ψ u : EuclideanSpace ℂ ι) : Prop

A direction u at ψ is torus-horizontal when every ψ̄ᵢ uᵢ is real: it changes the moduli of the coordinates and none of their phases, so it is orthogonal to the orbit of the coordinate-phase torus. It need not be tangent to the unit sphere (the radial direction ψ qualifies); the projective horizontal lift (horizontalLift, BraunsteinCaves.lean) removes the radial component.

Equations

• FisherRao.IsTorusHorizontal ψ u = ∀ (i : ι), ((starRingEnd ((fun (x : ι) => ℂ) i)) (ψ.ofLp i) * u.ofLp i).im = 0

theorem FisherRao.isTorusHorizontal_of_forall_eq {ι : Type u_1} (ψ u : EuclideanSpace ℂ ι) (a : ι → ℝ) (hu : ∀ (i : ι), u.ofLp i = ↑(a i) * ψ.ofLp i) : IsTorusHorizontal ψ u

A direction whose coordinates are real multiples of those of ψ is horizontal.

theorem FisherRao.bornDeriv_mul_div_bornWeight {ι : Type u_1} (ψ u v : EuclideanSpace ℂ ι) {i : ι} (h0 : ψ.ofLp i ≠ 0) (hu : ((starRingEnd ((fun (x : ι) => ℂ) i)) (ψ.ofLp i) * u.ofLp i).im = 0) : bornDeriv ψ u i * bornDeriv ψ v i / bornWeight ψ i = 4 * (inner ℂ (u.ofLp i) (v.ofLp i)).re

The pointwise identity behind the bridge: for ψᵢ ≠ 0 and ψ̄ᵢ uᵢ real, (2 Re(ψ̄ᵢ uᵢ)) (2 Re(ψ̄ᵢ vᵢ)) / ‖ψᵢ‖² = 4 Re(ūᵢ vᵢ).

Sums over the coordinates

theorem FisherRao.sum_bornWeight {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) : ∑ i : ι, bornWeight ψ i = ‖ψ‖ ^ 2

The Born weights sum to ‖ψ‖ ^ 2.

noncomputable def FisherRao.bornSimplex {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) (h0 : ∀ (i : ι), ψ.ofLp i ≠ 0) : OpenSimplex ι

The Born weights of a unit vector with no vanishing coordinate, as a point of the open probability simplex.

Equations

• FisherRao.bornSimplex ψ hψ h0 = { val := FisherRao.bornWeight ψ, pos := ⋯, sum_one := ⋯ }

@[simp]

theorem FisherRao.bornSimplex_val {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) (h0 : ∀ (i : ι), ψ.ofLp i ≠ 0) : (bornSimplex ψ hψ h0).val = bornWeight ψ

noncomputable def FisherRao.bornDerivCLM {ι : Type u_1} (ψ : EuclideanSpace ℂ ι) (i : ι) : EuclideanSpace ℂ ι →L[ℝ] ℝ

bornDeriv ψ · i as a real continuous linear map: 2 ⟪ψ i, · i⟫_ℝ.

Equations

• FisherRao.bornDerivCLM ψ i = 2 • (innerSL ℝ) (ψ.ofLp i) ∘SL ContinuousLinearMap.restrictScalars ℝ (EuclideanSpace.proj i)

theorem FisherRao.bornDerivCLM_apply {ι : Type u_1} (ψ u : EuclideanSpace ℂ ι) (i : ι) : (bornDerivCLM ψ i) u = bornDeriv ψ u i

theorem FisherRao.hasFDerivAt_bornWeight {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) (i : ι) : HasFDerivAt (fun (φ : EuclideanSpace ℂ ι) => bornWeight φ i) (bornDerivCLM ψ i) ψ

bornDeriv is the differential of the Born map: ψ ↦ ‖ψ i‖ ^ 2 has derivative bornDerivCLM ψ i at ψ.

theorem FisherRao.sum_bornDeriv {ι : Type u_1} [Fintype ι] (ψ u : EuclideanSpace ℂ ι) : ∑ i : ι, bornDeriv ψ u i = 2 * (inner ℂ ψ u).re

The displacement of the weights sums to 2 Re ⟪ψ, u⟫; in particular it sums to zero — it is tangent to the simplex — whenever u is tangent to the unit sphere at ψ.

theorem FisherRao.fisherRaoInner_bornDeriv {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) (h0 : ∀ (i : ι), ψ.ofLp i ≠ 0) {u : EuclideanSpace ℂ ι} (hu : IsTorusHorizontal ψ u) (v : EuclideanSpace ℂ ι) : (bornSimplex ψ hψ h0).fisherRaoInner (bornDeriv ψ u) (bornDeriv ψ v) = 4 * (inner ℂ u v).re

★ The bridge, at the vector level. For a torus-horizontal direction u and any direction v, the Fisher–Rao inner product of the Born displacements is four times the real inner product of the directions:

`g_FR(dΦ u, dΦ v) = 4 Re ⟪u, v⟫`.

Only u needs to be torus-horizontal; v is arbitrary. The 4 is the derivative of ‖·‖². When u and v are also tangent to the unit sphere at ψ, 4 Re ⟪u, v⟫ is the Fubini–Study inner product in the round-sphere normalisation; the projective statement that builds the tangency in is fisherRaoInner_bornDeriv_normalize (BraunsteinCaves.lean).

theorem FisherRao.fisherRaoSq_bornDeriv {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) (h0 : ∀ (i : ι), ψ.ofLp i ≠ 0) {u : EuclideanSpace ℂ ι} (hu : IsTorusHorizontal ψ u) : (bornSimplex ψ hψ h0).fisherRaoSq (bornDeriv ψ u) = 4 * ‖u‖ ^ 2

The Fisher–Rao quadratic form of a torus-horizontal Born displacement is 4 ‖u‖ ^ 2.