Metric compatibility along a curve

This file proves the product rule for a metric-compatible covariant derivative acting on tangent fields along a curve:

(d/dt) ⟪V, W⟫ = ⟪D V / dt, W⟫ + ⟪V, D W / dt⟫.

The product rule is first proved for an arbitrary pointwise bilinear pairing b of tangent vectors, neither symmetric nor nondegenerate, which pairs differentiable vector fields to differentiable functions and satisfies the ambient product rule v (b(Y, Z)) = b(∇_v Y, Z) + b(Y, ∇_v Z) at the current point of the curve. Fields pulled back from differentiable vector fields satisfy it by the chain rule. A differentiable field along the curve is locally a finite linear combination of pullbacks of smooth local-frame fields; the additive and scalar Leibniz laws of CovariantDerivative.alongCurveWithin finish the argument. The Riemannian product rule is the specialization to the inner product, using Mathlib's ambient CovariantDerivative.IsMetricCompatible.mvfderiv_inner_eq; metrics of other signatures specialize the same theorem.

Main results

• CovariantDerivative.hasDerivWithinAt_apply_alongCurveWithin: the within-set product rule for a pointwise bilinear pairing satisfying the ambient product rule.
• CovariantDerivative.IsMetricCompatible.hasDerivWithinAt_inner_alongCurveWithin: the within-set metric product rule for two differentiable tangent fields along a differentiable real curve.
• CovariantDerivative.IsMetricCompatible.differentiableWithinAt_inner and CovariantDerivative.IsMetricCompatible.derivWithin_inner_alongCurveWithin: its two principal consequences.
• CovariantDerivative.IsMetricCompatible.hasDerivAt_inner_alongCurve: the unrestricted form, with CovariantDerivative.IsMetricCompatible.differentiableAt_inner and CovariantDerivative.IsMetricCompatible.deriv_inner_alongCurve as consequences.
• CovariantDerivative.IsMetricCompatible.inner_alongCurveWithin_self_eq_zero_of_eventually_norm_eq and CovariantDerivative.IsMetricCompatible.inner_alongCurve_self_eq_zero_of_eventually_norm_eq: a field of locally constant length is orthogonal to its covariant derivative.
• CovariantDerivative.IsMetricCompatible.inner_eq_of_alongCurveWithin_eq_zero: parallel fields along a curve have constant inner product.
• CovariantDerivative.IsMetricCompatible.eq_of_alongCurveWithin_eq_zero and CovariantDerivative.IsMetricCompatible.eq_of_alongCurve_eq_zero: parallel fields that agree at one parameter agree on the whole preconnected parameter set.

References

• M. P. do Carmo, Riemannian Geometry, Chapter 2, Proposition 3.2.
• The proof organization is adapted from DoCarmoLib/Riemannian/Connection/MetricCompatibilityAlong.lean in the Apache-2.0 frenzymath/Poincare-Conjecture repository, revision 24f32e4d600878bfaac6bc2f2f9324175571c321, replacing its custom connection and metric APIs with Mathlib's CovariantDerivative.IsMetricCompatible and Tau Ceti's moving-chart derivative.

theorem CovariantDerivative.hasDerivWithinAt_apply_alongCurveWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [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 : ℝ} {b : (x : M) → TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ} (hdiff : ∀ ⦃Y Z : (x : M) → TangentSpace I x⦄, (MDiffAt fun (x : M) => ⟨x, Y x⟩) (γ t) → (MDiffAt fun (x : M) => ⟨x, Z x⟩) (γ t) → (MDiffAt fun (y : M) => ((b y) (Y y)) (Z y)) (γ t)) (hcompat : ∀ ⦃Y Z : (x : M) → TangentSpace I x⦄, (MDiffAt fun (x : M) => ⟨x, Y x⟩) (γ t) → (MDiffAt fun (x : M) => ⟨x, Z x⟩) (γ t) → ∀ (v : TangentSpace I (γ t)), ((d% fun (y : M) => ((b y) (Y y)) (Z y)) (γ t)) v = ((b (γ t)) ((↑cov Y (γ t)) v)) (Z (γ t)) + ((b (γ t)) (Y (γ t))) ((↑cov Z (γ t)) v)) (hγ : MDiffAt[s] γ t) {V W : (r : ℝ) → TangentSpace I (γ r)} (hV : DifferentiableWithinAt ℝ (TauCeti.Manifold.sectionCoord γ V (γ t)) s t) (hW : DifferentiableWithinAt ℝ (TauCeti.Manifold.sectionCoord γ W (γ t)) s t) : HasDerivWithinAt (fun (r : ℝ) => ((b (γ r)) (V r)) (W r)) (((b (γ t)) (cov.alongCurveWithin γ V s t)) (W t) + ((b (γ t)) (V t)) (cov.alongCurveWithin γ W s t)) s t

The product rule along a curve for a pointwise bilinear pairing b of tangent vectors. Suppose that b pairs vector fields differentiable at γ t to a function differentiable at γ t, and that the covariant derivative satisfies the ambient product rule v (b(Y, Z)) = b(∇_v Y, Z) + b(Y, ∇_v Z) there. Then for two tangent fields along γ whose coordinate readings are differentiable within s at t, (d/dt) b(V, W) = b(D V / dt, W) + b(V, D W / dt) within s at t.

Neither symmetry nor nondegeneracy of b is needed.

theorem CovariantDerivative.IsMetricCompatible.hasDerivWithinAt_inner_alongCurveWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [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 : ℝ} [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (hcov : cov.IsMetricCompatible) (hγ : MDiffAt[s] γ t) {V W : (r : ℝ) → TangentSpace I (γ r)} (hV : DifferentiableWithinAt ℝ (TauCeti.Manifold.sectionCoord γ V (γ t)) s t) (hW : DifferentiableWithinAt ℝ (TauCeti.Manifold.sectionCoord γ W (γ t)) s t) : HasDerivWithinAt (fun (r : ℝ) => inner ℝ (V r) (W r)) (inner ℝ (cov.alongCurveWithin γ V s t) (W t) + inner ℝ (V t) (cov.alongCurveWithin γ W s t)) s t

The within-set product rule for a metric-compatible covariant derivative acting on two differentiable tangent fields along a differentiable real curve.

theorem CovariantDerivative.IsMetricCompatible.differentiableWithinAt_inner {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [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 : ℝ} [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (hcov : cov.IsMetricCompatible) (hγ : MDiffAt[s] γ t) {V W : (r : ℝ) → TangentSpace I (γ r)} (hV : DifferentiableWithinAt ℝ (TauCeti.Manifold.sectionCoord γ V (γ t)) s t) (hW : DifferentiableWithinAt ℝ (TauCeti.Manifold.sectionCoord γ W (γ t)) s t) : DifferentiableWithinAt ℝ (fun (r : ℝ) => inner ℝ (V r) (W r)) s t

The fibrewise inner product of two differentiable tangent fields along a differentiable curve is differentiable within the parameter set.

theorem CovariantDerivative.IsMetricCompatible.derivWithin_inner_alongCurveWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [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 : ℝ} [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (hcov : cov.IsMetricCompatible) (hγ : MDiffAt[s] γ t) {V W : (r : ℝ) → TangentSpace I (γ r)} (hV : DifferentiableWithinAt ℝ (TauCeti.Manifold.sectionCoord γ V (γ t)) s t) (hW : DifferentiableWithinAt ℝ (TauCeti.Manifold.sectionCoord γ W (γ t)) s t) : derivWithin (fun (r : ℝ) => inner ℝ (V r) (W r)) s t = inner ℝ (cov.alongCurveWithin γ V s t) (W t) + inner ℝ (V t) (cov.alongCurveWithin γ W s t)

The derivative identity supplied by metric compatibility within a parameter set.

theorem CovariantDerivative.IsMetricCompatible.hasDerivAt_inner_alongCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [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 : ℝ} [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (hcov : cov.IsMetricCompatible) (hγ : MDiffAt γ t) {V W : (r : ℝ) → TangentSpace I (γ r)} (hV : DifferentiableAt ℝ (TauCeti.Manifold.sectionCoord γ V (γ t)) t) (hW : DifferentiableAt ℝ (TauCeti.Manifold.sectionCoord γ W (γ t)) t) : HasDerivAt (fun (r : ℝ) => inner ℝ (V r) (W r)) (inner ℝ (cov.alongCurve γ V t) (W t) + inner ℝ (V t) (cov.alongCurve γ W t)) t

The unrestricted product rule for a metric-compatible covariant derivative acting on two differentiable tangent fields along a differentiable real curve.

theorem CovariantDerivative.IsMetricCompatible.differentiableAt_inner {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [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 : ℝ} [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (hcov : cov.IsMetricCompatible) (hγ : MDiffAt γ t) {V W : (r : ℝ) → TangentSpace I (γ r)} (hV : DifferentiableAt ℝ (TauCeti.Manifold.sectionCoord γ V (γ t)) t) (hW : DifferentiableAt ℝ (TauCeti.Manifold.sectionCoord γ W (γ t)) t) : DifferentiableAt ℝ (fun (r : ℝ) => inner ℝ (V r) (W r)) t

The fibrewise inner product of two differentiable tangent fields along a differentiable curve is differentiable.

theorem CovariantDerivative.IsMetricCompatible.deriv_inner_alongCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [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 : ℝ} [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (hcov : cov.IsMetricCompatible) (hγ : MDiffAt γ t) {V W : (r : ℝ) → TangentSpace I (γ r)} (hV : DifferentiableAt ℝ (TauCeti.Manifold.sectionCoord γ V (γ t)) t) (hW : DifferentiableAt ℝ (TauCeti.Manifold.sectionCoord γ W (γ t)) t) : deriv (fun (r : ℝ) => inner ℝ (V r) (W r)) t = inner ℝ (cov.alongCurve γ V t) (W t) + inner ℝ (V t) (cov.alongCurve γ W t)

The product rule for a metric-compatible covariant derivative acting on two differentiable tangent fields along a differentiable real curve.

theorem CovariantDerivative.IsMetricCompatible.inner_alongCurveWithin_self_eq_zero_of_eventually_norm_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [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 : ℝ} [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (hcov : cov.IsMetricCompatible) (hu : UniqueDiffWithinAt ℝ s t) (hγ : MDiffAt[s] γ t) {V : (r : ℝ) → TangentSpace I (γ r)} (hV : DifferentiableWithinAt ℝ (TauCeti.Manifold.sectionCoord γ V (γ t)) s t) (hnorm : ∀ᶠ (r : ℝ) in nhdsWithin t s, ‖V r‖ = ‖V t‖) : inner ℝ (cov.alongCurveWithin γ V s t) (V t) = 0

A field of locally constant length is orthogonal to its covariant derivative. If a differentiable tangent field V along a differentiable real curve has constant metric length on the parameter set s near t, then D V / dt is orthogonal to V at t, for a metric-compatible covariant derivative.

theorem CovariantDerivative.IsMetricCompatible.inner_alongCurve_self_eq_zero_of_eventually_norm_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [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 : ℝ} [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (hcov : cov.IsMetricCompatible) (hγ : MDiffAt γ t) {V : (r : ℝ) → TangentSpace I (γ r)} (hV : DifferentiableAt ℝ (TauCeti.Manifold.sectionCoord γ V (γ t)) t) (hnorm : ∀ᶠ (r : ℝ) in nhds t, ‖V r‖ = ‖V t‖) : inner ℝ (cov.alongCurve γ V t) (V t) = 0

A field of locally constant length is orthogonal to its covariant derivative, for the unrestricted covariant derivative along a differentiable real curve.

theorem CovariantDerivative.IsMetricCompatible.inner_eq_of_alongCurveWithin_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [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 ℝ} [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (hcov : cov.IsMetricCompatible) (hconn : IsPreconnected s) (hγ : MDiff[s] γ) {V W : (r : ℝ) → TangentSpace I (γ r)} (hV : ∀ t ∈ s, DifferentiableWithinAt ℝ (TauCeti.Manifold.sectionCoord γ V (γ t)) s t) (hW : ∀ t ∈ s, DifferentiableWithinAt ℝ (TauCeti.Manifold.sectionCoord γ W (γ t)) s t) (hV₀ : ∀ t ∈ s, cov.alongCurveWithin γ V s t = 0) (hW₀ : ∀ t ∈ s, cov.alongCurveWithin γ W s t = 0) {a b : ℝ} (ha : a ∈ s) (hb : b ∈ s) : inner ℝ (V a) (W a) = inner ℝ (V b) (W b)

Parallel transport preserves the inner product. On a preconnected parameter set, two tangent fields along a differentiable curve that have differentiable coordinate readings and are parallel, D V / dt = D W / dt = 0 on s, have the same inner product at every two parameters of s.

theorem CovariantDerivative.IsMetricCompatible.eq_of_alongCurveWithin_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [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 ℝ} [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (hcov : cov.IsMetricCompatible) (hconn : IsPreconnected s) (hγ : MDiff[s] γ) {V W : (r : ℝ) → TangentSpace I (γ r)} (hV : ∀ t ∈ s, DifferentiableWithinAt ℝ (TauCeti.Manifold.sectionCoord γ V (γ t)) s t) (hW : ∀ t ∈ s, DifferentiableWithinAt ℝ (TauCeti.Manifold.sectionCoord γ W (γ t)) s t) (hV₀ : ∀ t ∈ s, cov.alongCurveWithin γ V s t = 0) (hW₀ : ∀ t ∈ s, cov.alongCurveWithin γ W s t = 0) {a b : ℝ} (ha : a ∈ s) (hb : b ∈ s) (hinit : V a = W a) : V b = W b

Uniqueness of parallel fields. On a preconnected parameter set, two parallel tangent fields along a differentiable curve that agree at one parameter agree at every parameter of the set.

theorem CovariantDerivative.IsMetricCompatible.eq_of_alongCurve_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [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 ℝ} [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (hcov : cov.IsMetricCompatible) (hconn : IsPreconnected s) (hγ : ∀ t ∈ s, MDiffAt γ t) {V W : (r : ℝ) → TangentSpace I (γ r)} (hV : ∀ t ∈ s, DifferentiableAt ℝ (TauCeti.Manifold.sectionCoord γ V (γ t)) t) (hW : ∀ t ∈ s, DifferentiableAt ℝ (TauCeti.Manifold.sectionCoord γ W (γ t)) t) (hV₀ : ∀ t ∈ s, cov.alongCurve γ V t = 0) (hW₀ : ∀ t ∈ s, cov.alongCurve γ W t = 0) {a b : ℝ} (ha : a ∈ s) (hb : b ∈ s) (hinit : V a = W a) : V b = W b

Uniqueness of parallel fields, for the unrestricted covariant derivative: two parallel tangent fields along a differentiable curve that agree at one parameter agree on the whole preconnected parameter set.