Translation and scaling of integral curves #
New integral curves may be constructed by translating or scaling the domain of an existing integral curve.
Reference #
Tags #
integral curve, vector field
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]
{γ : ℝ → M}
{v : (x : M) → TangentSpace I x}
{s : Set ℝ}
(hγ : IsIntegralCurveOn γ v s)
(dt : ℝ)
:
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]
{γ : ℝ → M}
{v : (x : M) → TangentSpace I x}
{s : Set ℝ}
{dt : ℝ}
:
IsIntegralCurveOn γ v s ↔ IsIntegralCurveOn (γ ∘ fun (x : ℝ) => x + dt) v (-dt +ᵥ s)
theorem
isIntegralCurveOn_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 : ℝ}
:
IsIntegralCurveOn γ v s ↔ IsIntegralCurveOn (γ ∘ fun (x : ℝ) => x - dt) v (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]
{γ : ℝ → 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]
{γ : ℝ → M}
{v : (x : M) → TangentSpace I x}
{t₀ dt : ℝ}
:
IsIntegralCurveAt γ v t₀ ↔ IsIntegralCurveAt (γ ∘ fun (x : ℝ) => x + dt) v (t₀ - dt)
theorem
isIntegralCurveAt_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 : ℝ}
:
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]
{γ : ℝ → 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]
{γ : ℝ → M}
{v : (x : M) → TangentSpace I x}
{dt : ℝ}
:
IsIntegralCurve γ v ↔ IsIntegralCurve (γ ∘ fun (x : ℝ) => x + dt) v
theorem
isIntegralCurve_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 : ℝ}
:
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]
{γ : ℝ → M}
{v : (x : M) → TangentSpace I x}
{s : Set ℝ}
(hγ : IsIntegralCurveOn γ v s)
(a : ℝ)
:
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]
{γ : ℝ → 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]
{γ : ℝ → M}
{v : (x : M) → TangentSpace I x}
{t₀ : ℝ}
(hγ : IsIntegralCurveAt γ v t₀)
{a : ℝ}
(ha : a ≠ 0)
:
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]
{γ : ℝ → 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]
{γ : ℝ → 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]
{γ : ℝ → 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]
{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.