Existence and uniqueness of integral curves #
Main results #
exists_isIntegralCurveAt_of_contMDiffAt_boundaryless: Existence of local integral curves for a $C^1$ vector field. This follows from the existence theorem for solutions to ODEs (exists_forall_hasDerivAt_Ioo_eq_of_contDiffAt).isIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless: Uniqueness of local integral curves for a $C^1$ vector field. This follows from the uniqueness theorem for solutions to ODEs (ODE_solution_unique_of_mem_set_Ioo). This requires the manifold to be Hausdorff (T2Space).
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 #
- The case where the integral curve may venture to the boundary of the manifold. See Theorem 9.34, Lee. May require submanifolds.
Reference #
Tags #
integral curve, vector field, local existence, uniqueness
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]
[SmoothManifoldWithCorners I 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₀ ∧ IsIntegralCurveAt γ v t₀
Existence of local integral curves for a $C^1$ vector field at interior points of a smooth manifold.
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]
[SmoothManifoldWithCorners I 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₀ ∧ IsIntegralCurveAt γ v t₀
Existence of local integral curves for a $C^1$ vector field on a smooth manifold without boundary.
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]
[SmoothManifoldWithCorners I 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₀))
(hγ : IsIntegralCurveAt γ v t₀)
(hγ' : IsIntegralCurveAt γ' v t₀)
(h : γ t₀ = γ' 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₀.
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]
[SmoothManifoldWithCorners I 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₀))
(hγ : IsIntegralCurveAt γ v t₀)
(hγ' : IsIntegralCurveAt γ' v t₀)
(h : γ t₀ = γ' t₀)
:
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]
[SmoothManifoldWithCorners I M]
{γ γ' : ℝ → M}
{v : (x : M) → TangentSpace I x}
{t₀ : ℝ}
[T2Space M]
{a b : ℝ}
(ht₀ : t₀ ∈ Set.Ioo a b)
(hγt : ∀ t ∈ Set.Ioo a b, I.IsInteriorPoint (γ t))
(hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x })
(hγ : IsIntegralCurveOn γ v (Set.Ioo a b))
(hγ' : IsIntegralCurveOn γ' v (Set.Ioo a b))
(h : γ t₀ = γ' t₀)
:
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
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]
[SmoothManifoldWithCorners I 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 })
(hγ : IsIntegralCurveOn γ v (Set.Ioo a b))
(hγ' : IsIntegralCurveOn γ' v (Set.Ioo a b))
(h : γ t₀ = γ' t₀)
:
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]
[SmoothManifoldWithCorners I 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 })
(hγ : IsIntegralCurve γ v)
(hγ' : IsIntegralCurve γ' 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.
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]
[SmoothManifoldWithCorners I 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 })
(hγ : IsIntegralCurve γ v)
(hγ' : IsIntegralCurve γ' v)
(h : γ t₀ = γ' t₀)
:
γ = γ'
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]
[SmoothManifoldWithCorners I M]
{γ : ℝ → M}
{v : (x : M) → TangentSpace I x}
[T2Space M]
{a b : ℝ}
[BoundarylessManifold I M]
(hγ : IsIntegralCurve γ v)
(hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x })
(heq : γ a = γ b)
:
Function.Periodic γ (a - b)
For a global integral curve γ, if it crosses itself at a b : ℝ, then it is periodic with
period a - b.
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]
[SmoothManifoldWithCorners I M]
{γ : ℝ → M}
{v : (x : M) → TangentSpace I x}
[T2Space M]
[BoundarylessManifold I M]
(hγ : IsIntegralCurve γ v)
(hv : ContMDiff I I.tangent 1 fun (x : M) => { proj := x, snd := v x })
:
Xor' (∃ T > 0, Function.Periodic γ T) (Function.Injective γ)
A global integral curve is injective xor periodic with positive period.