The local contraction equation for Moser deformation

Let B₀ and B₁ be families of bilinear forms which both agree at x₀ with a fixed invertible bilinear form L. The contraction maps of (1 - t) • B₀ x + t • B₁ x are invertible on a single spatial neighbourhood of x₀, for every t ∈ [0, 1]. In fact, the time interval can also be enlarged to an open neighbourhood.

For smooth B₀, B₁ and a smooth one-form α, construct the jointly smooth vector field X(t, x) uniquely determined by

((1 - t) • B₀ x + t • B₁ x) (X(t, x)) = -α x.

This is the local algebraic step in Moser's argument. For Darboux's theorem B₀ is the constant family L; for the relative Darboux theorem both families vary. Alternation and closedness of B₀, B₁ are not needed for this step and are not imposed here.

The analytic step is Moser's identity: for closed forms ω₀, ω₁ with ω₁ - ω₀ = dα, a family of maps ψₜ moving along a field Xₜ with ι_{Xₜ} ((1 - t) • ω₀ + t • ω₁) = -α pulls ω₁ back at time 1 to the pullback of ω₀ at time 0 (TauCeti.compContinuousLinearMap_fderiv_eq_of_curryLeft_eq_neg). The flow ψₜ itself and the Darboux chart are not constructed here.

The argument follows McDuff--Salamon, Introduction to Symplectic Topology, Section 3.2, and uses Mathlib's smooth inverse for continuous linear maps and its generalized tube lemma. Moser's identity combines the time derivative of pulled-back forms, TauCeti.hasDerivAt_compContinuousLinearMap_fderiv, with Cartan's formula TauCeti.lieDerivForm_eq_curryLeft_extDeriv_add.

theorem TauCeti.exists_isOpen_isInvertible_sub_smul_add_smul {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {W : Set V} {x₀ : V} {B₀ B₁ : V → V →L[ℝ] V →L[ℝ] ℝ} {L : V →L[ℝ] V →L[ℝ] ℝ} (hL : L.IsInvertible) (hW : IsOpen W) (hx₀ : x₀ ∈ W) (hB₀ : ContinuousOn B₀ W) (hB₁ : ContinuousOn B₁ W) (hB₀x₀ : B₀ x₀ = L) (hB₁x₀ : B₁ x₀ = L) : ∃ (T : Set ℝ) (U : Set V), IsOpen T ∧ IsOpen U ∧ Set.Icc 0 1 ⊆ T ∧ x₀ ∈ U ∧ U ⊆ W ∧ ∀ p ∈ T ×ˢ U, ((1 - p.1) • B₀ p.2 + p.1 • B₁ p.2).IsInvertible

The straight-line family between two families of bilinear forms which agree at one point with an invertible bilinear form has invertible contraction maps on one neighbourhood, uniformly for all times in [0, 1]. The returned time neighbourhood is open, so subsequent smoothness is ordinary local smoothness, including at the endpoints.

theorem TauCeti.exists_contDiffOn_moserField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {W : Set V} {x₀ : V} {B₀ B₁ : V → V →L[ℝ] V →L[ℝ] ℝ} {L : V →L[ℝ] V →L[ℝ] ℝ} (hL : L.IsInvertible) {n : WithTop ℕ∞} (hW : IsOpen W) (hx₀ : x₀ ∈ W) (hB₀ : ContDiffOn ℝ n B₀ W) (hB₁ : ContDiffOn ℝ n B₁ W) (hB₀x₀ : B₀ x₀ = L) (hB₁x₀ : B₁ x₀ = L) {α : V → V →L[ℝ] ℝ} (hα : ContDiffOn ℝ n α W) : ∃ (T : Set ℝ) (U : Set V) (X : ℝ × V → V), IsOpen T ∧ IsOpen U ∧ Set.Icc 0 1 ⊆ T ∧ x₀ ∈ U ∧ U ⊆ W ∧ ContDiffOn ℝ n X (T ×ˢ U) ∧ ∀ p ∈ T ×ˢ U, ∀ (v : V), (∀ (w : V), (((1 - p.1) • B₀ p.2 + p.1 • B₁ p.2) v) w = -(α p.2) w) ↔ v = X p

Solve the local straight-line Moser contraction equation by a jointly C^n vector field, on an open time neighbourhood of [0, 1] and one spatial neighbourhood of x₀. The displayed equivalence characterizes the solution uniquely without unfolding it. Closedness and alternation of the varying bilinear forms are separate geometric hypotheses.

Moser's identity

theorem TauCeti.compContinuousLinearMap_fderiv_eq_of_curryLeft_eq_neg {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {ω₀ ω₁ : E → E [⋀^Fin (k + 1)]→L[ℝ] F} {α : E → E [⋀^Fin k]→L[ℝ] F} {ψ X : ℝ → E → E} {x : E} (hω₀ : ∀ t ∈ Set.Icc 0 1, DifferentiableAt ℝ ω₀ (ψ t x)) (hω₁ : ∀ t ∈ Set.Icc 0 1, DifferentiableAt ℝ ω₁ (ψ t x)) (hdω₀ : ∀ t ∈ Set.Icc 0 1, extDeriv ω₀ (ψ t x) = 0) (hdω₁ : ∀ t ∈ Set.Icc 0 1, extDeriv ω₁ (ψ t x) = 0) (hα : ∀ t ∈ Set.Icc 0 1, extDeriv α (ψ t x) = ω₁ (ψ t x) - ω₀ (ψ t x)) (hX : ∀ t ∈ Set.Icc 0 1, (fun (y : E) => ((1 - t) • ω₀ y + t • ω₁ y).curryLeft (X t y)) =ᶠ[nhds (ψ t x)] -α) (hXd : ∀ t ∈ Set.Icc 0 1, DifferentiableAt ℝ (X t) (ψ t x)) (hψ : ∀ t ∈ Set.Icc 0 1, HasDerivAt (fun (s : ℝ) => ψ s x) (X t (ψ t x)) t) (hDψ : ∀ t ∈ Set.Icc 0 1, HasDerivAt (fun (s : ℝ) => fderiv ℝ (ψ s) x) (fderiv ℝ (X t) (ψ t x) ∘SL fderiv ℝ (ψ t) x) t) : (ω₁ (ψ 1 x)).compContinuousLinearMap (fderiv ℝ (ψ 1) x) = (ω₀ (ψ 0 x)).compContinuousLinearMap (fderiv ℝ (ψ 0) x)

Moser's identity. Let ω₀, ω₁ be forms that are closed along the orbit t ↦ ψₜ x, t ∈ [0, 1], with ω₁ - ω₀ = dα there. If ψₜ moves along a time-dependent field Xₜ with ι_{Xₜ} ((1 - t) • ω₀ + t • ω₁) = -α near the orbit, and the derivative of ψₜ at x solves the variational equation, then ψ₁^* ω₁ = ψ₀^* ω₀ at x.