Metric compatibility and higher metric product rules

This module characterizes metric compatibility as the vanishing of derivMetricTensor, without assuming manifold regularity (CovariantDerivative.isMetricCompatible_iff_derivMetricTensor_eq_zero).

It also records the twice-differentiated product rule for a metric-compatible covariant derivative. It supplies the second-derivative calculation used to establish curvature skew-adjointness and can be reused in other calculations with metric-compatible connections.

It also restates metric compatibility with a bundled metric g, installed as the RiemannianBundle instance, in terms of the inner products of g (Bundle.ContMDiffRiemannianMetric.isMetricCompatible_iff_inner). This is the form in which connections are compared across different metrics on the same bundle.

For a metric-compatible torsion-free connection ∇ on the tangent bundle, it expresses the Lie derivative of the metric through ∇: (𝓛_X g)(Y, Z) = ⟪∇_Y X, Z⟫ + ⟪Y, ∇_Z X⟫ (CovariantDerivative.IsMetricCompatible.mvfderiv_inner_sub_inner_mlieBracket).

theorem CovariantDerivative.isMetricCompatible_iff_derivMetricTensor_eq_zero {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 : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → NormedAddCommGroup (V x)] [(x : M) → InnerProductSpace ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle 1 F V I] [IsContMDiffRiemannianBundle I 1 F V] {cov : CovariantDerivative I F V} : cov.IsMetricCompatible ↔ cov.derivMetricTensor = fun (x : M) => 0

Metric compatibility is precisely the vanishing of the covariant derivative of the metric as a tensor. Unlike the section-based characterization, this needs no manifold regularity.

theorem CovariantDerivative.IsMetricCompatible.hasMFDerivAt_inner_of_eq_zero {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 : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → NormedAddCommGroup (V x)] [(x : M) → InnerProductSpace ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle 1 F V I] [IsContMDiffRiemannianBundle I 1 F V] {cov : CovariantDerivative I F V} (hcov : cov.IsMetricCompatible) {σ τ : (x : M) → V x} {x : M} (hσ : (MDiffAt fun (x : M) => ⟨x, σ x⟩) x) (hτ : (MDiffAt fun (x : M) => ⟨x, τ x⟩) x) (hσ₀ : ↑cov σ x = 0) (hτ₀ : ↑cov τ x = 0) : HasMFDerivAt% (fun (y : M) => inner ℝ (σ y) (τ y)) x 0

The inner product of two sections parallel at a point has zero derivative there.

theorem CovariantDerivative.IsMetricCompatible.mvfderiv_mvfderiv_inner {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 : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → NormedAddCommGroup (V x)] [(x : M) → InnerProductSpace ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle 1 F V I] [IsContMDiffRiemannianBundle I 1 F V] {cov : CovariantDerivative I F V} [IsManifold I 1 M] {n : WithTop ℕ∞} [cov.ContMDiffCovariantDerivative n] (hcov : cov.IsMetricCompatible) {X Y : (x : M) → TangentSpace I x} {σ τ : (x : M) → V x} (hn : 1 ≤ n) (hY : ContMDiff I I.tangent n fun (x : M) => ⟨x, Y x⟩) (hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) (n + 1) fun (x : M) => ⟨x, σ x⟩) (hτ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) (n + 1) fun (x : M) => ⟨x, τ x⟩) (x : M) : ((d% fun (y : M) => ((d% fun (z : M) => inner ℝ (σ z) (τ z)) y) (Y y)) x) (X x) = inner ℝ ((↑cov (fun (y : M) => (↑cov σ y) (Y y)) x) (X x)) (τ x) + inner ℝ ((↑cov σ x) (Y x)) ((↑cov τ x) (X x)) + (inner ℝ ((↑cov σ x) (X x)) ((↑cov τ x) (Y x)) + inner ℝ (σ x) ((↑cov (fun (y : M) => (↑cov τ y) (Y y)) x) (X x)))

The twice-differentiated metric product rule for a C^n metric-compatible connection.

theorem CovariantDerivative.IsMetricCompatible.mvfderiv_inner_sub_inner_mlieBracket {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_7} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) {X Y Z : (x : M) → TangentSpace I x} {x : M} (hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) x) (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (hZ : (MDiffAt fun (x : M) => ⟨x, Z x⟩) x) : ((d% fun (y : M) => inner ℝ (Y y) (Z y)) x) (X x) - inner ℝ (VectorField.mlieBracket I X Y x) (Z x) - inner ℝ (Y x) (VectorField.mlieBracket I X Z x) = inner ℝ ((↑cov X x) (Y x)) (Z x) + inner ℝ (Y x) ((↑cov X x) (Z x))

For a metric-compatible torsion-free connection, the Lie derivative of the metric along X is (𝓛_X g)(Y, Z) = ⟪∇_Y X, Z⟫ + ⟪Y, ∇_Z X⟫.

theorem Bundle.ContMDiffRiemannianMetric.isMetricCompatible_iff_inner {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] [IsManifold I 1 M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5} [TopologicalSpace (TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle 1 F V I] {n : WithTop ℕ∞} (g : ContMDiffRiemannianMetric I n F V) (hn : 1 ≤ n) (cov : CovariantDerivative I F V) : cov.IsMetricCompatible ↔ ∀ ⦃x : M⦄ ⦃X : (x : M) → TangentSpace I x⦄ ⦃σ τ : (x : M) → V x⦄, (MDiffAt fun (x : M) => ⟨x, X x⟩) x → (MDiffAt fun (x : M) => ⟨x, σ x⟩) x → (MDiffAt fun (x : M) => ⟨x, τ x⟩) x → ((d% fun (y : M) => ((g.inner y) (σ y)) (τ y)) x) (X x) = ((g.inner x) ((↑cov σ x) (X x))) (τ x) + ((g.inner x) (σ x)) ((↑cov τ x) (X x))

Metric compatibility with a C¹ bundled metric g, installed as the RiemannianBundle instance, written with the inner products of g.