Maximal integral curves of compactly supported vector fields

Each maximal integral curve of a C¹ vector field vanishing outside a set on a boundaryless manifold stays in that set together with its initial point. When the set is compact, this makes the field complete (TauCeti.isCompleteVectorField_of_isCompact_of_eq_zero_off).

The ambient manifold need not be compact, and its model may be any real Banach space. This supplies completeness for vector fields obtained by cutting off local ambient motions. The compact set is explicit, avoiding any choice of a trivialization to define the support of a tangent-bundle section.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 9.16.

theorem TauCeti.mapsTo_maximalIntegralCurve_insert_of_eq_zero_off {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} {x : M} {K : Set M} (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hzero : ∀ y ∉ K, v y = 0) : Set.MapsTo (maximalIntegralCurve v x) (maximalIntegralCurveInterval v x) (insert x K)

A maximal integral curve of a C¹ vector field vanishing off K stays in K together with its initial point. No closedness or compactness of K is required.