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.

• IsIntegralCurve γ v: γ t is tangent to v (γ t) for all t : ℝ. That is, γ is a global integral curve of v.
• IsIntegralCurveOn γ v s: γ t is tangent to v (γ t) for all t ∈ s, where s : Set ℝ.
• IsIntegralCurveAt γ 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 IsIntegralCurveOn γ v s and IsIntegralCurveAt γ 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.

Reference

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

Tags

integral curve, vector field

def 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] (γ : ℝ → 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, IsIntegralCurveOn γ v s means γ t is tangent to v (γ t) for all t ∈ s. The value of γ outside of s is irrelevant and considered junk.

Equations

• IsIntegralCurveOn γ v s = ∀ t ∈ s, HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))

def IsIntegralCurveAt {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₀ : ℝ, IsIntegralCurveAt γ 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.

Equations

• IsIntegralCurveAt γ v t₀ = ∀ᶠ (t : ℝ) in nhds t₀, HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))

def IsIntegralCurve {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, IsIntegralCurve γ v means γ : ℝ → M is a global integral curve of v. That is, γ t is tangent to v (γ t) for all t : ℝ.

Equations

• IsIntegralCurve γ v = ∀ (t : ℝ), HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))

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

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

theorem isIntegralCurveAt_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₀ : ℝ} : IsIntegralCurveAt γ v t₀ ↔ ∃ s ∈ nhds t₀, IsIntegralCurveOn γ v s

theorem isIntegralCurveAt_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₀ : ℝ} : IsIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)

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

theorem IsIntegralCurve.isIntegralCurveAt {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 : IsIntegralCurve γ v) (t : ℝ) : IsIntegralCurveAt γ v t

theorem isIntegralCurve_iff_isIntegralCurveAt {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} : IsIntegralCurve γ v ↔ ∀ (t : ℝ), IsIntegralCurveAt γ v t

theorem IsIntegralCurveOn.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 : IsIntegralCurveOn γ v s) (hs : s' ⊆ s) : IsIntegralCurveOn γ v s'

theorem IsIntegralCurveOn.of_union {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 : IsIntegralCurveOn γ v s) (h' : IsIntegralCurveOn γ v s') : IsIntegralCurveOn γ v (s ∪ s')

theorem IsIntegralCurveAt.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 : IsIntegralCurveAt γ v t₀) : HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I γ t₀ (ContinuousLinearMap.smulRight 1 (v (γ t₀)))

theorem IsIntegralCurveOn.isIntegralCurveAt {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 : IsIntegralCurveOn γ v s) (hs : s ∈ nhds t₀) : IsIntegralCurveAt γ v t₀

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

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

theorem isIntegralCurveOn_iff_isIntegralCurveAt {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) : IsIntegralCurveOn γ v s ↔ ∀ t ∈ s, IsIntegralCurveAt γ v t

theorem IsIntegralCurveOn.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} {s : Set ℝ} {t₀ : ℝ} (hγ : IsIntegralCurveOn γ v s) (ht : t₀ ∈ s) : ContinuousAt γ t₀

theorem IsIntegralCurveOn.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γ : IsIntegralCurveOn γ v s) : ContinuousOn γ s

theorem IsIntegralCurveAt.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γ : IsIntegralCurveAt γ v t₀) : ContinuousAt γ t₀

theorem IsIntegralCurve.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γ : IsIntegralCurve γ v) : Continuous γ

theorem IsIntegralCurveOn.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} {s : Set ℝ} {t₀ : ℝ} [IsManifold I 1 M] (hγ : IsIntegralCurveOn γ v s) {t : ℝ} (ht : t ∈ s) (hsrc : γ t ∈ (extChartAt I (γ t₀)).source) : HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) 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 IsIntegralCurveAt.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γ : IsIntegralCurveAt γ v t₀) : ∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) t