Time-dependent flows near a rest point

Let X be a time-dependent vector field on a finite-dimensional real normed space, defined and jointly C^r (r ≥ 1) only on T × U, for an open set of times T ⊇ [0, 1] and an open set U, and suppose that x₀ ∈ U is a rest point: X t x₀ = 0 for all t ∈ T. The orbit of x₀ is then constant, so the orbits of nearby points stay close to x₀ up to time one, and the field generates a family of maps ψₜ near x₀ for t ∈ [0, 1].

TauCeti.exists_eventually_forall_hasDerivAt_fderiv_of_contDiffOn makes this precise. It cuts the field off by a bump function equal to one near [0, 1] × {x₀}, so that the suspended field is globally Lipschitz, and takes the global time-dependent flow TauCeti.timeDependentFlow from time 0. The resulting maps satisfy ψ₀ = id and fix every rest point of the field, in particular ψₜ x₀ = x₀; the time-one map is a C^r diffeomorphism of the whole space, and for every x near x₀ and t ∈ [0, 1] the point ψₜ x stays in U, the orbit solves ∂ₜ ψₜ x = Xₜ (ψₜ x), and the derivative Dψₜ(x) solves the variational equation ∂ₜ Dψₜ(x) = DXₜ(ψₜ x) ∘ Dψₜ(x).

These are exactly the hypotheses of Moser's identity (TauCeti.compContinuousLinearMap_fderiv_eq_of_curryLeft_eq_neg), so this is the flow used in Moser's deformation argument, for instance in the proof of Darboux's theorem, where the Moser field vanishes at the centre of the chart. In the relative Darboux theorem the Moser field vanishes along a whole submanifold, which the flow therefore fixes pointwise.

References

• D. McDuff and D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 3.2 (the Moser flow in the proof of Darboux's theorem).
• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Theorem 9.48 (time-dependent flows).

theorem TauCeti.exists_eventually_forall_hasDerivAt_fderiv_of_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {X : ℝ → E → E} {T : Set ℝ} {U : Set E} {x₀ : E} {r : ℕ∞} (hr : 1 ≤ r) (hT : IsOpen T) (hU : IsOpen U) (hTI : Set.Icc 0 1 ⊆ T) (hx₀ : x₀ ∈ U) (hX : ContDiffOn ℝ (↑r) (fun (p : ℝ × E) => X p.1 p.2) (T ×ˢ U)) (hX₀ : ∀ t ∈ T, X t x₀ = 0) : ∃ (ψ : ℝ → E → E) (ψ' : E → E), ContDiff ℝ (↑r) (ψ 1) ∧ ContDiff ℝ (↑r) ψ' ∧ Function.LeftInverse ψ' (ψ 1) ∧ Function.RightInverse ψ' (ψ 1) ∧ ψ 0 = id ∧ (∀ (y : E), (∀ t ∈ T, X t y = 0) → ∀ (t : ℝ), ψ t y = y) ∧ ∀ᶠ (x : E) in nhds x₀, ∀ t ∈ Set.Icc 0 1, ψ t x ∈ U ∧ HasDerivAt (fun (s : ℝ) => ψ s x) (X t (ψ t x)) t ∧ HasDerivAt (fun (s : ℝ) => fderiv ℝ (ψ s) x) (fderiv ℝ (X t) (ψ t x) ∘SL fderiv ℝ (ψ t) x) t

The local flow of a time-dependent field near a rest point. Let X be a time-dependent vector field on a finite-dimensional space, jointly C^r (r ≥ 1) on T × U for an open set of times T ⊇ [0, 1] and an open set U, and vanishing at x₀ ∈ U for all times in T. Then there is a family of maps ψ t, with ψ 0 = id and ψ t y = y at every point y where the field vanishes for all times in T (in particular ψ t x₀ = x₀), whose time-one map is a C^r diffeomorphism of the whole space, such that for every x near x₀ and every t ∈ [0, 1], the point ψ t x lies in U, the orbit s ↦ ψ s x solves x' = X(t, x) at t, and the derivative Dψ_t(x) solves the variational equation ∂ₜ Dψ_t(x) = DX_t(ψ_t x) ∘ Dψ_t(x).