Translation and scaling of integral curves

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

This file mirrors Mathlib/Analysis/ODE/Transform.

Reference

• [Lee, J. M. (2012). Introduction to Smooth Manifolds. Springer New York.][lee2012]

Tags

integral curve, vector field

Translation lemmas

theorem IsMIntegralCurveOn.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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {s : Set ℝ} (hγ : IsMIntegralCurveOn γ v s) (dt : ℝ) : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) => x + dt) v {t : ℝ | t + dt ∈ s}

theorem isMIntegralCurveOn_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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {s : Set ℝ} {dt : ℝ} : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) => x + dt) v {t : ℝ | t + dt ∈ s} ↔ IsMIntegralCurveOn γ v s

theorem isMIntegralCurveOn_comp_sub {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 ℝ} {dt : ℝ} : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) => x - dt) v {t : ℝ | t - dt ∈ s} ↔ IsMIntegralCurveOn γ v s

theorem IsMIntegralCurveAt.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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ} (hγ : IsMIntegralCurveAt γ v t₀) (dt : ℝ) : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) => x + dt) v (t₀ - dt)

theorem isMIntegralCurveAt_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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ dt : ℝ} : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) => x + dt) v (t₀ - dt) ↔ IsMIntegralCurveAt γ v t₀

theorem isMIntegralCurveAt_comp_sub {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₀ dt : ℝ} : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) => x - dt) v (t₀ + dt) ↔ IsMIntegralCurveAt γ v t₀

theorem IsMIntegralCurve.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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} (hγ : IsMIntegralCurve γ v) (dt : ℝ) : IsMIntegralCurve (γ ∘ fun (x : ℝ) => x + dt) v

theorem isMIntegralCurve_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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {dt : ℝ} : IsMIntegralCurve (γ ∘ fun (x : ℝ) => x + dt) v ↔ IsMIntegralCurve γ v

theorem isMIntegralCurve_comp_sub {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} {dt : ℝ} : IsMIntegralCurve (γ ∘ fun (x : ℝ) => x - dt) v ↔ IsMIntegralCurve γ v

Scaling lemmas

theorem IsMIntegralCurveOn.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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {s : Set ℝ} (hγ : IsMIntegralCurveOn γ v s) (a : ℝ) : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) => x * a) (a • v) {t : ℝ | t * a ∈ s}

theorem isMIntegralCurveOn_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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {s : Set ℝ} {a : ℝ} (ha : a ≠ 0) : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) => x * a) (a • v) {t : ℝ | t * a ∈ s} ↔ IsMIntegralCurveOn γ v s

theorem IsMIntegralCurveAt.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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ} (hγ : IsMIntegralCurveAt γ v t₀) {a : ℝ} (ha : a ≠ 0) : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) => x * a) (a • v) (t₀ / a)

theorem isMIntegralCurveAt_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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ a : ℝ} (ha : a ≠ 0) : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) => x * a) (a • v) (t₀ / a) ↔ IsMIntegralCurveAt γ v t₀

theorem IsMIntegralCurve.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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} (hγ : IsMIntegralCurve γ v) (a : ℝ) : IsMIntegralCurve (γ ∘ fun (x : ℝ) => x * a) (a • v)

theorem isMIntegralCurve_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] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {a : ℝ} (ha : a ≠ 0) : IsMIntegralCurve (γ ∘ fun (x : ℝ) => x * a) (a • v) ↔ IsMIntegralCurve γ v

theorem isMIntegralCurve_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] {v : (x : M) → TangentSpace I x} {x : M} (h : v x = 0) : IsMIntegralCurve (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.