Fubini–Study measure on complex projective space

Category: 1-Mathlib (CSD-free Mathlib upstream candidate).

Constructs the U(N)-invariant Borel probability measure on Projectivization ℂ (EuclideanSpace ℂ (Fin N)) by pushing the probability-normalised Haar measure unitaryHaarProb (from UnitaryHaar.lean) forward through the orbit map U ↦ U • p₀ for a fixed reference point p₀.

Invariance is stated over the full unitary group Matrix.unitaryGroup (Fin N) ℂ = U(N) — the group every definition and theorem here actually quantifies over. On projective space the central U(1) acts trivially, so U(N)- and SU(N)-invariance are the same condition on measures over ℂℙ^{N-1}; the literature's "SU(N)-invariant Fubini–Study measure" is this measure.

Main definitions

• Matrix.UnitaryGroup.orbitMap p₀ — the orbit map at p₀, U ↦ U • p₀ : Matrix.unitaryGroup (Fin N) ℂ → ℙ ℂ (EuclideanSpace ℂ (Fin N)).
• fubiniStudyMeasure p₀ — Measure.map (orbitMap p₀) unitaryHaarProb. The U(N)-invariant Borel probability measure on ℂℙ^{N-1}.
• defaultPoint, defaultFubiniStudyMeasure — canonical choice using EuclideanSpace.single 0 1 as the reference (requires [NeZero N]).

Main results

• orbit_map_continuous — continuity of the orbit map (Phase A).
• orbit_map_measurable — measurability corollary.
• instIsProbabilityMeasureFubiniStudyMeasure — pushforward is a probability measure.
• fubiniStudyMeasure_smul_invariant — U(N)-invariance.

Provenance

Staged as upstream Mathlib material. Intended location: Mathlib/LinearAlgebra/Projectivization/FubiniStudy.lean.

Tags

projectivization, Fubini-Study, Haar measure, U(N), invariant measure

Phase A — orbit map continuity

theorem Matrix.UnitaryGroup.toEuclideanLin_apply_continuous {N : ℕ} (v : EuclideanSpace ℂ (Fin N)) : Continuous fun (M : Matrix (Fin N) (Fin N) ℂ) => (toEuclideanLin M) v

For any fixed vector v, the map M ↦ Matrix.toEuclideanLin M v is continuous in M. Routes through Continuous.matrix_mulVec and PiLp.continuous_toLp.

theorem Matrix.UnitaryGroup.toEuclideanLin_unitary_apply_ne_zero {N : ℕ} (U : ↥(unitaryGroup (Fin N) ℂ)) {v : EuclideanSpace ℂ (Fin N)} (hv : v ≠ 0) : (toEuclideanLin ↑U) v ≠ 0

A unitary matrix's toEuclideanLin action preserves non-zero. Routes through toEuclideanLinearEquiv's injectivity.

noncomputable def Matrix.UnitaryGroup.orbitMap {N : ℕ} (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : ↥(unitaryGroup (Fin N) ℂ) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))

The orbit map at p₀, U ↦ U • p₀.

Equations

• Matrix.UnitaryGroup.orbitMap p₀ U = U • p₀

theorem Matrix.UnitaryGroup.orbit_map_continuous {N : ℕ} (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : Continuous (orbitMap p)

Phase A2. The orbit map is continuous.

Decomposition: U • p = mk' ⟨(toEuclideanLin U.val) p.rep, nonzero⟩ via the compHom action on the Projectivization MulAction. The non-zero proof routes through toEuclideanLin_unitary_apply_ne_zero.

theorem Matrix.UnitaryGroup.orbit_map_measurable {N : ℕ} (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : Measurable (orbitMap p)

Phase A3. The orbit map is measurable.

Phase B — definition of Fubini–Study measure

noncomputable def Matrix.UnitaryGroup.fubiniStudyMeasure {N : ℕ} (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : MeasureTheory.Measure (Projectivization ℂ (EuclideanSpace ℂ (Fin N)))

Fubini–Study measure at reference point p₀. Defined as the pushforward of the probability-normalised Haar measure on the unitary group under the orbit map U ↦ U • p₀.

Equations

• Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = MeasureTheory.Measure.map (Matrix.UnitaryGroup.orbitMap p₀) Matrix.UnitaryGroup.unitaryHaarProb

Phase C — probability measure

instance Matrix.UnitaryGroup.instIsProbabilityMeasureFubiniStudyMeasure {N : ℕ} (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : MeasureTheory.IsProbabilityMeasure (fubiniStudyMeasure p₀)

Pushforward of a probability measure by a measurable map is a probability measure.

Phase D — U(N)-invariance

theorem Matrix.UnitaryGroup.smul_comp_orbitMap {N : ℕ} (U' : ↥(unitaryGroup (Fin N) ℂ)) (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : (fun (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) => U' • p) ∘ orbitMap p₀ = orbitMap p₀ ∘ fun (U : ↥(unitaryGroup (Fin N) ℂ)) => U' * U

Compatibility lemma: (U' • ·) ∘ orbitMap p₀ = orbitMap p₀ ∘ (U' * ·). The MulAction axiom (U' * U) • p₀ = U' • (U • p₀) makes the two forms equal as functions.

theorem Matrix.UnitaryGroup.fubiniStudyMeasure_smul_invariant {N : ℕ} (U' : ↥(unitaryGroup (Fin N) ℂ)) (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : MeasureTheory.Measure.map (fun (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) => U' • p) (fubiniStudyMeasure p₀) = fubiniStudyMeasure p₀

U(N)-invariance of the Fubini–Study measure. For any unitary U', pushing forward fubiniStudyMeasure p₀ by the action of U' yields the same measure.

Proof via the chain:

1. unfold fubiniStudyMeasure to expose (orbitMap p₀).map unitaryHaarProb;
2. compose maps via Measure.map_map to push U' • · through the orbit map;
3. use smul_comp_orbitMap to re-express the composition as orbitMap p₀ ∘ (U' * ·);
4. push the multiplication-by-U' map back inside via Measure.map_map;
5. invoke unitaryHaarProb's left-invariance (IsMulLeftInvariant, inherited from unitaryHaarProb_isHaarMeasure) to kill the inner pushforward.

Phase E — the canonical reference point

fubiniStudyMeasure takes a base point, and every consumer has had to supply one. The measure does not in fact depend on it (fubiniStudyMeasure_basepoint_independent, proved in FubiniStudyUnique.lean where uniqueness is available), so a canonical choice can be named here and the dependence discharged there. Landed 2026-08-19; the module docstring had advertised these two definitions since the file was written without either existing.

noncomputable def Matrix.UnitaryGroup.defaultPoint (N : ℕ) [NeZero N] : Projectivization ℂ (EuclideanSpace ℂ (Fin N))

The canonical reference point [e₀] of ℂℙ^{N-1}: the ray through the first standard basis vector.

Equations

• Matrix.UnitaryGroup.defaultPoint N = Projectivization.mk ℂ (EuclideanSpace.single 0 1) ⋯

noncomputable def Matrix.UnitaryGroup.defaultFubiniStudyMeasure (N : ℕ) [NeZero N] : MeasureTheory.Measure (Projectivization ℂ (EuclideanSpace ℂ (Fin N)))

The Fubini–Study measure at the canonical point. By fubiniStudyMeasure_basepoint_independent this is the Fubini–Study measure: the base point is not a degree of freedom.

Equations

• Matrix.UnitaryGroup.defaultFubiniStudyMeasure N = Matrix.UnitaryGroup.fubiniStudyMeasure (Matrix.UnitaryGroup.defaultPoint N)

instance Matrix.UnitaryGroup.instIsProbabilityMeasureDefaultFubiniStudyMeasure (N : ℕ) [NeZero N] : MeasureTheory.IsProbabilityMeasure (defaultFubiniStudyMeasure N)