Documentation

Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Uniform time lemma for the global existence of integral curves #

Main results #

Reference #

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] [IsManifold I 1 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] [IsManifold I 1 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] [IsManifold I 1 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] [IsManifold I 1 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] [IsManifold I 1 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] [IsManifold I 1 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₀) :

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] [IsManifold I 1 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)][lee2012].