noncomputable def stdSymplForm (n : ℕ) : LinearMap.BilinForm ℝ ((Fin n → ℝ) × (Fin n → ℝ))

The standard symplectic form on $\mathbb{R}^{2n} = \mathbb{R}^n \times \mathbb{R}^n$: $\omega_0((p_1, q_1), (p_2, q_2)) = \sum_i (p_{1,i} q_{2,i} - p_{2,i} q_{1,i})$.

theorem stdSymplForm_apply (n : ℕ) (u v : (Fin n → ℝ) × (Fin n → ℝ)) : ((stdSymplForm n) u) v = ∑ i : Fin n, (u.1 i * v.2 i - v.1 i * u.2 i)

Unfolds the standard symplectic form to its explicit sum formula.

theorem stdSymplForm_alt (n : ℕ) : (stdSymplForm n).IsAlt

The standard symplectic form is alternating: $\omega_0(v, v) = 0$ for all $v$.

theorem stdSymplForm_separatingLeft (n : ℕ) : LinearMap.SeparatingLeft (stdSymplForm n)

The standard symplectic form is nondegenerate (separating in its left argument): if $\omega_0(x, \cdot) = 0$ then $x = 0$.

theorem bilinForm_basis_expand {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ι : Type u_2} [Fintype ι] (Ω : LinearMap.BilinForm ℝ V) (B : Module.Basis ι ℝ V) (u v : V) : (Ω u) v = ∑ i : ι, ∑ j : ι, (B.repr u) i * (B.repr v) j * (Ω (B i)) (B j)

Expansion of a bilinear form in a basis $B$: $\Omega(u, v) = \sum_{i,j} u_i v_j \Omega(b_i, b_j)$, where $u_i, v_j$ are the coordinates of $u, v$ in the basis.

theorem linear_darboux {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {Ω : LinearMap.BilinForm ℝ V} (hΩ : SymplecticLinearAlgebra.IsSymplecticForm Ω) : ∃ (n : ℕ) (φ : V ≃ₗ[ℝ] (Fin n → ℝ) × (Fin n → ℝ)), ∀ (u v : V), (Ω u) v = ((stdSymplForm n) (φ u)) (φ v)

Linear Darboux theorem. Every symplectic vector space $(V, \Omega)$ admits a linear isomorphism $\varphi : V \cong \mathbb{R}^{2n}$ pulling back the standard symplectic form: $\Omega(u, v) = \omega_0(\varphi u, \varphi v)$.

def IsDeformationEquivalent {Ω : ℕ → Type u_1} {VF : Type u_2} [DifferentialFormSpace Ω VF] [TopologicalSpace (Ω 2)] (ω₀ ω₁ : Ω 2) : Prop

Two symplectic forms $\omega_0, \omega_1$ are deformation equivalent if there is a continuous family $\omega_t$ of symplectic $2$-forms connecting them (closed and nondegenerate for $t \in [0, 1]$).

def IsIsotopic {Ω : ℕ → Type u_1} {VF : Type u_2} [DifferentialFormSpace Ω VF] [TopologicalSpace (Ω 2)] (ω₀ ω₁ : Ω 2) : Prop

Two symplectic forms $\omega_0, \omega_1$ are isotopic if they are connected by a continuous family $\omega_t$ of symplectic forms whose cohomology class is constant: $[\omega_t - \omega_0] = 0$ in $H^2$, i.e., $\omega_t - \omega_0 = d\alpha$ for some $\alpha$.

theorem IsIsotopic.toIsDeformationEquivalent {Ω : ℕ → Type u_1} {VF : Type u_2} [DifferentialFormSpace Ω VF] [TopologicalSpace (Ω 2)] {ω₀ ω₁ : Ω 2} (h : IsIsotopic ω₀ ω₁) : IsDeformationEquivalent ω₀ ω₁

Isotopy implies deformation equivalence: forgetting the cohomological condition.

structure MoserSetup {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] : Type (max u_1 u_2)

Setup data for Moser's trick: a smooth path of closed $2$-forms $\omega_t$ with time derivative $\dot\omega_t$, primitives $\alpha_t$ satisfying $d\alpha_t = \dot\omega_t$, and the canonically-induced vector fields $X_t$ solving $\iota_{X_t} \omega_t = -\alpha_t$.

• ω_t : ℝ → Ω 2
• closed_t (t : ℝ) : t ∈ Set.Icc 0 1 → DifferentialFormSpace.d VF (self.ω_t t) = 0
• α_t : ℝ → Ω 1
• dω_dt : ℝ → Ω 2
• derivative_consistency (t s : ℝ) : t ∈ Set.Icc 0 1 → s ∈ Set.Icc 0 1 → self.ω_t s - self.ω_t t = (s - t) • self.dω_dt t
• defining_eq (t : ℝ) : t ∈ Set.Icc 0 1 → DifferentialFormSpace.d VF (self.α_t t) = self.dω_dt t
• X_t : ℝ → VF
• X_t_eq (t : ℝ) : t ∈ Set.Icc 0 1 → DifferentialFormSpace.ι (self.X_t t) (self.ω_t t) = -self.α_t t

theorem moser_lie_deriv_eq {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (setup : MoserSetup) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : DifferentialFormSpace.L (setup.X_t t) (setup.ω_t t) = -DifferentialFormSpace.d VF (setup.α_t t)

Cartan's formula in Moser's setup: $\mathcal{L}_{X_t} \omega_t = -d\alpha_t$, derived from $\iota_{X_t} \omega_t = -\alpha_t$ and $d\omega_t = 0$.

structure MoserFlow {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (setup : MoserSetup) : Type u_1

The isotopy $\rho_t$ generated by the Moser vector field $X_t$: a time-dependent family of pullback morphisms with $\rho_0 = \mathrm{id}$ satisfying the flow ODE $\frac{d}{dt}\rho_t^*\omega_t = \rho_t^*(\mathcal{L}_{X_t}\omega_t + \dot\omega_t)$, so that if this derivative vanishes then $\rho_t^*\omega_t \equiv \omega_0$.

• ρ : ℝ → DFSMorphism Ω VF Ω VF
• ρ_zero {p : ℕ} (α : Ω p) : (self.ρ 0).pullback α = α
• pullback_deriv : ℝ → Ω 2
• flow_ode (t : ℝ) : t ∈ Set.Icc 0 1 → self.pullback_deriv t = (self.ρ t).pullback (DifferentialFormSpace.L (setup.X_t t) (setup.ω_t t) + setup.dω_dt t)
• deriv_zero_const : (∀ t ∈ Set.Icc 0 1, self.pullback_deriv t = 0) → ∀ t ∈ Set.Icc 0 1, (self.ρ t).pullback (setup.ω_t t) = setup.ω_t 0

theorem moser_transport_zero {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (setup : MoserSetup) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : DifferentialFormSpace.L (setup.X_t t) (setup.ω_t t) + setup.dω_dt t = 0

The Moser transport equation is satisfied: $\mathcal{L}_{X_t}\omega_t + \dot\omega_t = 0$, combining Cartan's formula with $d\alpha_t = \dot\omega_t$.

theorem moser_flow_transport_const {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (setup : MoserSetup) (flow : MoserFlow setup) : (∀ t ∈ Set.Icc 0 1, DifferentialFormSpace.L (setup.X_t t) (setup.ω_t t) + setup.dω_dt t = 0) → ∀ t ∈ Set.Icc 0 1, (flow.ρ t).pullback (setup.ω_t t) = setup.ω_t 0

Under the Moser transport equation, the flow pulls back $\omega_t$ to a constant: $\rho_t^* \omega_t = \omega_0$ for all $t \in [0,1]$.

theorem moser_theorem {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (setup : MoserSetup) (flow : MoserFlow setup) : (∀ {p : ℕ} (α : Ω p), (flow.ρ 0).pullback α = α) ∧ ∀ t ∈ Set.Icc 0 1, (flow.ρ t).pullback (setup.ω_t t) = setup.ω_t 0

Moser's theorem: the isotopy $\rho_t$ satisfies $\rho_0 = \mathrm{id}$ and $\rho_t^*\omega_t = \omega_0$ for all $t \in [0, 1]$, giving a diffeomorphism trivializing the family of symplectic forms.

theorem interpolating_closed {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (ω₀ ω₁ : Ω 2) (hclosed₀ : DifferentialFormSpace.d VF ω₀ = 0) (hclosed₁ : DifferentialFormSpace.d VF ω₁ = 0) (t : ℝ) : DifferentialFormSpace.d VF ((1 - t) • ω₀ + t • ω₁) = 0

The convex combination $(1 - t)\omega_0 + t\omega_1$ of two closed $2$-forms is closed.

theorem contraction_interpolation {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (X : VF) (ω₀ ω₁ : Ω 2) (t : ℝ) : DifferentialFormSpace.ι X ((1 - t) • ω₀ + t • ω₁) = (1 - t) • DifferentialFormSpace.ι X ω₀ + t • DifferentialFormSpace.ι X ω₁

Interior product distributes over convex combinations: $\iota_X((1-t)\omega_0 + t\omega_1) = (1-t)\iota_X\omega_0 + t\iota_X\omega_1$.

theorem contraction_interpolation_zero {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (X : VF) (ω₀ ω₁ : Ω 2) : DifferentialFormSpace.ι X ((1 - 0) • ω₀ + 0 • ω₁) = DifferentialFormSpace.ι X ω₀

Endpoint of the interpolated contraction at $t = 0$: recovers $\iota_X \omega_0$.

theorem contraction_interpolation_one {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (X : VF) (ω₀ ω₁ : Ω 2) : DifferentialFormSpace.ι X ((1 - 1) • ω₀ + 1 • ω₁) = DifferentialFormSpace.ι X ω₁

Endpoint of the interpolated contraction at $t = 1$: recovers $\iota_X \omega_1$.

class HasFiniteDimContraction (Ω : ℕ → Type u_1) (VF : Type u_2) [inst : DifferentialFormSpace Ω VF] : Prop

Axiomatization of finite-dimensional behavior of the interior-product map: for a nondegenerate $2$-form $\omega$, the map $X \mapsto \iota_X\omega$ is bijective, and the interpolation $(1 - t)\omega_0 + t\omega_1$ of two nondegenerate closed forms remains nondegenerate for $t \in [0, 1]$.

• contraction_surjective_of_injective (ω : Ω 2) : (Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ω) → Function.Surjective fun (X : VF) => DifferentialFormSpace.ι X ω
• interpolated_contraction_injective (ω₀ ω₁ : Ω 2) : DifferentialFormSpace.d VF ω₀ = 0 → DifferentialFormSpace.d VF ω₁ = 0 → (Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ω₀) → (Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ω₁) → ∀ t ∈ Set.Icc 0 1, Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ((1 - t) • ω₀ + t • ω₁)

theorem interpolated_form_nondegenerate {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hfdc : HasFiniteDimContraction Ω VF] (ω₀ ω₁ : Ω 2) (hclosed₀ : DifferentialFormSpace.d VF ω₀ = 0) (hclosed₁ : DifferentialFormSpace.d VF ω₁ = 0) (hnd₀ : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ω₀) (hnd₁ : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ω₁) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ((1 - t) • ω₀ + t • ω₁)

Nondegeneracy of $(1 - t)\omega_0 + t\omega_1$ for $t \in [0, 1]$ when $\omega_0, \omega_1$ are closed and nondegenerate (uses the HasFiniteDimContraction axiom).

theorem interpolated_form_contraction_surjective {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hfdc : HasFiniteDimContraction Ω VF] (ω₀ ω₁ : Ω 2) (hclosed₀ : DifferentialFormSpace.d VF ω₀ = 0) (hclosed₁ : DifferentialFormSpace.d VF ω₁ = 0) (hnd₀ : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ω₀) (hnd₁ : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ω₁) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : Function.Surjective fun (X : VF) => DifferentialFormSpace.ι X ((1 - t) • ω₀ + t • ω₁)

For the interpolated form $(1 - t)\omega_0 + t\omega_1$, the contraction $X \mapsto \iota_X((1-t)\omega_0 + t\omega_1)$ is surjective onto $\Omega^1$.

theorem local_moser_interior_product_solvable {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hfdc : HasFiniteDimContraction Ω VF] (ω₀ ω₁ : Ω 2) (α : Ω 1) (hclosed₀ : DifferentialFormSpace.d VF ω₀ = 0) (hclosed₁ : DifferentialFormSpace.d VF ω₁ = 0) (hnd₀ : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ω₀) (hnd₁ : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ω₁) (_hα : DifferentialFormSpace.d VF α = ω₁ - ω₀) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : ∃ (X : VF), DifferentialFormSpace.ι X ((1 - t) • ω₀ + t • ω₁) = -α

For the local Moser construction: given $d\alpha = \omega_1 - \omega_0$, one can solve $\iota_X((1 - t)\omega_0 + t\omega_1) = -\alpha$ for a vector field $X$ at each $t \in [0, 1]$.

theorem local_moser_theorem {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hfdc : HasFiniteDimContraction Ω VF] (ω₀ ω₁ : Ω 2) (hclosed₀ : DifferentialFormSpace.d VF ω₀ = 0) (hclosed₁ : DifferentialFormSpace.d VF ω₁ = 0) (hnd₀ : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ω₀) (hnd₁ : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ω₁) (hcohom : ∃ (α : Ω 1), DifferentialFormSpace.d VF α = ω₁ - ω₀) (hflow_exists : (s : MoserSetup) → MoserFlow s) : ∃ (φ : DFSMorphism Ω VF Ω VF), φ.pullback ω₁ = ω₀

Local Moser theorem. Given closed nondegenerate $\omega_0, \omega_1$ with $\omega_1 - \omega_0 = d\alpha$ exact, there exists a diffeomorphism $\varphi$ with $\varphi^*\omega_1 = \omega_0$.

def DFSMorphism.comp {Ω₁ : ℕ → Type u_1} {VF₁ : Type u_2} {Ω₂ : ℕ → Type u_3} {VF₂ : Type u_4} {Ω₃ : ℕ → Type u_5} {VF₃ : Type u_6} [inst₁ : DifferentialFormSpace Ω₁ VF₁] [inst₂ : DifferentialFormSpace Ω₂ VF₂] [inst₃ : DifferentialFormSpace Ω₃ VF₃] (g : DFSMorphism Ω₂ VF₂ Ω₃ VF₃) (f : DFSMorphism Ω₁ VF₁ Ω₂ VF₂) : DFSMorphism Ω₁ VF₁ Ω₃ VF₃

Composition of DFS morphisms: given $f : (\Omega_1, VF_1) \to (\Omega_2, VF_2)$ and $g : (\Omega_2, VF_2) \to (\Omega_3, VF_3)$, the composite pulls back via $g$ then $f$.

theorem smooth_chart_axiom {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) : ∃ (Ω' : ℕ → Type u_chart) (VF' : Type v_chart) (inst' : DifferentialFormSpace Ω' VF') (x : IsEuclideanDFS Ω' VF') (_ : HasFiniteDimContraction Ω' VF') (chart : DFSMorphism Ω VF Ω' VF') (omega_tilde : Ω' 2) (x : SymplecticManifold Ω' VF'), chart.pullback omega_tilde = S.ω ∧ DifferentialFormSpace.d VF' omega_tilde = 0 ∧ Function.Injective fun (X : VF') => DifferentialFormSpace.ι X omega_tilde

Axiomatized chart existence: every symplectic manifold admits a Euclidean-type chart $(\Omega', VF')$ with finite-dimensional contraction together with a symplectic form $\tilde\omega$ pulling back via the chart morphism to $S.\omega$.

theorem darboux_via_moser {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (hflow_gen : {Ω' : ℕ → Type u_chart} → {VF' : Type v_chart} → [inst' : DifferentialFormSpace Ω' VF'] → (s : MoserSetup) → MoserFlow s) : ∃ (Ω' : ℕ → Type u_chart) (VF' : Type v_chart) (x : DifferentialFormSpace Ω' VF') (φ : DFSMorphism Ω VF Ω' VF') (S' : SymplecticManifold Ω' VF'), φ.pullback S'.ω = S.ω

Darboux's theorem (via Moser's trick). Every symplectic manifold $(M, \omega)$ admits a chart $\varphi$ with $\varphi^*\omega' = \omega$ for some standard symplectic form $\omega'$, combining the chart axiom, the Poincaré lemma, and the local Moser theorem.

structure HasMoserFlowData {Ω_M : ℕ → Type u_M} {VF_M : Type v_M} [inst_M : DifferentialFormSpace Ω_M VF_M] {Ω_X : ℕ → Type u_X} {VF_X : Type v_X} [inst_X : DifferentialFormSpace Ω_X VF_X] (i : DFSMorphism Ω_X VF_X Ω_M VF_M) (ω₀ ω₁ : Ω_M 2) : Type (max (max (u_M + 1) u_X) (v_M + 1))

Relative Moser data along a submanifold inclusion $i : X \hookrightarrow M$: charts $U_0, U_1$ around $X$ and a diffeomorphism $\varphi : U_0 \to U_1$ pulling $\omega_1$ to $\omega_0$ while restricting to the identity on $X$. Encodes the local statement underlying relative versions of Moser's theorem (e.g., the relative Darboux/Weinstein neighborhood theorems).

• Ω_U₀ : ℕ → Type u_M
• VF_U₀ : Type v_M
• inst_U₀ : DifferentialFormSpace self.Ω_U₀ self.VF_U₀
• incl₀ : DFSMorphism self.Ω_U₀ self.VF_U₀ Ω_M VF_M
• i_X_U₀ : DFSMorphism Ω_X VF_X self.Ω_U₀ self.VF_U₀
• Ω_U₁ : ℕ → Type u_M
• VF_U₁ : Type v_M
• inst_U₁ : DifferentialFormSpace self.Ω_U₁ self.VF_U₁
• incl₁ : DFSMorphism self.Ω_U₁ self.VF_U₁ Ω_M VF_M
• i_X_U₁ : DFSMorphism Ω_X VF_X self.Ω_U₁ self.VF_U₁
• φ : DFSMorphism self.Ω_U₀ self.VF_U₀ self.Ω_U₁ self.VF_U₁
• φ_inv : DFSMorphism self.Ω_U₁ self.VF_U₁ self.Ω_U₀ self.VF_U₀
• compat₀ {p : ℕ} (α : Ω_M p) : self.i_X_U₀.pullback (self.incl₀.pullback α) = i.pullback α
• compat₁ {p : ℕ} (α : Ω_M p) : self.i_X_U₁.pullback (self.incl₁.pullback α) = i.pullback α
• pullback_eq : self.φ.pullback (self.incl₁.pullback ω₁) = self.incl₀.pullback ω₀
• φ_identity_on_X {p : ℕ} (α : self.Ω_U₁ p) : self.i_X_U₀.pullback (self.φ.pullback α) = self.i_X_U₁.pullback α
• φ_inv_left {p : ℕ} (α : self.Ω_U₁ p) : self.φ_inv.pullback (self.φ.pullback α) = α
• φ_inv_right {p : ℕ} (α : self.Ω_U₀ p) : self.φ.pullback (self.φ_inv.pullback α) = α
• φ_inv_identity_on_X {p : ℕ} (α : self.Ω_U₀ p) : self.i_X_U₁.pullback (self.φ_inv.pullback α) = self.i_X_U₀.pullback α