The along-curve derivative of a pulled-back vector field

CovariantDerivative.alongCurveWithin differentiates a tangent field along a curve by the moving-chart formula v' + Γ(v, u') of TauCeti/Geometry/Manifold/VectorBundle/CovariantDerivative/AlongCurve/Basic.lean, which reads the curve and the field in the chart centred at the current point. This file identifies that formula for a field which is pulled back from an ambient vector field, V t = X (γ t): there the formula returns ∇_{γ'(t)} X, the ambient covariant derivative of X in the direction of the velocity of γ. This is do Carmo 2.2(c), one of the properties characterising D/dt together with the linearity and Leibniz laws of AlongCurve/Basic.lean; it also makes the formula chart independent on pulled-back fields.

The identification is proved in an arbitrary chart, not only in the moving one: for any x whose chart contains γ t, the coordinate formula computed in the chart at x is the reading of ∇_{γ'(t)} X in the tangent-bundle trivialization at x. Transporting back therefore gives the same tangent vector for every such x.

The velocity of the curve is carried by a HasMFDerivWithinAt hypothesis, in the ContinuousLinearMap.smulRight 1 w form used by Mathlib's integral-curve API, so that no junk value can leak in; CovariantDerivative.alongCurveWithin_pullback_curveVelocityWithin restates the result for the canonical velocity TauCeti.Manifold.curveVelocityWithin.

The chart computation of this file also specializes to the velocity field t ↦ γ' t of the curve, which is not pulled back from an ambient vector field: reading it in a chart returns the derivative of the chart reading of the curve, so the moving-chart formula becomes the classical second-order expression u'' + Γ (u', u'). AlongCurve/Acceleration.lean builds the covariant acceleration of the curve on this computation.

Main results

• TauCeti.Manifold.derivWithin_extChartAt_comp: the derivative of a curve read in the chart at x is the reading of its velocity in the tangent-bundle trivialization at x, with TauCeti.Manifold.sectionCoord_curveVelocityWithin_eventuallyEq its eventual-equality form for the velocity field.
• TauCeti.Manifold.contDiffWithinAt_sectionCoord_curveVelocityWithin: a C^(n + 1) curve has a C^n coordinate velocity field; its C² differentiability specializations are TauCeti.Manifold.differentiableWithinAt_sectionCoord_curveVelocityWithin and TauCeti.Manifold.differentiableAt_sectionCoord_curveVelocity.
• TauCeti.Manifold.derivWithin_sectionCoord_pullback: the derivative of the coordinate reading of a pulled-back field is the reading of the flat frame derivative in the direction of the velocity.
• CovariantDerivative.alongCurveInChartWithin_pullback: the coordinate formula in the chart at x, for a pulled-back field, is the reading of ∇_{γ'(t)} X.
• CovariantDerivative.alongCurveWithin_pullback and CovariantDerivative.alongCurve_pullback: the along-curve derivative of a pulled-back field is ∇_{γ'(t)} X, within a parameter set and unrestricted.
• CovariantDerivative.symmL_alongCurveInChartWithin_pullback: on pulled-back fields the coordinate formula is chart independent -- reading it in any chart around γ t and transporting back gives the moving-chart value.
• CovariantDerivative.alongCurveWithin_pullback_curveVelocityWithin: the same identification with the velocity written as TauCeti.Manifold.curveVelocityWithin.
• CovariantDerivative.alongCurveInChartWithin_curveVelocityWithin: the coordinate formula for the velocity field of the curve is u'' + Γ (u', u').

References

• M. P. do Carmo, Riemannian Geometry, Birkhauser, 1992, Ch. 2, Proposition 2.2(c).
• The moving-chart operator characterized here was informed by formalized-sources/DoCarmo/DoCarmoLib/Riemannian/Connection/CovariantDerivativeAlong.lean in the Apache-2.0 frenzymath/Poincare-Conjecture repository at revision 24f32e4d600878bfaac6bc2f2f9324175571c321.

theorem TauCeti.Manifold.derivWithin_extChartAt_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (γ : 𝕜 → M) {x : M} {s : Set 𝕜} {t : 𝕜} {w : TangentSpace I (γ t)} (hx : γ t ∈ (trivializationAt E (TangentSpace I) x).baseSet) (hu : UniqueDiffWithinAt 𝕜 s t) (hγ : HasMFDerivAt[s] γ t (ContinuousLinearMap.smulRight 1 w)) : derivWithin (↑(extChartAt I x) ∘ γ) s t = (Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) x) (γ t)) w

The derivative of a curve read in the chart centred at x, taken within a parameter set with a unique derivative there, is the reading of the velocity of the curve in the tangent-bundle trivialization at x. The chart need not be the one centred at the current point of the curve.

theorem TauCeti.Manifold.sectionCoord_curveVelocityWithin_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (γ : 𝕜 → M) {x : M} {s : Set 𝕜} {t : 𝕜} (hγ : MDiff[s] γ) (ht : t ∈ s) (hx : γ t ∈ (trivializationAt E (TangentSpace I) x).baseSet) : sectionCoord γ (curveVelocityWithin I γ s) x =ᶠ[nhdsWithin t s] derivWithin (↑(extChartAt I x) ∘ γ) s

Along a curve differentiable within s, the coordinate reading of the velocity field in the tangent-bundle trivialization centred at x is the derivative within s of the curve read in the extended chart at x, at every nearby parameter of s at which the curve is still in that chart.

theorem TauCeti.Manifold.contDiffWithinAt_sectionCoord_curveVelocityWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (γ : 𝕜 → M) {n : WithTop ℕ∞} [IsManifold I (n + 1) M] {x : M} {s : Set 𝕜} {t : 𝕜} (hs : UniqueDiffOn 𝕜 s) (hγ : ContMDiffOn (modelWithCornersSelf 𝕜 𝕜) I (n + 1) γ s) (ht : t ∈ s) (hx : γ t ∈ (trivializationAt E (TangentSpace I) x).baseSet) : ContDiffWithinAt 𝕜 n (sectionCoord γ (curveVelocityWithin I γ s) x) s t

If a curve is C^(n + 1) on a parameter set with unique derivatives, then the coordinate reading of its velocity in any tangent-bundle chart containing the current point is C^n there. This is the regularity step which makes the derivative in the along-curve formula an honest second derivative when the curve is C².

theorem TauCeti.Manifold.differentiableWithinAt_sectionCoord_curveVelocityWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (γ : 𝕜 → M) [IsManifold I 2 M] {x : M} {s : Set 𝕜} {t : 𝕜} (hs : UniqueDiffOn 𝕜 s) (hγ : ContMDiffOn (modelWithCornersSelf 𝕜 𝕜) I 2 γ s) (ht : t ∈ s) (hx : γ t ∈ (trivializationAt E (TangentSpace I) x).baseSet) : DifferentiableWithinAt 𝕜 (sectionCoord γ (curveVelocityWithin I γ s) x) s t

The coordinate reading of the within-set velocity of a C² curve is differentiable within the parameter set.

theorem TauCeti.Manifold.differentiableAt_sectionCoord_curveVelocity {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (γ : 𝕜 → M) [IsManifold I 2 M] {s : Set 𝕜} {t : 𝕜} (hγ : ContMDiffOn (modelWithCornersSelf 𝕜 𝕜) I 2 γ s) (hs : IsOpen s) (ht : t ∈ s) : DifferentiableAt 𝕜 (sectionCoord γ (curveVelocity I γ) (γ t)) t

On an open parameter set, the coordinate reading of the unrestricted velocity of a C² curve is differentiable at every parameter in the set.

theorem TauCeti.Manifold.derivWithin_sectionCoord_pullback {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (γ : 𝕜 → M) {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(y : M) → AddCommGroup (V y)] [(y : M) → Module 𝕜 (V y)] [(y : M) → TopologicalSpace (V y)] [FiberBundle F V] [∀ (y : M), IsTopologicalAddGroup (V y)] [∀ (y : M), ContinuousSMul 𝕜 (V y)] [VectorBundle 𝕜 F V] [ContMDiffVectorBundle 1 F V I] {ι : Type u_7} [Fintype ι] (b : Module.Basis ι 𝕜 F) (Y : (y : M) → V y) {x : M} {s : Set 𝕜} {t : 𝕜} {w : TangentSpace I (γ t)} (hy : γ t ∈ (trivializationAt F V x).baseSet) (hu : UniqueDiffWithinAt 𝕜 s t) (hγ : HasMFDerivAt[s] γ t (ContinuousLinearMap.smulRight 1 w)) (hY : (MDiffAt fun (y : M) => ⟨y, Y y⟩) (γ t)) : derivWithin (sectionCoord γ (fun (r : 𝕜) => Y (γ r)) x) s t = (Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt F V x) (γ t)) ((frameCovariantDerivative I b (trivializationAt F V x) Y (γ t)) w)

Along a curve, the derivative of the coordinate reading of a pulled-back vector-bundle section is the reading of its flat frame derivative in the direction of the velocity.

theorem CovariantDerivative.alongCurveInChartWithin_pullback {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] (cov : CovariantDerivative I E fun (y : M) => TangentSpace I y) (γ : 𝕜 → M) (X : (y : M) → TangentSpace I y) {x : M} {s : Set 𝕜} {t : 𝕜} {w : TangentSpace I (γ t)} (hy : γ t ∈ (trivializationAt E (TangentSpace I) x).baseSet) (hu : UniqueDiffWithinAt 𝕜 s t) (hγ : HasMFDerivAt[s] γ t (ContinuousLinearMap.smulRight 1 w)) (hX : (MDiffAt fun (y : M) => ⟨y, X y⟩) (γ t)) : cov.alongCurveInChartWithin γ (fun (r : 𝕜) => X (γ r)) s x t = (Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) x) (γ t)) ((↑cov X (γ t)) w)

The moving-chart coordinate formula, evaluated in the chart at an arbitrary point x whose base set contains γ t, computes the reading of the ambient covariant derivative ∇_{γ'(t)} X in the tangent-bundle trivialization at x, whenever the differentiated field is pulled back from the vector field X.

theorem CovariantDerivative.alongCurveWithin_pullback {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] (cov : CovariantDerivative I E fun (y : M) => TangentSpace I y) (γ : 𝕜 → M) (X : (y : M) → TangentSpace I y) {s : Set 𝕜} {t : 𝕜} {w : TangentSpace I (γ t)} (hu : UniqueDiffWithinAt 𝕜 s t) (hγ : HasMFDerivAt[s] γ t (ContinuousLinearMap.smulRight 1 w)) (hX : (MDiffAt fun (y : M) => ⟨y, X y⟩) (γ t)) : cov.alongCurveWithin γ (fun (r : 𝕜) => X (γ r)) s t = (↑cov X (γ t)) w

Agreement with the ambient covariant derivative. The derivative along γ of the field pulled back from a vector field X is ∇_{γ'(t)} X, the ambient covariant derivative of X in the direction of the velocity of γ.

theorem CovariantDerivative.symmL_alongCurveInChartWithin_pullback {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] (cov : CovariantDerivative I E fun (y : M) => TangentSpace I y) (γ : 𝕜 → M) (X : (y : M) → TangentSpace I y) {x : M} {s : Set 𝕜} {t : 𝕜} {w : TangentSpace I (γ t)} (hy : γ t ∈ (trivializationAt E (TangentSpace I) x).baseSet) (hu : UniqueDiffWithinAt 𝕜 s t) (hγ : HasMFDerivAt[s] γ t (ContinuousLinearMap.smulRight 1 w)) (hX : (MDiffAt fun (y : M) => ⟨y, X y⟩) (γ t)) : (Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) x) (γ t)) (cov.alongCurveInChartWithin γ (fun (r : 𝕜) => X (γ r)) s x t) = cov.alongCurveWithin γ (fun (r : 𝕜) => X (γ r)) s t

Chart independence on pulled-back fields. Reading the coordinate formula in the chart at any point x whose base set contains γ t, and transporting the result back to TangentSpace I (γ t), gives the moving-chart value.

theorem CovariantDerivative.alongCurve_pullback {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] (cov : CovariantDerivative I E fun (y : M) => TangentSpace I y) (γ : 𝕜 → M) (X : (y : M) → TangentSpace I y) {t : 𝕜} {w : TangentSpace I (γ t)} (hγ : HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 w)) (hX : (MDiffAt fun (y : M) => ⟨y, X y⟩) (γ t)) : cov.alongCurve γ (fun (r : 𝕜) => X (γ r)) t = (↑cov X (γ t)) w

The unrestricted along-curve derivative of a pulled-back vector field is the ambient covariant derivative in the direction of the velocity of the curve.

theorem CovariantDerivative.alongCurveWithin_pullback_curveVelocityWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] (cov : CovariantDerivative I E fun (y : M) => TangentSpace I y) (γ : 𝕜 → M) (X : (y : M) → TangentSpace I y) {s : Set 𝕜} {t : 𝕜} (hu : UniqueDiffWithinAt 𝕜 s t) (hγ : MDiffAt[s] γ t) (hX : (MDiffAt fun (y : M) => ⟨y, X y⟩) (γ t)) : cov.alongCurveWithin γ (fun (r : 𝕜) => X (γ r)) s t = (↑cov X (γ t)) (TauCeti.Manifold.curveVelocityWithin I γ s t)

Agreement with the ambient covariant derivative, with the velocity of the curve written as the canonical TauCeti.Manifold.curveVelocityWithin.

The velocity field of the curve

theorem CovariantDerivative.alongCurveInChartWithin_curveVelocityWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] (cov : CovariantDerivative I E fun (y : M) => TangentSpace I y) (γ : 𝕜 → M) {x : M} {s : Set 𝕜} {t : 𝕜} (hγ : MDiff[s] γ) (ht : t ∈ s) (hx : γ t ∈ (trivializationAt E (TangentSpace I) x).baseSet) : cov.alongCurveInChartWithin γ (TauCeti.Manifold.curveVelocityWithin I γ s) s x t = derivWithin (derivWithin (↑(extChartAt I x) ∘ γ) s) s t + ((TauCeti.Manifold.christoffelMap (Module.finBasis 𝕜 E) ⋯ (γ t)) (derivWithin (↑(extChartAt I x) ∘ γ) s t)) (derivWithin (↑(extChartAt I x) ∘ γ) s t)

The moving-chart coordinate formula applied to the velocity field of the curve is the classical second-order expression u'' + Γ (u', u'), for u the curve read in the extended chart at x. The chart need not be the one centred at the current point of the curve.