Uniqueness of the invariant measure on complex projective space (Phases G1, G4, G5) #
Category: 1-Mathlib (CSD-free Mathlib upstream candidate).
Glossary: https://glossary.constraintsurfacedynamics.com/fubini-study-measure/
Plain-language, CSD-role and formal statements of the Fubini-Study measure, with
this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.
On upstreaming: this is a Category 1 file. Strip this Glossary block before any
Mathlib or Physlib PR; a personal project link has no place in a canonical header.
Strengthens the ContinuousConstSMul instance from Unitary.lean
(continuity in the projective argument for fixed unitary) to the
full ContinuousSMul (joint continuity in both arguments).
Argument #
Use the open-quotient-map structure of
Projectivization.mk' : V₀ → ℙ ℂ V (where V₀ := {v : V // v ≠ 0}):
id × mk' : G × V₀ → G × ℙ ℂ Vis an open quotient map (viaIsOpenQuotientMap.id.prodMap Projectivization.isOpenQuotientMap_mk').- A function out of
G × ℙ ℂ Vis continuous iff its precomposition withid × mk'is. - The precomposition
(U, ⟨v, hv⟩) ↦ U • mk' ⟨v, hv⟩ = mk' ⟨U.val.mulVec v, ...⟩is continuous, via joint continuity of matrix-vector multiplication (Continuous.matrix_mulVec),PiLp.continuous_toLp,continuous_mk', and subtype machinery.
Main results #
The file is named for its headline, fubiniStudyMeasure_unique, but it carries the
whole chain from joint continuity to base-point independence. (The title said only
Phase G1 until 2026-08-19, which understated it by two phases.)
- G1
Matrix.UnitaryGroup.instContinuousSMul_projectivization—ContinuousSMul (Matrix.unitaryGroup (Fin N) ℂ) (ℙ ℂ (EuclideanSpace ℂ (Fin N))). Joint continuity, hence joint measurability, which the Fubini swap in G4 needs. - ★★ G4
fubiniStudyMeasure_unique— anyU(N)-invariant probability measure onℂℙ^(N-1)ISfubiniStudyMeasure p₀. The uniqueness the whole programme leans on. - ★ G5
fubiniStudyMeasure_basepoint_independent/fubiniStudyMeasure_eq_default— the reference point is immaterial, sodefaultFubiniStudyMeasurenames the measure rather than one of a family. A corollary of G4.
What this unlocks #
Joint continuity gives joint measurability (Continuous.measurable),
which is the prerequisite for the Fubini swap in Phase G4
(fubiniStudyMeasure_unique).
Provenance #
Staged as upstream Mathlib material. Intended location:
Mathlib/LinearAlgebra/Projectivization/FubiniStudyUnique.lean.
Tags #
projectivization, continuous group action, joint continuity
Joint continuity of the unitary action on ℂℙ^(N-1).
The action (U, p) ↦ U • p is jointly continuous on
Matrix.unitaryGroup (Fin N) ℂ × ℙ ℂ (EuclideanSpace ℂ (Fin N)).
Phase G2 — right-invariance of unitaryHaarProb #
On a compact group, every Haar probability measure is both left- and
right-invariant. Mathlib gives left-invariance directly (via
IsHaarMeasure); we obtain right-invariance via Haar uniqueness:
the right-translate Measure.map (· * g) unitaryHaarProb is again a
Haar probability measure, hence equal to unitaryHaarProb.
unitaryHaarProb is right-invariant under group multiplication.
Proof: Measure.map (· * g) unitaryHaarProb is IsHaarMeasure (via
isHaarMeasure_map_mul_right, an instance) and IsProbabilityMeasure
(via Measure.isProbabilityMeasure_map', since (· * g) is measurable).
unitaryHaarProb itself is both. By Haar uniqueness on compact groups
(isHaarMeasure_eq_of_isProbabilityMeasure), the two measures coincide.
Phase G3 — Haar-orbit-indicator key lemma #
The Haar-measure mass of the set of unitaries mapping a fixed point
p into a target Borel set B is independent of p. By transitivity
(Phase F), any two base points are related by some unitary V;
by right-invariance of Haar (Phase G2), the right-translation by V
preserves the measure.
Phase G3. For any Borel set B ⊆ ℙ ℂ V and any two base points
p₀, p, the Haar mass of the set {U | U • p ∈ B} equals that of
{U | U • p₀ ∈ B}.
Proof: take V_p with V_p • p₀ = p (from IsPretransitive, which
auto-includes [NeZero N] from the section variable). Then
{U | U • p ∈ B} = (· * V_p) ⁻¹' {U | U • p₀ ∈ B} by smul_smul.
Right-invariance of Haar (Phase G2) discharges the measure equality.
Phase G4 — uniqueness of the U(N)-invariant probability measure #
Headline theorem: any U(N)-invariant probability measure on
ℂℙ^(N-1) equals fubiniStudyMeasure p₀ for any reference point p₀.
Proof via Fubini chain:
μ B = ∫⁻ U, μ B ∂λ -- λ is prob = ∫⁻ U, ∫⁻ p, B.indicator 1 (U • p) ∂μ ∂λ -- invariance of μ = ∫⁻ p, ∫⁻ U, B.indicator 1 (U • p) ∂λ ∂μ -- Fubini swap = ∫⁻ p, ν B ∂μ -- Phase G3 = ν B -- μ is prob
where λ = unitaryHaarProb, ν = fubiniStudyMeasure p₀.
Phase G4. Uniqueness of the U(N)-invariant probability measure
on ℂℙ^(N-1): any invariant probability measure μ equals
fubiniStudyMeasure p₀. ([NeZero N] is required by the implicit
transitivity-instance synthesis through haar_orbit_indicator_eq,
auto-included from the section variable.)
Phase G5 — invariant finite measures are scalar multiples of Fubini–Study #
fubiniStudyMeasure_unique pins every probability measure invariant under
the unitary action to fubiniStudyMeasure p₀. The two corollaries below
extend that to arbitrary finite invariant measures (normalising by the
total mass) and re-express the result in the ∃ c, μ = c • μFS shape that the
LF4 concrete measure bridges consume.
This is the invariant-measure-uniqueness fact for the ℂℙ^{N-1} / U(N)
instantiation: when LF4 instantiates SectorData with
P := ℙ ℂ (EuclideanSpace ℂ (Fin N)), G := Matrix.unitaryGroup (Fin N) ℂ,
and μFS := fubiniStudyMeasure p₀, the concrete bridges
(cp_measure_bridge / k_measure_bridge) route through
invariant_measure_uniqueness_cpn and cite no axiom. (Historically this was
the concrete realisation of an abstract CSD.LF2.invariant_measure_uniqueness
axiom — stated over an arbitrary pretransitive (P, G) with no topology; that
axiom and the abstract measure_bridge lemma it served were removed
2026-06-04, since nothing downstream used the abstract statement. The
concrete fact proved here is all that was ever load-bearing.)
Phase G5. Any finite measure on ℂℙ^{N-1} invariant under the unitary
action is a scalar multiple of the Fubini–Study measure at any reference
point. The scalar is the total mass μ Set.univ.
Proof: if the total mass is zero the measure is zero; otherwise normalise by
the total mass to obtain an invariant probability measure, pin it to
fubiniStudyMeasure p₀ via fubiniStudyMeasure_unique, and scale back.
Phase G5 — concrete realisation of CSD.LF2.invariant_measure_uniqueness.
For the ℂℙ^{N-1} / U(N) instantiation, any unitary-invariant probability
measure μFS and any unitary-invariant finite measure μ satisfy
∃ c, μ = c • μFS. This matches the LF2 spec axiom's conclusion shape (with
the reference point p₀ made explicit), and is proved — no axiom — from
fubiniStudyMeasure_unique plus invariant_finiteMeasure_eq_smul_fubiniStudy.
μFS is pinned to fubiniStudyMeasure p₀ by uniqueness; μ is a scalar
multiple of the same; composing gives μ = c • μFS.
Phase G5 — the base point is not a degree of freedom #
fubiniStudyMeasure is defined as a pushforward along the orbit map at a chosen p₀,
so on its face it is a family of measures. It is not: the choice is immaterial, and G4
says why in one step. Any U(N)-invariant probability measure equals
fubiniStudyMeasure p₀, and fubiniStudyMeasure p₁ is such a measure, so the two agree.
Recorded because it was a real defect rather than a missing convenience: the
FubiniStudy.lean module docstring advertised defaultPoint and
defaultFubiniStudyMeasure as the "canonical choice" while neither existed, and nothing
anywhere proved the base point could be dropped. Both are now supplied (2026-08-19).
⚠️ Deliberately not @[simp]. Rewriting every fubiniStudyMeasure p₀ in the corpus
to the default form would touch several hundred sites for no proof-level gain, and simp
lemmas that rename a widely-used term are how a build becomes unpredictable. Consumers
that want the canonical form should rewrite with it explicitly.
★ The Fubini–Study measure does not depend on its base point. Immediate from
Phase G4: fubiniStudyMeasure p₀ is a U(N)-invariant probability measure
(fubiniStudyMeasure_smul_invariant), and G4 says every such measure is
fubiniStudyMeasure p₁.
The Fubini–Study measure at any base point IS the canonical one. This is what makes
defaultFubiniStudyMeasure an honest name rather than one choice among many.
Atomlessness (Q28 item 1) #
Every singleton is μ_FS-null for 2 ≤ N, by pigeonhole: transitivity and
invariance make all singletons equal in measure, the projective space is
infinite, and a probability measure cannot give arbitrarily many disjoint
points a common positive mass. No stabiliser subgroup is consulted — the
"Haar-of-subgroup" route the corpus once assumed necessary
(LF4/KahlerInstance.lean) is bypassed entirely.
All singletons carry the same Fubini–Study mass: move one point onto the other by transitivity, and use invariance.
For 2 ≤ N the projective space is infinite: the rays [e₀ + t • e₁] for
t : ℕ are pairwise distinct.
★ The Fubini–Study measure is atomless (Q28 item 1): for 2 ≤ N every
singleton is null. Pigeonhole, with no stabiliser Haar measure anywhere: all
singletons share one mass a by transitivity + invariance; were a ≠ 0, a
finite set of more than 1/a distinct points — available since the space is
infinite — would carry measure exceeding 1.