The Fubini–Study metric of ℂℙⁿ pushes forward to Fisher–Rao along the moment map

Category: 1-Mathlib (CSD-free; the Kähler manifold ℂℙⁿ, its torus moment map and the open simplex of FisherRao.lean).

Glossary: https://glossary.constraintsurfacedynamics.com/fisher-rao-metric/

The Born-weight map Φ : ℂℙⁿ → Δⁿ, Φ([z])ₖ = ‖zₖ‖²/‖z‖² (Projectivization.momentMap), sends the regular stratum (every coordinate positive) into the open simplex. Its differential kills the orbit directions of the coordinate-phase torus — the vertical space at x — and on the Fubini–Study orthogonal complement, the horizontal space, it is an isometric embedding into the tangent space of the simplex:

`g_FS(u, v) = g_FR(dΦₓ u, dΦₓ v)`   for `u` horizontal at `x` and any `v`,

injective on the horizontal space (momentDeriv_injOn_horizontalSpace), with constant one in the normalisation of Projectivization.fsMetric (the round unit sphere for ℂℙ¹, Gram matrix 4 • 1 at a chart origin). That dΦₓ is then a linear isomorphism of the horizontal space onto the zero-sum hyperplane follows by dimension but is not packaged here.

A word on the name. Φ is the moment map of the torus action for fsForm up to the factor the form's normalisation fixes: the Hamiltonian of the action is 2 Σ θₖ Φₖ (torusHamiltonian, torusField_isHamiltonianVectorField), so the moment map in the Hamiltonian sense is 2Φ. The bridge is stated for Φ itself, the Born weights, and its constant one is for that map. The manifold statement is the vector-level identity of Analysis/InformationGeometry/FubiniStudyFisherRao.lean read in an affine chart: the point is the ray of ψ = insertOne i w, a chart direction u lifts to insertZero i u, and fsMetric at the point is fsInnerHom ψ on the lifts (★ fsMetric_eq_fsInnerHom, the standard formula 4 (Re ⟪δψ, δψ'⟫/‖ψ‖² − Re(⟪δψ, ψ⟫⟪ψ, δψ'⟫)/‖ψ‖⁴)).

Main declarations

• Projectivization.insertZero i u — the lift of a chart direction; momentMap_chartInv — the moment map in the chart is bornWeight (normalize (insertOne i w)).
• ★ fsMetric_eq_fsInnerHom — the Fubini–Study metric at x is the homogeneous formula on the lifts to insertOne (idx x) (chartFun (idx x) x).
• momentDeriv x — the differential of the moment map at x, with hasMFDerivAt_momentMap and mfderiv_momentMap; momentDeriv_apply — it is the Born displacement of the horizontal lift; sum_momentDeriv — it is tangent to the simplex; momentDeriv_torusField and momentDeriv_eq_zero_of_mem_verticalSpace — it kills the vertical space.
• verticalSpace x, horizontalSpace x — the torus-orbit directions and their fsMetric-orthogonal complement; ★ mem_horizontalSpace_iff — horizontal means every conj (wⱼ) uⱼ is real in the chart, i.e. the direction moves moduli and not phases; momentDeriv_eq_zero_iff_of_mem_horizontalSpace and momentDeriv_injOn_horizontalSpace — on the regular stratum the differential is injective on the horizontal space.
• regularStratum, toOpenSimplex — the moment map into OpenSimplex (Fin (n + 1)).
• ★★ fsMetric_eq_fisherRaoInner — the bridge: on the regular stratum, for u horizontal, fsMetric x u v = fisherRaoInner (toOpenSimplex x) (momentDeriv x u) (momentDeriv x v).

The constant

None is assumed: fsMetric is ω_FS(J·, ·) for the repository's Fubini–Study form, whose Gram matrix at a chart origin is 4 • 1 (toMatrix_fsModelMetric_zero), and the 4 on the Fisher–Rao side is the derivative of ‖·‖². They agree, so the constant is 1. In this normalisation fsMetric is the quantum Fisher information of a pure-state family (FisherRao.fsInnerHom_self_of_norm_eq_one); in the normalisation ‖δψ‖² − ‖⟪ψ, δψ⟫‖² of Bengtsson–Życzkowski, which the vector-level fsMetric of Empirical/Metrology/QuantumFisher.lean uses, the same statement reads 4 g_FS = g_FR ∘ dΦ and the quantum Fisher information is 4 g_FS.

Implementation notes

The tangent space of ℂℙⁿ at x is the model Fin n → ℂ (the chart's own coordinates), and fsMetric x is by definition fsModelMetric (chartFun (idx x) x). The differential momentDeriv x and the vertical/horizontal spaces are therefore stated on the model space; a tangent vector u : TangentSpace 𝓘(ℝ, Fin n → ℂ) x is used in them directly, as torusField already is.

References

• S. L. Braunstein, C. M. Caves, Phys. Rev. Lett. 72, 3439 (1994).
• I. Bengtsson, K. Życzkowski, Geometry of Quantum States, 2nd ed., §§4.4, 14.2.
• Analysis/InformationGeometry/FubiniStudyFisherRao.lean (the vector-level bridge); Instances/ProjectiveSpaceMomentMap.lean (torusField, the chart derivatives); Instances/ProjectiveSpaceFubiniStudyRiemannian.lean (fsMetric, fsModelMetric); Physlib PR #1652.

Provenance

Built 2026-09-16 for Physlib PR #1652; recorded in this repository's completed-work ledger (specs/future-work.md, KG-4) and claims ledger (CL-075).

Lifts of chart directions

def Projectivization.insertZero {n : ℕ} (i : Fin (n + 1)) (u : Fin n → ℂ) : Ambient n

Insert 0 in slot i: the lift of a direction in the i-th affine chart.

Equations

• Projectivization.insertZero i u = WithLp.toLp 2 (i.insertNth 0 u)

@[simp]

theorem Projectivization.insertZero_apply_same {n : ℕ} (i : Fin (n + 1)) (u : Fin n → ℂ) : (insertZero i u).ofLp i = 0

@[simp]

theorem Projectivization.insertZero_apply_succAbove {n : ℕ} (i : Fin (n + 1)) (u : Fin n → ℂ) (j : Fin n) : (insertZero i u).ofLp (i.succAbove j) = u j

theorem Projectivization.inner_insertZero_insertZero {n : ℕ} (i : Fin (n + 1)) (u v : Fin n → ℂ) : inner ℂ (insertZero i u) (insertZero i v) = inner ℂ (toLpCLM u) (toLpCLM v)

theorem Projectivization.inner_insertZero_insertOne {n : ℕ} (i : Fin (n + 1)) (u w : Fin n → ℂ) : inner ℂ (insertZero i u) (insertOne i w) = inner ℂ (toLpCLM u) (toLpCLM w)

theorem Projectivization.inner_insertOne_insertZero {n : ℕ} (i : Fin (n + 1)) (w u : Fin n → ℂ) : inner ℂ (insertOne i w) (insertZero i u) = inner ℂ (toLpCLM w) (toLpCLM u)

theorem Projectivization.norm_insertOne_sq {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : ‖insertOne i w‖ ^ 2 = 1 + ‖toLpCLM w‖ ^ 2

theorem Projectivization.norm_insertOne_sq_eq_chartDen {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : ‖insertOne i w‖ ^ 2 = chartDen w

theorem Projectivization.momentMap_chartInv {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) (k : Fin (n + 1)) : (chartInv i w).momentMap k = FisherRao.bornWeight (FisherRao.normalize (insertOne i w)) k

The moment map in the i-th chart is the Born weight of the normalised lift.

★ The Fubini–Study metric on the lifts

theorem Projectivization.fsModelMetric_eq_fsInnerHom {n : ℕ} (i : Fin (n + 1)) (w u v : Fin n → ℂ) : ((fsModelMetric w) u) v = FisherRao.fsInnerHom (insertOne i w) (insertZero i u) (insertZero i v)

The model metric at w is the homogeneous Fubini–Study formula on the lifts to insertOne i w.

theorem Projectivization.fsMetric_eq_fsInnerHom {n : ℕ} (x : Projectivization ℂ (Ambient n)) (u v : Fin n → ℂ) : x.fsMetric u v = FisherRao.fsInnerHom (insertOne x.idx (chartFun x.idx x)) (insertZero x.idx u) (insertZero x.idx v)

★ The Fubini–Study metric at x is the homogeneous formula on the lifts: with ψ = insertOne (idx x) (chartFun (idx x) x) a representative of x and insertZero (idx x) u the lift of a tangent vector u,

`fsMetric x u v = 4 (Re ⟪δu, δv⟫ / ‖ψ‖² − Re(⟪δu, ψ⟫ ⟪ψ, δv⟫) / ‖ψ‖⁴)`.

This identifies fsMetric with the Fubini–Study metric as usually written on lifts.

The differential of the moment map

noncomputable def Projectivization.momentNumDeriv {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : Fin (n + 1) → (Fin n → ℂ) →L[ℝ] ℝ

The derivative of the numerator ‖insertOne i w k‖² of the k-th moment coordinate in the i-th chart: 0 for k = i and normSqCoordDeriv j w for k = i.succAbove j.

Equations

• Projectivization.momentNumDeriv i w = i.insertNth 0 fun (j : Fin n) => Projectivization.normSqCoordDeriv j w

theorem Projectivization.momentNumDeriv_apply {n : ℕ} (i : Fin (n + 1)) (w u : Fin n → ℂ) (k : Fin (n + 1)) : (momentNumDeriv i w k) u = 2 * ((starRingEnd ((fun (x : Fin (n + 1)) => ℂ) k)) ((insertOne i w).ofLp k) * (insertZero i u).ofLp k).re

theorem Projectivization.hasFDerivAt_momentNum {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) (k : Fin (n + 1)) : HasFDerivAt (fun (w : Fin n → ℂ) => ‖(insertOne i w).ofLp k‖ ^ 2) (momentNumDeriv i w k) w

noncomputable def Projectivization.momentChartCoordDeriv {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) (k : Fin (n + 1)) : (Fin n → ℂ) →L[ℝ] ℝ

The derivative of the k-th moment coordinate in the i-th chart, from the product rule for ‖insertOne i w k‖² · (chartDen w)⁻¹.

Equations

• One or more equations did not get rendered due to their size.

theorem Projectivization.momentMap_chartInv_eq_mul_inv {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) (k : Fin (n + 1)) : (chartInv i w).momentMap k = ‖(insertOne i w).ofLp k‖ ^ 2 * (chartDen w)⁻¹

theorem Projectivization.hasFDerivAt_momentMap_chartInv {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) (k : Fin (n + 1)) : HasFDerivAt (fun (w : Fin n → ℂ) => (chartInv i w).momentMap k) (momentChartCoordDeriv i w k) w

theorem Projectivization.chartDenDeriv_apply' {n : ℕ} (i : Fin (n + 1)) (w u : Fin n → ℂ) : (chartDenDeriv w) u = 2 * (inner ℂ (insertOne i w) (insertZero i u)).re

theorem Projectivization.momentChartCoordDeriv_apply {n : ℕ} (i : Fin (n + 1)) (w u : Fin n → ℂ) (k : Fin (n + 1)) : (momentChartCoordDeriv i w k) u = FisherRao.bornDeriv (FisherRao.normalize (insertOne i w)) (FisherRao.horizontalLift (insertOne i w) (insertZero i u)) k

The k-th coordinate of the chart derivative is the Born displacement of the horizontal lift.

noncomputable def Projectivization.momentDeriv {n : ℕ} (x : Projectivization ℂ (Ambient n)) : (Fin n → ℂ) →L[ℝ] Fin (n + 1) → ℝ

The differential of the moment map at x, as a continuous linear map from the model tangent space Fin n → ℂ to Fin (n + 1) → ℝ: coordinatewise the chart derivatives at chartFun (idx x) x.

Equations

• x.momentDeriv = ContinuousLinearMap.pi fun (k : Fin (n + 1)) => Projectivization.momentChartCoordDeriv x.idx (Projectivization.chartFun x.idx x) k

theorem Projectivization.continuous_momentMap_pi {n : ℕ} : Continuous momentMap

theorem Projectivization.hasMFDerivAt_momentMap {n : ℕ} (x : Projectivization ℂ (Ambient n)) : HasMFDerivAt% momentMap x x.momentDeriv

The moment map is differentiable, with differential momentDeriv.

theorem Projectivization.mfderiv_momentMap {n : ℕ} (x : Projectivization ℂ (Ambient n)) : mfderiv% momentMap x = x.momentDeriv

theorem Projectivization.momentDeriv_apply {n : ℕ} (x : Projectivization ℂ (Ambient n)) (u : Fin n → ℂ) (k : Fin (n + 1)) : x.momentDeriv u k = FisherRao.bornDeriv (FisherRao.normalize (insertOne x.idx (chartFun x.idx x))) (FisherRao.horizontalLift (insertOne x.idx (chartFun x.idx x)) (insertZero x.idx u)) k

The differential of the moment map is the Born displacement of the horizontal lift of the direction.

theorem Projectivization.sum_momentDeriv {n : ℕ} (x : Projectivization ℂ (Ambient n)) (u : Fin n → ℂ) : ∑ k : Fin (n + 1), x.momentDeriv u k = 0

The differential of the moment map is tangent to the simplex: its coordinates sum to zero.

The vertical and horizontal spaces

noncomputable def Projectivization.verticalSpace {n : ℕ} (x : Projectivization ℂ (Ambient n)) : Submodule ℝ (Fin n → ℂ)

The vertical space at x: the span of the torus-orbit directions, in the model tangent space.

Equations

• x.verticalSpace = Submodule.span ℝ (Set.range fun (θ : Fin (n + 1) → ℝ) => Projectivization.tangentToModel (Projectivization.torusField θ x))

noncomputable def Projectivization.horizontalSpace {n : ℕ} (x : Projectivization ℂ (Ambient n)) : Submodule ℝ (Fin n → ℂ)

The horizontal space at x: the fsMetric-orthogonal complement of the vertical space. fsMetric x is, by definition, the model metric at the chart coordinate of x, so the orthogonal complement is taken for fsModelMetric (chartFun (idx x) x).

Equations

• x.horizontalSpace = (Projectivization.fsModelMetric (Projectivization.chartFun x.idx x)).orthogonal x.verticalSpace

theorem Projectivization.torusField_mem_verticalSpace {n : ℕ} (θ : Fin (n + 1) → ℝ) (x : Projectivization ℂ (Ambient n)) : tangentToModel (torusField θ x) ∈ x.verticalSpace

theorem Projectivization.mem_horizontalSpace_iff_forall {n : ℕ} (x : Projectivization ℂ (Ambient n)) (u : Fin n → ℂ) : u ∈ x.horizontalSpace ↔ ∀ (θ : Fin (n + 1) → ℝ), x.fsMetric (torusField θ x) u = 0

A tangent vector is horizontal iff it is fsMetric-orthogonal to every torus-orbit direction.

theorem Projectivization.fsModelMetric_torusChartField {n : ℕ} (i : Fin (n + 1)) (θ : Fin (n + 1) → ℝ) (w u : Fin n → ℂ) : ((fsModelMetric w) (torusChartField i θ w)) u = -(torusChartHamDeriv i θ w) (Complex.I • u)

The metric of a torus-orbit direction against u is minus the derivative of the chart Hamiltonian along i·u: g(X_θ, u) = ω(J X_θ, u) = −ω(X_θ, J u) = −dH_θ(J u), by the J-invariance of ω.

theorem Projectivization.two_mul_re_add_im_I (a b : ℂ) : 2 * (a.re * (Complex.I * b).re + a.im * (Complex.I * b).im) = -2 * ((starRingEnd ℂ) a * b).im

The pairing 2 (Re wⱼ Re (i uⱼ) + Im wⱼ Im (i uⱼ)) is −2 Im (conj wⱼ · uⱼ).

theorem Projectivization.fsModelMetric_torusChartField_eq {n : ℕ} (i : Fin (n + 1)) (θ : Fin (n + 1) → ℝ) (w u : Fin n → ℂ) : ((fsModelMetric w) (torusChartField i θ w)) u = 4 * ((chartDen w)⁻¹ * ∑ j : Fin n, θ (i.succAbove j) * ((starRingEnd ℂ) (w j) * u j).im - torusChartNum i θ w * (chartDen w ^ 2)⁻¹ * ∑ j : Fin n, ((starRingEnd ℂ) (w j) * u j).im)

The metric of a torus-orbit direction against u, in the chart: with Iⱼ = Im (conj wⱼ · uⱼ) and N = θᵢ + Σⱼ θ_{s j} ‖wⱼ‖², it is 4 (D⁻¹ Σⱼ θ_{s j} Iⱼ − N D⁻² Σⱼ Iⱼ).

theorem Projectivization.mem_horizontalSpace_iff {n : ℕ} (x : Projectivization ℂ (Ambient n)) (u : Fin n → ℂ) : u ∈ x.horizontalSpace ↔ ∀ (j : Fin n), ((starRingEnd ℂ) (chartFun x.idx x j) * u j).im = 0

★ Horizontal means moduli-only. A tangent vector u at x is fsMetric-orthogonal to every torus-orbit direction iff, in the chart at x, every product conj (wⱼ) uⱼ is real — the direction changes the moduli of the homogeneous coordinates and none of their phases.

theorem Projectivization.momentDeriv_torusField {n : ℕ} (θ : Fin (n + 1) → ℝ) (x : Projectivization ℂ (Ambient n)) : x.momentDeriv (tangentToModel (torusField θ x)) = 0

The differential of the moment map kills every torus-orbit direction.

theorem Projectivization.momentDeriv_eq_zero_of_mem_verticalSpace {n : ℕ} (x : Projectivization ℂ (Ambient n)) {v : Fin n → ℂ} (hv : v ∈ x.verticalSpace) : x.momentDeriv v = 0

The differential of the moment map vanishes on the vertical space.

The regular stratum and the bridge

def Projectivization.regularStratum {n : ℕ} : Set (Projectivization ℂ (Ambient n))

The regular stratum: the points at which every moment coordinate is positive, i.e. no homogeneous coordinate vanishes. The moment map sends it into the open simplex.

Equations

• Projectivization.regularStratum = {x : Projectivization ℂ (Projectivization.Ambient n) | ∀ (k : Fin (n + 1)), 0 < x.momentMap k}

noncomputable def Projectivization.toOpenSimplex {n : ℕ} (x : Projectivization ℂ (Ambient n)) (hx : x ∈ regularStratum) : FisherRao.OpenSimplex (Fin (n + 1))

The moment map on the regular stratum, as a point of the open simplex.

Equations

• x.toOpenSimplex hx = { val := x.momentMap, pos := hx, sum_one := ⋯ }

@[simp]

theorem Projectivization.toOpenSimplex_val {n : ℕ} (x : Projectivization ℂ (Ambient n)) (hx : x ∈ regularStratum) : (x.toOpenSimplex hx).val = x.momentMap

theorem Projectivization.chartInv_idx_chartFun {n : ℕ} (x : Projectivization ℂ (Ambient n)) : chartInv x.idx (chartFun x.idx x) = x

theorem Projectivization.insertOne_chartFun_ne_zero {n : ℕ} {x : Projectivization ℂ (Ambient n)} (hx : x ∈ regularStratum) (k : Fin (n + 1)) : (insertOne x.idx (chartFun x.idx x)).ofLp k ≠ 0

On the regular stratum, no coordinate of the chart representative vanishes.

theorem Projectivization.fsMetric_eq_fisherRaoInner {n : ℕ} {x : Projectivization ℂ (Ambient n)} (hx : x ∈ regularStratum) {u : Fin n → ℂ} (hu : u ∈ x.horizontalSpace) (v : Fin n → ℂ) : x.fsMetric u v = (x.toOpenSimplex hx).fisherRaoInner (x.momentDeriv u) (x.momentDeriv v)

★★ The bridge. On the regular stratum, for u horizontal at x and any v, the Fubini–Study metric of u and v is the Fisher–Rao inner product of their images under the differential of the moment map:

`fsMetric x u v = fisherRaoInner (toOpenSimplex x) (momentDeriv x u) (momentDeriv x v)`.

The constant is one: fsMetric is normalised so that ℂℙ¹ is the unit round sphere, and in that normalisation g_FS itself is the quantum Fisher information of the family, which the coordinate readout attains exactly on the horizontal directions (FisherRao.fisherInfo_bornDeriv_horizontalLift_eq_iff).

Injectivity on the horizontal space

theorem Projectivization.momentDeriv_eq_zero_iff_of_mem_horizontalSpace {n : ℕ} {x : Projectivization ℂ (Ambient n)} (hx : x ∈ regularStratum) {u : Fin n → ℂ} (hu : u ∈ x.horizontalSpace) : x.momentDeriv u = 0 ↔ u = 0

On the regular stratum, a horizontal direction with zero Born displacement is zero: in the chart the displacement of coordinate k is 2 (aₖ/D − pₖ S/D²) with aₖ = Re(ψ̄ₖ δuₖ) real by horizontality and S = Σ aₖ; the chart coordinate k = idx x has aₖ = 0 and pₖ = 1, which forces S = 0, hence every aₖ = 0, hence every uⱼ = 0 since no wⱼ vanishes.

theorem Projectivization.momentDeriv_injOn_horizontalSpace {n : ℕ} {x : Projectivization ℂ (Ambient n)} (hx : x ∈ regularStratum) : Set.InjOn ⇑x.momentDeriv ↑x.horizontalSpace

★ The differential of the moment map is injective on the horizontal space of every point of the regular stratum: together with fsMetric_eq_fisherRaoInner and sum_momentDeriv, an isometric embedding of the horizontal space into the zero-sum tangent space of the simplex.