The mass of the Fubini–Study volume: ω_FS^{∧n} = (4π)ⁿ · μ_FS

TERM-SCOPE(Kahler) TERM-SCOPE(Liouville) — this module uses the restricted senses of "Kahler" and "Liouville"; the source repository's terms register records what is backed and what is not.

Category: 1-Mathlib (CSD-free).

The constant. ProjectiveSpaceFubiniStudyVolume.lean proved that the normalised volume of the top power of the Fubini–Study form is fsMeasure p₀; this module computes the total mass, so the identity holds with its constant. Three steps.

• The density everywhere on the chart. mulVecCLM A (a complex matrix acting on ℂⁿ as a real linear map) with ★ det_mulVecCLM — its real determinant is |det_ℂ A|² (LinearMap.det_restrictScalars, Algebra.norm_complex_apply); fsModelForm_apply (the model form written out from fsChartForm_apply); ★ fsModelForm_mulVec — a unitary matrix acting linearly on the chart pulls the model form at U w back to the model form at w; fsScale r, the diagonal scaling diag(t⁻¹, t^{-1/2}, …) with t = 1 + r², and ★ fsModelForm_single — at r e₀ the model form is the pullback of the model form at the origin along it; hence ★ fsModelForm_eq_comp — the model form at every w is the pullback of the model form at the origin along a real linear map of determinant (1 + ‖w‖²)^{-(n+1)} (rotate w to the first axis by exists_unitary_map_unit, where the form is diagonal), and with the Jacobian rule compContinuousLinearMap_apply_basis and the count at the origin, ★★ wedgePow_fsModelForm_stdBasis: the coefficient of the top power at every w is (-4)ⁿ n! (1 + ‖w‖²)^{-(n+1)}; measurable_chartDensity_fsTopForm_origin_zero.
• The mass is one chart integral. chartAt_origin_source, chartAt_origin_symm; fsVolume_chartSource_zero (on the domain of the chart at origin 0 the volume is the chart integral over all of ℂⁿ) and ★ fsVolume_compl_chartSource_zero (the hyperplane z₀ = 0 is null: in every other affine chart it is a coordinate hyperplane, Measure.addHaar_submodule); ★ fsVolume_univ_eq_lintegral.
• The constant. ★★ fsVolume_univ — fsVolume n univ = (4π)ⁿ, by lintegral_pi_pow_inv_one_add_sum_norm_sq (∫_{ℂⁿ} (1 + ‖w‖²)^{-(n+1)} = πⁿ/n!); and ★★★ fsVolume_eq_smul_fsMeasure — fsVolume n = (4π)ⁿ • fsMeasure p₀: the measure of the top power of the Fubini–Study form is the Fubini–Study measure, up to the explicit constant (4π)ⁿ; ★ fsMeasure_compl_chartSource_zero, ★ fsMeasure_chartSource_zero — the hyperplane z₀ = 0 is null for fsMeasure too, so the chart domain at origin 0 has full measure.

Honest scope

⚠️ The constant is convention-bound. fsChartForm carries the factor -4 of its potential log(1 + ‖z‖²) (fsChartForm_zero : fsChartForm 0 = -4 • fundamentalFormAlt), and the wedge ContinuousAlternatingMap.wedge has its own normalisation (Alternating/Wedge.lean); the (4π)ⁿ is the mass of this top power against Lebesgue measure on the model, and the literal ωⁿ/n! of the textbooks is fsVolume n / n! with the same measure — the identity below is the honest form of that sentence, with every factor visible.

⚠️ n = 0 is included: the manifold is a point, fsVolume 0 = δ, and (4π)⁰ = 1.

Provenance and references. The top-power plan (M7); Instances/ProjectiveSpaceFubiniStudyVolume.lean (fsVolumeNormalized_eq_fsMeasure, wedgePow_fsModelForm_zero_stdBasis); Analysis/SpecialFunctions/JapaneseBracketIntegral.lean; LinearAlgebra/Projectivization/UnitaryTransitive.lean (exists_unitary_map_unit); LinearAlgebra/Projectivization/TransitionProbability.lean (inner_toEuclideanLin_unitary); Geometry/Manifold/TopFormMeasure.lean (chartMeasure_apply, topFormMeasure_apply_of_subset_source); Mathlib/RingTheory/Norm/Transitivity.lean (LinearMap.det_restrictScalars); the terms register (Liouville); the completed-work ledger.

Real determinants of complex matrices

noncomputable def Projectivization.mulVecCLM {n : ℕ} (A : Matrix (Fin n) (Fin n) ℂ) : (Fin n → ℂ) →L[ℝ] Fin n → ℂ

A complex matrix acting on the pi model, as a real continuous linear map.

Equations

• Projectivization.mulVecCLM A = LinearMap.toContinuousLinearMap (↑ℝ (Matrix.toLin' A))

theorem Projectivization.mulVecCLM_apply {n : ℕ} (A : Matrix (Fin n) (Fin n) ℂ) (v : Fin n → ℂ) : (mulVecCLM A) v = A.mulVec v

theorem Projectivization.det_mulVecCLM {n : ℕ} (A : Matrix (Fin n) (Fin n) ℂ) : (mulVecCLM A).det = Complex.normSq A.det

★ The real determinant of a complex matrix acting on ℂⁿ is the square modulus of its complex determinant.

theorem Projectivization.mulVecCLM_mul {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℂ) : mulVecCLM (A * B) = mulVecCLM A ∘SL mulVecCLM B

Matrices compose under mulVecCLM.

theorem Projectivization.normSq_det_unitary {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin n) ℂ)) : Complex.normSq (↑U).det = 1

theorem Projectivization.toLpCLM_mulVec {n : ℕ} (A : Matrix (Fin n) (Fin n) ℂ) (w : Fin n → ℂ) : toLpCLM (A.mulVec w) = (Matrix.toEuclideanLin A) (toLpCLM w)

theorem Projectivization.toLpCLM_apply {n : ℕ} (x : Fin n → ℂ) (j : Fin n) : (toLpCLM x).ofLp j = x j

The model form, and its rotation invariance

theorem Projectivization.fsModelForm_apply {n : ℕ} (w u v : Fin n → ℂ) : (fsModelForm w) ![u, v] = -4 * ((1 + ‖toLpCLM w‖ ^ 2)⁻¹ * (inner ℂ (toLpCLM u) (toLpCLM v)).im - (1 + ‖toLpCLM w‖ ^ 2)⁻¹ ^ 2 * (inner ℂ (toLpCLM u) (toLpCLM w) * inner ℂ (toLpCLM w) (toLpCLM v)).im)

The model form written out: -4 (t⁻¹ Im⟪u,v⟫ - t⁻² Im(⟪u,w⟫⟪w,v⟫)) with t = 1 + ‖w‖².

theorem Projectivization.fsModelForm_mulVec {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin n) ℂ)) (w : Fin n → ℂ) : (fsModelForm ((↑U).mulVec w)).compContinuousLinearMap (mulVecCLM ↑U) = fsModelForm w

★ Rotation invariance of the model form: a unitary matrix acting linearly on the chart pulls the model form at U w back to the model form at w.

The form on the first axis is a diagonal pullback of the form at the origin

noncomputable def Projectivization.fsScaleEntry {n : ℕ} [NeZero n] (r : ℝ) (j : Fin n) : ℝ

The diagonal entries t⁻¹, t^{-1/2}, …, t^{-1/2}, t = 1 + r².

Equations

• Projectivization.fsScaleEntry r j = if j = 0 then (1 + r ^ 2)⁻¹ else √(1 + r ^ 2)⁻¹

noncomputable def Projectivization.fsScale {n : ℕ} [NeZero n] (r : ℝ) : Matrix (Fin n) (Fin n) ℂ

The diagonal scaling diag(t⁻¹, t^{-1/2}, …, t^{-1/2}).

Equations

• Projectivization.fsScale r = Matrix.diagonal fun (j : Fin n) => ↑(Projectivization.fsScaleEntry r j)

theorem Projectivization.fsScale_mulVec_apply {n : ℕ} [NeZero n] (r : ℝ) (u : Fin n → ℂ) (j : Fin n) : (fsScale r).mulVec u j = ↑(fsScaleEntry r j) * u j

theorem Projectivization.fsScaleEntry_mul_self {n : ℕ} [NeZero n] (r : ℝ) (j : Fin n) : fsScaleEntry r j * fsScaleEntry r j = (1 + r ^ 2)⁻¹ - (1 + r ^ 2)⁻¹ ^ 2 * r ^ 2 * if j = 0 then 1 else 0

theorem Projectivization.inner_fsScale {n : ℕ} [NeZero n] (r : ℝ) (u v : Fin n → ℂ) : inner ℂ (toLpCLM ((fsScale r).mulVec u)) (toLpCLM ((fsScale r).mulVec v)) = ↑(1 + r ^ 2)⁻¹ * inner ℂ (toLpCLM u) (toLpCLM v) - ↑((1 + r ^ 2)⁻¹ ^ 2 * r ^ 2) * inner ℂ (u 0) (v 0)

theorem Projectivization.fsModelForm_single {n : ℕ} [NeZero n] (r : ℝ) : fsModelForm (Pi.single 0 ↑r) = (fsModelForm 0).compContinuousLinearMap (mulVecCLM (fsScale r))

★ At r e₀ the model form is the pullback of the model form at the origin along the diagonal scaling.

theorem Projectivization.normSq_det_fsScale {n : ℕ} [NeZero n] (r : ℝ) : Complex.normSq (fsScale r).det = (1 + r ^ 2)⁻¹ ^ (n + 1)

The model form everywhere is a pullback of the model form at the origin

theorem Projectivization.fsModelForm_eq_comp {n : ℕ} (w : Fin n → ℂ) : ∃ (L : (Fin n → ℂ) →L[ℝ] Fin n → ℂ), fsModelForm w = (fsModelForm 0).compContinuousLinearMap L ∧ L.det = (1 + ‖toLpCLM w‖ ^ 2)⁻¹ ^ (n + 1)

★ The model form at w is the pullback of the model form at the origin along a real linear map of determinant (1 + ‖w‖²)^{-(n+1)}: rotate w to the first axis by a unitary matrix (fsModelForm_mulVec, exists_unitary_map_unit), where the form is the diagonal pullback fsModelForm_single; the map is mulVecCLM (fsScale ‖w‖ * U).

The density everywhere

theorem Projectivization.wedgePow_fsModelForm_stdBasis {n : ℕ} (w : Fin n → ℂ) : ((fsModelForm w).wedgePow n) ⇑(stdBasis n) = (-4) ^ n * ↑n.factorial * (1 + ‖toLpCLM w‖ ^ 2)⁻¹ ^ (n + 1)

★★ The density of the top power, everywhere on the chart: the coefficient of fsModelForm w ^ ∧n against the standard basis is (-4)ⁿ n! (1 + ‖w‖²)^{-(n+1)} (fsModelForm_eq_comp and the Jacobian rule compContinuousLinearMap_apply_basis).

theorem Projectivization.chartDensity_fsTopForm_origin_zero {n : ℕ} (w : Fin n → ℂ) : DifferentialForm.chartDensity (stdBasis n) (fun (x : Projectivization ℂ (Ambient n)) => (fsTopForm n) x) (origin 0) w = ENNReal.ofReal (4 ^ n * ↑n.factorial * (1 + ∑ j : Fin n, ‖w j‖ ^ 2)⁻¹ ^ (n + 1))

The chart density of the Fubini–Study volume, at origin 0, as a function of the coordinate sum ∑ⱼ ‖wⱼ‖².

theorem Projectivization.measurable_chartDensity_fsTopForm_origin_zero {n : ℕ} : Measurable (DifferentialForm.chartDensity (stdBasis n) (fun (x : Projectivization ℂ (Ambient n)) => (fsTopForm n) x) (origin 0))

The chart density at origin 0 is measurable.

The mass is one chart integral

theorem Projectivization.chartAt_origin_source {n : ℕ} (i : Fin (n + 1)) : (chartAt (Fin n → ℂ) (origin i)).source = chartSource i

theorem Projectivization.chartAt_origin_symm {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : ↑(chartAt (Fin n → ℂ) (origin i)).symm w = chartInv i w

theorem Projectivization.fsVolume_chartSource_zero {n : ℕ} : (fsVolume n) (chartSource 0) = ∫⁻ (w : Fin n → ℂ), DifferentialForm.chartDensity (stdBasis n) (fun (x : Projectivization ℂ (Ambient n)) => (fsTopForm n) x) (origin 0) w

On the domain of the chart at origin 0, the Fubini–Study volume is the chart integral over all of ℂⁿ.

theorem Projectivization.fsVolume_compl_chartSource_zero {n : ℕ} : (fsVolume n) (chartSource 0)ᶜ = 0

★ The complement of the chart domain at origin 0 — the hyperplane z₀ = 0 — is null: in every other affine chart it is a coordinate hyperplane of ℂⁿ, which has Lebesgue measure zero.

theorem Projectivization.fsVolume_univ_eq_lintegral {n : ℕ} : (fsVolume n) Set.univ = ∫⁻ (w : Fin n → ℂ), DifferentialForm.chartDensity (stdBasis n) (fun (x : Projectivization ℂ (Ambient n)) => (fsTopForm n) x) (origin 0) w

★ The mass of the Fubini–Study volume is the chart-0 integral of its density.

The constant

theorem Projectivization.fsVolume_univ {n : ℕ} : (fsVolume n) Set.univ = ENNReal.ofReal ((4 * Real.pi) ^ n)

★★ The mass of the Fubini–Study volume is (4π)ⁿ.

theorem Projectivization.fsVolume_eq_smul_fsMeasure {n : ℕ} (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin (n + 1)))) : fsVolume n = ENNReal.ofReal ((4 * Real.pi) ^ n) • Matrix.UnitaryGroup.fsMeasure p₀

★★★ The measure of the top power of the Fubini–Study form is (4π)ⁿ times the Fubini–Study measure, for every base point p₀: ω_FS^{∧n} = (4π)ⁿ · μ_FS, with every factor visible.

theorem Projectivization.fsMeasure_compl_chartSource_zero {n : ℕ} (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin (n + 1)))) : (Matrix.UnitaryGroup.fsMeasure p₀) (chartSource 0)ᶜ = 0

★ The hyperplane z₀ = 0 is null for the Fubini–Study measure too.

theorem Projectivization.fsMeasure_chartSource_zero {n : ℕ} (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin (n + 1)))) : (Matrix.UnitaryGroup.fsMeasure p₀) (chartSource 0) = 1

★ The domain of the affine chart at origin 0 has full Fubini–Study measure.