Uniform time lemma for the global existence of integral curves

Main results

• exists_isIntegralCurve_of_isIntegralCurveOn: If there exists ε > 0 such that the local integral curve at each point x : M is defined at least on an open interval Ioo (-ε) ε, then every point on M has a global integral curve passing through it.

Reference

• Lee, J. M. (2012). Introduction to Smooth Manifolds. Springer New York.

Tags

integral curve, vector field, global existence

theorem eqOn_of_isIntegralCurveOn_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] [SmoothManifoldWithCorners I M] [T2Space M] {v : (x : M) → TangentSpace I x} [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) {x : M} (γ : ℝ → ℝ → M) (hγx : ∀ (a : ℝ), γ a 0 = x) (hγ : ∀ a > 0, IsIntegralCurveOn (γ a) v (Set.Ioo (-a) a)) {a a' : ℝ} (hpos : 0 < a') (hle : a' ≤ a) : Set.EqOn (γ a') (γ a) (Set.Ioo (-a') a')

This is the uniqueness theorem of integral curves applied to a real-indexed family of integral curves with the same starting point.

theorem eqOn_abs_add_one_of_isIntegralCurveOn_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] [SmoothManifoldWithCorners I M] [T2Space M] {v : (x : M) → TangentSpace I x} [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) {x : M} (γ : ℝ → ℝ → M) (hγx : ∀ (a : ℝ), γ a 0 = x) (hγ : ∀ a > 0, IsIntegralCurveOn (γ a) v (Set.Ioo (-a) a)) {a : ℝ} : Set.EqOn (fun (t : ℝ) => γ (|t| + 1) t) (γ a) (Set.Ioo (-a) a)

For a family of integral curves γ : ℝ → ℝ → M with the same starting point γ 0 = x such that each γ a is defined on Ioo (-a) a, the global curve γ_ext := fun t ↦ γ (|t| + 1) t agrees with each γ a on Ioo (-a) a. This will help us show that γ_ext is a global integral curve.

theorem isIntegralCurve_abs_add_one_of_isIntegralCurveOn_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] [SmoothManifoldWithCorners I M] [T2Space M] {v : (x : M) → TangentSpace I x} [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) {x : M} (γ : ℝ → ℝ → M) (hγx : ∀ (a : ℝ), γ a 0 = x) (hγ : ∀ a > 0, IsIntegralCurveOn (γ a) v (Set.Ioo (-a) a)) : IsIntegralCurve (fun (t : ℝ) => γ (|t| + 1) t) v

For a family of integral curves γ : ℝ → ℝ → M with the same starting point γ 0 = x such that each γ a is defined on Ioo (-a) a, the function γ_ext := fun t ↦ γ (|t| + 1) t is a global integral curve.

theorem exists_isIntegralCurve_iff_exists_isIntegralCurveOn_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] [SmoothManifoldWithCorners I M] [T2Space M] {v : (x : M) → TangentSpace I x} [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) (x : M) : (∃ (γ : ℝ → M), γ 0 = x ∧ IsIntegralCurve γ v) ↔ ∀ (a : ℝ), ∃ (γ : ℝ → M), γ 0 = x ∧ IsIntegralCurveOn γ v (Set.Ioo (-a) a)

The existence of a global integral curve is equivalent to the existence of a family of local integral curves γ : ℝ → ℝ → M with the same starting point γ 0 = x such that each γ a is defined on Ioo (-a) a.

theorem eqOn_piecewise_of_isIntegralCurveOn_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] [SmoothManifoldWithCorners I M] [T2Space M] {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ} [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) {a b a' b' : ℝ} (hγ : IsIntegralCurveOn γ v (Set.Ioo a b)) (hγ' : IsIntegralCurveOn γ' v (Set.Ioo a' b')) (ht₀ : t₀ ∈ Set.Ioo a b ∩ Set.Ioo a' b') (h : γ t₀ = γ' t₀) : Set.EqOn ((Set.Ioo a b).piecewise γ γ') γ' (Set.Ioo a' b')

Let γ and γ' be integral curves defined on Ioo a b and Ioo a' b', respectively. Then, piecewise (Ioo a b) γ γ' is equal to γ and γ' in their respective domains. Set.piecewise_eqOn shows the equality for γ by definition, while this lemma shows the equality for γ' by the uniqueness of integral curves.

theorem isIntegralCurveOn_piecewise {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] [SmoothManifoldWithCorners I M] [T2Space M] {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) {a b a' b' : ℝ} (hγ : IsIntegralCurveOn γ v (Set.Ioo a b)) (hγ' : IsIntegralCurveOn γ' v (Set.Ioo a' b')) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioo a b ∩ Set.Ioo a' b') (h : γ t₀ = γ' t₀) : IsIntegralCurveOn ((Set.Ioo a b).piecewise γ γ') v (Set.Ioo a b ∪ Set.Ioo a' b')

The extension of an integral curve by another integral curve is an integral curve.

If two integral curves are defined on overlapping open intervals, and they agree at a point in their common domain, then they can be patched together to form a longer integral curve.

This is stated for manifolds without boundary for simplicity. We actually only need to assume that the images of γ and γ' lie in the interior of the manifold. TODO: Generalise to manifolds with boundary.

theorem exists_isIntegralCurve_of_isIntegralCurveOn {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] [SmoothManifoldWithCorners I M] [T2Space M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) {ε : ℝ} (hε : 0 < ε) (h : ∀ (x : M), ∃ (γ : ℝ → M), γ 0 = x ∧ IsIntegralCurveOn γ v (Set.Ioo (-ε) ε)) (x : M) : ∃ (γ : ℝ → M), γ 0 = x ∧ IsIntegralCurve γ v

If there exists ε > 0 such that the local integral curve at each point x : M is defined at least on an open interval Ioo (-ε) ε, then every point on M has a global integral curve passing through it.

See Lemma 9.15, J.M. Lee (2012).