Extending an integral curve past a finite endpoint

Mathlib's integral-curve API produces a local integral curve through a point and shows that two integral curves on a common open interval agree. It says nothing about what happens at a finite endpoint of the interval of definition. This file supplies the missing extension criterion: an integral curve on Ioo a b with b < ∞ extends past b as soon as it accumulates at a point of the manifold as t → b⁻. Equivalently, a curve that cannot be extended must eventually leave every compact set.

The proof needs a uniform time of existence: the same ε > 0 must work for every initial point in a neighbourhood of the accumulation point y, so that a time t₁ < b with b - t₁ < ε and γ t₁ near y produces a solution defined past b. Uniqueness on the overlap then glues it to γ. The uniform time comes from ContDiffAt.exists_forall_mem_ball_exists_eq_forall_mem_Ioo_hasDerivAt_and_mem, read through the extended chart at y.

Main results

• exists_mem_nhds_forall_exists_isMIntegralCurveOn_Ioo: a uniform time of existence for the integral curves of a C^1 vector field near a point.
• IsMIntegralCurveOn.exists_gt_isMIntegralCurveOn_Ioo: the extension criterion at a finite right endpoint, and IsMIntegralCurveOn.exists_lt_isMIntegralCurveOn_Ioo at a finite left endpoint.
• IsMIntegralCurveOn.exists_gt_isMIntegralCurveOn_Ioo_of_tendsto and IsMIntegralCurveOn.exists_lt_isMIntegralCurveOn_Ioo_of_tendsto: their sequential forms.
• IsMIntegralCurveOn.eventually_notMem_nhdsLT and IsMIntegralCurveOn.eventually_notMem_nhdsGT: a nonextendable integral curve eventually leaves every compact set.

References

• [Lee, J. M. (2012). Introduction to Smooth Manifolds. Springer New York.][lee2012], Chapter 9.

theorem exists_mem_nhds_forall_exists_isMIntegralCurveOn_Ioo {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] {v : (x : M) → TangentSpace I x} [CompleteSpace E] [IsManifold I 1 M] [BoundarylessManifold I M] {x₀ : M} (hv : ContMDiffAt I I.tangent 1 (fun (x : M) => ⟨x, v x⟩) x₀) : ∃ w ∈ nhds x₀, ∃ ε > 0, ∀ (t₀ : ℝ), ∀ x ∈ w, ∃ (γ : ℝ → M), γ t₀ = x ∧ IsMIntegralCurveOn γ v (Set.Ioo (t₀ - ε) (t₀ + ε))

A uniform time of existence for the integral curves of a C^1 vector field: there is a neighbourhood w of x₀ and a single ε > 0 such that, at any prescribed initial time t₀, every point of w is the value at t₀ of an integral curve defined on all of Ioo (t₀ - ε) (t₀ + ε).

Mathlib's exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless gives an interval of existence that depends on the initial point; the content here is that it can be chosen uniformly. The field is autonomous, so the initial time is immaterial and ε is uniform in it too.

theorem IsMIntegralCurveOn.exists_gt_isMIntegralCurveOn_Ioo {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] {v : (x : M) → TangentSpace I x} {γ : ℝ → M} {a b : ℝ} {y : M} [CompleteSpace E] [IsManifold I 1 M] [BoundarylessManifold I M] [T2Space M] (hγ : IsMIntegralCurveOn γ v (Set.Ioo a b)) (hab : a < b) (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) (hy : MapClusterPt y (nhdsWithin b (Set.Iio b)) γ) : ∃ c > b, ∃ (δ : ℝ → M), IsMIntegralCurveOn δ v (Set.Ioo a c) ∧ Set.EqOn δ γ (Set.Ioo a b)

The finite-endpoint extension criterion. An integral curve on Ioo a b which accumulates at a point y of the manifold as t → b⁻ extends to an integral curve on a strictly longer interval Ioo a c.

The hypothesis is a cluster point rather than a limit: it suffices that γ t be arbitrarily close to y at times arbitrarily close to b.

theorem IsMIntegralCurveOn.exists_gt_isMIntegralCurveOn_Ioo_of_tendsto {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] {v : (x : M) → TangentSpace I x} {γ : ℝ → M} {a b : ℝ} {y : M} [CompleteSpace E] [IsManifold I 1 M] [BoundarylessManifold I M] [T2Space M] (hγ : IsMIntegralCurveOn γ v (Set.Ioo a b)) (hab : a < b) (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) {u : ℕ → ℝ} (hu : ∀ᶠ (n : ℕ) in Filter.atTop, u n < b) (hub : Filter.Tendsto u Filter.atTop (nhds b)) (hy : Filter.Tendsto (γ ∘ u) Filter.atTop (nhds y)) : ∃ c > b, ∃ (δ : ℝ → M), IsMIntegralCurveOn δ v (Set.Ioo a c) ∧ Set.EqOn δ γ (Set.Ioo a b)

The finite-endpoint extension criterion, sequential form. If u n → b, the sequence is eventually below b, and γ (u n) → y, then γ extends past b.

theorem IsMIntegralCurveOn.eventually_notMem_nhdsLT {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] {v : (x : M) → TangentSpace I x} {γ : ℝ → M} {a b : ℝ} [CompleteSpace E] [IsManifold I 1 M] [BoundarylessManifold I M] [T2Space M] (hγ : IsMIntegralCurveOn γ v (Set.Ioo a b)) (hab : a < b) (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) (hmax : ∀ c > b, ∀ (δ : ℝ → M), IsMIntegralCurveOn δ v (Set.Ioo a c) → ¬Set.EqOn δ γ (Set.Ioo a b)) {K : Set M} (hK : IsCompact K) : ∀ᶠ (t : ℝ) in nhdsWithin b (Set.Iio b), γ t ∉ K

The escape lemma. An integral curve on Ioo a b that admits no extension past its finite right endpoint eventually leaves every compact set as t → b⁻.

theorem IsMIntegralCurveOn.exists_lt_isMIntegralCurveOn_Ioo {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] {v : (x : M) → TangentSpace I x} {γ : ℝ → M} {a b : ℝ} {y : M} [CompleteSpace E] [IsManifold I 1 M] [BoundarylessManifold I M] [T2Space M] (hγ : IsMIntegralCurveOn γ v (Set.Ioo a b)) (hab : a < b) (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) (hy : MapClusterPt y (nhdsWithin a (Set.Ioi a)) γ) : ∃ c < a, ∃ (δ : ℝ → M), IsMIntegralCurveOn δ v (Set.Ioo c b) ∧ Set.EqOn δ γ (Set.Ioo a b)

The finite-endpoint extension criterion at the left endpoint. An integral curve on Ioo a b which accumulates at a point y of the manifold as t → a⁺ extends to an integral curve on a strictly longer interval Ioo c b.

theorem IsMIntegralCurveOn.exists_lt_isMIntegralCurveOn_Ioo_of_tendsto {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] {v : (x : M) → TangentSpace I x} {γ : ℝ → M} {a b : ℝ} {y : M} [CompleteSpace E] [IsManifold I 1 M] [BoundarylessManifold I M] [T2Space M] (hγ : IsMIntegralCurveOn γ v (Set.Ioo a b)) (hab : a < b) (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) {u : ℕ → ℝ} (hu : ∀ᶠ (n : ℕ) in Filter.atTop, a < u n) (hub : Filter.Tendsto u Filter.atTop (nhds a)) (hy : Filter.Tendsto (γ ∘ u) Filter.atTop (nhds y)) : ∃ c < a, ∃ (δ : ℝ → M), IsMIntegralCurveOn δ v (Set.Ioo c b) ∧ Set.EqOn δ γ (Set.Ioo a b)

The finite-endpoint extension criterion at the left endpoint, sequential form. If u n → a, the sequence is eventually above a, and γ (u n) → y, then γ extends before a.

theorem IsMIntegralCurveOn.eventually_notMem_nhdsGT {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] {v : (x : M) → TangentSpace I x} {γ : ℝ → M} {a b : ℝ} [CompleteSpace E] [IsManifold I 1 M] [BoundarylessManifold I M] [T2Space M] (hγ : IsMIntegralCurveOn γ v (Set.Ioo a b)) (hab : a < b) (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) (hmax : ∀ c < a, ∀ (δ : ℝ → M), IsMIntegralCurveOn δ v (Set.Ioo c b) → ¬Set.EqOn δ γ (Set.Ioo a b)) {K : Set M} (hK : IsCompact K) : ∀ᶠ (t : ℝ) in nhdsWithin a (Set.Ioi a), γ t ∉ K

The escape lemma at the left endpoint. An integral curve on Ioo a b that admits no extension before its finite left endpoint eventually leaves every compact set as t → a⁺.