A moving-chart formula for covariant differentiation along a curve

This file constructs a moving-chart candidate for the covariant derivative of a tangent field along a curve. At a parameter t, both the curve and the field are read in the tangent-bundle trivialization coming from the chart centred at the current point γ t. If u and v are those coordinate readings and Γ is the Christoffel map of the connection in that frame, the defining formula is

D V / dt = v' + Γ(v, u').

The result is transported back to TangentSpace I (γ t). Thus the definition uses the chart at the current point rather than a single global chart. Derivatives are taken within a parameter set s, so that the construction applies on a closed interval as well as on all of 𝕜; the unrestricted operator is the s = Set.univ case, exactly as Mathlib's fderiv is the Set.univ case of fderivWithin. This first part of the along-curve API proves the characteristic additive and scalar Leibniz laws, locality in the field and parameter set, and naturality under differentiable reparametrization. For a field pulled back from an ambient vector field, AlongCurve/Pullback.lean identifies the formula in an arbitrary fixed chart and with the ambient covariant derivative.

Main definitions and results

• TauCeti.Manifold.sectionCoord: the coordinate reading of a tangent field along a curve in a specified tangent-bundle trivialization; see VectorBundle/SectionAlongCurve/Basic.lean.
• CovariantDerivative.alongCurveInChartWithin: the model-space formula v' + Γ(v, u') within a parameter set, computed by CovariantDerivative.alongCurveInChartWithin_apply.
• CovariantDerivative.alongCurveWithin: the resulting tangent field along the curve, computed by CovariantDerivative.alongCurveWithin_apply, and its unrestricted case CovariantDerivative.alongCurve; CovariantDerivative.alongCurveWithin_univ relates them.
• CovariantDerivative.alongCurveWithin_add, CovariantDerivative.alongCurveWithin_smul and CovariantDerivative.alongCurveWithin_const_smul: additivity, the scalar Leibniz rule, and scalar homogeneity; each has an unrestricted counterpart.
• CovariantDerivative.alongCurveWithin_zero: the zero-field law, with CovariantDerivative.alongCurve_zero its unrestricted case.
• CovariantDerivative.alongCurveWithin_sum and CovariantDerivative.alongCurve_sum: additivity over finite sums of fields with differentiable coordinate readings.
• CovariantDerivative.alongCurveWithin_const: along a constant curve the candidate is the ordinary derivative of the field, with CovariantDerivative.alongCurve_const its unrestricted case; CovariantDerivative.alongCurveWithin_const_of_hasDerivWithinAt and CovariantDerivative.alongCurve_const_of_hasDerivAt read off a known derivative.
• CovariantDerivative.alongCurveWithin_inter, CovariantDerivative.alongCurveWithin_of_mem_nhds, CovariantDerivative.alongCurveWithin_subset, CovariantDerivative.alongCurveWithin_congr, and CovariantDerivative.alongCurveWithin_comp: parameter-set and field locality and reparametrization, with CovariantDerivative.alongCurve_congr and CovariantDerivative.alongCurve_comp their unrestricted cases.

References

• M. P. do Carmo, Riemannian Geometry, Birkhauser, 1992, Ch. 2, Proposition 2.2.
• The moving-chart construction was informed by formalized-sources/DoCarmo/DoCarmoLib/Riemannian/Connection/CovariantDerivativeAlong.lean and formalized-sources/DoCarmo/DoCarmoLib/Riemannian/Connection/AffineCovariantDerivativeAlong.lean in the Apache-2.0 frenzymath/Poincare-Conjecture repository at revision 24f32e4d600878bfaac6bc2f2f9324175571c321; this implementation instead uses Mathlib's CovariantDerivative and Tau Ceti's christoffelMap directly.

noncomputable def CovariantDerivative.alongCurveInChartWithin {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) (s : Set 𝕜) (x : M) (t : 𝕜) : E

The moving-chart coordinate formula for V along γ in the chart centred at x, taken within the parameter set s: v' + Γ(v, u'), where u = extChartAt I x ∘ γ and v = sectionCoord γ V x are the coordinate readings of the curve and the field, their derivatives are taken within s, and Γ is the Christoffel map of cov in the local frame of the fixed basis Module.finBasis 𝕜 E. Its chart independence and agreement with an ambient derivative are established for fields pulled back from ambient vector fields by CovariantDerivative.symmL_alongCurveInChartWithin_pullback; they remain open here for a general section along the curve. When the coordinate readings are not differentiable within s at t, UniqueDiffWithinAt 𝕜 s t fails, or γ does not stay in (trivializationAt E (TangentSpace I) x).baseSet near t within s, its components may carry their junk value 0.

theorem CovariantDerivative.alongCurveInChartWithin_apply {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) (s : Set 𝕜) (x : M) (t : 𝕜) : cov.alongCurveInChartWithin γ V s x t = derivWithin (TauCeti.Manifold.sectionCoord γ V x) s t + ((TauCeti.Manifold.christoffelMap (Module.finBasis 𝕜 E) ⋯ (γ t)) (TauCeti.Manifold.sectionCoord γ V x t)) (derivWithin (↑(extChartAt I x) ∘ γ) s t)

The defining formula for the coordinate covariant derivative within a parameter set.

noncomputable def CovariantDerivative.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 1 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 : 𝕜) : TangentSpace I (γ t)

The moving-chart candidate for the covariant derivative of V along γ within the parameter set s, transported from the model space to TangentSpace I (γ t). Its identification with the ambient covariant derivative is established for pulled-back fields by CovariantDerivative.alongCurveWithin_pullback; it remains open here for a general section along the curve. It inherits the junk values of alongCurveInChartWithin. The Christoffel map is read in the local frame of the fixed basis Module.finBasis 𝕜 E.

theorem CovariantDerivative.alongCurveWithin_apply {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) (s : Set 𝕜) (t : 𝕜) : cov.alongCurveWithin γ V s t = (Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) (γ t)) (γ t)) (cov.alongCurveInChartWithin γ V s (γ t) t)

The defining formula for the along-curve candidate within a parameter set: the coordinate formula in the chart at the current point, transported back to the tangent space there.

theorem CovariantDerivative.continuousLinearMapAt_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 1 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) {γ : 𝕜 → M} {s : Set 𝕜} {t : 𝕜} {C : TangentSpace I (γ t) →L[𝕜] E} (hC : C = Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) (γ t)) (γ t)) (Q : (r : 𝕜) → TangentSpace I (γ r)) : C (cov.alongCurveWithin γ Q s t) = derivWithin (TauCeti.Manifold.sectionCoord γ Q (γ t)) s t + ((TauCeti.Manifold.christoffelMap (Module.finBasis 𝕜 E) ⋯ (γ t)) (C (Q t))) (derivWithin (↑(extChartAt I (γ t)) ∘ γ) s t)

In the trivialization C at γ t, the covariant derivative along γ of Q is the ordinary derivative of its coordinate reading plus the Christoffel term.

theorem CovariantDerivative.alongCurveWithin_of_not_uniqueDiffWithinAt {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) {s : Set 𝕜} {t : 𝕜} (hu : ¬UniqueDiffWithinAt 𝕜 s t) : cov.alongCurveWithin γ V s t = 0

The junk value of the along-curve candidate: it vanishes where the parameter set does not have unique derivatives, because derivWithin is then 0.

theorem CovariantDerivative.alongCurveWithin_eq_derivWithin_sectionCoord_of_eq_zero {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) {s : Set 𝕜} {t : 𝕜} (hV : V t = 0) : cov.alongCurveWithin γ V s t = derivWithin (TauCeti.Manifold.sectionCoord γ V (γ t)) s t

At a zero of a field, its covariant derivative is its ordinary coordinate derivative in the canonical tangent trivialization at that point.

noncomputable def CovariantDerivative.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 1 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) (t : 𝕜) : TangentSpace I (γ t)

The moving-chart candidate for the covariant derivative of V along γ, with unrestricted derivatives. This is the s = Set.univ case of alongCurveWithin, and carries the same junk values and the same fixed local frame.

@[simp]

theorem CovariantDerivative.alongCurveWithin_univ {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) (t : 𝕜) : cov.alongCurveWithin γ V Set.univ t = cov.alongCurve γ V t

Restricting the moving-chart candidate to the whole parameter space gives its unrestricted version.

theorem CovariantDerivative.alongCurve_apply {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) (t : 𝕜) : cov.alongCurve γ V t = (Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) (γ t)) (γ t)) (cov.alongCurveInChartWithin γ V Set.univ (γ t) t)

The defining formula for the unrestricted along-curve candidate: the coordinate formula in the chart at the current point, transported back to the tangent space there.

Algebra laws

theorem CovariantDerivative.alongCurveWithin_add {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V W : (t : 𝕜) → TangentSpace I (γ t)) (s : Set 𝕜) {t : 𝕜} (hV : DifferentiableWithinAt 𝕜 (TauCeti.Manifold.sectionCoord γ V (γ t)) s t) (hW : DifferentiableWithinAt 𝕜 (TauCeti.Manifold.sectionCoord γ W (γ t)) s t) : cov.alongCurveWithin γ (fun (r : 𝕜) => V r + W r) s t = cov.alongCurveWithin γ V s t + cov.alongCurveWithin γ W s t

The moving-chart candidate within a parameter set is additive in the field.

theorem CovariantDerivative.alongCurve_add {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V W : (t : 𝕜) → TangentSpace I (γ t)) {t : 𝕜} (hV : DifferentiableAt 𝕜 (TauCeti.Manifold.sectionCoord γ V (γ t)) t) (hW : DifferentiableAt 𝕜 (TauCeti.Manifold.sectionCoord γ W (γ t)) t) : cov.alongCurve γ (fun (r : 𝕜) => V r + W r) t = cov.alongCurve γ V t + cov.alongCurve γ W t

The unrestricted moving-chart candidate is additive in the field.

theorem CovariantDerivative.alongCurveWithin_sub {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V W : (t : 𝕜) → TangentSpace I (γ t)) (s : Set 𝕜) {t : 𝕜} (hV : DifferentiableWithinAt 𝕜 (TauCeti.Manifold.sectionCoord γ V (γ t)) s t) (hW : DifferentiableWithinAt 𝕜 (TauCeti.Manifold.sectionCoord γ W (γ t)) s t) : cov.alongCurveWithin γ (fun (r : 𝕜) => V r - W r) s t = cov.alongCurveWithin γ V s t - cov.alongCurveWithin γ W s t

Covariant differentiation within a parameter set respects subtraction of differentiable fields.

theorem CovariantDerivative.alongCurve_sub {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V W : (t : 𝕜) → TangentSpace I (γ t)) {t : 𝕜} (hV : DifferentiableAt 𝕜 (TauCeti.Manifold.sectionCoord γ V (γ t)) t) (hW : DifferentiableAt 𝕜 (TauCeti.Manifold.sectionCoord γ W (γ t)) t) : cov.alongCurve γ (fun (r : 𝕜) => V r - W r) t = cov.alongCurve γ V t - cov.alongCurve γ W t

Covariant differentiation along a curve respects subtraction of differentiable fields.

theorem CovariantDerivative.alongCurveWithin_smul {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) (f : 𝕜 → 𝕜) (s : Set 𝕜) {t : 𝕜} (hf : DifferentiableWithinAt 𝕜 f s t) (hV : DifferentiableWithinAt 𝕜 (TauCeti.Manifold.sectionCoord γ V (γ t)) s t) : cov.alongCurveWithin γ (fun (r : 𝕜) => f r • V r) s t = derivWithin f s t • V t + f t • cov.alongCurveWithin γ V s t

The moving-chart candidate within a parameter set obeys the scalar Leibniz rule.

theorem CovariantDerivative.alongCurve_smul {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) (f : 𝕜 → 𝕜) {t : 𝕜} (hf : DifferentiableAt 𝕜 f t) (hV : DifferentiableAt 𝕜 (TauCeti.Manifold.sectionCoord γ V (γ t)) t) : cov.alongCurve γ (fun (r : 𝕜) => f r • V r) t = deriv f t • V t + f t • cov.alongCurve γ V t

The unrestricted moving-chart candidate obeys the scalar Leibniz rule.

@[simp]

theorem CovariantDerivative.alongCurveWithin_const_smul {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) (c : 𝕜) (s : Set 𝕜) (t : 𝕜) : cov.alongCurveWithin γ (fun (r : 𝕜) => c • V r) s t = c • cov.alongCurveWithin γ V s t

The moving-chart candidate within a parameter set commutes with multiplication by a constant scalar, without a differentiability hypothesis on the field.

@[simp]

theorem CovariantDerivative.alongCurve_const_smul {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) (c t : 𝕜) : cov.alongCurve γ (fun (r : 𝕜) => c • V r) t = c • cov.alongCurve γ V t

The unrestricted moving-chart candidate commutes with multiplication by a constant scalar, without a differentiability hypothesis on the field.

@[simp]

theorem CovariantDerivative.alongCurveWithin_zero {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (s : Set 𝕜) (t : 𝕜) : cov.alongCurveWithin γ (fun (r : 𝕜) => 0) s t = 0

The moving-chart candidate of the zero field within a parameter set is zero.

@[simp]

theorem CovariantDerivative.alongCurve_zero {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (t : 𝕜) : cov.alongCurve γ (fun (r : 𝕜) => 0) t = 0

The unrestricted moving-chart candidate of the zero field is zero.

Constant curves

@[simp]

theorem CovariantDerivative.alongCurveWithin_const {𝕜 : 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 (x : M) => TangentSpace I x) (x : M) (W : 𝕜 → E) {s : Set 𝕜} {t : 𝕜} (hs : UniqueDiffWithinAt 𝕜 s t) : cov.alongCurveWithin (fun (x_1 : 𝕜) => x) W s t = derivWithin W s t

Along a constant curve at x, the moving-chart candidate within a parameter set is the ordinary derivative within that set of the field, read in the model space E = T_x M, wherever the set has unique derivatives. No differentiability of the field is needed.

@[simp]

theorem CovariantDerivative.alongCurve_const {𝕜 : 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 (x : M) => TangentSpace I x) (x : M) (W : 𝕜 → E) (t : 𝕜) : cov.alongCurve (fun (x_1 : 𝕜) => x) W t = deriv W t

Along a constant curve at x, the unrestricted moving-chart candidate is the ordinary derivative of the field, read in the model space E = T_x M.

theorem CovariantDerivative.alongCurveWithin_const_of_hasDerivWithinAt {𝕜 : 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 (x : M) => TangentSpace I x) (x : M) {W : 𝕜 → TangentSpace I x} {W' : TangentSpace I x} {s : Set 𝕜} {t : 𝕜} (hW : HasDerivWithinAt W W' s t) (hs : UniqueDiffWithinAt 𝕜 s t) : cov.alongCurveWithin (fun (x_1 : 𝕜) => x) W s t = W'

Along a constant curve at x, the moving-chart candidate within a parameter set is the ordinary derivative of the field in the fixed tangent space TangentSpace I x.

theorem CovariantDerivative.alongCurve_const_of_hasDerivAt {𝕜 : 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 (x : M) => TangentSpace I x) (x : M) {W : 𝕜 → TangentSpace I x} {W' : TangentSpace I x} {t : 𝕜} (hW : HasDerivAt W W' t) : cov.alongCurve (fun (x_1 : 𝕜) => x) W t = W'

Along a constant curve at x, the unrestricted moving-chart candidate is the ordinary derivative of the field in the fixed tangent space TangentSpace I x.

Locality and reparametrization

theorem CovariantDerivative.alongCurveWithin_inter {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) {s u : Set 𝕜} {t : 𝕜} (hu : u ∈ nhds t) : cov.alongCurveWithin γ V (s ∩ u) t = cov.alongCurveWithin γ V s t

Intersecting the parameter set with a neighbourhood of t does not change the moving-chart candidate there.

theorem CovariantDerivative.alongCurveWithin_of_mem_nhds {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) {s : Set 𝕜} {t : 𝕜} (hs : s ∈ nhds t) : cov.alongCurveWithin γ V s t = cov.alongCurve γ V t

On a parameter set which is a neighbourhood of t, the restricted moving-chart candidate equals the unrestricted one.

theorem CovariantDerivative.alongCurveWithin_subset {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) {s u : Set 𝕜} {t : 𝕜} (hsu : s ⊆ u) (hs : UniqueDiffWithinAt 𝕜 s t) (hV : DifferentiableWithinAt 𝕜 (TauCeti.Manifold.sectionCoord γ V (γ t)) u t) (hγ : DifferentiableWithinAt 𝕜 (↑(extChartAt I (γ t)) ∘ γ) u t) : cov.alongCurveWithin γ V s t = cov.alongCurveWithin γ V u t

Restricting the parameter set preserves the moving-chart candidate when derivatives on the larger set are defined and the smaller set has a unique derivative at t.

theorem CovariantDerivative.alongCurveWithin_congr {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) {W : (t : 𝕜) → TangentSpace I (γ t)} {s : Set 𝕜} {t : 𝕜} (h : ∀ᶠ (r : 𝕜) in nhdsWithin t s, V r = W r) (ht : V t = W t) : cov.alongCurveWithin γ V s t = cov.alongCurveWithin γ W s t

The moving-chart candidate within a parameter set depends only on the germ of the field along that set, together with its value at the parameter under consideration.

theorem CovariantDerivative.alongCurve_congr {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) {W : (t : 𝕜) → TangentSpace I (γ t)} {t : 𝕜} (h : ∀ᶠ (r : 𝕜) in nhds t, V r = W r) : cov.alongCurve γ V t = cov.alongCurve γ W t

The unrestricted moving-chart candidate depends only on the germ of the field at the parameter under consideration.

theorem CovariantDerivative.alongCurveWithin_comp {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) (φ : 𝕜 → 𝕜) {s s' : Set 𝕜} {t : 𝕜} (hφ : DifferentiableWithinAt 𝕜 φ s' t) (hmaps : Set.MapsTo φ s' s) (hγ : DifferentiableWithinAt 𝕜 (↑(extChartAt I (γ (φ t))) ∘ γ) s (φ t)) (hV : DifferentiableWithinAt 𝕜 (TauCeti.Manifold.sectionCoord γ V (γ (φ t))) s (φ t)) : cov.alongCurveWithin (γ ∘ φ) (fun (r : 𝕜) => V (φ r)) s' t = derivWithin φ s' t • cov.alongCurveWithin γ V s (φ t)

The moving-chart candidate within a parameter set is natural under differentiable reparametrization mapping that set into the parameter set of the original curve. The curve and the field must both read differentiably at φ t in the chart centred at γ (φ t).

theorem CovariantDerivative.alongCurve_comp {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) (φ : 𝕜 → 𝕜) {t : 𝕜} (hφ : DifferentiableAt 𝕜 φ t) (hγ : DifferentiableAt 𝕜 (↑(extChartAt I (γ (φ t))) ∘ γ) (φ t)) (hV : DifferentiableAt 𝕜 (TauCeti.Manifold.sectionCoord γ V (γ (φ t))) (φ t)) : cov.alongCurve (γ ∘ φ) (fun (r : 𝕜) => V (φ r)) t = deriv φ t • cov.alongCurve γ V (φ t)

The unrestricted moving-chart candidate is natural under differentiable reparametrization. The curve and the field must both read differentiably at φ t in the chart centred at γ (φ t).

Finite sums

theorem CovariantDerivative.alongCurveWithin_sum {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) {ι : Type u_5} (A : Finset ι) (W : ι → (r : 𝕜) → TangentSpace I (γ r)) {s : Set 𝕜} {t : 𝕜} (hW : ∀ i ∈ A, DifferentiableWithinAt 𝕜 (TauCeti.Manifold.sectionCoord γ (W i) (γ t)) s t) : cov.alongCurveWithin γ (fun (r : 𝕜) => ∑ i ∈ A, W i r) s t = ∑ i ∈ A, cov.alongCurveWithin γ (W i) s t

Covariant differentiation within a parameter set commutes with finite sums of fields having differentiable coordinate readings.

theorem CovariantDerivative.alongCurve_sum {𝕜 : 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 (x : M) => TangentSpace I x) (γ : 𝕜 → M) {ι : Type u_5} (A : Finset ι) (W : ι → (r : 𝕜) → TangentSpace I (γ r)) {t : 𝕜} (hW : ∀ i ∈ A, DifferentiableAt 𝕜 (TauCeti.Manifold.sectionCoord γ (W i) (γ t)) t) : cov.alongCurve γ (fun (r : 𝕜) => ∑ i ∈ A, W i r) t = ∑ i ∈ A, cov.alongCurve γ (W i) t

Covariant differentiation along a curve commutes with finite sums of fields having differentiable coordinate readings.