Darboux's theorem by Moser's trick #

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #8 (Q31 = G18), the assembly.

A closed 2-form that is non-degenerate at a point is, near that point, the pullback of a constant form by a local diffeomorphism — Moser's proof. With ω₀ = ω(x₀), η = ω − ω₀ and the interpolation ω_t = ω₀ + tη:

η is closed and vanishes at x₀, so the Poincaré lemma (Analysis/Calculus/DifferentialForm/Poincare.lean) gives a C¹ primitive β with dβ = η, β(x₀) = 0, Dβ(x₀) = 0 — moserPrimitive;
non-degeneracy is open (isOpen_nondegenerate: it is invertibility of curryLeft, and ContinuousLinearEquiv.isOpen), so ω_t is non-degenerate near x₀ for |t| < 2 (exists_moser_radius), and Moser's field X_t = −(ω_t)^♭⁻¹ β, i.e. ι_{X_t} ω_t = −β (moserField, curryLeft_moserForm_moserField), is jointly C¹ (contDiffOn_moserFieldJoint, through contDiffAt_map_inverse) and vanishes to second order at x₀ (hasFDerivAt_moserField_self);
its flow up to time 1 exists on a small ball (Analysis/ODE/FlowDerivative.lean, exists_flow_hasFDerivAt_of_norm_fderiv_le, with ‖DX_t‖ ≤ ¼ there by a tube-lemma argument), and transports the interpolation: ∂ₜω_t + L_{X_t} ω_t = η + d(ι_{X_t} ω_t) + ι_{X_t} dω_t = η − dβ + 0 = 0 (the flat Cartan formula flatLieDeriv_eq_extDeriv_flatInteriorProduct_add), so form_invariant_of_flatLieDeriv_eq_zero_timeDependent gives φ_1^* ω = φ_0^* ω₀ = ω₀;
the time-1 map approximates the identity with constant ¼ e^{¼} < 1 (approximatesLinearOn_flow, Grönwall + the mean value inequality), so it is an OpenPartialHomeomorph by Mathlib's inverse function theorem (ApproximatesLinearOn.toOpenPartialHomeomorph); its derivative is invertible because the pullback of a non-degenerate form is non-degenerate.
★★ exists_openPartialHomeomorph_pullback_eq — Darboux on a ball: for ω of class C^n (1 ≤ n ≤ ∞) and closed on ball x₀ R with ω(x₀) non-degenerate, there is an open partial homeomorphism Φ of E with x₀ ∈ Φ.source ⊆ ball x₀ R, Φ x₀ = x₀, C^n on its source with C^n inverse on its target, differentiable at every point of its source with invertible derivative D, and ω(Φ x)(D u, D v) = ω(x₀)(u, v): Φ^* ω = ω(x₀). The C^n regularity is contDiffOn_flow_of_contDiffOn (Analysis/ODE/FlowSmooth.lean: C^n dependence of the flow of the jointly C^n Moser field on the initial point, contDiffOn_moserFieldJoint') and Mathlib's OpenPartialHomeomorph.contDiffAt_symm for the inverse;
★ exists_openPartialHomeomorph_symm_pullback_eq — the same read on the chart Φ.symm: ω y (u, v) = ω(x₀)(D(Φ⁻¹)(y) u, D(Φ⁻¹)(y) v) on Φ.target — in the chart Φ⁻¹, ω is the constant form ω(x₀);
mem_contDiffGroupoid_of_contDiffOn — an open partial homeomorphism of the model space that is C^n with C^n inverse belongs to the C^n groupoid; StructureGroupoid.trans_mem_maximalAtlas — a chart of the maximal atlas composed with a member of the groupoid stays in the maximal atlas;
★★ DifferentialForm.IsSymplectic.exists_openPartialHomeomorph_localRep_pullback_eq — Darboux on a symplectic manifold: at every point the local representative of the form in the chart is, after a further open partial homeomorphism Φ of the model space fixing the point, the constant form ω_loc(chart x₀); the Darboux chart Φ⁻¹ ∘ chartAt E x₀ contains x₀, is C^∞ with C^∞ inverse and belongs to the C^∞ maximal atlas of M. The standard form ∑ dpᵢ ∧ dqᵢ is Geometry/Manifold/DarbouxStandardForm.lean.

Honest scope #

Order n. For ω of class C^n (1 ≤ n ≤ ∞) the Poincaré primitive is C^n (Analysis/Calculus/ContDiffParametricIntervalIntegral.lean), Moser's field is jointly C^n (contDiffOn_moserFieldJoint'), its flow is C^n in the initial point (contDiffOn_flow_of_contDiffOn, Analysis/ODE/FlowSmooth.lean), and so the chart Φ is C^n with C^n inverse; on a symplectic manifold the Darboux chart is C^∞ and a member of the C^∞ maximal atlas.

The constant form here; the standard form downstream. Moser's trick produces the constant form ω(x₀); Geometry/Manifold/DarbouxStandardForm.lean composes the chart with the coordinates of a symplectic basis of ω(x₀) (LinearAlgebra/BilinearForm/SymplecticBasis.lean) and states the textbook form ω = Ψ^* (∑ dpᵢ ∧ dqᵢ) on ℝ^{2n}, with finrank E = 2n.

References: J. Moser, On the volume elements on a manifold, Trans. AMS 120 (1965); A. Weinstein, Symplectic manifolds and their Lagrangian submanifolds, Adv. Math. 6 (1971); D. McDuff, D. Salamon, Introduction to Symplectic Topology, Thm 3.2.2; Analysis/Calculus/DifferentialForm/Poincare.lean; Analysis/ODE/FlowDerivative.lean; Geometry/Manifold/HamiltonianLieDerivative.lean; specs/BACKLOG.md #8; specs/generator-layer-scoping.md §9 (G18) and Q31.

Darboux's theorem by Moser's trick #

Honest scope #

Non-degeneracy is open #

Moser's data #

The assembly #

Darboux's theorem on a ball #

Charts of the C^n maximal atlas #

Darboux on a symplectic manifold #

Charts of the `C^n` maximal atlas #