The torus moment map on complex projective space, in coordinates

Category: 1-Mathlib (CSD-free; the coordinate function [z] ↦ (|zᵢ|²/‖z‖²)ᵢ on ℙ ℂ (ℂⁿ)).

A point of ℙ ℂ (EuclideanSpace ℂ ι) is a ray [z], and the squared moduli of its coordinates, normalised by ‖z‖², do not depend on the representative. The resulting function

`momentMap [z] i = ‖z i‖² / ‖z‖²`

takes values in the standard simplex: every coordinate is nonnegative and the coordinates sum to one. It is the moment map of the coordinate-phase torus action for the Fubini–Study form, up to the factor that form's normalisation fixes (the Hamiltonian of the action is 2 Σ θₖ momentMap · k, so the moment map in the Hamiltonian sense is twice this function); this file proves only the coordinate facts, and the manifold-level statement that earns the name lives downstream (Projectivization.torusField_isHamiltonianVectorField and range_momentMap in Geometry/Manifold/Instances/ProjectiveSpaceMomentMap.lean).

Main declarations

• Projectivization.momentMap — the coordinate function, defined through rep.
• momentMap_mk — its value on mk ℂ ψ hψ is ‖ψ i‖² / ‖ψ‖² (representative independence).
• momentMap_nonneg, momentMap_sum_eq_one, momentMap_le_one — the simplex constraints.
• momentMap_mk_eq_inner_sq — for a unit vector, momentMap [ψ] i = ‖⟨eᵢ, ψ⟩‖² with eᵢ = EuclideanSpace.single i 1: the coordinate is the squared overlap with the i-th basis vector.
• momentMap_mk_of_norm_eq — equal-modulus coordinates land at the barycentre 1/N.
• continuous_momentMap, measurable_momentMap — regularity, by descent through the quotient map mk' (the defining formula goes through the choice-based rep, which is not continuous).

Provenance

Moved verbatim from CsdLean4/LF4/MomentMap.lean (2026-09-16), where it was introduced as the torus moment map whose coordinates are the Born weights of a preparation in the measurement eigenbasis. CSD.LF4 re-exports these names, so that file remains the entry point for the programme-level reading; this file is the mathematics. Recorded in the completed-work ledger (specs/future-work.md, KG-4).

References

• Bengtsson, Życzkowski, Geometry of Quantum States, 2nd ed., §4.4 (the Fubini–Study geometry of ℂℙⁿ and the torus action).

noncomputable def Projectivization.momentMap {ι : Type u_1} [Fintype ι] (p : Projectivization ℂ (EuclideanSpace ℂ ι)) (i : ι) : ℝ

The torus moment map on ℙ ℂ (ℂᴺ), in coordinates: Φ([z])ᵢ = ‖zᵢ‖²/‖z‖². Well defined on the projective point (scale invariant; see momentMap_mk).

Equations

• p.momentMap i = ‖p.rep.ofLp i‖ ^ 2 / ‖p.rep‖ ^ 2

theorem Projectivization.momentMap_nonneg {ι : Type u_1} [Fintype ι] (p : Projectivization ℂ (EuclideanSpace ℂ ι)) (i : ι) : 0 ≤ p.momentMap i

Each moment coordinate is nonnegative.

theorem Projectivization.momentMap_sum_eq_one {ι : Type u_1} [Fintype ι] (p : Projectivization ℂ (EuclideanSpace ℂ ι)) : ∑ i : ι, p.momentMap i = 1

The moment coordinates sum to one: the image lands in the standard simplex.

theorem Projectivization.momentMap_le_one {ι : Type u_1} [Fintype ι] (p : Projectivization ℂ (EuclideanSpace ℂ ι)) (i : ι) : p.momentMap i ≤ 1

Each moment coordinate is at most one (‖p.rep i‖² ≤ ∑ⱼ ‖p.rep j‖² = ‖p.rep‖²).

theorem Projectivization.momentRatio_smul {ι : Type u_1} [Fintype ι] (c : ℂ) (hc : c ≠ 0) (v : EuclideanSpace ℂ ι) (i : ι) : ‖(c • v).ofLp i‖ ^ 2 / ‖c • v‖ ^ 2 = ‖v.ofLp i‖ ^ 2 / ‖v‖ ^ 2

The coordinate ratio ‖vᵢ‖²/‖v‖² is invariant under nonzero rescaling of v (the projective well-definedness of momentMap).

theorem Projectivization.momentMap_mk {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) (hψ : ψ ≠ 0) (i : ι) : (mk ℂ ψ hψ).momentMap i = ‖ψ.ofLp i‖ ^ 2 / ‖ψ‖ ^ 2

The moment map evaluated at a representative ψ: Φ([ψ])ᵢ = ‖ψᵢ‖²/‖ψ‖². The value depends only on ψ (not on the chosen rep), by scale invariance.

theorem Projectivization.momentMap_mk_eq_inner_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : EuclideanSpace ℂ ι) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : ι) : (mk ℂ ψ hψ0).momentMap i = ‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2

The moment coordinate is a squared overlap. For a unit vector ψ, the i-th coordinate of the moment map at [ψ] equals ‖⟨eᵢ, ψ⟩‖² for the standard basis vector eᵢ = EuclideanSpace.single i 1.

theorem Projectivization.momentMap_mk_of_norm_eq {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) (hψ0 : ψ ≠ 0) {a : ℝ} (hψ : ∀ (j : ι), ‖ψ.ofLp j‖ = a) (i : ι) : (mk ℂ ψ hψ0).momentMap i = 1 / ↑(Fintype.card ι)

Equal-modulus coordinates sit at the barycentre. If every coordinate of ψ has the same modulus, the moment map of [ψ] is the uniform weight 1/|ι| in every coordinate; the normalisation is immaterial (momentMap_mk divides it out).

Regularity: momentMap is continuous, hence measurable

momentMap is defined through p.rep, a Classical.choice representative, so it cannot be attacked directly: Projectivization.rep is not continuous as a map out of ℙ. The route is the quotient. The coordinate ratio v ↦ ‖vᵢ‖²/‖v‖² is continuous on the nonzero subtype and scale invariant (momentRatio_smul), and mk' is a quotient map (isQuotientMap_mk'), so the descended function is continuous. Measurability follows because ℙ K V carries the Borel σ-algebra of that topology (instBorelSpace).

theorem Projectivization.continuous_momentMap {ι : Type u_1} [Fintype ι] (i : ι) : Continuous fun (p : Projectivization ℂ (EuclideanSpace ℂ ι)) => p.momentMap i

The moment coordinate is continuous, by descent through the quotient map mk'.

theorem Projectivization.measurable_momentMap {ι : Type u_1} [Fintype ι] (i : ι) : Measurable fun (p : Projectivization ℂ (EuclideanSpace ℂ ι)) => p.momentMap i

The moment coordinate is measurable, since ℙ ℂ V carries the Borel σ-algebra of the quotient topology (instBorelSpace).