Documentation

Mathlib.Geometry.Manifold.IntegralCurve.Basic

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 ℝ) :

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.

Equations

Instances For

@[deprecated IsMIntegralCurveOn (since := "2025-08-12")]

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 ℝ) :

Alias of IsMIntegralCurveOn.

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.

Equations

Instances For

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₀ : ℝ) :

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.

Equations

Instances For

@[deprecated IsMIntegralCurveAt (since := "2025-08-12")]

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₀ : ℝ) :

Alias of IsMIntegralCurveAt.

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.

Equations

Instances For

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) :

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 : ℝ.

Equations

Instances For

@[deprecated IsMIntegralCurve (since := "2025-08-12")]

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) :

Alias of IsMIntegralCurve.

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 : ℝ.

Equations

Instances For

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

@[deprecated IsMIntegralCurve.isMIntegralCurveOn (since := "2025-08-12")]

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 : IsMIntegralCurve γ v) (s : Set ℝ) :

IsMIntegralCurveOn γ v s

Alias of IsMIntegralCurve.isMIntegralCurveOn.

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

@[deprecated isMIntegralCurve_iff_isMIntegralCurveOn (since := "2025-08-12")]

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} :

IsMIntegralCurve γ v ↔ IsMIntegralCurveOn γ v Set.univ

Alias of isMIntegralCurve_iff_isMIntegralCurveOn.

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

@[deprecated isMIntegralCurveAt_iff (since := "2025-08-12")]

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₀ : ℝ} :

IsMIntegralCurveAt γ v t₀ ↔ ∃ s ∈ nhds t₀, IsMIntegralCurveOn γ v s

Alias of isMIntegralCurveAt_iff.

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₀.

@[deprecated isMIntegralCurveAt_iff' (since := "2025-08-12")]

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₀ : ℝ} :

IsMIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)

Alias of isMIntegralCurveAt_iff'.

γ 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

@[deprecated IsMIntegralCurve.isMIntegralCurveAt (since := "2025-08-12")]

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 : IsMIntegralCurve γ v) (t : ℝ) :

IsMIntegralCurveAt γ v t

Alias of IsMIntegralCurve.isMIntegralCurveAt.

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

@[deprecated isMIntegralCurve_iff_isMIntegralCurveAt (since := "2025-08-12")]

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} :

IsMIntegralCurve γ v ↔ ∀ (t : ℝ), IsMIntegralCurveAt γ v t

Alias of isMIntegralCurve_iff_isMIntegralCurveAt.

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'

@[deprecated IsMIntegralCurveOn.mono (since := "2025-08-12")]

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

IsMIntegralCurveOn γ v s'

Alias of IsMIntegralCurveOn.mono.

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₀)))

@[deprecated IsMIntegralCurveAt.hasMFDerivAt (since := "2025-08-12")]

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 : IsMIntegralCurveAt γ v t₀) :

HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I γ t₀ (ContinuousLinearMap.smulRight 1 (v (γ t₀)))

Alias of IsMIntegralCurveAt.hasMFDerivAt.

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₀

@[deprecated IsMIntegralCurveOn.isMIntegralCurveAt (since := "2025-08-12")]

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 : IsMIntegralCurveOn γ v s) (hs : s ∈ nhds t₀) :

IsMIntegralCurveAt γ v t₀

Alias of IsMIntegralCurveOn.isMIntegralCurveAt.

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.

@[deprecated IsMIntegralCurveAt.isMIntegralCurveOn (since := "2025-08-12")]

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, IsMIntegralCurveAt γ v t) :

IsMIntegralCurveOn γ v s

Alias of IsMIntegralCurveAt.isMIntegralCurveOn.

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

@[deprecated isMIntegralCurveOn_iff_isMIntegralCurveAt (since := "2025-08-12")]

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) :

IsMIntegralCurveOn γ v s ↔ ∀ t ∈ s, IsMIntegralCurveAt γ v t

Alias of isMIntegralCurveOn_iff_isMIntegralCurveAt.

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₀

@[deprecated IsMIntegralCurveOn.continuousWithinAt (since := "2025-08-12")]

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γ : IsMIntegralCurveOn γ v s) (ht : t₀ ∈ s) :

ContinuousWithinAt γ s t₀

Alias of IsMIntegralCurveOn.continuousWithinAt.

@[deprecated IsMIntegralCurveOn.continuousWithinAt (since := "2025-08-12")]

theorem IsIntegralCurveOn.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₀

Alias of IsMIntegralCurveOn.continuousWithinAt.

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

@[deprecated IsMIntegralCurveOn.continuousOn (since := "2025-08-12")]

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γ : IsMIntegralCurveOn γ v s) :

ContinuousOn γ s

Alias of IsMIntegralCurveOn.continuousOn.

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₀

@[deprecated IsMIntegralCurveAt.continuousAt (since := "2025-08-12")]

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γ : IsMIntegralCurveAt γ v t₀) :

ContinuousAt γ t₀

Alias of IsMIntegralCurveAt.continuousAt.

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) :

@[deprecated IsMIntegralCurve.continuous (since := "2025-08-12")]

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γ : IsMIntegralCurve γ v) :

Alias of IsMIntegralCurve.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₀.

@[deprecated IsMIntegralCurveOn.hasDerivWithinAt (since := "2025-08-12")]

theorem IsIntegralCurveOn.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

Alias of IsMIntegralCurveOn.hasDerivWithinAt.

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

@[deprecated IsMIntegralCurveAt.eventually_hasDerivAt (since := "2025-08-12")]

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γ : IsMIntegralCurveAt γ v t₀) :

∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) t

Alias of IsMIntegralCurveAt.eventually_hasDerivAt.