Integral curves in coordinates

This file records the correspondence between an integral curve and the solution of the coordinate equation it becomes when read in one fixed extended chart, in both directions, and the uniqueness statement that comes with it: two integral curves on an open interval which agree once agree throughout, as soon as one of them stays in a fixed chart over which the coordinate field is continuously differentiable. It also identifies the constant integral curves with the zeros of the field.

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_const_iff: a constant curve is an integral curve exactly at a zero of the field.
• TauCeti.isMIntegralCurve_congr_vectorField: being an integral curve only depends on the values of the vector field along the curve.
• TauCeti.isMIntegralCurveOn_iff_isIntegralCurveOn: in a vector space, integral curves of a vector field are the solutions of the autonomous differential equation it defines.
• IsMIntegralCurveAt.of_extChartAt_symm, IsMIntegralCurveOn.of_extChartAt_symm: a coordinate solution, on a neighbourhood of a time or on an open set of times, gives a manifold integral curve. Conversely, HasMFDerivAt.hasDerivAt_extChartAt_comp shows that a curve read in a fixed extended chart has the coordinate expression of its velocity as velocity, so an integral curve solves the coordinate equation there.
• IsMIntegralCurveOn.eqOn_of_contDiffOn_extChartAt: uniqueness of integral curves on an open interval, with the field regular in one fixed chart only.

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.
• Mathlib's isMIntegralCurveOn_Ioo_eqOn_of_contMDiff, whose connectedness argument is followed by IsMIntegralCurveOn.eqOn_of_contDiffOn_extChartAt.
• 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.

@[simp]

theorem isMIntegralCurve_const_iff {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} : IsMIntegralCurve (fun (x_1 : ℝ) => x) v ↔ v x = 0

Constant integral curves are the zeros of the field. The constant curve at x is an integral curve of v exactly when v x = 0.

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 TauCeti.isMIntegralCurve_congr_vectorField {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 w : (x : M) → TangentSpace I x} (hvw : ∀ (t : ℝ), v (γ t) = w (γ t)) : IsMIntegralCurve γ v ↔ IsMIntegralCurve γ w

Being an integral curve only depends on the vector field along the curve. If two vector fields agree at every point of a curve, it is an integral curve of one exactly when it is an integral curve of the other.

theorem TauCeti.isMIntegralCurveOn_iff_isIntegralCurveOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : (x : E) → TangentSpace (modelWithCornersSelf ℝ E) x} {s : Set ℝ} : IsMIntegralCurveOn γ v s ↔ IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => v x_1) s

Integral curves in a vector space. For the model 𝓘(ℝ, E) of E on itself, a curve is an integral curve of a vector field on a set exactly when it solves, on that set, the autonomous differential equation γ' = v ∘ γ in the sense of Mathlib's IsIntegralCurveOn.

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 IsMIntegralCurveOn.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} {Φ : ℝ → E} {s : Set ℝ} {v : (x : M) → TangentSpace I x} (hs : IsOpen s) (hderiv : ∀ t ∈ s, HasDerivAt Φ ((tangentCoordChange I (↑(extChartAt I x₀).symm (Φ t)) x₀ (↑(extChartAt I x₀).symm (Φ t))) (v (↑(extChartAt I x₀).symm (Φ t)))) t) (htarget : ∀ t ∈ s, Φ t ∈ interior (extChartAt I x₀).target) : IsMIntegralCurveOn (↑(extChartAt I x₀).symm ∘ Φ) v s

A curve in the extended chart at x₀ that solves the coordinate equation and stays in the interior of the chart target on an open set s is an integral curve of v on s once pulled back through the inverse chart.

theorem TauCeti.isMIntegralCurveOn_extChartAt_symm_comp {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) (a : M) {f : ℝ → E} {s : Set ℝ} (hs : IsOpen s) (hmem : ∀ t ∈ s, f t ∈ interior (extChartAt I a).target) (hderiv : ∀ t ∈ s, HasDerivAt f (↑(trivializationAt E (TangentSpace I) a) ⟨↑(extChartAt I a).symm (f t), v (↑(extChartAt I a).symm (f t))⟩).2 t) : IsMIntegralCurveOn (↑(extChartAt I a).symm ∘ f) v s

A curve in the model space which stays in the interior of the chart target and solves the coordinate equation of a vector field on an open set of times gives an integral curve of the field on the manifold, after applying the inverse extended chart.

theorem IsMIntegralCurveOn.eqOn_of_contDiffOn_extChartAt {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] [T2Space M] {v : (x : M) → TangentSpace I x} {x₀ : M} {a b t₀ : ℝ} {γ δ : ℝ → M} {u : Set E} (hu : IsOpen u) (hv : ContDiffOn ℝ 1 (fun (z : E) => (tangentCoordChange I (↑(extChartAt I x₀).symm z) x₀ (↑(extChartAt I x₀).symm z)) (v (↑(extChartAt I x₀).symm z))) u) (hγ : IsMIntegralCurveOn γ v (Set.Ioo a b)) (hδ : IsMIntegralCurveOn δ v (Set.Ioo a b)) (hγsrc : ∀ t ∈ Set.Ioo a b, γ t ∈ (extChartAt I x₀).source) (hγu : ∀ t ∈ Set.Ioo a b, ↑(extChartAt I x₀) (γ t) ∈ u) (ht₀ : t₀ ∈ Set.Ioo a b) (heq : γ t₀ = δ t₀) : Set.EqOn γ δ (Set.Ioo a b)

Fixed-chart uniqueness of integral curves. Two integral curves on an open interval which take the same value at one time of that interval agree on it, as soon as one of them stays in a fixed extended chart, over an open set on which the coordinate expression of the field is continuously differentiable. Unlike isMIntegralCurveOn_Ioo_eqOn_of_contMDiff, the field has to be regular only in that one chart, not in the chart at each point of the curve.