Fubini–Study as a Lebesgue-absolutely-continuous pushforward

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

The Fubini–Study measure was built (FubiniStudy.lean) as a Haar pushforward from the unitary group, and characterised (FubiniStudyUnique.lean) as THE U(N)-invariant probability measure on ℂℙ^{N−1}. This file gives it a Lebesgue-absolutely-continuous source: the normalized Lebesgue measure on the punctured unit ball of ℂᴺ pushes forward through Projectivization.mk to a U(N)-invariant probability measure — hence, by uniqueness, to fubiniStudyMeasure p₀.

The payoff is a null-set transport principle: any ray set whose vector cone is Lebesgue-null is Fubini–Study-null (fubiniStudyMeasure_null_of_cone). Combined with the elementary slicing lemmas proved here (the zero set of the coordinate quadratic v a · v b = v c · v d is null — Fubini slicing, no polynomial theory), this is what turns "the entangled rays have positive measure" into "almost every ray is entangled" downstream (RecordLayer/EntangledMeasure.lean).

Main declarations

• pi_null_of_ae_slice_null — the Fubini slicing vehicle on Fin (n+1) → ℂ.
• pi_coord_zero_null, pi_quadratic_null — coordinate hyperplanes and the coordinate quadratic's zero set are Lebesgue-null. (A general polynomial_zeroSet_null would subsume these; it is deliberately NOT built — nothing in flight needs it. See specs/mathlib-gaps-plan.md.)
• volume_ofLp_preimage_null — null sets transport from the pi space to EuclideanSpace ℂ (two additive Haar measures agree up to a positive scalar; no exact normalisation chased).
• toEuclideanIsometry — a unitary matrix as a ℂ-linear isometry equiv of ℂᴺ (through Matrix.toEuclideanCLM), with the ℝ-restriction toEuclideanIsometryReal feeding LinearIsometryEquiv.measurePreserving.
• ballMeasure — the normalized Lebesgue measure on the punctured unit ball; projOfVec — the junk-totalised mk.
• map_ballMeasure_eq_fubiniStudy — ★ the pushforward identity, by uniqueness.
• fubiniStudyMeasure_null_of_cone — ★★ the null-transport principle.

Fubini slicing on the pi space

theorem Matrix.UnitaryGroup.pi_null_of_ae_slice_null {n : ℕ} (i : Fin (n + 1)) {S : Set (Fin (n + 1) → ℂ)} (hS : MeasurableSet S) (h : ∀ᵐ (y : Fin n → ℂ) ∂MeasureTheory.Measure.pi fun (x : Fin n) => MeasureTheory.volume, MeasureTheory.volume {z : ℂ | i.insertNth z y ∈ S} = 0) : (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => MeasureTheory.volume) S = 0

The slicing vehicle: a set of Fin (n+1) → ℂ is Lebesgue-null as soon as, for almost every value of the remaining coordinates, its slice in coordinate i is null in ℂ.

theorem Matrix.UnitaryGroup.pi_coord_zero_null {n : ℕ} (b : Fin (n + 1)) : (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => MeasureTheory.volume) {v : Fin (n + 1) → ℂ | v b = 0} = 0

Coordinate hyperplanes are Lebesgue-null.

theorem Matrix.UnitaryGroup.pi_quadratic_null {n : ℕ} {a b c d : Fin (n + 1)} (hb : b ≠ a) (hc : c ≠ a) (hd : d ≠ a) : (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => MeasureTheory.volume) {v : Fin (n + 1) → ℂ | v a * v b = v c * v d} = 0

The coordinate quadratic's zero set is Lebesgue-null: for indices b, c, d distinct from a, the set {v | v a · v b = v c · v d} is null. Fubini slicing: for almost every choice of the other coordinates the b-value is nonzero (coordinate hyperplanes are null), and then the a-slice is a single point.

theorem Matrix.UnitaryGroup.pi_quadratic_null' {M : ℕ} [NeZero M] {a b c d : Fin M} (hb : b ≠ a) (hc : c ≠ a) (hd : d ≠ a) : (MeasureTheory.Measure.pi fun (x : Fin M) => MeasureTheory.volume) {v : Fin M → ℂ | v a * v b = v c * v d} = 0

pi_quadratic_null at an arbitrary positive dimension (the form consumers apply, where the dimension is a product rather than a literal successor).

Null transport from the pi space to EuclideanSpace ℂ

noncomputable def Matrix.UnitaryGroup.euclideanCLE (N : ℕ) : EuclideanSpace ℂ (Fin N) ≃L[ℂ] Fin N → ℂ

The identity EuclideanSpace ℂ (Fin N) ≃L (Fin N → ℂ).

Equations

• Matrix.UnitaryGroup.euclideanCLE N = PiLp.continuousLinearEquiv 2 ℂ fun (x : Fin N) => ℂ

theorem Matrix.UnitaryGroup.isAddHaarMeasure_map_euclideanCLE {N : ℕ} : (MeasureTheory.Measure.map (⇑(euclideanCLE N)) MeasureTheory.volume).IsAddHaarMeasure

The pushforward of the canonical volume on EuclideanSpace ℂ (Fin N) through the identity to the pi space is an additive Haar measure.

theorem Matrix.UnitaryGroup.volume_ofLp_preimage_null {N : ℕ} {S : Set (Fin N → ℂ)} (hS : MeasurableSet S) (h : (MeasureTheory.Measure.pi fun (x : Fin N) => MeasureTheory.volume) S = 0) : MeasureTheory.volume (⇑(euclideanCLE N) ⁻¹' S) = 0

Null transport: a Lebesgue-null set of the pi space pulls back to a volume-null set of EuclideanSpace ℂ (Fin N). Two additive Haar measures on the pi space are mutually absolutely continuous, so their null sets coincide; no exact normalisation is needed.

The unitary group acts by volume-preserving isometries of ℂᴺ

theorem Matrix.UnitaryGroup.toEuclideanCLM_apply_eq {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (x : EuclideanSpace ℂ (Fin N)) : (toEuclideanCLM A) x = (toEuclideanLin A) x

The application-level bridge from Matrix.toEuclideanCLM to Matrix.toEuclideanLin (their coincidence is rfl in Mathlib's own module; only the coercion layer is unfolded here, so the unexposed internals never block it).

theorem Matrix.UnitaryGroup.toEuclideanLin_comp_apply {N : ℕ} (A B : Matrix (Fin N) (Fin N) ℂ) (x : EuclideanSpace ℂ (Fin N)) : (toEuclideanLin A) ((toEuclideanLin B) x) = (toEuclideanLin (A * B)) x

Composition of matrix actions is the action of the product — through map_mul of the star-algebra equivalence, dodging the cross-module defeq wall.

theorem Matrix.UnitaryGroup.toEuclideanLin_one_apply {N : ℕ} (x : EuclideanSpace ℂ (Fin N)) : (toEuclideanLin 1) x = x

The identity matrix acts as the identity.

noncomputable def Matrix.UnitaryGroup.toEuclideanIsometry {N : ℕ} (U : ↥(unitaryGroup (Fin N) ℂ)) : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)

A unitary matrix as a ℂ-linear isometry equiv of ℂᴺ: the inverse is the star, and a unitary operator preserves the inner product via the adjoint.

Equations

• Matrix.UnitaryGroup.toEuclideanIsometry U = (LinearEquiv.ofLinearMap (Matrix.toEuclideanLin ↑U) (Matrix.toEuclideanLin (star ↑U)) ⋯ ⋯).isometryOfInner ⋯

@[simp]

theorem Matrix.UnitaryGroup.toEuclideanIsometry_apply {N : ℕ} (U : ↥(unitaryGroup (Fin N) ℂ)) (v : EuclideanSpace ℂ (Fin N)) : (toEuclideanIsometry U) v = (toEuclideanLin ↑U) v

noncomputable def Matrix.UnitaryGroup.toEuclideanIsometryReal {N : ℕ} (U : ↥(unitaryGroup (Fin N) ℂ)) : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℝ] EuclideanSpace ℂ (Fin N)

The ℝ-restriction of the unitary isometry (feeding LinearIsometryEquiv.measurePreserving).

Equations

• Matrix.UnitaryGroup.toEuclideanIsometryReal U = { toLinearEquiv := LinearEquiv.restrictScalars ℝ (Matrix.UnitaryGroup.toEuclideanIsometry U).toLinearEquiv, norm_map' := ⋯ }

theorem Matrix.UnitaryGroup.measurePreserving_toEuclideanLin {N : ℕ} (U : ↥(unitaryGroup (Fin N) ℂ)) : MeasureTheory.MeasurePreserving (fun (v : EuclideanSpace ℂ (Fin N)) => (toEuclideanLin ↑U) v) MeasureTheory.volume MeasureTheory.volume

The unitary action on ℂᴺ preserves the canonical volume.

theorem Matrix.UnitaryGroup.toEuclideanLin_preimage_ball {N : ℕ} (U : ↥(unitaryGroup (Fin N) ℂ)) : (fun (v : EuclideanSpace ℂ (Fin N)) => (toEuclideanLin ↑U) v) ⁻¹' (Metric.ball 0 1 \ {0}) = Metric.ball 0 1 \ {0}

The unitary action preserves the punctured unit ball.

The normalized ball measure and its projective pushforward

def Matrix.UnitaryGroup.puncturedBall (N : ℕ) : Set (EuclideanSpace ℂ (Fin N))

The punctured unit ball of ℂᴺ.

Equations

• Matrix.UnitaryGroup.puncturedBall N = Metric.ball 0 1 \ {0}

theorem Matrix.UnitaryGroup.measurableSet_puncturedBall {N : ℕ} : MeasurableSet (puncturedBall N)

theorem Matrix.UnitaryGroup.volume_singleton_zero {N : ℕ} [NeZero N] : MeasureTheory.volume {0} = 0

The origin is volume-null (positive complex dimension) — routed through the pi space and the coordinate-hyperplane lemma, needing no atom-class instance on EuclideanSpace.

theorem Matrix.UnitaryGroup.volume_puncturedBall_pos {N : ℕ} [NeZero N] : 0 < MeasureTheory.volume (puncturedBall N)

theorem Matrix.UnitaryGroup.volume_puncturedBall_lt_top {N : ℕ} : MeasureTheory.volume (puncturedBall N) < ⊤

noncomputable def Matrix.UnitaryGroup.ballMeasure (N : ℕ) : MeasureTheory.Measure (EuclideanSpace ℂ (Fin N))

The normalized Lebesgue measure on the punctured unit ball of ℂᴺ: an absolutely continuous, U(N)-invariant probability measure on the nonzero vectors.

Equations

• Matrix.UnitaryGroup.ballMeasure N = (MeasureTheory.volume (Matrix.UnitaryGroup.puncturedBall N))⁻¹ • MeasureTheory.volume.restrict (Matrix.UnitaryGroup.puncturedBall N)

instance Matrix.UnitaryGroup.instIsProbabilityMeasureEuclideanSpaceComplexFinBallMeasure {N : ℕ} [NeZero N] : MeasureTheory.IsProbabilityMeasure (ballMeasure N)

theorem Matrix.UnitaryGroup.ballMeasure_absolutelyContinuous {N : ℕ} : (ballMeasure N).AbsolutelyContinuous MeasureTheory.volume

theorem Matrix.UnitaryGroup.map_toEuclideanLin_ballMeasure {N : ℕ} (U : ↥(unitaryGroup (Fin N) ℂ)) : MeasureTheory.Measure.map (fun (v : EuclideanSpace ℂ (Fin N)) => (toEuclideanLin ↑U) v) (ballMeasure N) = ballMeasure N

The unitary action preserves the ball measure.

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

The junk-totalised projectivization map: mk off zero, an arbitrary fixed ray at zero.

Equations

• Matrix.UnitaryGroup.projOfVec N v = if h : v = 0 then Projectivization.mk ℂ (EuclideanSpace.single 0 1) ⋯ else Projectivization.mk ℂ v h

theorem Matrix.UnitaryGroup.projOfVec_of_ne_zero {N : ℕ} [NeZero N] {v : EuclideanSpace ℂ (Fin N)} (hv : v ≠ 0) : projOfVec N v = Projectivization.mk ℂ v hv

theorem Matrix.UnitaryGroup.measurable_projOfVec {N : ℕ} [NeZero N] : Measurable (projOfVec N)

★ The pushforward identity and ★★ the null-transport principle

theorem Matrix.UnitaryGroup.map_ballMeasure_eq_fubiniStudy {N : ℕ} [NeZero N] (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : MeasureTheory.Measure.map (projOfVec N) (ballMeasure N) = fubiniStudyMeasure p₀

★ The Fubini–Study measure is the projectivization of normalized Lebesgue measure on the punctured unit ball — by invariance and the uniqueness theorem. This gives Fubini–Study an absolutely-continuous source.

theorem Matrix.UnitaryGroup.fubiniStudyMeasure_null_of_cone {N : ℕ} [NeZero N] (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) {S : Set (Projectivization ℂ (EuclideanSpace ℂ (Fin N)))} (hS : MeasurableSet S) (hcone : MeasureTheory.volume {v : EuclideanSpace ℂ (Fin N) | ∃ (h : v ≠ 0), Projectivization.mk ℂ v h ∈ S} = 0) : (fubiniStudyMeasure p₀) S = 0

★★ The null-transport principle: a ray set whose vector cone is Lebesgue-null is Fubini–Study-null. The cone is taken over the nonzero vectors.

★★ Rays inside a proper subspace are null

A companion to fubiniStudyMeasure_null_of_cone, and the reason a "microcanonical restriction to a spectral sector" cannot be defined by restricting μ_FS: the rays lying inside a proper subspace form a Fubini–Study-null set, because their cone is that subspace, and a proper subspace is Lebesgue-null (Measure.addHaar_submodule).

def Matrix.UnitaryGroup.subspaceRays {N : ℕ} (R : Submodule ℂ (EuclideanSpace ℂ (Fin N))) : Set (Projectivization ℂ (EuclideanSpace ℂ (Fin N)))

The rays lying inside a subspace.

Equations

• Matrix.UnitaryGroup.subspaceRays R = {p : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) | p.rep ∈ R}

theorem Matrix.UnitaryGroup.mem_subspaceRays_mk {N : ℕ} (R : Submodule ℂ (EuclideanSpace ℂ (Fin N))) {v : EuclideanSpace ℂ (Fin N)} (hv : v ≠ 0) : Projectivization.mk ℂ v hv ∈ subspaceRays R ↔ v ∈ R

Membership is representative-independent: a ray lies in R exactly when any (hence every) representative does.

theorem Matrix.UnitaryGroup.measurableSet_subspaceRays {N : ℕ} (R : Submodule ℂ (EuclideanSpace ℂ (Fin N))) : MeasurableSet (subspaceRays R)

theorem Matrix.UnitaryGroup.fubiniStudyMeasure_subspaceRays {N : ℕ} [NeZero N] (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) {R : Submodule ℂ (EuclideanSpace ℂ (Fin N))} (hR : R ≠ ⊤) : (fubiniStudyMeasure p₀) (subspaceRays R) = 0

★★ The rays of a proper subspace are Fubini–Study-null. Their cone is the subspace itself, and a proper subspace is Lebesgue-null. Consequence for statistical mechanics: a "microcanonical restriction to a spectral sector" is not definable by restricting μ_FS — the restriction is the zero measure.