LF4 plan B, Part 1 (Option 2): gaussianCP = fsMeasure via ℝ⁴

Category: 3-Local (gaussianCP = fsMeasure via ℝ⁴).

Identifies the Fubini–Study measure on ℂℙ¹ with the projectivized standard Gaussian, working through a hand-built real coordinate isometry coords : ℝ⁴ ≃ₗᵢ[ℝ] ℂ² to keep stdGaussian on the clean real space (avoiding the ℝ/ℂ typeclass diamond on EuclideanSpace ℂ (Fin 2)). See specs/plan-b-detail.md Part 1 (Option 2).

noncomputable def CSD.LF4.coords : EuclideanSpace ℝ (Fin 4) ≃ₗᵢ[ℝ] EuclideanSpace ℂ (Fin 2)

C1. The real coordinate isometry ℝ⁴ ≃ₗᵢ[ℝ] ℂ²: y ↦ (y₀ + y₁·i, y₂ + y₃·i).

Equations

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

noncomputable def CSD.LF4.gaussianH : MeasureTheory.Measure (EuclideanSpace ℂ (Fin 2))

C2. The standard Gaussian transported to ℂ² via the coordinate isometry. A probability measure on ℂ² (kept off the diamond-prone direct stdGaussian (EuclideanSpace ℂ (Fin 2))).

Equations

• CSD.LF4.gaussianH = MeasureTheory.Measure.map (⇑CSD.LF4.coords) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin 4)))

instance CSD.LF4.instProbGaussianH : MeasureTheory.IsProbabilityMeasure gaussianH

noncomputable def CSD.LF4.gaussianProj (p₀ : CPN 2) (v : EuclideanSpace ℂ (Fin 2)) : CPN 2

The projectivization map ℂ² → ℂℙ¹, with junk value p₀ at 0 (which is gaussianH-null).

Equations

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

theorem CSD.LF4.measurable_gaussianProj (p₀ : CPN 2) : Measurable (gaussianProj p₀)

noncomputable def CSD.LF4.gaussianCP (p₀ : CPN 2) : MeasureTheory.Measure (CPN 2)

C3. The projectivized Gaussian on ℂℙ¹.

Equations

• CSD.LF4.gaussianCP p₀ = MeasureTheory.Measure.map (CSD.LF4.gaussianProj p₀) CSD.LF4.gaussianH

instance CSD.LF4.instProbGaussianCP (p₀ : CPN 2) : MeasureTheory.IsProbabilityMeasure (gaussianCP p₀)

C4 — U(2)-invariance of gaussianCP

theorem CSD.LF4.measurable_toEuclideanLin (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) : Measurable ⇑(Matrix.toEuclideanLin ↑U)

The ℂ-linear matrix action toEuclideanLin U.val is measurable (continuous on a finite-dimensional space).

theorem CSD.LF4.unitary_conjTranspose_mul (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) : (↑U).conjTranspose * ↑U = 1

Uᴴ * U = 1 for a unitary matrix.

theorem CSD.LF4.unitary_mul_conjTranspose (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) : ↑U * (↑U).conjTranspose = 1

U * Uᴴ = 1 for a unitary matrix.

theorem CSD.LF4.toEuclideanLin_real_smul (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) (c : ℝ) (w : EuclideanSpace ℂ (Fin 2)) : (Matrix.toEuclideanLin ↑U) (c • w) = c • (Matrix.toEuclideanLin ↑U) w

toEuclideanLin U.val is ℝ-linear for the scalar action (it is ℂ-linear, and the ℝ-action commutes with mulVec componentwise).

noncomputable def CSD.LF4.conjR (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) : EuclideanSpace ℝ (Fin 4) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4)

The real conjugate isometry conjR U : ℝ⁴ ≃ₗᵢ[ℝ] ℝ⁴, conjugating the unitary action toEuclideanLin U.val on ℂ² through the coordinate isometry coords. Built by hand on ℝ⁴ (the restrictScalars ℝ route diamonds in the full LF4 import context — see specs/plan-b-detail.md).

Equations

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

theorem CSD.LF4.coords_conjR (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) (y : EuclideanSpace ℝ (Fin 4)) : coords ((conjR U) y) = (Matrix.toEuclideanLin ↑U) (coords y)

coords ∘ conjR U = toEuclideanLin U.val ∘ coords pointwise.

theorem CSD.LF4.gaussianH_map_unitary (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) : MeasureTheory.Measure.map (⇑(Matrix.toEuclideanLin ↑U)) gaussianH = gaussianH

gaussianH is invariant under the unitary matrix action on ℂ².

theorem CSD.LF4.stdGaussian_ne_dirac (x : EuclideanSpace ℝ (Fin 4)) : ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin 4)) ≠ MeasureTheory.Measure.dirac x

stdGaussian (EuclideanSpace ℝ (Fin 4)) is not a Dirac measure: it has a dual direction (innerSL against a unit coordinate vector) with variance 1 ≠ 0.

instance CSD.LF4.instNoAtomsStdGaussian4 : MeasureTheory.NullSingletonClass (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin 4)))

theorem CSD.LF4.gaussianH_singleton_zero : gaussianH {0} = 0

The origin is gaussianH-null (the junk value of gaussianProj at 0 is therefore irrelevant a.e.).

C4 (invariance) and C5 (identification)

theorem CSD.LF4.gaussianCP_smul_invariant (p₀ : CPN 2) (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) : MeasureTheory.Measure.map (fun (p : CPN 2) => U • p) (gaussianCP p₀) = gaussianCP p₀

C4. gaussianCP p₀ is U(2)-invariant.

theorem CSD.LF4.gaussianCP_eq_fubiniStudy (p₀ : CPN 2) : gaussianCP p₀ = Matrix.UnitaryGroup.fsMeasure p₀

C5. The projectivized Gaussian equals the Fubini–Study measure.