Regularity of integral curves

An integral curve gains one derivative over its vector field. In particular, integral curves of smooth vector fields on boundaryless smooth manifolds are smooth.

Main results

• IsMIntegralCurveOn.map_of_mfderiv_eq: a map differentiable along an integral curve whose derivative intertwines the vector fields there sends it to an integral curve of the second field.
• IsMIntegralCurveAt.map_of_mfderiv_eq: the corresponding result for local integral curves.
• IsMIntegralCurveOn.congr: being an integral curve on a set only depends on the values of the curve on that set.
• IsMIntegralCurve.contMDiff_succ: an integral curve of a C^n vector field is C^(n + 1).
• IsMIntegralCurve.contMDiff: an integral curve of a smooth vector field is smooth.
• IsMIntegralCurveAt.of_extChartAt_symm: a coordinate solution gives a manifold integral curve.

References

• Mathlib's proof of exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless, whose extended-chart calculation is adapted by IsMIntegralCurveAt.of_extChartAt_symm in the reverse direction.
• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 0, "The exponential map", and Layer 1, "The group adjoint".

theorem IsMIntegralCurveOn.map_of_mfderiv_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_4} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {V : (x : M) → TangentSpace I x} {W : (x : M') → TangentSpace I' x} {γ : ℝ → M} {s : Set ℝ} (hf : ∀ t ∈ s, MDiffAt f (γ t)) (hVW : ∀ t ∈ s, (mfderiv% f (γ t)) (V (γ t)) = W (f (γ t))) (hγ : IsMIntegralCurveOn γ V s) : IsMIntegralCurveOn (f ∘ γ) W s

A map differentiable along an integral curve whose derivative intertwines the vector fields there sends it to an integral curve of the second field.

theorem IsMIntegralCurveOn.congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] {V : (x : M) → TangentSpace I x} {γ γ' : ℝ → M} {s : Set ℝ} (hγ : IsMIntegralCurveOn γ V s) (h : Set.EqOn γ' γ s) : IsMIntegralCurveOn γ' V s

Being an integral curve on a set is a property of the values on that set. The values of a curve outside its parameter set are junk, so a curve agreeing with an integral curve on the set is again an integral curve there.

theorem IsMIntegralCurveAt.map_of_mfderiv_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_4} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {V : (x : M) → TangentSpace I x} {W : (x : M') → TangentSpace I' x} {γ : ℝ → M} {t₀ : ℝ} (hf : ∀ᶠ (t : ℝ) in nhds t₀, MDiffAt f (γ t)) (hVW : ∀ᶠ (t : ℝ) in nhds t₀, (mfderiv% f (γ t)) (V (γ t)) = W (f (γ t))) (hγ : IsMIntegralCurveAt γ V t₀) : IsMIntegralCurveAt (f ∘ γ) W t₀

A map eventually differentiable along a local integral curve whose derivative eventually intertwines the vector fields sends it to a local integral curve of the second field.

theorem IsMIntegralCurveAt.of_extChartAt_symm {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] {x₀ : M} {f : ℝ → E} {t₀ : ℝ} {v : (x : M) → TangentSpace I x} (htarget : ∀ᶠ (t : ℝ) in nhds t₀, f t ∈ interior (extChartAt I x₀).target) (hderiv : ∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt f ((tangentCoordChange I (↑(extChartAt I x₀).symm (f t)) x₀ (↑(extChartAt I x₀).symm (f t))) (v (↑(extChartAt I x₀).symm (f t)))) t) : IsMIntegralCurveAt (↑(extChartAt I x₀).symm ∘ f) v t₀

A coordinate curve whose values stay in an extended-chart target and whose derivative is the coordinate expression of a vector field gives a manifold integral curve after applying the inverse chart.

theorem IsMIntegralCurve.contMDiff_succ {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 IsMIntegralCurve.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] [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.