Documentation

Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

Existence and uniqueness of integral curves #

Main results #

Implementation notes #

For the existence and uniqueness theorems, we assume that the image of the integral curve lies in the interior of the manifold. The case where the integral curve may lie on the boundary of the manifold requires special treatment, and we leave it as a TODO.

We state simpler versions of the theorem for boundaryless manifolds as corollaries.

TODO #

Reference #

Tags #

integral curve, vector field, local existence, uniqueness

theorem exists_isMIntegralCurveAt_of_contMDiffAt {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] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (t₀ : ) {x₀ : M} [CompleteSpace E] (hv : ContMDiffAt I I.tangent 1 (fun (x : M) => { proj := x, snd := v x }) x₀) (hx : I.IsInteriorPoint x₀) :
∃ (γ : M), γ t₀ = x₀ IsMIntegralCurveAt γ v t₀

Existence of local integral curves for a $C^1$ vector field at interior points of a C^1 manifold.

@[deprecated exists_isMIntegralCurveAt_of_contMDiffAt (since := "2025-08-12")]
theorem exists_isIntegralCurveAt_of_contMDiffAt {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] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (t₀ : ) {x₀ : M} [CompleteSpace E] (hv : ContMDiffAt I I.tangent 1 (fun (x : M) => { proj := x, snd := v x }) x₀) (hx : I.IsInteriorPoint x₀) :
∃ (γ : M), γ t₀ = x₀ IsMIntegralCurveAt γ v t₀

Alias of exists_isMIntegralCurveAt_of_contMDiffAt.


Existence of local integral curves for a $C^1$ vector field at interior points of a C^1 manifold.

theorem exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless {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] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (t₀ : ) {x₀ : M} [CompleteSpace E] [BoundarylessManifold I M] (hv : ContMDiffAt I I.tangent 1 (fun (x : M) => { proj := x, snd := v x }) x₀) :
∃ (γ : M), γ t₀ = x₀ IsMIntegralCurveAt γ v t₀

Existence of local integral curves for a $C^1$ vector field on a C^1 manifold without boundary.

@[deprecated exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless (since := "2025-08-12")]
theorem exists_isIntegralCurveAt_of_contMDiffAt_boundaryless {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] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (t₀ : ) {x₀ : M} [CompleteSpace E] [BoundarylessManifold I M] (hv : ContMDiffAt I I.tangent 1 (fun (x : M) => { proj := x, snd := v x }) x₀) :
∃ (γ : M), γ t₀ = x₀ IsMIntegralCurveAt γ v t₀

Alias of exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless.


Existence of local integral curves for a $C^1$ vector field on a C^1 manifold without boundary.

theorem isMIntegralCurveAt_eventuallyEq_of_contMDiffAt {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] [IsManifold I 1 M] {γ γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } (hγt₀ : I.IsInteriorPoint (γ t₀)) (hv : ContMDiffAt I I.tangent 1 (fun (x : M) => { proj := x, snd := v x }) (γ t₀)) ( : IsMIntegralCurveAt γ v t₀) (hγ' : IsMIntegralCurveAt γ' v t₀) (h : γ t₀ = γ' t₀) :
γ =ᶠ[nhds t₀] γ'

Local integral curves are unique.

If a $C^1$ vector field v admits two local integral curves γ γ' : ℝ → M at t₀ with γ t₀ = γ' t₀, then γ and γ' agree on some open interval containing t₀.

@[deprecated isMIntegralCurveAt_eventuallyEq_of_contMDiffAt (since := "2025-08-12")]
theorem isIntegralCurveAt_eventuallyEq_of_contMDiffAt {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] [IsManifold I 1 M] {γ γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } (hγt₀ : I.IsInteriorPoint (γ t₀)) (hv : ContMDiffAt I I.tangent 1 (fun (x : M) => { proj := x, snd := v x }) (γ t₀)) ( : IsMIntegralCurveAt γ v t₀) (hγ' : IsMIntegralCurveAt γ' v t₀) (h : γ t₀ = γ' t₀) :
γ =ᶠ[nhds t₀] γ'

Alias of isMIntegralCurveAt_eventuallyEq_of_contMDiffAt.


Local integral curves are unique.

If a $C^1$ vector field v admits two local integral curves γ γ' : ℝ → M at t₀ with γ t₀ = γ' t₀, then γ and γ' agree on some open interval containing t₀.

theorem isMIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless {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] [IsManifold I 1 M] {γ γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } [BoundarylessManifold I M] (hv : ContMDiffAt I I.tangent 1 (fun (x : M) => { proj := x, snd := v x }) (γ t₀)) ( : IsMIntegralCurveAt γ v t₀) (hγ' : IsMIntegralCurveAt γ' v t₀) (h : γ t₀ = γ' t₀) :
γ =ᶠ[nhds t₀] γ'
@[deprecated isMIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless (since := "2025-08-12")]
theorem isIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless {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] [IsManifold I 1 M] {γ γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } [BoundarylessManifold I M] (hv : ContMDiffAt I I.tangent 1 (fun (x : M) => { proj := x, snd := v x }) (γ t₀)) ( : IsMIntegralCurveAt γ v t₀) (hγ' : IsMIntegralCurveAt γ' v t₀) (h : γ t₀ = γ' t₀) :
γ =ᶠ[nhds t₀] γ'

Alias of isMIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless.

theorem isMIntegralCurveOn_Ioo_eqOn_of_contMDiff {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] [IsManifold I 1 M] {γ γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } [T2Space M] {a b : } (ht₀ : t₀ Set.Ioo a b) (hγt : tSet.Ioo a b, I.IsInteriorPoint (γ t)) (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) ( : IsMIntegralCurveOn γ v (Set.Ioo a b)) (hγ' : IsMIntegralCurveOn γ' v (Set.Ioo a b)) (h : γ t₀ = γ' t₀) :
Set.EqOn γ γ' (Set.Ioo a b)

Integral curves are unique on open intervals.

If a $C^1$ vector field v admits two integral curves γ γ' : ℝ → M on some open interval Ioo a b, and γ t₀ = γ' t₀ for some t ∈ Ioo a b, then γ and γ' agree on Ioo a b.

@[deprecated isMIntegralCurveOn_Ioo_eqOn_of_contMDiff (since := "2025-08-12")]
theorem isIntegralCurveOn_Ioo_eqOn_of_contMDiff {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] [IsManifold I 1 M] {γ γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } [T2Space M] {a b : } (ht₀ : t₀ Set.Ioo a b) (hγt : tSet.Ioo a b, I.IsInteriorPoint (γ t)) (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) ( : IsMIntegralCurveOn γ v (Set.Ioo a b)) (hγ' : IsMIntegralCurveOn γ' v (Set.Ioo a b)) (h : γ t₀ = γ' t₀) :
Set.EqOn γ γ' (Set.Ioo a b)

Alias of isMIntegralCurveOn_Ioo_eqOn_of_contMDiff.


Integral curves are unique on open intervals.

If a $C^1$ vector field v admits two integral curves γ γ' : ℝ → M on some open interval Ioo a b, and γ t₀ = γ' t₀ for some t ∈ Ioo a b, then γ and γ' agree on Ioo a b.

theorem isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless {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] [IsManifold I 1 M] {γ γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } [T2Space M] {a b : } [BoundarylessManifold I M] (ht₀ : t₀ Set.Ioo a b) (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) ( : IsMIntegralCurveOn γ v (Set.Ioo a b)) (hγ' : IsMIntegralCurveOn γ' v (Set.Ioo a b)) (h : γ t₀ = γ' t₀) :
Set.EqOn γ γ' (Set.Ioo a b)
@[deprecated isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless (since := "2025-08-12")]
theorem isIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless {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] [IsManifold I 1 M] {γ γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } [T2Space M] {a b : } [BoundarylessManifold I M] (ht₀ : t₀ Set.Ioo a b) (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) ( : IsMIntegralCurveOn γ v (Set.Ioo a b)) (hγ' : IsMIntegralCurveOn γ' v (Set.Ioo a b)) (h : γ t₀ = γ' t₀) :
Set.EqOn γ γ' (Set.Ioo a b)

Alias of isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless.

theorem isMIntegralCurve_eq_of_contMDiff {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] [IsManifold I 1 M] {γ γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } [T2Space M] (hγt : ∀ (t : ), I.IsInteriorPoint (γ t)) (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) ( : IsMIntegralCurve γ v) (hγ' : IsMIntegralCurve γ' v) (h : γ t₀ = γ' t₀) :
γ = γ'

Global integral curves are unique.

If a continuously differentiable vector field v admits two global integral curves γ γ' : ℝ → M, and γ t₀ = γ' t₀ for some t₀, then γ and γ' are equal.

@[deprecated isMIntegralCurve_eq_of_contMDiff (since := "2025-08-12")]
theorem isIntegralCurve_eq_of_contMDiff {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] [IsManifold I 1 M] {γ γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } [T2Space M] (hγt : ∀ (t : ), I.IsInteriorPoint (γ t)) (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) ( : IsMIntegralCurve γ v) (hγ' : IsMIntegralCurve γ' v) (h : γ t₀ = γ' t₀) :
γ = γ'

Alias of isMIntegralCurve_eq_of_contMDiff.


Global integral curves are unique.

If a continuously differentiable vector field v admits two global integral curves γ γ' : ℝ → M, and γ t₀ = γ' t₀ for some t₀, then γ and γ' are equal.

theorem isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless {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] [IsManifold I 1 M] {γ γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } [T2Space M] [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) ( : IsMIntegralCurve γ v) (hγ' : IsMIntegralCurve γ' v) (h : γ t₀ = γ' t₀) :
γ = γ'
@[deprecated isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless (since := "2025-08-12")]
theorem isIntegralCurve_Ioo_eq_of_contMDiff_boundaryless {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] [IsManifold I 1 M] {γ γ' : M} {v : (x : M) → TangentSpace I x} {t₀ : } [T2Space M] [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) ( : IsMIntegralCurve γ v) (hγ' : IsMIntegralCurve γ' v) (h : γ t₀ = γ' t₀) :
γ = γ'

Alias of isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless.

theorem IsMIntegralCurve.periodic_of_eq {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] [IsManifold I 1 M] {γ : M} {v : (x : M) → TangentSpace I x} [T2Space M] {a b : } [BoundarylessManifold I M] ( : IsMIntegralCurve γ v) (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) (heq : γ a = γ b) :

For a global integral curve γ, if it crosses itself at a b : ℝ, then it is periodic with period a - b.

@[deprecated IsMIntegralCurve.periodic_of_eq (since := "2025-08-12")]
theorem IsIntegralCurve.periodic_of_eq {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] [IsManifold I 1 M] {γ : M} {v : (x : M) → TangentSpace I x} [T2Space M] {a b : } [BoundarylessManifold I M] ( : IsMIntegralCurve γ v) (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) (heq : γ a = γ b) :

Alias of IsMIntegralCurve.periodic_of_eq.


For a global integral curve γ, if it crosses itself at a b : ℝ, then it is periodic with period a - b.

theorem IsMIntegralCurve.periodic_xor_injective {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] [IsManifold I 1 M] {γ : M} {v : (x : M) → TangentSpace I x} [T2Space M] [BoundarylessManifold I M] ( : IsMIntegralCurve γ v) (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) :

A global integral curve is injective xor periodic with positive period.

@[deprecated IsMIntegralCurve.periodic_xor_injective (since := "2025-08-12")]
theorem IsIntegralCurve.periodic_xor_injective {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] [IsManifold I 1 M] {γ : M} {v : (x : M) → TangentSpace I x} [T2Space M] [BoundarylessManifold I M] ( : IsMIntegralCurve γ v) (hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x }) :

Alias of IsMIntegralCurve.periodic_xor_injective.


A global integral curve is injective xor periodic with positive period.