The maximal integral curve of a vector field

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, and TauCeti/Geometry/Manifold/IntegralCurve/Extension.lean extends an integral curve past a finite endpoint at which it accumulates. What is still missing is the object those results describe: the maximal integral curve of a C^1 vector field v through a point x, defined on the largest open interval around 0 on which any integral curve through x exists.

This file builds it. maximalIntegralCurveInterval v x is the union of the open intervals around 0 carrying an integral curve of v taking the value x at time 0, and maximalIntegralCurve v x is the curve obtained by reading off, at each time of that set, the value of one such witness, chosen arbitrarily. That choice becomes immaterial once M is a separated boundaryless C^1 manifold and v is a C^1 field: uniqueness of integral curves on a common interval then makes the reading unambiguous, so the maximal curve restricts to every witness, is itself an integral curve on the whole interval, and is the largest one: every integral curve through x on an open interval around 0 is one of its restrictions.

The interval is open and Set.OrdConnected, hence an interval in the order sense, and it contains 0 as soon as v is C^1 at x on a boundaryless manifold. At a finite endpoint the extension criterion of Extension.lean applies with its maximality hypothesis discharged: the maximal curve has no cluster point in M as the endpoint is approached, so in particular it leaves every compact set there. Consequently a maximal curve confined to a compact set is defined for all time, and every C^1 vector field on a compact manifold is complete.

Only the initial time 0 is used, matching the intended geodesic application: for the geodesic spray on the tangent bundle, maximalIntegralCurveInterval is the maximal interval J(p, v) of the geodesic with initial data (p, v). Since the fields considered here are autonomous, an arbitrary initial time is recovered by translating the parameter with IsMIntegralCurveOn.comp_add.

Main definitions

• maximalIntegralCurveInterval v x: the maximal interval of existence of an integral curve of v through x at time 0.
• maximalIntegralCurve v x: the maximal integral curve of v through x, junk-valued outside maximalIntegralCurveInterval v x.

Main results

• isOpen_maximalIntegralCurveInterval, ordConnected_maximalIntegralCurveInterval and isPreconnected_maximalIntegralCurveInterval: the maximal interval of existence is an open interval, and zero_mem_maximalIntegralCurveInterval puts 0 in it, uniformly in the initial point in TauCeti.eventually_mem_maximalIntegralCurveInterval.
• isMIntegralCurveOn_maximalIntegralCurve: the maximal curve is an integral curve of v on the maximal interval, with maximalIntegralCurve_zero giving its value at 0; it is a global integral curve when that interval is all of ℝ (TauCeti.isMIntegralCurve_maximalIntegralCurve_of_eq_univ).
• IsMIntegralCurve.maximalIntegralCurve_eq: a global integral curve is the maximal integral curve through its initial point.
• IsMIntegralCurveOn.eqOn_maximalIntegralCurve and IsMIntegralCurveOn.subset_maximalIntegralCurveInterval: every integral curve through x on an open interval around 0 is a restriction of the maximal one. Their Ioi forms apply on open forward rays containing 0.
• IsMIntegralCurveOn.eqOn_maximalIntegralCurve_Ici and IsMIntegralCurveOn.Ioi_subset_maximalIntegralCurveInterval_of_Ici: moving the time origin to any interior time compares a prescribed closed-ray curve with the maximal curve, without requiring a two-sided derivative at the endpoint. IsMIntegralCurveOn.mapsTo_maximalIntegralCurve_Ici transfers forward trapping sets, and IsMIntegralCurveOn.tendsto_maximalIntegralCurve_iff transfers limits at positive infinity.
• exists_Ioo_subset_maximalIntegralCurveInterval_of_isLUB and its IsGLB counterpart: a finite endpoint of the maximal interval is reached by an open subinterval straddling 0.
• not_mapClusterPt_nhdsLT_maximalIntegralCurve and not_mapClusterPt_nhdsGT_maximalIntegralCurve: at a finite endpoint of the maximal interval the maximal curve has no cluster point in the manifold, with eventually_notMem_nhdsLT_maximalIntegralCurve and eventually_notMem_nhdsGT_maximalIntegralCurve the compact-set forms.
• maximalIntegralCurveInterval_eq_univ_of_not_bddAbove_not_bddBelow: an interval of existence unbounded on both sides is all of ℝ.
• Ici_subset_maximalIntegralCurveInterval_of_isCompact_of_mapsTo: a maximal curve whose forward part is confined to a compact set is defined for all positive time.
• maximalIntegralCurveInterval_eq_univ_of_isCompact_of_mapsTo: a maximal curve confined to a compact set is defined for all time, and isMIntegralCurve_maximalIntegralCurve specializes this to a compact manifold: a C^1 vector field on a compact manifold is complete (stated as TauCeti.isCompleteVectorField_of_compactSpace).
• maximalIntegralCurveInterval_eq_univ_iff: the maximal interval is all of ℝ exactly when some global integral curve passes through x at time 0.

References

• [Lee, J. M. (2012). Introduction to Smooth Manifolds. Springer New York.][lee2012], Chapter 9, Theorems 9.12 and 9.16.
• michaellee94, mathlib4#26413: Existence of maximal solutions for ODEs meeting Picard--Lindelöf conditions, for the maximal-solution and maximal-domain API direction.
• Winston Yin, mathlib4#26394: Existence of local flows on manifolds, for the manifold local-flow formulation and uniform local existence near an initial point.

def maximalIntegralCurveInterval {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) (x : M) : Set ℝ

The maximal interval of existence of an integral curve of v through x: the set of times lying in some open interval around 0 on which an integral curve of v taking the value x at time 0 is defined.

It is open and order-connected (isOpen_maximalIntegralCurveInterval, ordConnected_maximalIntegralCurveInterval). Under the local-existence hypotheses of zero_mem_maximalIntegralCurveInterval, it contains 0, and maximalIntegralCurve v x is an integral curve of v on it.

theorem IsMIntegralCurveOn.subset_maximalIntegralCurveInterval {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 : ℝ} {x : M} (hγ : IsMIntegralCurveOn γ v (Set.Ioo a b)) (h0 : 0 ∈ Set.Ioo a b) (hx : γ 0 = x) : Set.Ioo a b ⊆ maximalIntegralCurveInterval v x

An integral curve of v through x on an open interval around 0 is defined on a subset of the maximal interval of existence.

theorem IsMIntegralCurveOn.Ioi_subset_maximalIntegralCurveInterval {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 : ℝ} {x : M} (hγ : IsMIntegralCurveOn γ v (Set.Ioi a)) (ha : a < 0) (hx : γ 0 = x) : Set.Ioi a ⊆ maximalIntegralCurveInterval v x

A curve on an open forward ray containing zero supplies existence on that whole ray.

theorem IsMIntegralCurveOn.comp_add_Ioi_sub_of_Ici {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 : ℝ} (hγ : IsMIntegralCurveOn γ v (Set.Ici a)) (b : ℝ) : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) => x + b) v (Set.Ioi (a - b))

Translating a curve on a closed forward ray gives an integral curve on the translated open ray.

theorem IsMIntegralCurveOn.Ioi_subset_maximalIntegralCurveInterval_of_Ici {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 : ℝ} (hγ : IsMIntegralCurveOn γ v (Set.Ici a)) (hb : a < b) : Set.Ioi (a - b) ⊆ maximalIntegralCurveInterval v (γ b)

Moving the time origin to an interior time of a closed forward ray supplies existence on the corresponding open ray.

theorem isOpen_maximalIntegralCurveInterval {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} {x : M} : IsOpen (maximalIntegralCurveInterval v x)

The maximal interval of existence is open.

theorem ordConnected_maximalIntegralCurveInterval {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} {x : M} : (maximalIntegralCurveInterval v x).OrdConnected

The maximal interval of existence is order-connected: it is an interval. Every witness interval straddles 0, so a time between two of its elements lies in the witness interval of whichever of them is on the same side of 0.

theorem isPreconnected_maximalIntegralCurveInterval {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} {x : M} : IsPreconnected (maximalIntegralCurveInterval v x)

The maximal interval of existence is preconnected. This is the hypothesis under which a constant-speed statement for the curves defined on it can be read.

theorem TauCeti.zero_mem_maximalIntegralCurveInterval_of_nonempty {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} {x : M} (h : (maximalIntegralCurveInterval v x).Nonempty) : 0 ∈ maximalIntegralCurveInterval v x

The maximal interval of existence is nonempty exactly when it contains the initial time: every witness interval straddles 0.

theorem exists_Ioo_subset_maximalIntegralCurveInterval_of_isLUB {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} {b : ℝ} {x : M} (hb : IsLUB (maximalIntegralCurveInterval v x) b) : ∃ a < 0, 0 < b ∧ Set.Ioo a b ⊆ maximalIntegralCurveInterval v x

The maximal interval of existence contains an open interval with the same right endpoint and a negative left endpoint. In particular a finite least upper bound of the interval is positive.

theorem exists_Ioo_subset_maximalIntegralCurveInterval_of_isGLB {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} {a : ℝ} {x : M} (ha : IsGLB (maximalIntegralCurveInterval v x) a) : ∃ b > 0, a < 0 ∧ Set.Ioo a b ⊆ maximalIntegralCurveInterval v x

The maximal interval of existence contains an open interval with the same left endpoint and a positive right endpoint. In particular a finite greatest lower bound of the interval is negative.

theorem zero_mem_maximalIntegralCurveInterval {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} {x : M} [CompleteSpace E] [IsManifold I 1 M] [BoundarylessManifold I M] (hv : ContMDiffAt I I.tangent 1 (fun (y : M) => ⟨y, v y⟩) x) : 0 ∈ maximalIntegralCurveInterval v x

Local existence puts the initial time in the maximal interval of existence.

theorem TauCeti.eventually_mem_maximalIntegralCurveInterval {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} {x : M} [CompleteSpace E] [IsManifold I 1 M] [BoundarylessManifold I M] (hv : ContMDiffAt I I.tangent 1 (fun (y : M) => ⟨y, v y⟩) x) : ∀ᶠ (p : M × ℝ) in nhds (x, 0), p.2 ∈ maximalIntegralCurveInterval v p.1

The domain of the maximal flow contains a neighbourhood of (x, 0). For a vector field which is C^1 at x, every initial point near x has a maximal integral curve defined at every time near 0. This is the uniform-in-the-initial-point form of zero_mem_maximalIntegralCurveInterval.

noncomputable def maximalIntegralCurve {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) (x : M) (t : ℝ) : M

The maximal integral curve of v through x: at a time of maximalIntegralCurveInterval v x it is the value there of one integral curve of v through x defined at that time, chosen arbitrarily, and outside that set it is junk-valued at x.

No hypothesis on M or v is imposed here, so at this generality the definition only selects the value of some witness. Under the hypotheses of IsMIntegralCurveOn.eqOn_maximalIntegralCurve — M separated, boundaryless and C^1, and v a C^1 field — uniqueness of integral curves makes the value independent of the witness, and that theorem, rather than this definition, is what all the results below use.

@[simp]

theorem maximalIntegralCurve_eq_of_not_mem {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} {t : ℝ} {x : M} (h : t ∉ maximalIntegralCurveInterval v x) : maximalIntegralCurve v x t = x

Outside the maximal interval of existence, the junk value of the maximal integral curve is its initial point.

theorem exists_isMIntegralCurveOn_maximalIntegralCurve_eq {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} {t : ℝ} {x : M} (h : t ∈ maximalIntegralCurveInterval v x) : ∃ (γ : ℝ → M) (a : ℝ) (b : ℝ), IsMIntegralCurveOn γ v (Set.Ioo a b) ∧ γ 0 = x ∧ 0 ∈ Set.Ioo a b ∧ t ∈ Set.Ioo a b ∧ maximalIntegralCurve v x t = γ t

At a time of the maximal interval of existence, the maximal integral curve takes the value of some integral curve of v through x.

theorem zero_mem_maximalIntegralCurveInterval_of_mem {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} {t : ℝ} {x : M} (h : t ∈ maximalIntegralCurveInterval v x) : 0 ∈ maximalIntegralCurveInterval v x

Time zero belongs to the maximal interval of existence as soon as some time does.

@[simp]

theorem maximalIntegralCurve_zero {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} {x : M} : maximalIntegralCurve v x 0 = x

At the initial time, the maximal integral curve takes its prescribed initial value.

theorem IsMIntegralCurveOn.eqOn_maximalIntegralCurve {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 : ℝ} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hγ : IsMIntegralCurveOn γ v (Set.Ioo a b)) (h0 : 0 ∈ Set.Ioo a b) (hx : γ 0 = x) : Set.EqOn (maximalIntegralCurve v x) γ (Set.Ioo a b)

The maximal integral curve extends every integral curve through x. An integral curve of v on an open interval around 0 taking the value x at time 0 is the restriction of maximalIntegralCurve v x to that interval.

theorem IsMIntegralCurveOn.eqOn_maximalIntegralCurve_Ioi {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 : ℝ} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hγ : IsMIntegralCurveOn γ v (Set.Ioi a)) (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (ha : a < 0) (hx : γ 0 = x) : Set.EqOn (maximalIntegralCurve v x) γ (Set.Ioi a)

On an open forward ray containing zero, a prescribed integral curve agrees with the maximal curve with the same initial value.

theorem IsMIntegralCurveOn.eqOn_maximalIntegralCurve_Ici {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 : ℝ} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hγ : IsMIntegralCurveOn γ v (Set.Ici a)) (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hb : a < b) : Set.EqOn (maximalIntegralCurve v (γ b)) (γ ∘ fun (x : ℝ) => x + b) (Set.Ioi (a - b))

A prescribed curve on a closed forward ray agrees in its interior with the maximal curve through any chosen interior time, after translating the time parameter.

theorem IsMIntegralCurveOn.mapsTo_maximalIntegralCurve_Ici {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 : ℝ} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hγ : IsMIntegralCurveOn γ v (Set.Ici a)) (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hb : a < b) {S : Set M} (hmem : Set.MapsTo γ (Set.Ici a) S) : Set.MapsTo (maximalIntegralCurve v (γ b)) (Set.Ici 0) S

A set containing a prescribed curve on a closed forward ray also contains the forward maximal curve through any of its interior points.

theorem IsMIntegralCurveOn.tendsto_maximalIntegralCurve_iff {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 : ℝ} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hγ : IsMIntegralCurveOn γ v (Set.Ici a)) (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hb : a < b) {p : M} : Filter.Tendsto (maximalIntegralCurve v (γ b)) Filter.atTop (nhds p) ↔ Filter.Tendsto γ Filter.atTop (nhds p)

A curve on a closed forward ray has the same limit at positive infinity as the maximal curve through any of its interior points.

theorem isMIntegralCurveOn_maximalIntegralCurve {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} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) : IsMIntegralCurveOn (maximalIntegralCurve v x) v (maximalIntegralCurveInterval v x)

The maximal integral curve is an integral curve of v on the maximal interval of existence.

theorem TauCeti.isMIntegralCurve_maximalIntegralCurve_of_eq_univ {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} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (h : maximalIntegralCurveInterval v x = Set.univ) : IsMIntegralCurve (maximalIntegralCurve v x) v

If the maximal interval of existence is all of ℝ, the maximal integral curve is a global integral curve of v.

theorem IsMIntegralCurve.maximalIntegralCurve_eq {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} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hγ : IsMIntegralCurve γ v) (t : ℝ) : maximalIntegralCurve v (γ 0) t = γ t

A global integral curve is the maximal integral curve through its initial point.

theorem not_mapClusterPt_nhdsLT_maximalIntegralCurve {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} {b : ℝ} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] [CompleteSpace E] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hb : IsLUB (maximalIntegralCurveInterval v x) b) (y : M) : ¬MapClusterPt y (nhdsWithin b (Set.Iio b)) (maximalIntegralCurve v x)

A maximal integral curve has no cluster point at a finite right endpoint. If the maximal interval of existence is bounded above, with least upper bound b, then maximalIntegralCurve v x does not accumulate at any point of M as t → b⁻.

The finite-endpoint extension criterion would otherwise extend the curve past b, and the extension would put times beyond b in the maximal interval. This is the form in which metric completeness is turned into completeness of the field: a limit of the curve at a finite endpoint is exactly what the criterion forbids.

theorem eventually_notMem_nhdsLT_maximalIntegralCurve {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} {b : ℝ} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] [CompleteSpace E] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hb : IsLUB (maximalIntegralCurveInterval v x) b) {K : Set M} (hK : IsCompact K) : ∀ᶠ (t : ℝ) in nhdsWithin b (Set.Iio b), maximalIntegralCurve v x t ∉ K

The escape lemma for the maximal integral curve at a finite right endpoint. If the maximal interval of existence is bounded above, with least upper bound b, the maximal integral curve leaves every compact set as t → b⁻.

theorem not_mapClusterPt_nhdsGT_maximalIntegralCurve {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} {a : ℝ} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] [CompleteSpace E] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (ha : IsGLB (maximalIntegralCurveInterval v x) a) (y : M) : ¬MapClusterPt y (nhdsWithin a (Set.Ioi a)) (maximalIntegralCurve v x)

A maximal integral curve has no cluster point at a finite left endpoint. If the maximal interval of existence is bounded below, with greatest lower bound a, then maximalIntegralCurve v x does not accumulate at any point of M as t → a⁺.

theorem eventually_notMem_nhdsGT_maximalIntegralCurve {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} {a : ℝ} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] [CompleteSpace E] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (ha : IsGLB (maximalIntegralCurveInterval v x) a) {K : Set M} (hK : IsCompact K) : ∀ᶠ (t : ℝ) in nhdsWithin a (Set.Ioi a), maximalIntegralCurve v x t ∉ K

The escape lemma for the maximal integral curve at a finite left endpoint. If the maximal interval of existence is bounded below, with greatest lower bound a, the maximal integral curve leaves every compact set as t → a⁺.

theorem maximalIntegralCurveInterval_eq_univ_of_not_bddAbove_not_bddBelow {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} {x : M} (hup : ¬BddAbove (maximalIntegralCurveInterval v x)) (hlow : ¬BddBelow (maximalIntegralCurveInterval v x)) : maximalIntegralCurveInterval v x = Set.univ

The maximal interval of existence is all of ℝ once it is unbounded on both sides. It is an interval containing 0, so unboundedness in both directions leaves no time out.

theorem Ici_subset_maximalIntegralCurveInterval_of_isCompact_of_mapsTo {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} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] [CompleteSpace E] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) {K : Set M} (hK : IsCompact K) (hmem : Set.MapsTo (maximalIntegralCurve v x) (maximalIntegralCurveInterval v x ∩ Set.Ici 0) K) : Set.Ici 0 ⊆ maximalIntegralCurveInterval v x

A maximal integral curve whose forward part is confined to a compact set is defined for all positive time. A finite right endpoint of the maximal interval is impossible, since the escape lemma would force the curve out of the compact set just before it.

theorem maximalIntegralCurveInterval_eq_univ_of_isCompact_of_mapsTo {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} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] [CompleteSpace E] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) {K : Set M} (hK : IsCompact K) (hmem : Set.MapsTo (maximalIntegralCurve v x) (maximalIntegralCurveInterval v x) K) : maximalIntegralCurveInterval v x = Set.univ

A maximal integral curve confined to a compact set is defined for all time. Neither endpoint of the maximal interval can be finite, since the escape lemma would force the curve out of the compact set there.

theorem isMIntegralCurve_maximalIntegralCurve {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} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] [CompactSpace M] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) : IsMIntegralCurve (maximalIntegralCurve v x) v

A C^1 vector field on a compact boundaryless manifold is complete: its maximal integral curve through any point is defined for all time.

theorem maximalIntegralCurveInterval_eq_univ_iff {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} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) : maximalIntegralCurveInterval v x = Set.univ ↔ ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v

The maximal interval of existence is all of ℝ exactly when a global integral curve of v passes through x at time 0. This is the form in which completeness of the field at a point is stated.