Integral curves of vector fields on a manifold

Let M be a manifold and v : (x : M) → TangentSpace I x be a vector field on M. An integral curve of v is a function γ : ℝ → M such that the derivative of γ at t equals v (γ t). The integral curve may only be defined for all t within some subset of ℝ.

This is the first of a series of files, organised as follows:

• Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean (this file): Basic definitions and lemmas relating them to each other and to continuity and differentiability
• Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean: Lemmas about translating or scaling the domain of an integral curve by a constant
• Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean: Local existence and uniqueness theorems for integral curves

Main definitions

Let v : M → TM be a vector field on M, and let γ : ℝ → M.

• IsMIntegralCurve γ v: γ t is tangent to v (γ t) for all t : ℝ. That is, γ is a global integral curve of v.
• IsMIntegralCurveOn γ v s: γ t is tangent to v (γ t) for all t ∈ s, where s : Set ℝ.
• IsMIntegralCurveAt γ v t₀: γ t is tangent to v (γ t) for all t in some open interval around t₀. That is, γ is a local integral curve of v.

For IsMIntegralCurveOn γ v s and IsMIntegralCurveAt γ v t₀, even though γ is defined for all time, its value outside of the set s or a small interval around t₀ is irrelevant and considered junk.

TODO

• Implement IsMIntegralCurveWithinAt.

Reference

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

Tags

integral curve, vector field

def IsMIntegralCurveOn {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] (γ : ℝ → M) (v : (x : M) → TangentSpace I x) (s : Set ℝ) : Prop

If γ : ℝ → M is $C^1$ on s : Set ℝ and v is a vector field on M, IsMIntegralCurveOn γ v s means γ t is tangent to v (γ t) for all t ∈ s. The value of γ outside of s is irrelevant and considered junk.

def IsMIntegralCurveAt {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] (γ : ℝ → M) (v : (x : M) → TangentSpace I x) (t₀ : ℝ) : Prop

If v is a vector field on M and t₀ : ℝ, IsMIntegralCurveAt γ v t₀ means γ : ℝ → M is a local integral curve of v in a neighbourhood containing t₀. The value of γ outside of this interval is irrelevant and considered junk.

def IsMIntegralCurve {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] (γ : ℝ → M) (v : (x : M) → TangentSpace I x) : Prop

If v : M → TM is a vector field on M, IsMIntegralCurve γ v means γ : ℝ → M is a global integral curve of v. That is, γ t is tangent to v (γ t) for all t : ℝ.

theorem IsMIntegralCurve.isMIntegralCurveOn {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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} (h : IsMIntegralCurve γ v) (s : Set ℝ) : IsMIntegralCurveOn γ v s

theorem isMIntegralCurve_iff_isMIntegralCurveOn {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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} : IsMIntegralCurve γ v ↔ IsMIntegralCurveOn γ v Set.univ

theorem isMIntegralCurveAt_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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ} : IsMIntegralCurveAt γ v t₀ ↔ ∃ s ∈ nhds t₀, IsMIntegralCurveOn γ v s

theorem isMIntegralCurveAt_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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ} : IsMIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)

γ is an integral curve for v at t₀ iff γ is an integral curve on some interval containing t₀.

theorem IsMIntegralCurve.isMIntegralCurveAt {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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} (h : IsMIntegralCurve γ v) (t : ℝ) : IsMIntegralCurveAt γ v t

theorem isMIntegralCurve_iff_isMIntegralCurveAt {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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} : IsMIntegralCurve γ v ↔ ∀ (t : ℝ), IsMIntegralCurveAt γ v t

theorem IsMIntegralCurveOn.mono {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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {s s' : Set ℝ} (h : IsMIntegralCurveOn γ v s) (hs : s' ⊆ s) : IsMIntegralCurveOn γ v s'

theorem IsMIntegralCurveAt.hasMFDerivAt {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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ} (h : IsMIntegralCurveAt γ v t₀) : HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I γ t₀ (ContinuousLinearMap.smulRight 1 (v (γ t₀)))

theorem IsMIntegralCurveOn.isMIntegralCurveAt {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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {s : Set ℝ} {t₀ : ℝ} (h : IsMIntegralCurveOn γ v s) (hs : s ∈ nhds t₀) : IsMIntegralCurveAt γ v t₀

theorem IsMIntegralCurveAt.isMIntegralCurveOn {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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {s : Set ℝ} (h : ∀ t ∈ s, IsMIntegralCurveAt γ v t) : IsMIntegralCurveOn γ v s

If γ is an integral curve at each t ∈ s, it is an integral curve on s.

theorem isMIntegralCurveOn_iff_isMIntegralCurveAt {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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {s : Set ℝ} (hs : IsOpen s) : IsMIntegralCurveOn γ v s ↔ ∀ t ∈ s, IsMIntegralCurveAt γ v t

theorem IsMIntegralCurveOn.continuousWithinAt {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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {s : Set ℝ} {t₀ : ℝ} (hγ : IsMIntegralCurveOn γ v s) (ht : t₀ ∈ s) : ContinuousWithinAt γ s t₀

theorem IsMIntegralCurveOn.continuousOn {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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {s : Set ℝ} (hγ : IsMIntegralCurveOn γ v s) : ContinuousOn γ s

theorem IsMIntegralCurveAt.continuousAt {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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ} (hγ : IsMIntegralCurveAt γ v t₀) : ContinuousAt γ t₀

theorem IsMIntegralCurve.continuous {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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} (hγ : IsMIntegralCurve γ v) : Continuous γ

theorem IsMIntegralCurveOn.hasDerivWithinAt {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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {s : Set ℝ} {t₀ : ℝ} [IsManifold I 1 M] (hγ : IsMIntegralCurveOn γ v s) {t : ℝ} (ht : t ∈ s) (hsrc : γ t ∈ (extChartAt I (γ t₀)).source) : HasDerivWithinAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) s t

If γ is an integral curve of a vector field v, then γ t is tangent to v (γ t) when expressed in the local chart around the initial point γ t₀.

theorem IsMIntegralCurveAt.eventually_hasDerivAt {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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ} [IsManifold I 1 M] (hγ : IsMIntegralCurveAt γ v t₀) : ∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) t