Integral curves of vector fields on a normed vector space

Let E be a normed vector space and v : ℝ → E → E be a time-dependent vector field on E. An integral curve of v is a function γ : ℝ → E such that the derivative of γ at t equals v t (γ t). The integral curve may only be defined for all t within some subset of ℝ.

Main definitions

Let v : ℝ → E → E be a time-dependent vector field on E, and let γ : ℝ → E.

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

TODO

• Implement IsIntegralCurveWithinAt.

Tags

integral curve, vector field

def IsIntegralCurveOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (γ : ℝ → E) (v : ℝ → E → E) (s : Set ℝ) : Prop

IsIntegralCurveOn γ v s means γ t is tangent to v t (γ t) within s for all t ∈ s.

def IsIntegralCurveAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (γ : ℝ → E) (v : ℝ → E → E) (t₀ : ℝ) : Prop

IsIntegralCurveAt γ v t₀ means γ : ℝ → E is a local integral curve of v in a neighbourhood containing t₀.

def IsIntegralCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (γ : ℝ → E) (v : ℝ → E → E) : Prop

IsIntegralCurve γ v means γ : ℝ → E is a global integral curve of v. That is, γ t is tangent to v t (γ t) for all t : ℝ.

theorem IsIntegralCurve.isIntegralCurveOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} (h : IsIntegralCurve γ v) (s : Set ℝ) : IsIntegralCurveOn γ v s

theorem isIntegralCurveOn_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} : IsIntegralCurveOn γ v Set.univ ↔ IsIntegralCurve γ v

theorem isIntegralCurveAt_iff_exists_mem_nhds {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ : ℝ} : IsIntegralCurveAt γ v t₀ ↔ ∃ s ∈ nhds t₀, IsIntegralCurveOn γ v s

theorem isIntegralCurveAt_iff_exists_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {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] {γ : ℝ → E} {v : ℝ → E → E} (h : IsIntegralCurve γ v) (t : ℝ) : IsIntegralCurveAt γ v t

theorem isIntegralCurve_iff_isIntegralCurveAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} : IsIntegralCurve γ v ↔ ∀ (t : ℝ), IsIntegralCurveAt γ v t

theorem IsIntegralCurveOn.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s s' : Set ℝ} (h : IsIntegralCurveOn γ v s) (hs : s' ⊆ s) : IsIntegralCurveOn γ v s'

theorem IsIntegralCurveAt.hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ : ℝ} (h : IsIntegralCurveAt γ v t₀) : HasDerivAt γ (v t₀ (γ t₀)) t₀

theorem IsIntegralCurveOn.isIntegralCurveAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {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] {γ : ℝ → E} {v : ℝ → E → E} {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] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ} (hs : IsOpen s) : IsIntegralCurveOn γ v s ↔ ∀ t ∈ s, IsIntegralCurveAt γ v t

theorem IsIntegralCurveOn.continuousWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ} {t₀ : ℝ} (hγ : IsIntegralCurveOn γ v s) (ht : t₀ ∈ s) : ContinuousWithinAt γ s t₀

theorem IsIntegralCurveOn.continuousOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ} (hγ : IsIntegralCurveOn γ v s) : ContinuousOn γ s

theorem IsIntegralCurveAt.continuousAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ : ℝ} (hγ : IsIntegralCurveAt γ v t₀) : ContinuousAt γ t₀

theorem IsIntegralCurve.continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} (hγ : IsIntegralCurve γ v) : Continuous γ