LF4 general-N Part 1: gaussianCPN = fubiniStudyMeasure on ℂℙ^{N-1}

Category: 3-Local (gaussianCPN = fubiniStudyMeasure on ℂℙ^{N-1}).

The general-N analogue of GaussianCP.lean (which handled the qubit N = 2): the Fubini–Study measure on ℂℙ^{N-1} is the projectivised standard Gaussian on ℂ^N. This is Slice B of the general-N Duistermaat–Heckman programme (specs/general-n-dh-plan.md), the cleanest standalone increment, and unblocks the Gaussian-route block law (Part 2a) and the Gamma→Dirichlet crux (Part 2b).

To keep stdGaussian on a clean real EuclideanSpace (avoiding the ℝ/ℂ typeclass diamond on EuclideanSpace ℂ (Fin N)), we transport through a hand-built real coordinate isometry coordsN : ℝ^{N×2} ≃ₗᵢ[ℝ] ℂ^N, y ↦ (i ↦ y(i,0) + y(i,1)·I). The real space is indexed by Fin N × Fin 2 (rather than Fin (2N)) so each complex coordinate i reads its real/imaginary parts off the clean pair (i,0), (i,1) — no 2i/2i+1 index arithmetic.

The discharged qubit file GaussianCP.lean is left untouched: its Fin 4-indexed machinery (coords, regroup4, …) is load-bearing for the retired fs_moment_pushforward_uniform axiom, so this is a parallel general-N development rather than a refactor.

C1 — the real coordinate isometry ℝ^{N×2} ≃ₗᵢ[ℝ] ℂ^N

noncomputable def CSD.LF4.coordsN {N : ℕ} : EuclideanSpace ℝ (Fin N × Fin 2) ≃ₗᵢ[ℝ] EuclideanSpace ℂ (Fin N)

C1 (general N). The real coordinate isometry ℝ^{N×2} ≃ₗᵢ[ℝ] ℂ^N, y ↦ (i ↦ y(i,0) + y(i,1)·I).

Equations

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

C2/C3 — the projectivised Gaussian

noncomputable def CSD.LF4.gaussianHN {N : ℕ} : MeasureTheory.Measure (EuclideanSpace ℂ (Fin N))

C2 (general N). The standard Gaussian transported to ℂ^N.

Equations

• CSD.LF4.gaussianHN = MeasureTheory.Measure.map (⇑CSD.LF4.coordsN) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin N × Fin 2)))

instance CSD.LF4.instProbGaussianHN {N : ℕ} : MeasureTheory.IsProbabilityMeasure gaussianHN

noncomputable def CSD.LF4.gaussianProjN {N : ℕ} (p₀ : CPN N) (v : EuclideanSpace ℂ (Fin N)) : CPN N

The projectivisation map ℂ^N → ℂℙ^{N-1}, junk value p₀ at 0.

Equations

• CSD.LF4.gaussianProjN p₀ v = if h : v = 0 then p₀ else Projectivization.mk ℂ v h

theorem CSD.LF4.measurable_gaussianProjN {N : ℕ} (p₀ : CPN N) : Measurable (gaussianProjN p₀)

noncomputable def CSD.LF4.gaussianCPN {N : ℕ} (p₀ : CPN N) : MeasureTheory.Measure (CPN N)

C3 (general N). The projectivised Gaussian on ℂℙ^{N-1}.

Equations

• CSD.LF4.gaussianCPN p₀ = MeasureTheory.Measure.map (CSD.LF4.gaussianProjN p₀) CSD.LF4.gaussianHN

instance CSD.LF4.instProbGaussianCPN {N : ℕ} (p₀ : CPN N) : MeasureTheory.IsProbabilityMeasure (gaussianCPN p₀)

C4 — U(N)-invariance

theorem CSD.LF4.measurable_toEuclideanLinN {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : Measurable ⇑(Matrix.toEuclideanLin ↑U)

The ℂ-linear matrix action toEuclideanLin U.val is measurable.

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

A unitary's toEuclideanLin action sends nonzero vectors to nonzero vectors.

theorem CSD.LF4.unitary_conjTranspose_mulN {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : (↑U).conjTranspose * ↑U = 1

Uᴴ * U = 1 for a unitary matrix.

theorem CSD.LF4.unitary_mul_conjTransposeN {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : ↑U * (↑U).conjTranspose = 1

U * Uᴴ = 1 for a unitary matrix.

theorem CSD.LF4.toEuclideanLinN_real_smul {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (c : ℝ) (w : EuclideanSpace ℂ (Fin N)) : (Matrix.toEuclideanLin ↑U) (c • w) = c • (Matrix.toEuclideanLin ↑U) w

toEuclideanLin U.val is ℝ-linear for the scalar action.

noncomputable def CSD.LF4.conjRN {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : EuclideanSpace ℝ (Fin N × Fin 2) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin N × Fin 2)

The real conjugate isometry conjRN U : ℝ^{N×2} ≃ₗᵢ[ℝ] ℝ^{N×2}, conjugating the unitary action on ℂ^N through coordsN.

Equations

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

theorem CSD.LF4.coordsN_conjRN {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (y : EuclideanSpace ℝ (Fin N × Fin 2)) : coordsN ((conjRN U) y) = (Matrix.toEuclideanLin ↑U) (coordsN y)

coordsN ∘ conjRN U = toEuclideanLin U.val ∘ coordsN.

theorem CSD.LF4.gaussianHN_map_unitary {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : MeasureTheory.Measure.map (⇑(Matrix.toEuclideanLin ↑U)) gaussianHN = gaussianHN

gaussianHN is invariant under the unitary matrix action on ℂ^N.

No-atoms at the origin

theorem CSD.LF4.stdGaussianN_ne_dirac {N : ℕ} [NeZero N] (x : EuclideanSpace ℝ (Fin N × Fin 2)) : ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin N × Fin 2)) ≠ MeasureTheory.Measure.dirac x

stdGaussian (ℝ^{N×2}) is not a Dirac measure (needs the space nonempty, i.e. N ≥ 1).

instance CSD.LF4.instNoAtomsStdGaussianN {N : ℕ} [NeZero N] : MeasureTheory.NullSingletonClass (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin N × Fin 2)))

theorem CSD.LF4.gaussianHN_singleton_zero {N : ℕ} [NeZero N] : gaussianHN {0} = 0

The origin is gaussianHN-null.

C4 (invariance) and C5 (identification)

theorem CSD.LF4.gaussianCPN_smul_invariant {N : ℕ} [NeZero N] (p₀ : CPN N) (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : MeasureTheory.Measure.map (fun (p : CPN N) => U • p) (gaussianCPN p₀) = gaussianCPN p₀

C4 (general N). gaussianCPN p₀ is U(N)-invariant.

theorem CSD.LF4.gaussianCPN_eq_fubiniStudy {N : ℕ} [NeZero N] (p₀ : CPN N) : gaussianCPN p₀ = Matrix.UnitaryGroup.fubiniStudyMeasure p₀

C5 (general N): the projectivised Gaussian equals the Fubini–Study measure on ℂℙ^{N-1}. The general-N analogue of gaussianCP_eq_fubiniStudy.