Regularity of the Levi-Civita connection

On a C^m manifold carrying a C^k Riemannian metric, Mathlib's Levi-Civita connection CovariantDerivative.leviCivitaConnection is C^n once n + 2 ≤ m and n + 1 ≤ k: it sends a C^(n+1) section of the tangent bundle to a C^n section of Hom(TM, TM). This file proves that, in the class form ContMDiffCovariantDerivative which Mathlib's covariant-derivative API consumes — a class which already carries that one-derivative loss, asking a C^(n+1) section to produce a C^n one — together with the set-local form on an arbitrary open set. Taking n = m = k = ∞ the loss is invisible and the Levi-Civita connection of a C^∞ metric on a C^∞ manifold is C^∞, which is the instance CovariantDerivative.instContMDiffCovariantDerivativeLeviCivitaConnection.

The proof follows the Koszul formula 2 ⟪∇_X Y, Z⟫ = koszul I X Y Z. The right-hand side is built from derivatives of pointwise inner products and from Lie brackets, so it loses exactly one degree of smoothness; that is where n + 1 ≤ k comes from, and the extra degree in n + 2 ≤ m is the one Mathlib's Lie-bracket regularity asks of the manifold. Concretely:

• TauCeti.Manifold.contMDiffOn_koszul reads the Koszul expression as a sum of directional derivatives of inner products (ContMDiffOn.contMDiffOn_mvfderiv_apply) and of inner products with Lie brackets (ContMDiffWithinAt.mlieBracketWithin_vectorField);
• the fibrewise Riesz dual of Riemannian.Tensor.contMDiffAt_rieszDual turns smoothness of the numbers ⟪∇_{e_j} σ, e_k⟫ into smoothness of the vector fields ∇_{e_j} σ, for e the chart-local frame;
• TauCeti.Manifold.contMDiffOn_hom_of_localFrame assembles those directions into the hom-bundle section ∇σ demanded by ContMDiffCovariantDerivativeOn.

With the class available, the local Christoffel data of TauCeti.Geometry.Manifold.VectorBundle.CovariantDerivative.LocalFrame becomes unconditional for the Levi-Civita connection: its scalar Christoffel symbols and its model-space Christoffel map are C^n on the base set of every trivialization in the atlas.

The ambient orders m and k are carried as instance arguments and compared to the conclusion by the hypotheses n + 2 ≤ m and n + 1 ≤ k, rather than being spelled n + 2 and n + 1 outright, so that the C^∞ case remains an instantiation: Mathlib's instance search derives IsManifold I m M from IsManifold I ∞ M for m = ∞, but not IsManifold I (n + 2) M for a variable n. The low-order hypotheses [IsManifold I 2 M] and [IsContMDiffRiemannianBundle I 1 E _], which CovariantDerivative.leviCivitaConnection needs merely to be written down, are carried for the same reason.

Main results

• TauCeti.Manifold.contMDiffOn_koszulBilinear_family: the same, jointly in the parameter and the point, for a family of bilinear pairings parametrized by a manifold.
• TauCeti.Manifold.contMDiffOn_koszulBilinear: the Koszul expression of a C^(n+1) bilinear pairing and three C^(n+1) vector fields is C^n, without symmetry or nondegeneracy.
• TauCeti.Manifold.contMDiffOn_koszul: the Koszul expression of three C^(n+1) sections is C^n.
• CovariantDerivative.contMDiffOn_leviCivitaConnection: on an open set, the Levi-Civita connection carries a C^(n+1) section to a C^n section of Hom(TM, TM).
• CovariantDerivative.contMDiffCovariantDerivativeOn_leviCivitaConnection and the instance CovariantDerivative.instContMDiffCovariantDerivativeLeviCivitaConnection: the Levi-Civita connection is of class C^n, and in particular C^∞ for a C^∞ metric.
• CovariantDerivative.contMDiffOn_christoffelSymbol_leviCivitaConnection and CovariantDerivative.contMDiffOn_christoffelMap_leviCivitaConnection: its Christoffel symbols and its model-space Christoffel map are C^n on a trivialization base set.
• TauCeti.Manifold.contMDiffOn_alongCurveWithin_leviCivitaConnection and TauCeti.Manifold.differentiableWithinAt_sectionCoord_alongCurveWithin_leviCivitaConnection: along a curve, the Levi-Civita derivative of a section with a C² tangent-bundle lift has a C¹ lift and differentiable coordinate readings.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 2, §3.
• J. M. Lee, Introduction to Riemannian Manifolds, GTM 176, 2018, Thm. 5.10.

theorem TauCeti.Manifold.contMDiffOn_koszulBilinear_family {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] {n m : WithTop ℕ∞} [IsManifold I 1 M] [IsManifold I m M] [CompleteSpace E] {EP : Type u_4} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_5} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_6} [TopologicalSpace P] [ChartedSpace HP P] [IsManifold IP 1 P] {s : Set M} (hs : IsOpen s) (hm : n + 2 ≤ m) {b : P → (x : M) → TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ} (hb : ContMDiffOn (IP.prod I) (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) (n + 1) (fun (q : P × M) => ⟨q.2, b q.1 q.2⟩) (Set.univ ×ˢ s)) {X Y Z : (x : M) → TangentSpace I x} (hX : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ E)) (n + 1) (fun (y : M) => ⟨y, X y⟩) s) (hY : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ E)) (n + 1) (fun (y : M) => ⟨y, Y y⟩) s) (hZ : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ E)) (n + 1) (fun (y : M) => ⟨y, Z y⟩) s) : ContMDiffOn (IP.prod I) (modelWithCornersSelf ℝ ℝ) n (fun (q : P × M) => koszulBilinear I (b q.1) X Y Z q.2) (Set.univ ×ˢ s)

The Koszul expressions of a family of fields of bilinear forms, parametrized by P and jointly C^(n+1) in the parameter and the point, and of three C^(n+1) vector fields are jointly C^n on the product of P with an open set. Neither symmetry nor nondegeneracy is needed.

theorem TauCeti.Manifold.contMDiffOn_koszulBilinear {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] {n m : WithTop ℕ∞} [IsManifold I 1 M] [IsManifold I m M] [CompleteSpace E] {s : Set M} (hs : IsOpen s) (hm : n + 2 ≤ m) {b : (x : M) → TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ} (hb : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) (n + 1) (fun (y : M) => ⟨y, b y⟩) s) {X Y Z : (x : M) → TangentSpace I x} (hX : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ E)) (n + 1) (fun (y : M) => ⟨y, X y⟩) s) (hY : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ E)) (n + 1) (fun (y : M) => ⟨y, Y y⟩) s) (hZ : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ E)) (n + 1) (fun (y : M) => ⟨y, Z y⟩) s) : ContMDiffOn I (modelWithCornersSelf ℝ ℝ) n (koszulBilinear I b X Y Z) s

The Koszul expression of a C^(n+1) field of bilinear forms and three C^(n+1) vector fields is C^n on an open set. Neither symmetry nor nondegeneracy is needed.

theorem TauCeti.Manifold.contMDiffOn_koszul {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {n m k : WithTop ℕ∞} [IsManifold I 1 M] [IsManifold I m M] [IsContMDiffRiemannianBundle I k E fun (x : M) => TangentSpace I x] {s : Set M} (hs : IsOpen s) (hm : n + 2 ≤ m) (hk : n + 1 ≤ k) {X Y Z : (x : M) → TangentSpace I x} (hX : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ E)) (n + 1) (fun (y : M) => ⟨y, X y⟩) s) (hY : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ E)) (n + 1) (fun (y : M) => ⟨y, Y y⟩) s) (hZ : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ E)) (n + 1) (fun (y : M) => ⟨y, Z y⟩) s) : ContMDiffOn I (modelWithCornersSelf ℝ ℝ) n (koszul I X Y Z) s

The Koszul expression of three C^(n+1) sections is C^n. Both the derivative terms and the Lie-bracket terms lose one degree of smoothness, whence the two hypotheses on the smoothness of the manifold and of the metric.

theorem CovariantDerivative.contMDiffOn_leviCivitaConnection {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {n m k : WithTop ℕ∞} [IsManifold I m M] [IsContMDiffRiemannianBundle I k E fun (x : M) => TangentSpace I x] {u : Set M} (hu : IsOpen u) (hm : n + 2 ≤ m) (hk : n + 1 ≤ k) {σ : (x : M) → TangentSpace I x} (hσ : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ E)) (n + 1) (fun (y : M) => ⟨y, σ y⟩) u) : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E))) n (fun (y : M) => ⟨y, ↑(leviCivitaConnection I M) σ y⟩) u

The Levi-Civita connection differentiates with one derivative lost. On an open set u, a section of the tangent bundle which is C^(n+1) on u has a covariant derivative which is C^n on u as a section of Hom(TM, TM).

theorem CovariantDerivative.contMDiffCovariantDerivativeOn_leviCivitaConnection {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {n m k : WithTop ℕ∞} [IsManifold I m M] [IsContMDiffRiemannianBundle I k E fun (x : M) => TangentSpace I x] {u : Set M} (hu : IsOpen u) (hm : n + 2 ≤ m) (hk : n + 1 ≤ k) : ContMDiffCovariantDerivativeOn E n (↑(leviCivitaConnection I M)) u

The Levi-Civita connection is of class C^n, in the set-local form used to read it in a local frame.

theorem CovariantDerivative.contMDiffOn_christoffelSymbol_leviCivitaConnection {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {n m k : WithTop ℕ∞} [IsManifold I m M] [IsContMDiffRiemannianBundle I k E fun (x : M) => TangentSpace I x] {ι : Type u_4} (b : Module.Basis ι ℝ E) {e : Bundle.Trivialization E Bundle.TotalSpace.proj} [MemTrivializationAtlas e] (hm : n + 2 ≤ m) (hk : n + 1 ≤ k) (i j l : ι) : ContMDiffOn I (modelWithCornersSelf ℝ ℝ) n (TauCeti.Manifold.christoffelSymbol I b e (↑(leviCivitaConnection I M)) i j l) e.baseSet

The scalar Christoffel symbols of the Levi-Civita connection in a local frame are C^n on the base set of the trivialization defining the frame.

theorem CovariantDerivative.contMDiffOn_christoffelMap_leviCivitaConnection {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {n m k : WithTop ℕ∞} [IsManifold I m M] [IsContMDiffRiemannianBundle I k E fun (x : M) => TangentSpace I x] {ι : Type u_4} (b : Module.Basis ι ℝ E) {e : Bundle.Trivialization E Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [Fintype ι] (hm : n + 2 ≤ m) (hk : n + 1 ≤ k) : ContMDiffOn I (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] E)) n (TauCeti.Manifold.christoffelMap b ⋯) e.baseSet

The model-space Christoffel map of the Levi-Civita connection is C^n on the base set of the trivialization defining its coordinates.

instance CovariantDerivative.instContMDiffCovariantDerivativeLeviCivitaConnection {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] : (leviCivitaConnection I M).ContMDiffCovariantDerivative ↑⊤

The Levi-Civita connection of a C^∞ metric on a C^∞ manifold is C^∞.

theorem TauCeti.Manifold.contMDiffOn_alongCurveWithin_leviCivitaConnection {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 (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {V : (t : ℝ) → TangentSpace I (γ t)} {s : Set ℝ} (hs : UniqueDiffOn ℝ s) (hV : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I.tangent 2 (fun (r : ℝ) => ⟨γ r, V r⟩) s) : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I.tangent 1 (fun (r : ℝ) => ⟨γ r, (CovariantDerivative.leviCivitaConnection I M).alongCurveWithin γ V s r⟩) s

The Levi-Civita covariant derivative of a section with a C² tangent-bundle lift, within a parameter set with unique derivatives, has a C¹ tangent-bundle lift.

theorem TauCeti.Manifold.differentiableWithinAt_sectionCoord_alongCurveWithin_leviCivitaConnection {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 (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {V : (t : ℝ) → TangentSpace I (γ t)} {s : Set ℝ} {t : ℝ} (hs : UniqueDiffOn ℝ s) (hV : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I.tangent 2 (fun (r : ℝ) => ⟨γ r, V r⟩) s) (ht : t ∈ s) : DifferentiableWithinAt ℝ (sectionCoord γ ((CovariantDerivative.leviCivitaConnection I M).alongCurveWithin γ V s) (γ t)) s t

The Levi-Civita covariant derivative of a section with a C² tangent-bundle lift, within a parameter set with unique derivatives, has differentiable coordinate readings there.