Translation and scaling of integral curves

New integral curves may be constructed by translating or scaling the domain of an existing integral curve.

Tags

integral curve, vector field

Translation lemmas

theorem IsIntegralCurveOn.comp_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ} (hγ : IsIntegralCurveOn γ v s) (dt : ℝ) : IsIntegralCurveOn (γ ∘ fun (x : ℝ) => x + dt) (v ∘ fun (x : ℝ) => x + dt) (-dt +ᵥ s)

theorem isIntegralCurveOn_comp_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ} {dt : ℝ} : IsIntegralCurveOn (γ ∘ fun (x : ℝ) => x + dt) (v ∘ fun (x : ℝ) => x + dt) (-dt +ᵥ s) ↔ IsIntegralCurveOn γ v s

theorem isIntegralCurveOn_comp_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ} {dt : ℝ} : IsIntegralCurveOn (γ ∘ fun (x : ℝ) => x - dt) (v ∘ fun (x : ℝ) => x - dt) (dt +ᵥ s) ↔ IsIntegralCurveOn γ v s

theorem IsIntegralCurveOn.comp_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ} (hγ : IsIntegralCurveOn γ v s) (dt : ℝ) : IsIntegralCurveOn (γ ∘ fun (x : ℝ) => x - dt) (v ∘ fun (x : ℝ) => x - dt) (dt +ᵥ s)

theorem isIntegralCurveAt_comp_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ dt : ℝ} : IsIntegralCurveAt (γ ∘ fun (x : ℝ) => x + dt) (v ∘ fun (x : ℝ) => x + dt) (t₀ - dt) ↔ IsIntegralCurveAt γ v t₀

theorem IsIntegralCurveAt.comp_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ : ℝ} (hγ : IsIntegralCurveAt γ v t₀) (dt : ℝ) : IsIntegralCurveAt (γ ∘ fun (x : ℝ) => x + dt) (v ∘ fun (x : ℝ) => x + dt) (t₀ - dt)

theorem isIntegralCurveAt_comp_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ dt : ℝ} : IsIntegralCurveAt (γ ∘ fun (x : ℝ) => x - dt) (v ∘ fun (x : ℝ) => x - dt) (t₀ + dt) ↔ IsIntegralCurveAt γ v t₀

theorem IsIntegralCurveAt.comp_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ : ℝ} (hγ : IsIntegralCurveAt γ v t₀) (dt : ℝ) : IsIntegralCurveAt (γ ∘ fun (x : ℝ) => x - dt) (v ∘ fun (x : ℝ) => x - dt) (t₀ + dt)

theorem IsIntegralCurve.comp_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} (hγ : IsIntegralCurve γ v) (dt : ℝ) : IsIntegralCurve (γ ∘ fun (x : ℝ) => x + dt) (v ∘ fun (x : ℝ) => x + dt)

theorem isIntegralCurve_comp_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {dt : ℝ} : IsIntegralCurve (γ ∘ fun (x : ℝ) => x + dt) (v ∘ fun (x : ℝ) => x + dt) ↔ IsIntegralCurve γ v

theorem isIntegralCurve_comp_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {dt : ℝ} : IsIntegralCurve (γ ∘ fun (x : ℝ) => x - dt) (v ∘ fun (x : ℝ) => x - dt) ↔ IsIntegralCurve γ v

theorem IsIntegralCurve.comp_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} (hγ : IsIntegralCurve γ v) (dt : ℝ) : IsIntegralCurve (γ ∘ fun (x : ℝ) => x - dt) (v ∘ fun (x : ℝ) => x - dt)

Scaling lemmas

theorem IsIntegralCurveOn.comp_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ} (hγ : IsIntegralCurveOn γ v s) (a : ℝ) : IsIntegralCurveOn (γ ∘ fun (x : ℝ) => x * a) (a • v ∘ fun (x : ℝ) => x * a) {t : ℝ | t * a ∈ s}

theorem isIntegralCurveOn_comp_mul_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ} {a : ℝ} (ha : a ≠ 0) : IsIntegralCurveOn (γ ∘ fun (x : ℝ) => x * a) (a • v ∘ fun (x : ℝ) => x * a) (a⁻¹ • s) ↔ IsIntegralCurveOn γ v s

theorem IsIntegralCurveAt.comp_mul_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ : ℝ} (hγ : IsIntegralCurveAt γ v t₀) {a : ℝ} (ha : a ≠ 0) : IsIntegralCurveAt (γ ∘ fun (x : ℝ) => x * a) (a • v ∘ fun (x : ℝ) => x * a) (t₀ / a)

theorem isIntegralCurveAt_comp_mul_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ a : ℝ} (ha : a ≠ 0) : IsIntegralCurveAt (γ ∘ fun (x : ℝ) => x * a) (a • v ∘ fun (x : ℝ) => x * a) (t₀ / a) ↔ IsIntegralCurveAt γ v t₀

theorem IsIntegralCurve.comp_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} (hγ : IsIntegralCurve γ v) (a : ℝ) : IsIntegralCurve (γ ∘ fun (x : ℝ) => x * a) (a • v ∘ fun (x : ℝ) => x * a)

theorem isIntegralCurve_comp_mul_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {a : ℝ} (ha : a ≠ 0) : IsIntegralCurve (γ ∘ fun (x : ℝ) => x * a) (a • v ∘ fun (x : ℝ) => x * a) ↔ IsIntegralCurve γ v

theorem isIntegralCurve_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {x : E} (h : ∀ (t : ℝ), v t x = 0) : IsIntegralCurve (fun (x_1 : ℝ) => x) v

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