The transverse derivatives of the metric pairings along a variation

A variation of a curve γ in a manifold is a two-parameter family F : ℝ → ℝ → M with F 0 = γ, whose first argument is the variation parameter s and whose second argument is the curve parameter t. Its variation field V = TauCeti.Manifold.variationField I F, defined in TauCeti.Geometry.Manifold.MFDeriv.Curve, is the transverse velocity V(t) = ∂F/∂s (0, t), a tangent vector at γ t. Hypotheses on a variation are stated on the uncurried map fun z : ℝ × ℝ ↦ F z.1 z.2.

In a Riemannian manifold with its Levi-Civita connection, this file records the two pointwise derivative formulas that variational arguments consume, valid at every parameter where the family is C²: the transverse derivative of the squared speed of the curves F s, and the product rule for ⟪V, γ'⟫ along γ. They are the pointwise content of the Gauss lemma (TauCeti.Geometry.Manifold.Riemannian.Geodesic.Gauss.Basic) and of the first variation of energy (TauCeti.Geometry.Manifold.Riemannian.FirstVariation.Basic).

Main results

• TauCeti.Manifold.hasDerivAt_norm_sq_curveVelocity: the transverse derivative of the squared speed is 2 ⟪D_t V, γ'⟫.
• TauCeti.Manifold.hasDerivAt_inner_variationField_curveVelocity: the product rule d/dt ⟪V, γ'⟫ = ⟪D_t V, γ'⟫ + ⟪V, D_t γ'⟫.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 3, §3, Lemma 3.5 and Ch. 9, §2, Proposition 2.4, whose proofs are the two derivative formulas.
• J. M. Lee, Introduction to Riemannian Manifolds, GTM 176, 2nd ed., 2018, Ch. 6, variations of curves and their variation fields.

theorem TauCeti.Manifold.hasDerivAt_norm_sq_curveVelocity {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] {F : ℝ → ℝ → M} [FiniteDimensional ℝ E] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {t : ℝ} (hf : ContMDiffAt (modelWithCornersSelf ℝ (ℝ × ℝ)) I 2 (fun (z : ℝ × ℝ) => F z.1 z.2) (0, t)) : HasDerivAt (fun (s : ℝ) => ‖curveVelocity I (F s) t‖ ^ 2) (2 * inner ℝ ((CovariantDerivative.leviCivitaConnection I M).alongCurve (F 0) (variationField I F) t) (curveVelocity I (F 0) t)) 0

The transverse derivative of the squared speed. At a parameter t where the family is C², the function s ↦ ‖∂_t F (s, t)‖² has derivative 2 ⟪D_t V(t), γ'(t)⟫ at s = 0, where V is the variation field and γ = F 0. Integrated over [a, b], this is the derivative of the energy of the curves F s in the first variation formula.

theorem TauCeti.Manifold.hasDerivAt_inner_variationField_curveVelocity {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] {F : ℝ → ℝ → M} [FiniteDimensional ℝ E] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {t : ℝ} (hf : ContMDiffAt (modelWithCornersSelf ℝ (ℝ × ℝ)) I 2 (fun (z : ℝ × ℝ) => F z.1 z.2) (0, t)) : HasDerivAt (fun (r : ℝ) => inner ℝ (variationField I F r) (curveVelocity I (F 0) r)) (inner ℝ ((CovariantDerivative.leviCivitaConnection I M).alongCurve (F 0) (variationField I F) t) (curveVelocity I (F 0) t) + inner ℝ (variationField I F t) ((CovariantDerivative.leviCivitaConnection I M).acceleration (F 0) t)) t

The product rule for the variation field against the velocity. At a parameter where the family is C², the function t ↦ ⟪V(t), γ'(t)⟫ has derivative ⟪D_t V, γ'⟫ + ⟪V, D_t γ'⟫. Integrated over [a, b], this is the integration by parts in the first variation formula.