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(this file): Basic definitions and lemmas relating them to each other and to continuity and differentiabilityMathlib.Geometry.Manifold.IntegralCurve.Transform: Lemmas about translating or scaling the domain of an integral curve by a constantMathlib.Geometry.Manifold.IntegralCurve.ExistUnique: 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:γ tis tangent tov (γ t)for allt : ℝ. That is,γis a global integral curve ofv.IsIntegralCurveOn γ v s:γ tis tangent tov (γ t)for allt ∈ s, wheres : Set ℝ.IsIntegralCurveAt γ v t₀:γ tis tangent tov (γ t)for alltin some open interval aroundt₀. That is,γis a local integral curve ofv.
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 ℝ)
:
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)))
Instances For
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₀ : ℝ)
:
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)))
Instances For
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)
:
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)))
Instances For
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)
:
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₀ : ℝ}
[SmoothManifoldWithCorners I 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₀ : ℝ}
[SmoothManifoldWithCorners I M]
(hγ : IsIntegralCurveAt γ v t₀)
:
∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) t