Documentation

Mathlib.Geometry.Manifold.IntegralCurve.Transform

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 #

Tags #

integral curve, vector field

Translation lemmas #

source
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}
source
@[deprecated IsMIntegralCurveOn.comp_add (since := "2025-08-12")]
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γ : IsMIntegralCurveOn γ v s) (dt : ℝ) :
IsMIntegralCurveOn (γ ∘ fun (x : ℝ) => x + dt) v {t : ℝ | t + dt ∈ s}

Alias of IsMIntegralCurveOn.comp_add.

source
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 γ v s ↔ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) => x + dt) v {t : ℝ | t + dt ∈ s}
source
@[deprecated isMIntegralCurveOn_comp_add (since := "2025-08-12")]
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 : ℝ} :
IsMIntegralCurveOn γ v s ↔ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) => x + dt) v {t : ℝ | t + dt ∈ s}

Alias of isMIntegralCurveOn_comp_add.

source
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 γ v s ↔ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) => x - dt) v {t : ℝ | t - dt ∈ s}
source
@[deprecated isMIntegralCurveOn_comp_sub (since := "2025-08-12")]
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 : ℝ} :
IsMIntegralCurveOn γ v s ↔ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) => x - dt) v {t : ℝ | t - dt ∈ s}

Alias of isMIntegralCurveOn_comp_sub.

source
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)
source
@[deprecated IsMIntegralCurveAt.comp_add (since := "2025-08-12")]
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γ : IsMIntegralCurveAt γ v t₀) (dt : ℝ) :
IsMIntegralCurveAt (γ ∘ fun (x : ℝ) => x + dt) v (t₀ - dt)

Alias of IsMIntegralCurveAt.comp_add.

source
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 γ v t₀ ↔ IsMIntegralCurveAt (γ ∘ fun (x : ℝ) => x + dt) v (t₀ - dt)
source
@[deprecated isMIntegralCurveAt_comp_add (since := "2025-08-12")]
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 : ℝ} :
IsMIntegralCurveAt γ v t₀ ↔ IsMIntegralCurveAt (γ ∘ fun (x : ℝ) => x + dt) v (t₀ - dt)

Alias of isMIntegralCurveAt_comp_add.

source
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 γ v t₀ ↔ IsMIntegralCurveAt (γ ∘ fun (x : ℝ) => x - dt) v (t₀ + dt)
source
@[deprecated isMIntegralCurveAt_comp_sub (since := "2025-08-12")]
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 : ℝ} :
IsMIntegralCurveAt γ v t₀ ↔ IsMIntegralCurveAt (γ ∘ fun (x : ℝ) => x - dt) v (t₀ + dt)

Alias of isMIntegralCurveAt_comp_sub.

source
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
source
@[deprecated IsMIntegralCurve.comp_add (since := "2025-08-12")]
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γ : IsMIntegralCurve γ v) (dt : ℝ) :
IsMIntegralCurve (γ ∘ fun (x : ℝ) => x + dt) v

Alias of IsMIntegralCurve.comp_add.

source
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 γ v ↔ IsMIntegralCurve (γ ∘ fun (x : ℝ) => x + dt) v
source
@[deprecated isMIntegralCurve_comp_add (since := "2025-08-12")]
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 : ℝ} :
IsMIntegralCurve γ v ↔ IsMIntegralCurve (γ ∘ fun (x : ℝ) => x + dt) v

Alias of isMIntegralCurve_comp_add.

source
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 γ v ↔ IsMIntegralCurve (γ ∘ fun (x : ℝ) => x - dt) v
source
@[deprecated isMIntegralCurve_comp_sub (since := "2025-08-12")]
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 : ℝ} :
IsMIntegralCurve γ v ↔ IsMIntegralCurve (γ ∘ fun (x : ℝ) => x - dt) v

Alias of isMIntegralCurve_comp_sub.

Scaling lemmas #

source
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}
source
@[deprecated IsMIntegralCurveOn.comp_mul (since := "2025-08-12")]
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γ : IsMIntegralCurveOn γ v s) (a : ℝ) :
IsMIntegralCurveOn (γ ∘ fun (x : ℝ) => x * a) (a • v) {t : ℝ | t * a ∈ s}

Alias of IsMIntegralCurveOn.comp_mul.

source
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 γ v s ↔ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) => x * a) (a • v) {t : ℝ | t * a ∈ s}
source
@[deprecated isMIntegralCurveOn_comp_mul_ne_zero (since := "2025-08-12")]
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) :
IsMIntegralCurveOn γ v s ↔ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) => x * a) (a • v) {t : ℝ | t * a ∈ s}

Alias of isMIntegralCurveOn_comp_mul_ne_zero.

source
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)
source
@[deprecated IsMIntegralCurveAt.comp_mul_ne_zero (since := "2025-08-12")]
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γ : IsMIntegralCurveAt γ v t₀) {a : ℝ} (ha : a ≠ 0) :
IsMIntegralCurveAt (γ ∘ fun (x : ℝ) => x * a) (a • v) (t₀ / a)

Alias of IsMIntegralCurveAt.comp_mul_ne_zero.

source
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 γ v t₀ ↔ IsMIntegralCurveAt (γ ∘ fun (x : ℝ) => x * a) (a • v) (t₀ / a)
source
@[deprecated isMIntegralCurveAt_comp_mul_ne_zero (since := "2025-08-12")]
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) :
IsMIntegralCurveAt γ v t₀ ↔ IsMIntegralCurveAt (γ ∘ fun (x : ℝ) => x * a) (a • v) (t₀ / a)

Alias of isMIntegralCurveAt_comp_mul_ne_zero.

source
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)
source
@[deprecated IsMIntegralCurve.comp_mul (since := "2025-08-12")]
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γ : IsMIntegralCurve γ v) (a : ℝ) :
IsMIntegralCurve (γ ∘ fun (x : ℝ) => x * a) (a • v)

Alias of IsMIntegralCurve.comp_mul.

source
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 γ v ↔ IsMIntegralCurve (γ ∘ fun (x : ℝ) => x * a) (a • v)
source
@[deprecated isMIntegralCurve_comp_mul_ne_zero (since := "2025-08-12")]
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) :
IsMIntegralCurve γ v ↔ IsMIntegralCurve (γ ∘ fun (x : ℝ) => x * a) (a • v)

Alias of isMIntegralCurve_comp_mul_ne_zero.

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

source
@[deprecated isMIntegralCurve_const (since := "2025-08-12")]
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) :
IsMIntegralCurve (fun (x_1 : ℝ) => x) v

Alias of isMIntegralCurve_const.

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