Documentation

TauCeti.Geometry.Manifold.VectorBundle.CovariantDerivative.AlongCurve.Acceleration

The covariant acceleration of a curve #

The covariant acceleration of a curve γ for a connection ∇ on the tangent bundle is the covariant derivative of its velocity field along γ, D_t γ'. It is the along-curve derivative CovariantDerivative.alongCurveWithin of AlongCurve/Basic.lean specialised to the velocity field TauCeti.Manifold.curveVelocityWithin, both taken within a parameter set s; the unrestricted acceleration is the s = Set.univ case. Geodesics are the curves whose covariant acceleration for the Levi-Civita connection vanishes, and the first variation formula for the energy integrates the inner product of the acceleration with the variation field.

In a chart the acceleration is the classical second-order expression u'' + Γ (u', u'), where u is the curve read in the extended chart and Γ is the Christoffel map of the connection. For a C² curve this holds in every chart whose trivialization contains the current point of the curve, by the chart independence CovariantDerivative.symmL_alongCurveInChartWithin of the along-curve derivative. Under a reparametrization φ the acceleration obeys the chain rule D_t (γ ∘ φ)' = φ'' γ'(φ t) + (φ')² D_t γ'(φ t).

Main definitions and results #

References #

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

The covariant acceleration D_t γ' of the curve γ within the parameter set s: the derivative along γ, for the connection cov, of the velocity field of γ within s. It inherits the junk values of CovariantDerivative.alongCurveWithin where the curve is not differentiable or s does not have unique derivatives.

Instances For
    source
    noncomputable def CovariantDerivative.acceleration {𝕜 : 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 : 𝕜) :
    TangentSpace I (γ t)

    The covariant acceleration D_t γ' of the curve γ, with unrestricted derivatives. This is the s = Set.univ case of CovariantDerivative.accelerationWithin.

    Instances For
      source
      theorem CovariantDerivative.accelerationWithin_def {𝕜 : 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.accelerationWithin γ s t = cov.alongCurveWithin γ (TauCeti.Manifold.curveVelocityWithin I γ s) s t

      The covariant acceleration within a parameter set is the derivative of the velocity field along the curve.

      source
      @[simp]
      theorem CovariantDerivative.accelerationWithin_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) (t : 𝕜) :
      cov.accelerationWithin γ Set.univ t = cov.acceleration γ t

      Restricting the acceleration to the whole parameter space gives the unrestricted acceleration.

      source
      theorem CovariantDerivative.acceleration_def {𝕜 : 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.acceleration γ t = cov.alongCurve γ (TauCeti.Manifold.curveVelocity I γ) t

      The unrestricted covariant acceleration is the unrestricted derivative of the unrestricted velocity field along the curve.

      source
      theorem CovariantDerivative.accelerationWithin_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) {s : Set 𝕜} {t : 𝕜} (hs : s ∈ nhds t) :
      cov.accelerationWithin γ s t = cov.acceleration γ t

      On a parameter set which is a neighbourhood of t, the acceleration within that set is the unrestricted acceleration: both the velocity near t and its derivative along the curve are then the unrestricted ones.

      source
      @[simp]
      theorem CovariantDerivative.accelerationWithin_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) (s : Set 𝕜) (t : 𝕜) :
      cov.accelerationWithin (fun (x_1 : 𝕜) => x) s t = 0

      A constant curve has zero covariant acceleration within any parameter set.

      source
      @[simp]
      theorem CovariantDerivative.acceleration_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) (t : 𝕜) :
      cov.acceleration (fun (x_1 : 𝕜) => x) t = 0

      A constant curve has zero unrestricted covariant acceleration.

      source
      theorem CovariantDerivative.accelerationWithin_eq_zero_iff {𝕜 : 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 : 𝕜} (hγ : MDiff[s] γ) (ht : t ∈ s) :
      cov.accelerationWithin γ s t = 0 ↔ derivWithin (derivWithin (↑(extChartAt I (γ t)) ∘ γ) s) s t + ((TauCeti.Manifold.christoffelMap (Module.finBasis 𝕜 E) ⋯ (γ t)) (derivWithin (↑(extChartAt I (γ t)) ∘ γ) s t)) (derivWithin (↑(extChartAt I (γ t)) ∘ γ) s t) = 0

      The covariant acceleration vanishes exactly when the curve read in the extended chart at the current point solves the second-order equation u'' + Γ (u', u') = 0 there.

      source
      theorem CovariantDerivative.accelerationWithin_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) {φ : 𝕜 → 𝕜} {s u : Set 𝕜} {t : 𝕜} (hu : UniqueDiffOn 𝕜 u) (ht : t ∈ u) (hφ : DifferentiableOn 𝕜 φ u) (hφ' : DifferentiableWithinAt 𝕜 (derivWithin φ u) u t) (hmaps : Set.MapsTo φ u s) (hγ : MDiff[s] γ) (hV : DifferentiableWithinAt 𝕜 (TauCeti.Manifold.sectionCoord γ (TauCeti.Manifold.curveVelocityWithin I γ s) (γ (φ t))) s (φ t)) :
      cov.accelerationWithin (γ ∘ φ) u t = derivWithin (derivWithin φ u) u t • TauCeti.Manifold.curveVelocityWithin I γ s (φ t) + derivWithin φ u t ^ 2 • cov.accelerationWithin γ s (φ t)

      The chain rule for the covariant acceleration. If φ maps the parameter set u into s and is differentiable on u, with derivWithin φ u differentiable at t, then D_t (γ ∘ φ)' = φ''(t) γ'(φ t) + φ'(t)² D_t γ'(φ t). The curve must be differentiable on s, and its velocity field must read differentiably at φ t in the chart centred at γ (φ t).

      source
      theorem CovariantDerivative.acceleration_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) {φ : 𝕜 → 𝕜} {t : 𝕜} (hφ : Differentiable 𝕜 φ) (hφ' : DifferentiableAt 𝕜 (deriv φ) t) (hγ : MDiff γ) (hV : DifferentiableAt 𝕜 (TauCeti.Manifold.sectionCoord γ (TauCeti.Manifold.curveVelocity I γ) (γ (φ t))) (φ t)) :
      cov.acceleration (γ ∘ φ) t = deriv (deriv φ) t • TauCeti.Manifold.curveVelocity I γ (φ t) + deriv φ t ^ 2 • cov.acceleration γ (φ t)

      The chain rule for the unrestricted covariant acceleration: D_t (γ ∘ φ)' = φ''(t) γ'(φ t) + φ'(t)² D_t γ'(φ t).

      source
      theorem CovariantDerivative.accelerationWithin_eq_symmL {𝕜 : 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) {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) :
      cov.accelerationWithin γ s t = (Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) 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 covariant acceleration in a chart. For a C² curve on a parameter set with unique derivatives, the acceleration at t is the classical second-order expression u'' + Γ (u', u'), for u the curve read in the extended chart at x and Γ the Christoffel map of cov there, transported back from the trivialization at x. The chart is arbitrary, provided its trivialization contains γ t.