Darboux's theorem in the standard form ∑ dpᵢ ∧ dqᵢ

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #50, Darboux residue (b).

Glossary: https://glossary.constraintsurfacedynamics.com/darboux-theorem/ Plain-language, CSD-role and formal statements of Darboux's theorem, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

Geometry/Manifold/Darboux.lean produces, by Moser's trick, a C¹ chart in which a closed non-degenerate 2-form is the constant form ω(x₀). This file composes that chart with the linear change of coordinates given by a symplectic basis of ω(x₀) (LinearAlgebra/BilinearForm/SymplecticBasis.lean) and obtains the textbook statement: a C^n chart into ℝ^{2n} in which the form is the standard symplectic form ω_std = ∑ᵢ dpᵢ ∧ dqᵢ, i.e. ω = Ψ^* ω_std; in particular the dimension is 2n.

• ContinuousAlternatingMap.toBilinForm — the bilinear form (u, v) ↦ ξ ![u, v] of a 2-form; it is alternating (toBilinForm_isAlt) and non-degenerate when ξ is (toBilinForm_nondegenerate);
• standardSymplecticForm ι — the standard symplectic form on ι ⊕ ι → ℝ, ω_std(u, v) = ∑ᵢ (u_{pᵢ} v_{qᵢ} − u_{qᵢ} v_{pᵢ}) (inl = the p's, inr = the q's), as a continuous alternating 2-form (standardSymplecticForm_apply);
• ★ exists_continuousLinearEquiv_eq_standardSymplecticForm_comp — linear Darboux: a non-degenerate 2-form on a finite-dimensional real space is the pullback of ω_std on ℝ^{2n} by a linear isomorphism, and finrank E = 2n (the symplectic basis);
• ★★ exists_openPartialHomeomorph_pullback_standard — Darboux on a ball, standard form: for ω of class C^k (1 ≤ k ≤ ∞) and closed on ball x₀ R with ω(x₀) non-degenerate, there is n with finrank E = 2n and a C^k chart Ψ : E → ℝ^{2n} with C^k inverse, x₀ ∈ Ψ.source ⊆ ball x₀ R, differentiable at every point y of its source with invertible derivative D, and ω(y)(u, v) = ω_std(D u, D v): ω = Ψ^* ω_std;
• ★★ DifferentialForm.IsSymplectic.exists_openPartialHomeomorph_localRep_pullback_standard — Darboux on a symplectic manifold, standard form: at every point the local representative of the form is, in a further C^∞ chart Ψ of the model space into ℝ^{2n}, the pullback of ω_std; the Darboux chart is Ψ ∘ chartAt E x₀;
• ★ DifferentialForm.IsSymplectic.even_finrank — a symplectic manifold has even dimension.

Honest scope

Order k. The chart inherits the regularity of Darboux.lean: C^k for ω of class C^k (1 ≤ k ≤ ∞), C^∞ on a symplectic manifold. The linear change of coordinates is C^∞.

References: J. Moser, On the volume elements on a manifold, Trans. AMS 120 (1965); D. McDuff, D. Salamon, Introduction to Symplectic Topology, Thm 3.2.2 and Lemma 2.1.2 (the symplectic basis); Geometry/Manifold/Darboux.lean; LinearAlgebra/BilinearForm/SymplecticBasis.lean; specs/BACKLOG.md #50; specs/generator-layer-scoping.md Q31.

The bilinear form of a 2-form

theorem ContinuousAlternatingMap.apply_vecCons_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (ξ : E [⋀^Fin (n + 1)]→L[ℝ] ℝ) (m : Fin n → E) (x y : E) : ξ (Matrix.vecCons (x + y) m) = ξ (Matrix.vecCons x m) + ξ (Matrix.vecCons y m)

Additivity of a continuous alternating map in the head of a vecCons.

theorem ContinuousAlternatingMap.apply_vecCons_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (ξ : E [⋀^Fin (n + 1)]→L[ℝ] ℝ) (m : Fin n → E) (c : ℝ) (x : E) : ξ (Matrix.vecCons (c • x) m) = c • ξ (Matrix.vecCons x m)

Homogeneity of a continuous alternating map in the head of a vecCons.

def ContinuousAlternatingMap.toBilinForm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ξ : E [⋀^Fin 2]→L[ℝ] ℝ) : LinearMap.BilinForm ℝ E

The bilinear form (u, v) ↦ ξ ![u, v] of a continuous 2-form.

Equations

• ξ.toBilinForm = LinearMap.mk₂ ℝ (fun (u v : E) => ξ ![u, v]) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem ContinuousAlternatingMap.toBilinForm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ξ : E [⋀^Fin 2]→L[ℝ] ℝ) (u v : E) : (ξ.toBilinForm u) v = ξ ![u, v]

theorem ContinuousAlternatingMap.toBilinForm_isAlt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ξ : E [⋀^Fin 2]→L[ℝ] ℝ) : ξ.toBilinForm.IsAlt

The bilinear form of a 2-form is alternating.

theorem ContinuousAlternatingMap.toBilinForm_nondegenerate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ξ : E [⋀^Fin 2]→L[ℝ] ℝ) (hnd : ∀ (v : E), v ≠ 0 → ∃ (u : E), ξ ![v, u] ≠ 0) : ξ.toBilinForm.Nondegenerate

The bilinear form of a non-degenerate 2-form is non-degenerate.

The standard symplectic form on ℝ^{2n}

noncomputable def standardSymplecticBilin (ι : Type u_1) [Fintype ι] : (ι ⊕ ι → ℝ) →L[ℝ] (ι ⊕ ι → ℝ) →L[ℝ] ℝ

The standard symplectic form on ι ⊕ ι → ℝ as a bilinear map, (u, v) ↦ ∑ᵢ (u_{pᵢ} v_{qᵢ} − u_{qᵢ} v_{pᵢ}) with p = inl, q = inr.

Equations

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

theorem standardSymplecticBilin_apply (ι : Type u_1) [Fintype ι] (u v : ι ⊕ ι → ℝ) : ((standardSymplecticBilin ι) u) v = ∑ i : ι, (u (Sum.inl i) * v (Sum.inr i) - u (Sum.inr i) * v (Sum.inl i))

theorem standardSymplecticBilin_self (ι : Type u_1) [Fintype ι] (u : ι ⊕ ι → ℝ) : ((standardSymplecticBilin ι) u) u = 0

noncomputable def standardSymplecticMulti (ι : Type u_1) [Fintype ι] : (ι ⊕ ι → ℝ) [×2]→L[ℝ] ℝ

The standard symplectic form as a continuous multilinear map on Fin 2 → (ι ⊕ ι → ℝ).

Equations

• standardSymplecticMulti ι = ((continuousMultilinearCurryFin1 ℝ (ι ⊕ ι → ℝ) ℝ).symm.toLinearIsometry.toContinuousLinearMap ∘SL standardSymplecticBilin ι).uncurryLeft

@[simp]

theorem standardSymplecticMulti_apply (ι : Type u_1) [Fintype ι] (v : Fin 2 → ι ⊕ ι → ℝ) : (standardSymplecticMulti ι) v = ((standardSymplecticBilin ι) (v 0)) (v 1)

noncomputable def standardSymplecticForm (ι : Type u_1) [Fintype ι] : (ι ⊕ ι → ℝ) [⋀^Fin 2]→L[ℝ] ℝ

The standard symplectic form ω_std = ∑ᵢ dpᵢ ∧ dqᵢ on ι ⊕ ι → ℝ, as a continuous alternating 2-form: ω_std(u, v) = ∑ᵢ (u_{pᵢ} v_{qᵢ} − u_{qᵢ} v_{pᵢ}).

Equations

• standardSymplecticForm ι = { toContinuousMultilinearMap := standardSymplecticMulti ι, map_eq_zero_of_eq' := ⋯ }

@[simp]

theorem standardSymplecticForm_apply (ι : Type u_1) [Fintype ι] (v : Fin 2 → ι ⊕ ι → ℝ) : (standardSymplecticForm ι) v = ∑ i : ι, (v 0 (Sum.inl i) * v 1 (Sum.inr i) - v 0 (Sum.inr i) * v 1 (Sum.inl i))

Linear Darboux

theorem exists_continuousLinearEquiv_eq_standardSymplecticForm_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (ξ : E [⋀^Fin 2]→L[ℝ] ℝ) (hnd : ∀ (v : E), v ≠ 0 → ∃ (u : E), ξ ![v, u] ≠ 0) : ∃ (n : ℕ) (L : E ≃L[ℝ] Fin n ⊕ Fin n → ℝ), Module.finrank ℝ E = 2 * n ∧ ξ = (standardSymplecticForm (Fin n)).compContinuousLinearMap ↑L

★ Linear Darboux. A non-degenerate 2-form on a finite-dimensional real space is the pullback of the standard symplectic form on ℝ^{2n} by a linear isomorphism L, and finrank E = 2n: the coordinates of a symplectic basis of ξ.

Darboux on a ball, standard form

theorem exists_openPartialHomeomorph_pullback_standard {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {x₀ : E} {R : ℝ} {k : ℕ∞} (hk : 1 ≤ k) (hω : ContDiffOn ℝ (↑k) ω (Metric.ball x₀ R)) (hR : 0 < R) (hclosed : ∀ y ∈ Metric.ball x₀ R, extDeriv ω y = 0) (hnd : ∀ (v : E), v ≠ 0 → ∃ (u : E), (ω x₀) ![v, u] ≠ 0) : ∃ (n : ℕ) (Ψ : OpenPartialHomeomorph E (Fin n ⊕ Fin n → ℝ)), Module.finrank ℝ E = 2 * n ∧ Ψ.source ⊆ Metric.ball x₀ R ∧ x₀ ∈ Ψ.source ∧ ContDiffOn ℝ (↑k) (↑Ψ) Ψ.source ∧ ContDiffOn ℝ (↑k) (↑Ψ.symm) Ψ.target ∧ ∀ y ∈ Ψ.source, ∃ (D : E ≃L[ℝ] Fin n ⊕ Fin n → ℝ), HasFDerivAt (↑Ψ) (↑D) y ∧ ω y = (standardSymplecticForm (Fin n)).compContinuousLinearMap ↑D

★★ Darboux's theorem on a ball, standard form. If ω is C^k (1 ≤ k ≤ ∞) and closed on ball x₀ R and ω(x₀) is non-degenerate, then finrank E = 2n for some n and there is a C^k chart Ψ : E → ℝ^{2n} with C^k inverse, x₀ ∈ Ψ.source ⊆ ball x₀ R, differentiable at every point y of its source with an invertible derivative D, such that ω(y)(u, v) = ω_std(D u, D v): ω = Ψ^* ω_std with ω_std = ∑ᵢ dpᵢ ∧ dqᵢ.

Darboux on a symplectic manifold, standard form

theorem DifferentialForm.IsSymplectic.exists_openPartialHomeomorph_localRep_pullback_standard {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) (Fin 2) ℝ} (hα : α.IsSymplectic) (x₀ : M) : ∃ (n : ℕ) (Ψ : OpenPartialHomeomorph E (Fin n ⊕ Fin n → ℝ)), Module.finrank ℝ E = 2 * n ∧ Ψ.source ⊆ (chartAt E x₀).target ∧ ↑(chartAt E x₀) x₀ ∈ Ψ.source ∧ ContDiffOn ℝ (↑⊤) (↑Ψ) Ψ.source ∧ ContDiffOn ℝ (↑⊤) (↑Ψ.symm) Ψ.target ∧ ∀ w ∈ Ψ.source, ∃ (D : E ≃L[ℝ] Fin n ⊕ Fin n → ℝ), HasFDerivAt (↑Ψ) (↑D) w ∧ localRep (fun (x : M) => α x) x₀ w = (standardSymplecticForm (Fin n)).compContinuousLinearMap ↑D

★★ Darboux's theorem on a symplectic manifold, standard form. At every point x₀, finrank E = 2n and there is a C^∞ chart Ψ of the model space into ℝ^{2n} with C^∞ inverse, containing chartAt E x₀ x₀ and contained in the chart's target, along which the local representative of the form is the pullback of the standard symplectic form ω_std = ∑ᵢ dpᵢ ∧ dqᵢ: the Darboux chart is Ψ ∘ chartAt E x₀.

theorem DifferentialForm.IsSymplectic.even_finrank {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) (Fin 2) ℝ} (hα : α.IsSymplectic) (x₀ : M) : Even (Module.finrank ℝ E)

★ A symplectic manifold has even dimension.