Curvature as a function of the second-order jet of a metric

In coordinates, the curvature of a metric at a point is a universal expression in the value and the first and second derivatives of its coefficients there: polynomial in the derivatives and in the entries of the inverse Gram matrix. This file writes that expression down and identifies it with the curvature of the Levi-Civita connection. For a basis b of the model space, the coordinate jet of a metric at a point consists of its Gram matrix g_ij = g(b i, b j), the first derivatives ∂ₖ g_ij and the second derivatives ∂ₘ ∂ₖ g_ij of these coefficients in the directions of b. From such a jet we define

• the Christoffel symbols christoffelOfJet, Γᵏᵢⱼ = (1/2) Σ_l g^(kl) (∂ᵢ g_jl + ∂ⱼ g_il - ∂_l g_ij);
• their derivatives christoffelDerivOfJet, obtained by differentiating g(Γ(∂ᵢ, ∂ⱼ), ∂_l) = (∂ᵢ g_jl + ∂ⱼ g_il - ∂_l g_ij) / 2;
• the curvature coefficients riemannOfJet, the l-th coordinate of R(∂ᵢ, ∂ⱼ)∂ₖ;
• the scalar curvature scalarCurvatureOfJet, the contraction Σⱼₖ g^(jk) Σᵢ Rⁱᵢⱼₖ.

These functions, and in particular the scalar curvature of a jet, depend continuously on the jet wherever its Gram matrix is invertible (ContinuousAt.scalarCurvatureOfJet). For the Levi-Civita connection of a smooth metric read in a chart, the Christoffel symbols, their derivatives along the coordinate frame and the curvature coefficients are those of the coordinate jet of the chart metric, for metrics of any signature; for a smooth Riemannian metric, so is the scalar curvature (Bundle.ContMDiffRiemannianMetric.scalarCurvature_eq_scalarCurvatureOfJet). Thus scalar curvature is a continuous second-order differential expression in the metric. In particular, for a family of metrics whose chart coefficients and their first and second derivatives depend jointly continuously on a parameter, the scalar curvature is jointly continuous in the parameter and the point (TauCeti.Manifold.continuousAt_scalarCurvature_of_continuousAt_chartMetric). This is the input for the openness of positive scalar curvature under C² perturbations and for uniform scalar-curvature bounds over compact families of metrics.

The coordinate identifications hold at points of a chart domain whose chart image is an interior point of the model, hence everywhere on a manifold without boundary. Jets of fields of bilinear forms are taken through their scalar coefficients z ↦ G z (b i) (b j), so that no iterated derivative valued in spaces of multilinear maps is needed.

The index and sign conventions are those of TauCeti.Geometry.Manifold.VectorBundle.CovariantDerivative.Curvature.Coordinates, following J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 7: R(X,Y)Z = ∇_X ∇_Y Z - ∇_Y ∇_X Z - ∇_[X,Y] Z.

Main definitions and results

• TauCeti.Manifold.christoffelOfJet, TauCeti.Manifold.christoffelDerivOfJet, TauCeti.Manifold.riemannOfJet and TauCeti.Manifold.scalarCurvatureOfJet: the Christoffel symbols, their derivatives, the curvature coefficients and the scalar curvature of a coordinate jet.
• ContinuousAt.christoffelOfJet, ContinuousAt.christoffelDerivOfJet, ContinuousAt.riemannOfJet and ContinuousAt.scalarCurvatureOfJet: the Christoffel symbols, their derivatives, the curvature coefficients and the scalar curvature of a jet are continuous at jets with invertible Gram matrix.
• TauCeti.Manifold.repr_fderiv_christoffelSecondKind_eq_christoffelDerivOfJet and TauCeti.Manifold.fderiv_repr_christoffelSecondKind_eq_christoffelDerivOfJet: the derivatives of the Christoffel symbols of a field of symmetric nondegenerate bilinear forms on a vector space, and of their coordinates.
• IsLeviCivitaConnection.christoffelSymbol_eq_christoffelOfJet, IsLeviCivitaConnection.mvfderiv_christoffelSymbol_eq_christoffelDerivOfJet and IsLeviCivitaConnection.localFrameCoeff_curvatureOperator_eq_riemannOfJet, in the namespace TauCeti.Manifold.ContMDiffNondegenerateMetric: the Christoffel symbols, their derivatives and the curvature coefficients of a Levi-Civita connection in a chart.
• Bundle.ContMDiffRiemannianMetric.scalarCurvature_eq_scalarCurvatureOfJet: the scalar curvature of a smooth Riemannian metric in a chart.
• TauCeti.Manifold.continuousAt_scalarCurvature_of_continuousAt_chartMetric: joint continuity of scalar curvature along a C²-continuous family of metrics.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapters 5 and 7: the Christoffel symbols and the curvature of a metric in coordinates.
• M. P. do Carmo, Riemannian Geometry, Birkhäuser (1992), Chapter 4.

Curvature of a coordinate jet

noncomputable def TauCeti.Manifold.christoffelOfJet {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Matrix ι ι ℝ) (dg : ι → ι → ι → ℝ) (i j k : ι) : ℝ

The Christoffel symbols of a coordinate jet. For a metric whose Gram matrix in a basis is g and whose coefficients have first derivatives dg k i j = ∂ₖ g_ij, these are Γᵏᵢⱼ = (1/2) Σ_l g^(kl) (∂ᵢ g_jl + ∂ⱼ g_il - ∂_l g_ij), with g^(kl) the inverse of g.

theorem TauCeti.Manifold.christoffelOfJet_def {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Matrix ι ι ℝ) (dg : ι → ι → ι → ℝ) (i j k : ι) : christoffelOfJet g dg i j k = 2⁻¹ * ∑ l : ι, g⁻¹ k l * (dg i j l + dg j i l - dg l i j)

The defining formula of the Christoffel symbols of a coordinate jet.

noncomputable def TauCeti.Manifold.christoffelDerivOfJet {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Matrix ι ι ℝ) (dg : ι → ι → ι → ℝ) (ddg : ι → ι → ι → ι → ℝ) (m i j k : ι) : ℝ

The derivatives of the Christoffel symbols of a coordinate jet. For a metric whose Gram matrix is g, with first derivatives dg k i j = ∂ₖ g_ij and second derivatives ddg m k i j = ∂ₘ ∂ₖ g_ij, this is ∂ₘ Γᵏᵢⱼ = Σ_l g^(kl) ((∂ₘ∂ᵢ g_jl + ∂ₘ∂ⱼ g_il - ∂ₘ∂_l g_ij) / 2 - Σ_q ∂ₘ g_ql Γ^qᵢⱼ), obtained by differentiating g(Γ(∂ᵢ, ∂ⱼ), ∂_l) = (∂ᵢ g_jl + ∂ⱼ g_il - ∂_l g_ij) / 2.

theorem TauCeti.Manifold.christoffelDerivOfJet_def {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Matrix ι ι ℝ) (dg : ι → ι → ι → ℝ) (ddg : ι → ι → ι → ι → ℝ) (m i j k : ι) : christoffelDerivOfJet g dg ddg m i j k = ∑ l : ι, g⁻¹ k l * (2⁻¹ * (ddg m i j l + ddg m j i l - ddg m l i j) - ∑ q : ι, dg m q l * christoffelOfJet g dg i j q)

The defining formula of the derivatives of the Christoffel symbols of a coordinate jet.

noncomputable def TauCeti.Manifold.riemannOfJet {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Matrix ι ι ℝ) (dg : ι → ι → ι → ℝ) (ddg : ι → ι → ι → ι → ℝ) (i j k l : ι) : ℝ

The curvature coefficients of a coordinate jet: the l-th coordinate of R(∂ᵢ, ∂ⱼ)∂ₖ, ∂ᵢ Γˡⱼₖ - ∂ⱼ Γˡᵢₖ + Σₘ (Γᵐⱼₖ Γˡᵢₘ - Γᵐᵢₖ Γˡⱼₘ), for the Christoffel symbols christoffelOfJet and their derivatives christoffelDerivOfJet.

theorem TauCeti.Manifold.riemannOfJet_def {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Matrix ι ι ℝ) (dg : ι → ι → ι → ℝ) (ddg : ι → ι → ι → ι → ℝ) (i j k l : ι) : riemannOfJet g dg ddg i j k l = christoffelDerivOfJet g dg ddg i j k l - christoffelDerivOfJet g dg ddg j i k l + ∑ m : ι, (christoffelOfJet g dg j k m * christoffelOfJet g dg i m l - christoffelOfJet g dg i k m * christoffelOfJet g dg j m l)

The defining formula of the curvature coefficients of a coordinate jet.

noncomputable def TauCeti.Manifold.scalarCurvatureOfJet {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Matrix ι ι ℝ) (dg : ι → ι → ι → ℝ) (ddg : ι → ι → ι → ι → ℝ) : ℝ

The scalar curvature of a coordinate jet (g, ∂g, ∂²g): the contraction Σⱼₖ g^(jk) Σᵢ Rⁱᵢⱼₖ of the curvature coefficients riemannOfJet against the inverse of the Gram matrix g.

theorem TauCeti.Manifold.scalarCurvatureOfJet_def {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Matrix ι ι ℝ) (dg : ι → ι → ι → ℝ) (ddg : ι → ι → ι → ι → ℝ) : scalarCurvatureOfJet g dg ddg = ∑ j : ι, ∑ k : ι, g⁻¹ j k * ∑ i : ι, riemannOfJet g dg ddg i j k i

The defining formula of the scalar curvature of a coordinate jet.

Continuity in the jet

theorem ContinuousAt.christoffelOfJet {ι : Type u_1} [Fintype ι] [DecidableEq ι] {X : Type u_2} [TopologicalSpace X] {g : X → Matrix ι ι ℝ} {dg : X → ι → ι → ι → ℝ} {x : X} (hg : ContinuousAt g x) (hdet : (g x).det ≠ 0) (hdg : ContinuousAt dg x) (i j k : ι) : ContinuousAt (fun (y : X) => TauCeti.Manifold.christoffelOfJet (g y) (dg y) i j k) x

The Christoffel symbols of a coordinate jet depend continuously on the jet at every jet whose Gram matrix is invertible.

theorem ContinuousAt.christoffelDerivOfJet {ι : Type u_1} [Fintype ι] [DecidableEq ι] {X : Type u_2} [TopologicalSpace X] {g : X → Matrix ι ι ℝ} {dg : X → ι → ι → ι → ℝ} {ddg : X → ι → ι → ι → ι → ℝ} {x : X} (hg : ContinuousAt g x) (hdet : (g x).det ≠ 0) (hdg : ContinuousAt dg x) (hddg : ContinuousAt ddg x) (m i j k : ι) : ContinuousAt (fun (y : X) => TauCeti.Manifold.christoffelDerivOfJet (g y) (dg y) (ddg y) m i j k) x

The derivatives of the Christoffel symbols of a coordinate jet depend continuously on the jet at every jet whose Gram matrix is invertible.

theorem ContinuousAt.riemannOfJet {ι : Type u_1} [Fintype ι] [DecidableEq ι] {X : Type u_2} [TopologicalSpace X] {g : X → Matrix ι ι ℝ} {dg : X → ι → ι → ι → ℝ} {ddg : X → ι → ι → ι → ι → ℝ} {x : X} (hg : ContinuousAt g x) (hdet : (g x).det ≠ 0) (hdg : ContinuousAt dg x) (hddg : ContinuousAt ddg x) (i j k l : ι) : ContinuousAt (fun (y : X) => TauCeti.Manifold.riemannOfJet (g y) (dg y) (ddg y) i j k l) x

The curvature coefficients of a coordinate jet depend continuously on the jet at every jet whose Gram matrix is invertible.

theorem ContinuousAt.scalarCurvatureOfJet {ι : Type u_1} [Fintype ι] [DecidableEq ι] {X : Type u_2} [TopologicalSpace X] {g : X → Matrix ι ι ℝ} {dg : X → ι → ι → ι → ℝ} {ddg : X → ι → ι → ι → ι → ℝ} {x : X} (hg : ContinuousAt g x) (hdet : (g x).det ≠ 0) (hdg : ContinuousAt dg x) (hddg : ContinuousAt ddg x) : ContinuousAt (fun (y : X) => TauCeti.Manifold.scalarCurvatureOfJet (g y) (dg y) (ddg y)) x

Scalar curvature is continuous in the second-order jet of the metric. The scalar curvature of a coordinate jet depends continuously on the jet at every jet whose Gram matrix is invertible.

The jet of a field of bilinear forms on a vector space

theorem TauCeti.Manifold.repr_christoffelSecondKind_eq_christoffelOfJet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {G : E → E →L[ℝ] E →L[ℝ] ℝ} {z : E} (b : Module.Basis ι ℝ E) (hG : DifferentiableAt ℝ G z) (hsymm : LinearMap.IsSymm (G z).toBilinForm) (hnd : (G z).toBilinForm.Nondegenerate) (i j k : ι) : (b.repr (((christoffelSecondKind G z) (b i)) (b j))) k = christoffelOfJet ((LinearMap.toMatrix₂ b b) (G z).toBilinForm) (fun (k i j : ι) => (fderiv ℝ (fun (y : E) => ((G y) (b i)) (b j)) z) (b k)) i j k

In a basis, the Christoffel symbols of the second kind of a field G of symmetric nondegenerate bilinear forms are the Christoffel symbols of its coordinate jet.

theorem TauCeti.Manifold.repr_fderiv_christoffelSecondKind_eq_christoffelDerivOfJet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {G : E → E →L[ℝ] E →L[ℝ] ℝ} {z : E} (b : Module.Basis ι ℝ E) (hG : ContDiffAt ℝ 2 G z) (hsymm : LinearMap.IsSymm (G z).toBilinForm) (hnd : (G z).toBilinForm.Nondegenerate) (m i j k : ι) : (b.repr ((((fderiv ℝ (christoffelSecondKind G) z) (b m)) (b i)) (b j))) k = christoffelDerivOfJet ((LinearMap.toMatrix₂ b b) (G z).toBilinForm) (fun (k i j : ι) => (fderiv ℝ (fun (y : E) => ((G y) (b i)) (b j)) z) (b k)) (fun (m k i j : ι) => (fderiv ℝ (fun (y : E) => (fderiv ℝ (fun (y' : E) => ((G y') (b i)) (b j)) y) (b k)) z) (b m)) m i j k

The derivatives of the Christoffel symbols in a basis. For a field G of bilinear forms that is C² at z, nondegenerate and symmetric at z, the k-th coordinate of ∂ₘ Γ(b i, b j) is the derivative christoffelDerivOfJet of the Christoffel symbols of the coordinate jet (g, ∂g, ∂²g) of G at z.

theorem TauCeti.Manifold.fderiv_repr_christoffelSecondKind_eq_christoffelDerivOfJet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {G : E → E →L[ℝ] E →L[ℝ] ℝ} {z : E} (b : Module.Basis ι ℝ E) (hG : ContDiffAt ℝ 2 G z) (hsymm : LinearMap.IsSymm (G z).toBilinForm) (hnd : (G z).toBilinForm.Nondegenerate) (m i j k : ι) : (fderiv ℝ (fun (y : E) => (b.repr (((christoffelSecondKind G y) (b i)) (b j))) k) z) (b m) = christoffelDerivOfJet ((LinearMap.toMatrix₂ b b) (G z).toBilinForm) (fun (k i j : ι) => (fderiv ℝ (fun (y : E) => ((G y) (b i)) (b j)) z) (b k)) (fun (m k i j : ι) => (fderiv ℝ (fun (y : E) => (fderiv ℝ (fun (y' : E) => ((G y') (b i)) (b j)) y) (b k)) z) (b m)) m i j k

The derivatives of the coordinates of the Christoffel symbols. For a field G of bilinear forms that is C² at z, nondegenerate and symmetric at z, the derivative along b m of the k-th coordinate of Γ(b i, b j) is christoffelDerivOfJet of the coordinate jet (g, ∂g, ∂²g) of G at z.

Christoffel symbols and curvature of a Levi-Civita connection in a chart

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.christoffelSymbol_eq_christoffelOfJet {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] {g : ContMDiffNondegenerateMetric} {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} {ι : Type u_4} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℝ E) {x₀ y : M} (h : g.IsLeviCivitaConnection cov) (hy : y ∈ (extChartAt I x₀).source) (hint : ↑(extChartAt I x₀) y ∈ interior (Set.range ↑I)) (i j k : ι) : christoffelSymbol I b (trivializationAt E (TangentSpace I) x₀) (↑cov) i j k y = christoffelOfJet ((LinearMap.toMatrix₂ b b) (g.chartMetric x₀ (↑(extChartAt I x₀) y)).toBilinForm) (fun (k i j : ι) => (fderiv ℝ (fun (z : E) => ((g.chartMetric x₀ z) (b i)) (b j)) (↑(extChartAt I x₀) y)) (b k)) i j k

At a point y of the chart domain at x₀ whose chart image z is interior, the Christoffel symbol Γᵏᵢⱼ of a Levi-Civita connection of g, in the frame of b, is christoffelOfJet of the coordinate jet (g, ∂g) of the chart metric at z.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.mvfderiv_christoffelSymbol_eq_christoffelDerivOfJet {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] {g : ContMDiffNondegenerateMetric} {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} {ι : Type u_4} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℝ E) {x₀ y : M} (h : g.IsLeviCivitaConnection cov) (hy : y ∈ (extChartAt I x₀).source) (hint : ↑(extChartAt I x₀) y ∈ interior (Set.range ↑I)) (m i j k : ι) : (d% (christoffelSymbol I b (trivializationAt E (TangentSpace I) x₀) (↑cov) i j k) y) ((trivializationAt E (TangentSpace I) x₀).localFrame b m y) = christoffelDerivOfJet ((LinearMap.toMatrix₂ b b) (g.chartMetric x₀ (↑(extChartAt I x₀) y)).toBilinForm) (fun (k i j : ι) => (fderiv ℝ (fun (z : E) => ((g.chartMetric x₀ z) (b i)) (b j)) (↑(extChartAt I x₀) y)) (b k)) (fun (m k i j : ι) => (fderiv ℝ (fun (z : E) => (fderiv ℝ (fun (z' : E) => ((g.chartMetric x₀ z') (b i)) (b j)) z) (b k)) (↑(extChartAt I x₀) y)) (b m)) m i j k

The derivatives of the Christoffel symbols of a Levi-Civita connection in a chart. At a point y of the chart domain at x₀ whose chart image z is interior, the derivative of the Christoffel symbol Γᵏᵢⱼ of a Levi-Civita connection of g along the m-th frame vector is christoffelDerivOfJet of the coordinate jet (g, ∂g, ∂²g) of the chart metric at z.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.localFrameCoeff_curvatureOperator_eq_riemannOfJet {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] {g : ContMDiffNondegenerateMetric} {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} {ι : Type u_4} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℝ E) {x₀ y : M} (h : g.IsLeviCivitaConnection cov) [ContMDiffCovariantDerivativeOn E 1 (↑cov) (trivializationAt E (TangentSpace I) x₀).baseSet] (hy : y ∈ (extChartAt I x₀).source) (hint : ↑(extChartAt I x₀) y ∈ interior (Set.range ↑I)) (i j k l : ι) : (Bundle.Trivialization.localFrameCoeff I (trivializationAt E (TangentSpace I) x₀) b l y) (cov.curvatureOperator ((trivializationAt E (TangentSpace I) x₀).localFrame b i) ((trivializationAt E (TangentSpace I) x₀).localFrame b j) ((trivializationAt E (TangentSpace I) x₀).localFrame b k) y) = riemannOfJet ((LinearMap.toMatrix₂ b b) (g.chartMetric x₀ (↑(extChartAt I x₀) y)).toBilinForm) (fun (k i j : ι) => (fderiv ℝ (fun (z : E) => ((g.chartMetric x₀ z) (b i)) (b j)) (↑(extChartAt I x₀) y)) (b k)) (fun (m k i j : ι) => (fderiv ℝ (fun (z : E) => (fderiv ℝ (fun (z' : E) => ((g.chartMetric x₀ z') (b i)) (b j)) z) (b k)) (↑(extChartAt I x₀) y)) (b m)) i j k l

The curvature of a Levi-Civita connection in a chart. At a point y of the chart domain at x₀ whose chart image z is interior, the l-th coefficient of R(∂ᵢ, ∂ⱼ)∂ₖ in the frame of b, for a Levi-Civita connection of g, is riemannOfJet of the coordinate jet (g, ∂g, ∂²g) of the chart metric at z.

Scalar curvature of a Riemannian metric in a chart

theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_eq_scalarCurvatureOfJet {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] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {ι : Type u_4} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℝ E) {x₀ y : M} (hy : y ∈ (extChartAt I x₀).source) (hint : ↑(extChartAt I x₀) y ∈ interior (Set.range ↑I)) : g.scalarCurvature y = TauCeti.Manifold.scalarCurvatureOfJet ((LinearMap.toMatrix₂ b b) (g.toNondegenerateMetric.chartMetric x₀ (↑(extChartAt I x₀) y)).toBilinForm) (fun (k i j : ι) => (fderiv ℝ (fun (z : E) => ((g.toNondegenerateMetric.chartMetric x₀ z) (b i)) (b j)) (↑(extChartAt I x₀) y)) (b k)) fun (m k i j : ι) => (fderiv ℝ (fun (z : E) => (fderiv ℝ (fun (z' : E) => ((g.toNondegenerateMetric.chartMetric x₀ z') (b i)) (b j)) z) (b k)) (↑(extChartAt I x₀) y)) (b m)

Scalar curvature as a second-order expression in the metric. At a point y of the chart domain at x₀ whose chart image z is interior, the scalar curvature of a smooth Riemannian metric g is scalarCurvatureOfJet of the coordinate jet of the chart metric G of g at z, in any basis b of the model: the Gram matrix G_ij(z), the first derivatives ∂ₖ G_ij(z) and the second derivatives ∂ₘ ∂ₖ G_ij(z).

Continuity of scalar curvature along families of metrics

theorem TauCeti.Manifold.continuousAt_scalarCurvature_of_continuousAt_chartMetric {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] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℝ E) {P : Type u_5} [TopologicalSpace P] (g : P → Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {p₀ : P} {y₀ : M} (hint : ↑(extChartAt I y₀) y₀ ∈ interior (Set.range ↑I)) (h₀ : ContinuousAt (fun (q : P × E) => (LinearMap.toMatrix₂ b b) ((g q.1).toNondegenerateMetric.chartMetric y₀ q.2).toBilinForm) (p₀, ↑(extChartAt I y₀) y₀)) (h₁ : ContinuousAt (fun (q : P × E) (k i j : ι) => (fderiv ℝ (fun (z : E) => (((g q.1).toNondegenerateMetric.chartMetric y₀ z) (b i)) (b j)) q.2) (b k)) (p₀, ↑(extChartAt I y₀) y₀)) (h₂ : ContinuousAt (fun (q : P × E) (m k i j : ι) => (fderiv ℝ (fun (z : E) => (fderiv ℝ (fun (z' : E) => (((g q.1).toNondegenerateMetric.chartMetric y₀ z') (b i)) (b j)) z) (b k)) q.2) (b m)) (p₀, ↑(extChartAt I y₀) y₀)) : ContinuousAt (fun (q : P × M) => (g q.1).scalarCurvature q.2) (p₀, y₀)

Scalar curvature is continuous along C²-continuous families of metrics. Let g p be a family of smooth Riemannian metrics indexed by a topological space P, and y₀ a point whose image in its own chart is interior. If the Gram matrix, first and second derivatives of the chart metrics of g p at y₀, in a basis b, depend continuously on (p, z) at (p₀, z₀), where z₀ is the chart image of y₀, then (p, y) ↦ Scal(g p)(y) is continuous at (p₀, y₀).