Documentation

Mathlib.Geometry.Manifold.IntegralCurve

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 .

Main definitions #

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

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.

Main results #

Implementation notes #

For the existence and uniqueness theorems, we assume that the image of the integral curve lies in the interior of the manifold. The case where the integral curve may lie on the boundary of the manifold requires special treatment, and we leave it as a TODO.

We state simpler versions of the theorem for boundaryless manifolds as corollaries.

TODO #

Reference #

Tags #

integral curve, vector field, local existence, uniqueness

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] [SmoothManifoldWithCorners I 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
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] [SmoothManifoldWithCorners I 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
    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] [SmoothManifoldWithCorners I 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
      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] [SmoothManifoldWithCorners I M] {γ : M} {v : (x : M) → TangentSpace I x} (h : IsIntegralCurve γ v) (s : Set ) :
        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] [SmoothManifoldWithCorners I M] {γ : M} {v : (x : M) → TangentSpace I x} {t₀ : } :
        IsIntegralCurveAt γ v t₀ snhds 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] [SmoothManifoldWithCorners I 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] [SmoothManifoldWithCorners I M] {γ : M} {v : (x : M) → TangentSpace I x} (h : IsIntegralCurve γ 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] [SmoothManifoldWithCorners I 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] [SmoothManifoldWithCorners I M] {γ : M} {v : (x : M) → TangentSpace I x} {s : Set } {s' : Set } (h : IsIntegralCurveOn γ v s) (hs : s' 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] [SmoothManifoldWithCorners I M] {γ : M} {v : (x : M) → TangentSpace I x} {s : Set } {s' : Set } (h : IsIntegralCurveOn γ v s) (h' : IsIntegralCurveOn γ v 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] [SmoothManifoldWithCorners I M] {γ : M} {v : (x : M) → TangentSpace I x} {t₀ : } (h : IsIntegralCurveAt γ 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] [SmoothManifoldWithCorners I M] {γ : M} {v : (x : M) → TangentSpace I x} {s : Set } {t₀ : } (h : IsIntegralCurveOn γ v s) (hs : s nhds 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] [SmoothManifoldWithCorners I M] {γ : M} {v : (x : M) → TangentSpace I x} {s : Set } (h : ts, IsIntegralCurveAt γ v t) :

        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] [SmoothManifoldWithCorners I M] {γ : M} {v : (x : M) → TangentSpace I x} {s : Set } (hs : IsOpen s) :
        IsIntegralCurveOn γ v s ts, 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] [SmoothManifoldWithCorners I 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] [SmoothManifoldWithCorners I M] {γ : M} {v : (x : M) → TangentSpace I x} {s : Set } (hγ : IsIntegralCurveOn γ v 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] [SmoothManifoldWithCorners I 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] [SmoothManifoldWithCorners I 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] [SmoothManifoldWithCorners I M] {γ : M} {v : (x : M) → TangentSpace I x} {s : Set } {t₀ : } (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] [SmoothManifoldWithCorners I M] {γ : M} {v : (x : M) → TangentSpace I x} {t₀ : } (hγ : IsIntegralCurveAt γ v t₀) :
        ∀ᶠ (t : ) in nhds t₀, HasDerivAt ((extChartAt I (γ t₀)) γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) t

        Translation lemmas #

        theorem IsIntegralCurveOn.comp_add {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] {γ : M} {v : (x : M) → TangentSpace I x} {s : Set } (hγ : IsIntegralCurveOn γ v s) (dt : ) :
        IsIntegralCurveOn (γ fun (x : ) => x + dt) v {t : | t + dt s}
        theorem isIntegralCurveOn_comp_add {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] {γ : M} {v : (x : M) → TangentSpace I x} {s : Set } {dt : } :
        IsIntegralCurveOn γ v s IsIntegralCurveOn (γ fun (x : ) => x + dt) v {t : | t + dt s}
        theorem IsIntegralCurveAt.comp_add {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] {γ : M} {v : (x : M) → TangentSpace I x} {t₀ : } (hγ : IsIntegralCurveAt γ v t₀) (dt : ) :
        IsIntegralCurveAt (γ fun (x : ) => x + dt) v (t₀ - dt)
        theorem isIntegralCurveAt_comp_add {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] {γ : M} {v : (x : M) → TangentSpace I x} {t₀ : } {dt : } :
        IsIntegralCurveAt γ v t₀ IsIntegralCurveAt (γ fun (x : ) => x + dt) v (t₀ - dt)
        theorem IsIntegralCurve.comp_add {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] {γ : M} {v : (x : M) → TangentSpace I x} (hγ : IsIntegralCurve γ v) (dt : ) :
        IsIntegralCurve (γ fun (x : ) => x + dt) v
        theorem isIntegralCurve_comp_add {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] {γ : M} {v : (x : M) → TangentSpace I x} {dt : } :
        IsIntegralCurve γ v IsIntegralCurve (γ fun (x : ) => x + dt) v

        Scaling lemmas #

        theorem IsIntegralCurveOn.comp_mul {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] {γ : M} {v : (x : M) → TangentSpace I x} {s : Set } (hγ : IsIntegralCurveOn γ v s) (a : ) :
        IsIntegralCurveOn (γ fun (x : ) => x * a) (a v) {t : | t * a s}
        theorem isIntegralCurveOn_comp_mul_ne_zero {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] {γ : M} {v : (x : M) → TangentSpace I x} {s : Set } {a : } (ha : a 0) :
        IsIntegralCurveOn γ v s IsIntegralCurveOn (γ fun (x : ) => x * a) (a v) {t : | t * a s}
        theorem IsIntegralCurveAt.comp_mul_ne_zero {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] {γ : M} {v : (x : M) → TangentSpace I x} {t₀ : } (hγ : IsIntegralCurveAt γ v t₀) {a : } (ha : a 0) :
        IsIntegralCurveAt (γ fun (x : ) => x * a) (a v) (t₀ / a)
        theorem isIntegralCurveAt_comp_mul_ne_zero {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] {γ : M} {v : (x : M) → TangentSpace I x} {t₀ : } {a : } (ha : a 0) :
        IsIntegralCurveAt γ v t₀ IsIntegralCurveAt (γ fun (x : ) => x * a) (a v) (t₀ / a)
        theorem IsIntegralCurve.comp_mul {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] {γ : M} {v : (x : M) → TangentSpace I x} (hγ : IsIntegralCurve γ v) (a : ) :
        IsIntegralCurve (γ fun (x : ) => x * a) (a v)
        theorem isIntegralCurve_comp_mul_ne_zero {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] {γ : M} {v : (x : M) → TangentSpace I x} {a : } (ha : a 0) :
        IsIntegralCurve γ v IsIntegralCurve (γ fun (x : ) => x * a) (a v)
        theorem isIntegralCurve_const {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] {v : (x : M) → TangentSpace I x} {x : M} (h : v x = 0) :
        IsIntegralCurve (fun (x_1 : ) => x) v

        If the vector field v vanishes at x₀, then the constant curve at x₀ is a global integral curve of v.

        Existence and uniqueness #

        theorem exists_isIntegralCurveAt_of_contMDiffAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {v : (x : M) → TangentSpace I x} (t₀ : ) {x₀ : M} (hv : ContMDiffAt I I.tangent 1 (fun (x : M) => { proj := x, snd := v x }) x₀) (hx : I.IsInteriorPoint x₀) :
        ∃ (γ : M), γ t₀ = x₀ IsIntegralCurveAt γ v t₀

        Existence of local integral curves for a $C^1$ vector field at interior points of a smooth manifold.

        theorem exists_isIntegralCurveAt_of_contMDiffAt_boundaryless {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {v : (x : M) → TangentSpace I x} (t₀ : ) {x₀ : M} [BoundarylessManifold I M] (hv : ContMDiffAt I I.tangent 1 (fun (x : M) => { proj := x, snd := v x }) x₀) :
        ∃ (γ : M), γ t₀ = x₀ IsIntegralCurveAt γ v t₀

        Existence of local integral curves for a $C^1$ vector field on a smooth manifold without boundary.

        theorem isIntegralCurveAt_eventuallyEq_of_contMDiffAt {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] {γ : M} {γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } (hγt₀ : I.IsInteriorPoint (γ t₀)) (hv : ContMDiffAt I I.tangent 1 (fun (x : M) => { proj := x, snd := v x }) (γ t₀)) (hγ : IsIntegralCurveAt γ v t₀) (hγ' : IsIntegralCurveAt γ' v t₀) (h : γ t₀ = γ' t₀) :
        γ =ᶠ[nhds t₀] γ'

        Local integral curves are unique.

        If a $C^1$ vector field v admits two local integral curves γ γ' : ℝ → M at t₀ with γ t₀ = γ' t₀, then γ and γ' agree on some open interval containing t₀.

        theorem isIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless {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] {γ : M} {γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } [BoundarylessManifold I M] (hv : ContMDiffAt I I.tangent 1 (fun (x : M) => { proj := x, snd := v x }) (γ t₀)) (hγ : IsIntegralCurveAt γ v t₀) (hγ' : IsIntegralCurveAt γ' v t₀) (h : γ t₀ = γ' t₀) :
        γ =ᶠ[nhds t₀] γ'
        theorem isIntegralCurveOn_Ioo_eqOn_of_contMDiff {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] {γ : M} {γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } [T2Space M] {a : } {b : } (ht₀ : t₀ Set.Ioo a b) (hγt : tSet.Ioo a b, I.IsInteriorPoint (γ t)) (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) (hγ : IsIntegralCurveOn γ v (Set.Ioo a b)) (hγ' : IsIntegralCurveOn γ' v (Set.Ioo a b)) (h : γ t₀ = γ' t₀) :
        Set.EqOn γ γ' (Set.Ioo a b)

        Integral curves are unique on open intervals.

        If a $C^1$ vector field v admits two integral curves γ γ' : ℝ → M on some open interval Ioo a b, and γ t₀ = γ' t₀ for some t ∈ Ioo a b, then γ and γ' agree on Ioo a b.

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

        Global integral curves are unique.

        If a continuously differentiable vector field v admits two global integral curves γ γ' : ℝ → M, and γ t₀ = γ' t₀ for some t₀, then γ and γ' are equal.

        theorem isIntegralCurve_Ioo_eq_of_contMDiff_boundaryless {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] {γ : M} {γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } [T2Space M] [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) (hγ : IsIntegralCurve γ v) (hγ' : IsIntegralCurve γ' v) (h : γ t₀ = γ' t₀) :
        γ = γ'
        theorem IsIntegralCurve.periodic_of_eq {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] {γ : M} {v : (x : M) → TangentSpace I x} [T2Space M] {a : } {b : } [BoundarylessManifold I M] (hγ : IsIntegralCurve γ v) (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) (heq : γ a = γ b) :

        For a global integral curve γ, if it crosses itself at a b : ℝ, then it is periodic with period a - b.

        theorem IsIntegralCurve.periodic_xor_injective {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] {γ : M} {v : (x : M) → TangentSpace I x} [T2Space M] [BoundarylessManifold I M] (hγ : IsIntegralCurve γ v) (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) :

        A global integral curve is injective xor periodic with positive period.