Braunstein–Caves for the coordinate readout, algebraically and projectively

Category: 1-Mathlib (CSD-free; FubiniStudyFisherRao.lean and the open simplex of FisherRao.lean).

Along a general direction the phases of the coordinates also move and Fisher–Rao only sees the moduli. The inequality Σᵢ dpᵢ²/pᵢ ≤ 4 ‖u‖² holds for every direction u with equality exactly on the torus-horizontal directions (FubiniStudyFisherRao.lean); read on the projective horizontal lift it is Braunstein–Caves for the computational-basis measurement: the classical Fisher information of the coordinate readout is at most the quantum Fisher information 4 (‖u‖² − ‖⟪ψ, u⟫‖²), with equality exactly when the projected direction is torus-horizontal.

The projective form needs homogeneous coordinates. A point of the state space is a ray [ψ] with ψ ≠ 0 and a direction at it is any vector u; the pairs (ψ, u) and (ψ, u + c ψ) describe the same tangent vector. The unit vector on the ray is normalize ψ = ‖ψ‖⁻¹ • ψ, the horizontal lift of u removes the component of u along ψ and rescales, and the Fubini–Study inner product of two directions is fsInnerHom ψ u v, which is 4 Re ⟪horizontalLift ψ u, horizontalLift ψ v⟫. This is the form the affine charts of ℂℙⁿ meet (Geometry/Manifold/Instances/ProjectiveSpaceFisherRao.lean).

Main declarations

• fisherInfo_bornDeriv_le — fisherInfo (bornWeight ψ) (bornDeriv ψ u) ≤ 4 * ‖u‖ ^ 2 for every u, and fisherInfo_bornDeriv_eq_iff — with equality iff u is torus-horizontal. These are the algebraic form; 4 ‖u‖² is the quantum Fisher information only for u tangent to the sphere.
• Homogeneous coordinates: normalize ψ, horizontalLift ψ u, fsInnerHom ψ u v (the Fubini–Study inner product at a nonzero ψ), ★ inner_horizontalLift (fsInnerHom is 4 Re ⟪·,·⟫ of the horizontal lifts), fsInnerHom_self_of_norm_eq_one (fsInnerHom ψ u u = 4 (‖u‖² − ‖⟪ψ, u⟫‖²), the quantum Fisher information, for unit ψ) and ★ fisherRaoInner_bornDeriv_normalize, the bridge stated at normalize ψ.
• ★ fisherInfo_bornDeriv_horizontalLift_le and fisherInfo_bornDeriv_horizontalLift_eq_iff — Braunstein–Caves, projectively: the coordinate readout's Fisher information along the horizontal lift of u is at most fsInnerHom ψ u u, the quantum Fisher information, with equality iff the lift is torus-horizontal.

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

Split 2026-09-18 from FubiniStudyFisherRao.lean (built 2026-09-16 for Physlib PR #1652) so that each file is one Physlib-sized pull request; recorded in this repository's completed-work ledger (specs/future-work.md, KG-4).

Pointwise bounds on one coordinate

theorem FisherRao.bornDeriv_sq_div_bornWeight_le {ι : Type u_1} (ψ u : EuclideanSpace ℂ ι) {i : ι} (h0 : ψ.ofLp i ≠ 0) : bornDeriv ψ u i ^ 2 / bornWeight ψ i ≤ 4 * ‖u.ofLp i‖ ^ 2

Pointwise: (2 Re(ψ̄ᵢ uᵢ))² / ‖ψᵢ‖² ≤ 4 ‖uᵢ‖², since Re z ≤ ‖z‖ and ‖ψ̄ᵢ uᵢ‖ = ‖ψᵢ‖ ‖uᵢ‖.

theorem FisherRao.im_eq_zero_of_bornDeriv_sq_div_bornWeight_eq {ι : Type u_1} (ψ u : EuclideanSpace ℂ ι) {i : ι} (h0 : ψ.ofLp i ≠ 0) (h : bornDeriv ψ u i ^ 2 / bornWeight ψ i = 4 * ‖u.ofLp i‖ ^ 2) : ((starRingEnd ((fun (x : ι) => ℂ) i)) (ψ.ofLp i) * u.ofLp i).im = 0

Pointwise equality in bornDeriv_sq_div_bornWeight_le forces ψ̄ᵢ uᵢ to be real.

Braunstein–Caves for the coordinate readout

theorem FisherRao.fisherInfo_bornDeriv_le {ι : Type u_1} [Fintype ι] (ψ u : EuclideanSpace ℂ ι) (h0 : ∀ (i : ι), ψ.ofLp i ≠ 0) : fisherInfo (bornWeight ψ) (bornDeriv ψ u) ≤ 4 * ‖u‖ ^ 2

The algebraic Braunstein–Caves bound: the classical Fisher information of the coordinate readout along u is at most 4 ‖u‖ ^ 2, for every direction u. For u tangent to the unit sphere at ψ that bound is the quantum Fisher information; for a general u it is not (the radial direction has 4 ‖ψ‖² = 4 and quantum Fisher information 0), and the projective form is fisherInfo_bornDeriv_horizontalLift_le.

theorem FisherRao.fisherInfo_bornDeriv_eq_iff {ι : Type u_1} [Fintype ι] (ψ u : EuclideanSpace ℂ ι) (h0 : ∀ (i : ι), ψ.ofLp i ≠ 0) : fisherInfo (bornWeight ψ) (bornDeriv ψ u) = 4 * ‖u‖ ^ 2 ↔ IsTorusHorizontal ψ u

Equality in the algebraic bound holds exactly on the torus-horizontal directions. The projective form, where the right-hand side is the quantum Fisher information, is fisherInfo_bornDeriv_horizontalLift_eq_iff.

Homogeneous coordinates

A point of projective space is a ray [ψ] with ψ ≠ 0, and a direction at it is any vector u; the pairs (ψ, u) and (ψ, u + c ψ) describe the same tangent vector. The unit vector on the ray is normalize ψ = ‖ψ‖⁻¹ • ψ, and the horizontal lift of u removes the component of u along ψ and rescales: horizontalLift ψ u = ‖ψ‖⁻¹ • (u − (⟪ψ, u⟫/‖ψ‖²) ψ). In these terms the Fubini–Study inner product of two directions is

`fsInnerHom ψ u v = 4 (Re ⟪u, v⟫ / ‖ψ‖² − Re(⟪u, ψ⟫ ⟪ψ, v⟫) / ‖ψ‖⁴)`,

which is 4 Re ⟪horizontalLift ψ u, horizontalLift ψ v⟫ (inner_horizontalLift), and the Born weights of the ray are ‖ψ k‖² / ‖ψ‖² with displacement 2 (Re(ψ̄ₖ uₖ) / ‖ψ‖² − ‖ψ k‖² Re ⟪ψ, u⟫ / ‖ψ‖⁴). The bridge in this form (fisherRaoInner_bornDeriv_normalize) is what the affine charts of ℂℙⁿ meet.

noncomputable def FisherRao.normalize {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) : EuclideanSpace ℂ ι

The unit vector on the ray of ψ.

Equations

• FisherRao.normalize ψ = (↑‖ψ‖)⁻¹ • ψ

theorem FisherRao.norm_normalize {ι : Type u_1} [Fintype ι] {ψ : EuclideanSpace ℂ ι} (hψ : ψ ≠ 0) : ‖normalize ψ‖ = 1

theorem FisherRao.normalize_apply {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) (k : ι) : (normalize ψ).ofLp k = (↑‖ψ‖)⁻¹ * ψ.ofLp k

theorem FisherRao.normalize_apply_ne_zero {ι : Type u_1} [Fintype ι] {ψ : EuclideanSpace ℂ ι} (hψ : ψ ≠ 0) {k : ι} (hk : ψ.ofLp k ≠ 0) : (normalize ψ).ofLp k ≠ 0

theorem FisherRao.bornWeight_normalize {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) (k : ι) : bornWeight (normalize ψ) k = ‖ψ.ofLp k‖ ^ 2 / ‖ψ‖ ^ 2

The Born weights of the ray of ψ: ‖ψ k‖² / ‖ψ‖².

noncomputable def FisherRao.horizontalLift {ι : Type u_1} [Fintype ι] (ψ u : EuclideanSpace ℂ ι) : EuclideanSpace ℂ ι

The horizontal lift of a direction u at ψ: the component of u orthogonal to ψ, scaled by ‖ψ‖⁻¹.

Equations

• FisherRao.horizontalLift ψ u = (↑‖ψ‖)⁻¹ • (u - (inner ℂ ψ u / ↑‖ψ‖ ^ 2) • ψ)

theorem FisherRao.horizontalLift_apply {ι : Type u_1} [Fintype ι] (ψ u : EuclideanSpace ℂ ι) (k : ι) : (horizontalLift ψ u).ofLp k = (↑‖ψ‖)⁻¹ * (u.ofLp k - inner ℂ ψ u / ↑‖ψ‖ ^ 2 * ψ.ofLp k)

theorem FisherRao.inner_normalize_horizontalLift {ι : Type u_1} [Fintype ι] {ψ : EuclideanSpace ℂ ι} (hψ : ψ ≠ 0) (u : EuclideanSpace ℂ ι) : inner ℂ (normalize ψ) (horizontalLift ψ u) = 0

The horizontal lift is orthogonal to ψ, so it is tangent to the unit sphere at normalize ψ.

noncomputable def FisherRao.fsInnerHom {ι : Type u_1} [Fintype ι] (ψ u v : EuclideanSpace ℂ ι) : ℝ

The Fubini–Study inner product of two directions at ψ, in homogeneous coordinates: 4 (Re ⟪u, v⟫ / ‖ψ‖² − Re(⟪u, ψ⟫ ⟪ψ, v⟫) / ‖ψ‖⁴).

Equations

• FisherRao.fsInnerHom ψ u v = 4 * ((inner ℂ u v).re / ‖ψ‖ ^ 2 - (inner ℂ u ψ * inner ℂ ψ v).re / ‖ψ‖ ^ 4)

theorem FisherRao.inner_horizontalLift_eq {ι : Type u_1} [Fintype ι] {ψ : EuclideanSpace ℂ ι} (hψ : ψ ≠ 0) (u v : EuclideanSpace ℂ ι) : inner ℂ (horizontalLift ψ u) (horizontalLift ψ v) = (inner ℂ u v - inner ℂ u ψ * inner ℂ ψ v / ↑‖ψ‖ ^ 2) / ↑‖ψ‖ ^ 2

The inner product of two horizontal lifts, as a complex number.

theorem FisherRao.inner_horizontalLift {ι : Type u_1} [Fintype ι] {ψ : EuclideanSpace ℂ ι} (hψ : ψ ≠ 0) (u v : EuclideanSpace ℂ ι) : 4 * (inner ℂ (horizontalLift ψ u) (horizontalLift ψ v)).re = fsInnerHom ψ u v

★ The Fubini–Study inner product is the inner product of the horizontal lifts: 4 Re ⟪horizontalLift ψ u, horizontalLift ψ v⟫ = fsInnerHom ψ u v.

theorem FisherRao.conj_normalize_mul_horizontalLift {ι : Type u_1} [Fintype ι] (ψ u : EuclideanSpace ℂ ι) (k : ι) : (starRingEnd ((fun (x : ι) => ℂ) k)) ((normalize ψ).ofLp k) * (horizontalLift ψ u).ofLp k = ((starRingEnd ((fun (x : ι) => ℂ) k)) (ψ.ofLp k) * u.ofLp k - ↑(‖ψ.ofLp k‖ ^ 2) * inner ℂ ψ u / ↑(‖ψ‖ ^ 2)) / ↑(‖ψ‖ ^ 2)

The product conj (normalize ψ k) * horizontalLift ψ u k, as a complex number.

theorem FisherRao.bornDeriv_normalize_horizontalLift {ι : Type u_1} [Fintype ι] (ψ u : EuclideanSpace ℂ ι) (k : ι) : bornDeriv (normalize ψ) (horizontalLift ψ u) k = 2 * (((starRingEnd ((fun (x : ι) => ℂ) k)) (ψ.ofLp k) * u.ofLp k).re / ‖ψ‖ ^ 2 - ‖ψ.ofLp k‖ ^ 2 * (inner ℂ ψ u).re / ‖ψ‖ ^ 4)

The Born displacement of the ray along u, in homogeneous coordinates.

theorem FisherRao.isTorusHorizontal_normalize_horizontalLift {ι : Type u_1} [Fintype ι] {ψ u : EuclideanSpace ℂ ι} (hu : ∀ (k : ι), ((starRingEnd ((fun (x : ι) => ℂ) k)) (ψ.ofLp k) * u.ofLp k).im = 0) : IsTorusHorizontal (normalize ψ) (horizontalLift ψ u)

If every ψ̄ₖ uₖ is real then the horizontal lift of u is a horizontal direction at normalize ψ: the projection off ψ and the rescaling preserve the reality of every coordinate product, because ⟪ψ, u⟫ = Σ ψ̄ₖ uₖ is then real as well.

theorem FisherRao.fisherRaoInner_bornDeriv_normalize {ι : Type u_1} [Fintype ι] {ψ : EuclideanSpace ℂ ι} (hψ : ψ ≠ 0) (h0 : ∀ (k : ι), ψ.ofLp k ≠ 0) {u : EuclideanSpace ℂ ι} (hu : ∀ (k : ι), ((starRingEnd ((fun (x : ι) => ℂ) k)) (ψ.ofLp k) * u.ofLp k).im = 0) (v : EuclideanSpace ℂ ι) : (bornSimplex (normalize ψ) ⋯ ⋯).fisherRaoInner (bornDeriv (normalize ψ) (horizontalLift ψ u)) (bornDeriv (normalize ψ) (horizontalLift ψ v)) = fsInnerHom ψ u v

★ The bridge in homogeneous coordinates. For ψ ≠ 0 with no vanishing coordinate, a direction u with every ψ̄ₖ uₖ real, and any direction v, the Fisher–Rao inner product of the Born displacements of the ray equals the Fubini–Study inner product of the directions:

`g_FR(dΦ u, dΦ v) = fsInnerHom ψ u v = 4 (Re ⟪u, v⟫ / ‖ψ‖² − Re(⟪u, ψ⟫ ⟪ψ, v⟫) / ‖ψ‖⁴)`.

This is fisherRaoInner_bornDeriv at normalize ψ along the horizontal lifts.

Braunstein–Caves, projectively

fisherInfo_bornDeriv_le bounds the readout's Fisher information by 4 ‖u‖², which is the quantum Fisher information only when u is tangent to the unit sphere. The projective statement takes an arbitrary direction u at ψ ≠ 0, replaces it by its horizontal lift (the component orthogonal to ψ, rescaled), and compares with fsInnerHom ψ u u — which for unit ψ is 4 (‖u‖² − ‖⟪ψ, u⟫‖²), the quantum Fisher information of the family.

theorem FisherRao.fsInnerHom_self_of_norm_eq_one {ι : Type u_1} [Fintype ι] {ψ : EuclideanSpace ℂ ι} (hψ : ‖ψ‖ = 1) (u : EuclideanSpace ℂ ι) : fsInnerHom ψ u u = 4 * (‖u‖ ^ 2 - ‖inner ℂ ψ u‖ ^ 2)

For a unit vector, the Fubini–Study quadratic form is the quantum Fisher information of a pure-state family: fsInnerHom ψ u u = 4 (‖u‖² − ‖⟪ψ, u⟫‖²).

theorem FisherRao.fsInnerHom_self_eq_norm_horizontalLift {ι : Type u_1} [Fintype ι] {ψ : EuclideanSpace ℂ ι} (hψ : ψ ≠ 0) (u : EuclideanSpace ℂ ι) : fsInnerHom ψ u u = 4 * ‖horizontalLift ψ u‖ ^ 2

The Fisher–Rao quadratic form of the lift's displacement, as 4 ‖horizontalLift ψ u‖².

theorem FisherRao.fisherInfo_bornDeriv_horizontalLift_le {ι : Type u_1} [Fintype ι] {ψ : EuclideanSpace ℂ ι} (hψ : ψ ≠ 0) (h0 : ∀ (k : ι), ψ.ofLp k ≠ 0) (u : EuclideanSpace ℂ ι) : fisherInfo (bornWeight (normalize ψ)) (bornDeriv (normalize ψ) (horizontalLift ψ u)) ≤ fsInnerHom ψ u u

★ Braunstein–Caves for the coordinate readout, projectively. For ψ ≠ 0 with no vanishing coordinate and any direction u, the classical Fisher information of the coordinate readout along the horizontal lift of u is at most the Fubini–Study quadratic form fsInnerHom ψ u u, i.e. the quantum Fisher information of the family (fsInnerHom_self_of_norm_eq_one).

theorem FisherRao.fisherInfo_bornDeriv_horizontalLift_eq_iff {ι : Type u_1} [Fintype ι] {ψ : EuclideanSpace ℂ ι} (hψ : ψ ≠ 0) (h0 : ∀ (k : ι), ψ.ofLp k ≠ 0) (u : EuclideanSpace ℂ ι) : fisherInfo (bornWeight (normalize ψ)) (bornDeriv (normalize ψ) (horizontalLift ψ u)) = fsInnerHom ψ u u ↔ IsTorusHorizontal (normalize ψ) (horizontalLift ψ u)

★ Equality in projective Braunstein–Caves holds exactly when the horizontal lift is torus-horizontal: the coordinate readout extracts the full quantum Fisher information of a direction iff, after the radial component is removed, the direction changes only the moduli of the coordinates.