Regularity of covariant differentiation along curves

A C^(n + 1) tangent field along a C^(n + 1) curve has a C^n covariant derivative. The field is an arbitrary section along the curve, with its original tangent-space carriers; it need not extend to a vector field on the manifold. The within-set version applies to parameter sets with unique derivatives, including nondegenerate closed intervals.

In a fixed chart, the coordinates of the covariant derivative are the derivative of the section coordinates plus the Christoffel contraction of the section coordinates and the curve velocity. The connection is required to be C^n locally on the trivialization base sets, as in ContMDiffCovariantDerivativeOn E n.

Repeated differentiation supplies regularity for second covariant derivatives: for a locally C¹ connection and the stated manifold and tangent-bundle hypotheses, a C² section lift has a C¹ first covariant derivative and hence a continuous second covariant derivative. This ensures continuity of the second covariant derivative occurring in the Jacobi equation.

References

• J. M. Lee, Introduction to Riemannian Manifolds, GTM 176, 2018, Ch. 4 and 10.

theorem CovariantDerivative.eventuallyEq_sectionCoord_alongCurveWithin {𝕜 : 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 2 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) {s : Set 𝕜} {t : 𝕜} {x : M} (hs : UniqueDiffOn 𝕜 s) (ht : t ∈ s) (hx : γ t ∈ (trivializationAt E (TangentSpace I) x).baseSet) (hV : ContMDiffWithinAt (modelWithCornersSelf 𝕜 𝕜) I.tangent 1 (fun (r : 𝕜) => ⟨γ r, V r⟩) s t) : TauCeti.Manifold.sectionCoord γ (cov.alongCurveWithin γ V s) x =ᶠ[nhdsWithin t s] cov.alongCurveInChartWithin γ V s x

Near a parameter where the curve and section lift are C¹, the reading of the native covariant derivative in any fixed chart is its defining fixed-chart coordinate formula.

theorem CovariantDerivative.contMDiffWithinAt_alongCurveWithin {𝕜 : 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 2 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) {n : WithTop ℕ∞} [IsManifold I (n + 1) M] [ContMDiffVectorBundle (n + 1) E (TangentSpace I) I] {s : Set 𝕜} {t : 𝕜} {x : M} [ContMDiffCovariantDerivativeOn E n (↑cov) (trivializationAt E (TangentSpace I) x).baseSet] (hs : UniqueDiffOn 𝕜 s) (ht : t ∈ s) (hx : γ t ∈ (trivializationAt E (TangentSpace I) x).baseSet) (hV : ContMDiffWithinAt (modelWithCornersSelf 𝕜 𝕜) I.tangent (n + 1) (fun (r : 𝕜) => ⟨γ r, V r⟩) s t) : ContMDiffWithinAt (modelWithCornersSelf 𝕜 𝕜) I.tangent n (fun (r : 𝕜) => ⟨γ r, cov.alongCurveWithin γ V s r⟩) s t

Covariant differentiation loses one derivative for an arbitrary section lift along a curve. Only local C^n regularity of the connection in one chart containing γ t is needed.

theorem CovariantDerivative.contMDiffOn_alongCurveWithin {𝕜 : 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 2 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) {n : WithTop ℕ∞} [IsManifold I (n + 1) M] [ContMDiffVectorBundle (n + 1) E (TangentSpace I) I] {s : Set 𝕜} (hcov : ∀ (x : M), ContMDiffCovariantDerivativeOn E n (↑cov) (trivializationAt E (TangentSpace I) x).baseSet) (hs : UniqueDiffOn 𝕜 s) (hV : ContMDiffOn (modelWithCornersSelf 𝕜 𝕜) I.tangent (n + 1) (fun (r : 𝕜) => ⟨γ r, V r⟩) s) : ContMDiffOn (modelWithCornersSelf 𝕜 𝕜) I.tangent n (fun (r : 𝕜) => ⟨γ r, cov.alongCurveWithin γ V s r⟩) s

On a parameter set with unique derivatives, differentiating a C^(n + 1) section lift along a C^(n + 1) curve produces a C^n section lift. The connection is C^n on each canonical trivialization base set.

theorem CovariantDerivative.contMDiff_alongCurve {𝕜 : 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 2 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) {n : WithTop ℕ∞} [IsManifold I (n + 1) M] [ContMDiffVectorBundle (n + 1) E (TangentSpace I) I] (hcov : ∀ (x : M), ContMDiffCovariantDerivativeOn E n (↑cov) (trivializationAt E (TangentSpace I) x).baseSet) (hV : ContMDiff (modelWithCornersSelf 𝕜 𝕜) I.tangent (n + 1) fun (r : 𝕜) => ⟨γ r, V r⟩) : ContMDiff (modelWithCornersSelf 𝕜 𝕜) I.tangent n fun (r : 𝕜) => ⟨γ r, cov.alongCurve γ V r⟩

The unrestricted covariant derivative of a C^(n + 1) section along a C^(n + 1) curve is C^n, for a connection C^n on the canonical trivialization base sets.