Smooth dependence of integral curves on their initial point

A smooth vector field on a finite-dimensional boundaryless manifold admits, near every point, a family of local integral curves that depends smoothly on both the initial point and time. This is the manifold form of smooth dependence for ordinary differential equations: express the field in one extended chart, apply the model-space local-flow theorem, and return through the inverse chart. The resulting family inherits the flow law whenever its first time lies in the common local domain.

The family is only asserted as a germ near the chosen point and time zero. This is the natural local statement: outside that germ both the chart and the model-space extension carry arbitrary values. Uniqueness of integral curves can subsequently identify overlapping germs and assemble the maximal flow.

Main result

• TauCeti.Manifold.exists_contMDiffAt_localFlow: a smooth vector field has a jointly smooth family of local integral curves through all nearby initial points, satisfying the flow law.

References

• J. M. Lee, Introduction to Smooth Manifolds, Chapter 9.
• Winston Yin, mathlib4#26394: Existence of local flows on manifolds, for the passage between a model-space flow and manifold integral curves.

theorem TauCeti.Manifold.exists_contMDiffAt_localFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [I.Boundaryless] [IsManifold I (↑⊤) M] (v : (x : M) → TangentSpace I x) (a : M) {V : Set M} (hv : ContMDiffOn I I.tangent (↑⊤) (fun (x : M) => ⟨x, v x⟩) V) (hV : V ∈ nhds a) : ∃ U ∈ nhds a, ∃ s ∈ nhds 0, IsOpen s ∧ ∃ (Φ : M → ℝ → M), ContMDiffAt (I.prod (modelWithCornersSelf ℝ ℝ)) I (↑⊤) (fun (p : M × ℝ) => Φ p.1 p.2) (a, 0) ∧ ∀ x ∈ U, Φ x 0 = x ∧ IsMIntegralCurveOn (Φ x) v s ∧ ∀ t ∈ s, ∀ (u : ℝ), Φ x (t + u) = Φ (Φ x t) u

Smooth dependence of integral curves on their initial point.

If a tangent vector field is smooth on a neighbourhood of a, then there is a family Φ x t which is jointly smooth at (a, 0), starts at x for every x in a neighbourhood of a, and is an integral curve of the field on one common open time neighbourhood. Its values outside that common domain provide only a total extension of the local flow.