The volume of ℂℙⁿ × T²: the top power of π₁^* ω_FS + π₂^* (dθ₁ ∧ dθ₂)

Category: 1-Mathlib (CSD-free).

On the product ℙ ℂ (Ambient n) × (AddCircle T × AddCircle T'), charted over (Fin n → ℂ) × (ℝ × ℝ), the sum of the Fubini–Study form and the torus area form (prodForm, ProductForm.lean) has an (n + 1)-st power whose coefficient on the product basis is (n + 1) times the Fubini–Study coefficient: the product basis is a weighted pair tuple for the flat sum, with weight -4 on the n sector pairs and 1 on the torus pair (WedgePowPairs.lean), and the model form at every chart point is a pullback of the model form at the origin (fsModelForm_eq_comp). The measure of the top power on a product chart domain then factorises through Tonelli into (n + 1) times the mass of the Fubini–Study volume (fsVolume_univ) times the area of the torus chart.

• prodTorusBasis n — the basis of the product model: the standard basis of Fin n → ℂ followed by the two coordinate vectors of ℝ × ℝ, re-indexed along powEquiv n;
• prodTorusWeight, isWeightedPairFamily_prodTorus, isWeightedPairTuple_prodTorusBasis, ★ wedgePow_prodSum_stdForm_areaForm_prodTorusBasis — the count on the product basis: (-4)ⁿ (n + 1)!;
• ★★ wedgePow_prodSum_fsModelForm_areaForm_prodTorusBasis — the coefficient everywhere on the chart: (-4)ⁿ (n + 1)! (1 + ‖w‖²)^{-(n+1)}, so (n + 1) times the Fubini–Study coefficient (wedgePow_fsModelForm_stdBasis);
• ★ chartDensity_prodTorus — the chart density of the product top form at a product chart point is (n + 1) times the Fubini–Study chart density of the sector coordinate;
• AddCircle.volume_singleton, AddCircle.volume_compl_singleton, volume_prod_chartAt_target — the Lebesgue area of a torus chart target is T · T';
• ★★ topFormMeasure_prodTorus_chartAt_source — the measure of the top power of the product form on a product chart domain is (n + 1) (4π)ⁿ · T T', for every chart cover; ★ topFormMeasure_prodTorus_ne_zero.

Honest scope

⚠️ One chart domain, not the whole product. The measure of the complement of a product chart domain is not shown null here; a consumer that has identified the measure with a product measure (as the source repository does by uniqueness of the invariant measures) reads the total mass off the chart value. The general statement, that the top-power measure of π₁^* α + π₂^* β is (m + 1) times the product of the factors' top-power measures, is not proved (ProductForm.lean, honest scope): the count here is for this pair of forms on this basis.

⚠️ The torus factor is AddCircle T × AddCircle T' charted by translation (TranslationAtlasForm.lean); nothing is said about the torus area form on its own (its top-form measure is not identified with Haar measure).

References: Geometry/Manifold/WedgePowPairs.lean; Geometry/Manifold/ProductForm.lean (localRep_prodFamily); Geometry/Manifold/TranslationAtlasForm.lean (areaForm, torusAreaForm, localRep_constFamily); Instances/ProjectiveSpaceFubiniStudyMass.lean (fsModelForm_eq_comp, fsVolume_univ_eq_lintegral, fsVolume_univ); Geometry/Manifold/TopFormMeasure.lean (topFormMeasure_apply_of_subset_source, chartMeasure_apply); Mathlib/MeasureTheory/Measure/Prod.lean (lintegral_prod_mul).

The basis of the product model

noncomputable def Projectivization.prodTorusBasis (n : ℕ) : Module.Basis (Fin (2 * (n + 1))) ℝ ((Fin n → ℂ) × ℝ × ℝ)

The real basis of the product model (Fin n → ℂ) × (ℝ × ℝ): the standard basis of the sector factor followed by the two coordinate vectors of the torus factor, indexed by Fin (2 * (n + 1)) along powEquiv n.

Equations

• Projectivization.prodTorusBasis n = ((Projectivization.stdBasis n).prod (Module.Basis.finTwoProd ℝ)).reindex (DifferentialForm.powEquiv n)

theorem Projectivization.prodTorusBasis_powEquiv {n : ℕ} (x : Fin (2 * n) ⊕ Fin 2) : (prodTorusBasis n) ((DifferentialForm.powEquiv n) x) = ((stdBasis n).prod (Module.Basis.finTwoProd ℝ)) x

The count on the product basis

def Projectivization.prodTorusWeight (n : ℕ) (j : Fin (n + 1)) : ℝ

The weights of the product basis for π₁^*(-4 ω_std) + π₂^* (dθ₁ ∧ dθ₂): -4 on the n sector pairs, 1 on the torus pair.

Equations

• Projectivization.prodTorusWeight n j = if j = Fin.last n then 1 else -4

theorem Projectivization.prod_prodTorusWeight (n : ℕ) : ∏ j : Fin (n + 1), prodTorusWeight n j = (-4) ^ n

theorem Projectivization.isWeightedPairFamily_prodTorus {n : ℕ} : ((-4 • stdForm n).prodSum TorusForm.areaForm).IsWeightedPairFamily (prodTorusWeight n) ⇑((stdBasis n).prod (Module.Basis.finTwoProd ℝ))

The product basis, as a family on Fin (2n) ⊕ Fin 2, is a weighted pair family for π₁^*(-4 ω_std) + π₂^* (dθ₁ ∧ dθ₂).

theorem Projectivization.isWeightedPairTuple_prodTorusBasis {n : ℕ} : ((-4 • stdForm n).prodSum TorusForm.areaForm).IsWeightedPairTuple (prodTorusWeight n) ⇑(prodTorusBasis n)

The product basis is a weighted pair tuple for π₁^*(-4 ω_std) + π₂^* (dθ₁ ∧ dθ₂).

theorem Projectivization.wedgePow_prodSum_stdForm_areaForm_prodTorusBasis {n : ℕ} : (((-4 • stdForm n).prodSum TorusForm.areaForm).wedgePow (n + 1)) ⇑(prodTorusBasis n) = (-4) ^ n * ↑(n + 1).factorial

★ The count on the product basis: the (n + 1)-st power of π₁^*(-4 ω_std) + π₂^* (dθ₁ ∧ dθ₂) on the product basis is (-4)ⁿ (n + 1)!.

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

★★ The coefficient of the top power of the product form on the product basis, everywhere on the chart: (-4)ⁿ (n + 1)! (1 + ‖w‖²)^{-(n+1)}, i.e. (n + 1) times the Fubini–Study coefficient wedgePow_fsModelForm_stdBasis. The model form at w is the pullback of the model form at the origin along L (fsModelForm_eq_comp), so the flat sum at w is the pullback of the flat sum at the origin along L × id, whose determinant is that of L.

The chart density of the product form

instance Projectivization.instIsAddHaarMeasure_torusModel : (MeasureTheory.volume.prod MeasureTheory.volume).IsAddHaarMeasure

Lebesgue measure on the torus model ℝ × ℝ, as an explicit product, is Haar (instance search does not see it through volume).

instance Projectivization.instIsAddHaarMeasure_prodTorusModel (n : ℕ) : (MeasureTheory.volume.prod (MeasureTheory.volume.prod MeasureTheory.volume)).IsAddHaarMeasure

Lebesgue measure on the product model (Fin n → ℂ) × (ℝ × ℝ), as an explicit product, is Haar.

theorem Projectivization.chartDensity_prodTorus {n : ℕ} {T T' : ℝ} [hT : Fact (0 < T)] [hT' : Fact (0 < T')] (x₀ : Projectivization ℂ (Ambient n)) (y₀ : AddCircle T × AddCircle T') (w₁ : Fin n → ℂ) {w₂ : ℝ × ℝ} (hw₂ : w₂ ∈ (chartAt (ℝ × ℝ) y₀).target) : DifferentialForm.chartDensity (prodTorusBasis n) (fun (p : Projectivization ℂ (Ambient n) × AddCircle T × AddCircle T') => ((fsForm.prodForm AddCircle.torusAreaForm).wedgePow (n + 1)) p) (x₀, y₀) (w₁, w₂) = ENNReal.ofReal (↑n + 1) * DifferentialForm.chartDensity (stdBasis n) (fun (x : Projectivization ℂ (Ambient n)) => (fsTopForm n) x) x₀ w₁

★ The chart density of the top power of the product form at a product chart point is (n + 1) times the Fubini–Study chart density of the sector coordinate: the torus factor's constant form has coefficient 1 in every translation chart.

The area of a torus chart

theorem AddCircle.volume_singleton {T : ℝ} [hT : Fact (0 < T)] (a : AddCircle T) : MeasureTheory.volume {a} = 0

A point of the circle is null.

theorem AddCircle.volume_compl_singleton {T : ℝ} [hT : Fact (0 < T)] (a : AddCircle T) : MeasureTheory.volume {a}ᶜ = ENNReal.ofReal T

The circle minus a point has full measure T.

theorem Projectivization.volume_prod_chartAt_target {T T' : ℝ} [hT : Fact (0 < T)] [hT' : Fact (0 < T')] (y₀ : AddCircle T × AddCircle T') : (MeasureTheory.volume.prod MeasureTheory.volume) (chartAt (ℝ × ℝ) y₀).target = ENNReal.ofReal T * ENNReal.ofReal T'

The Lebesgue area of the torus chart target (a, a + T) × (b, b + T') is T · T'.

The measure of a product chart domain

theorem Projectivization.topFormMeasure_prodTorus_chartAt_source {n : ℕ} {T T' : ℝ} [hT : Fact (0 < T)] [hT' : Fact (0 < T')] (c : ChartCover ((Fin n → ℂ) × ℝ × ℝ) (Projectivization ℂ (Ambient n) × AddCircle T × AddCircle T')) (y₀ : AddCircle T × AddCircle T') : (DifferentialForm.topFormMeasure (MeasureTheory.volume.prod (MeasureTheory.volume.prod MeasureTheory.volume)) (prodTorusBasis n) (fun (p : Projectivization ℂ (Ambient n) × AddCircle T × AddCircle T') => ((fsForm.prodForm AddCircle.torusAreaForm).wedgePow (n + 1)) p) c) (chartAt ((Fin n → ℂ) × ℝ × ℝ) (origin 0, y₀)).source = ENNReal.ofReal ((↑n + 1) * (4 * Real.pi) ^ n * (T * T'))

★★ The measure of the top power of the product form on a product chart domain is (n + 1) (4π)ⁿ · T T', for every chart cover: on the chart at (origin 0, y₀) the chart integral factorises through Tonelli into (n + 1) times the mass of the Fubini–Study volume (fsVolume_univ) times the area of the torus chart.

theorem Projectivization.topFormMeasure_prodTorus_ne_zero {n : ℕ} {T T' : ℝ} [hT : Fact (0 < T)] [hT' : Fact (0 < T')] (c : ChartCover ((Fin n → ℂ) × ℝ × ℝ) (Projectivization ℂ (Ambient n) × AddCircle T × AddCircle T')) : DifferentialForm.topFormMeasure (MeasureTheory.volume.prod (MeasureTheory.volume.prod MeasureTheory.volume)) (prodTorusBasis n) (fun (p : Projectivization ℂ (Ambient n) × AddCircle T × AddCircle T') => ((fsForm.prodForm AddCircle.torusAreaForm).wedgePow (n + 1)) p) c ≠ 0

★ The measure of the top power of the product form is nonzero.