Regularity of integral curves on parameter sets

An integral curve gains one derivative when its vector field is C^n at every point of the curve image and those points are interior to the manifold. Regularity is within any parameter set with unique derivatives, including nondegenerate closed intervals: no extension of the curve beyond its endpoints is assumed.

In coordinates the first derivative is the vector field evaluated along the curve. The within-set ODE regularity theorem then gives C^(n + 1) regularity. Applied to the geodesic spray, this removes the separate regularity assumption on the projected curve in the spray characterization of geodesics.

Main results

• TauCeti.Manifold.contMDiffOn_succ_of_isMIntegralCurveOn: regularity on parameter sets with unique derivatives.
• TauCeti.Manifold.contMDiffAt_two_of_isMIntegralCurveAt: local C² regularity.
• TauCeti.Manifold.contMDiff_succ_of_isMIntegralCurve and TauCeti.Manifold.contMDiff_of_isMIntegralCurve: all-time finite-order and smooth regularity.

References

• The chart calculation adapts the original Tau Ceti proof of IsMIntegralCurveAt.contMDiffAt_two, formerly in TauCeti.Geometry.Manifold.IntegralCurve.Basic, to within-derivatives on UniqueDiffOn sets. The local and all-time regularity results below now follow from that general calculation.

theorem TauCeti.Manifold.contMDiffOn_succ_of_isMIntegralCurveOn {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] (n : ℕ) [IsManifold I (↑(n + 1)) M] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {s : Set ℝ} (hs : UniqueDiffOn ℝ s) (hγ : IsMIntegralCurveOn γ v s) (hinterior : ∀ t ∈ s, I.IsInteriorPoint (γ t)) (hv : have x := ⋯; ∀ t ∈ s, ContMDiffAt I I.tangent (↑n) (fun (x : M) => ⟨x, v x⟩) (γ t)) : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I (↑(n + 1)) γ s

An integral curve is C^(n + 1) within a parameter set with unique derivatives if the vector field is C^n at every point of the curve image and those points are interior to the manifold.

theorem TauCeti.Manifold.contMDiffOn_two_of_isMIntegralCurveOn {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] [BoundarylessManifold I M] [IsManifold I 2 M] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {s : Set ℝ} (hs : UniqueDiffOn ℝ s) (hγ : IsMIntegralCurveOn γ v s) (hv : ∀ t ∈ s, ContMDiffAt I I.tangent 1 (fun (x : M) => ⟨x, v x⟩) (γ t)) : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 2 γ s

An integral curve on a boundaryless manifold is C² within a parameter set with unique derivatives when the vector field is C¹ at every point of the curve image. This includes the endpoints of a nondegenerate closed interval.

theorem TauCeti.Manifold.contMDiffAt_two_of_isMIntegralCurveAt {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] [BoundarylessManifold I M] [IsManifold I 2 M] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ} (hγ : IsMIntegralCurveAt γ v t₀) (hv : ContMDiffAt I I.tangent 1 (fun (x : M) => ⟨x, v x⟩) (γ t₀)) : ContMDiffAt (modelWithCornersSelf ℝ ℝ) I 2 γ t₀

A local integral curve on a boundaryless manifold is C² at its initial parameter if the vector field is C¹ at the corresponding point of the curve.

theorem TauCeti.Manifold.contMDiff_succ_of_isMIntegralCurve {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] [BoundarylessManifold I M] (n : ℕ) [IsManifold I (↑(n + 1)) M] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} (hγ : IsMIntegralCurve γ v) (hv : have x := ⋯; ContMDiff I I.tangent ↑n fun (x : M) => ⟨x, v x⟩) : ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑(n + 1)) γ

An integral curve of a C^n vector field on a boundaryless smooth manifold is C^(n + 1).

theorem TauCeti.Manifold.contMDiff_of_isMIntegralCurve {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] [BoundarylessManifold I M] [IsManifold I (↑⊤) M] {γ : ℝ → M} {v : (x : M) → TangentSpace I x} (hγ : IsMIntegralCurve γ v) (hv : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, v x⟩) : ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑⊤) γ

An integral curve of an infinitely smooth vector field on a boundaryless smooth manifold is infinitely smooth.