The divergence in a chart

Let ρ = √det (gᵢⱼ) be the Riemannian volume density in the chart frame e₁, …, eₙ at α, and write Xᵏ for the coefficients of a vector field X in that frame. This file proves the classical coordinate formula for the Riemannian divergence

ρ div X = ∑ₖ ∂ₖ (ρ Xᵏ),

where ∂ₖ is differentiation along eₖ. Thus ρ div X is a flat divergence in the chart, which is what lets the integral of a divergence against the Riemannian volume be computed by the flat divergence theorem in coordinates. No orientation is involved, and the formulas hold at every point of the chart domain, including boundary and corner points.

The formula rests on the derivative of the volume density. For any connection compatible with the metric, differentiating the Gram matrix gives dG = Pᵀ G + G P, where P is the matrix of the connection form in the chart frame, and Jacobi's formula d (det G) = det G * trace (G⁻¹ dG) turns this into dρ = ρ trace P; these general identities are Riemannian.Tensor.mvfderiv_det_chartGramMatrix and TauCeti.mvfderiv_chartVolumeDensity. For the Levi-Civita connection, torsion-freeness identifies trace P (eⱼ) with the contracted Christoffel symbol ∑ₖ Γᵏₖⱼ, which appears when the trace of ∇X is expanded in the frame.

Main results

• TauCeti.mvfderiv_chartVolumeDensity_chartLocalFrame: ∂ⱼ log ρ = ∑ₖ Γᵏₖⱼ for the Levi-Civita connection.
• TauCeti.divergence_eq_sum_christoffelSymbol: div X = ∑ₖ (∂ₖ Xᵏ + ∑ⱼ Xʲ Γᵏₖⱼ).
• TauCeti.chartVolumeDensity_mul_divergence: the coordinate formula ρ div X = ∑ₖ ∂ₖ (ρ Xᵏ).

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 2 (the divergence and the Riemannian density) and Chapter 5 (the Levi-Civita connection and its Christoffel symbols in coordinates).

theorem TauCeti.divergence_eq_sum_christoffelSymbol {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 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (α : M) {y : M} (hy : y ∈ (trivializationAt E (TangentSpace I) α).baseSet) {X : (x : M) → TangentSpace I x} (hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) y) : Manifold.divergence I X y = ∑ k : Fin (Module.finrank ℝ E), (((d% fun (z : M) => (Bundle.Trivialization.localFrameCoeff I (trivializationAt E (TangentSpace I) α) (Module.finBasis ℝ E) k z) (X z)) y) (Riemannian.Tensor.chartLocalFrame α k y) + ∑ j : Fin (Module.finrank ℝ E), (Bundle.Trivialization.localFrameCoeff I (trivializationAt E (TangentSpace I) α) (Module.finBasis ℝ E) j y) (X y) * Manifold.christoffelSymbol I (Module.finBasis ℝ E) (trivializationAt E (TangentSpace I) α) (↑(CovariantDerivative.leviCivitaConnection I M)) k j k y)

The divergence in a chart frame. In the chart frame e₁, …, eₙ at α, the divergence of a vector field X with coefficients Xᵏ is div X = ∑ₖ (∂ₖ Xᵏ + ∑ⱼ Xʲ Γᵏₖⱼ) at every point of the chart domain where X is differentiable, where ∂ₖ is the derivative along eₖ and Γᵏᵢⱼ are the Christoffel symbols of the Levi-Civita connection in that frame.

theorem TauCeti.mvfderiv_chartVolumeDensity_chartLocalFrame {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 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (α : M) {y : M} (hy : y ∈ (trivializationAt E (TangentSpace I) α).baseSet) (j : Fin (Module.finrank ℝ E)) : (d% (chartVolumeDensity α) y) (Riemannian.Tensor.chartLocalFrame α j y) = chartVolumeDensity α y * ∑ k : Fin (Module.finrank ℝ E), Manifold.christoffelSymbol I (Module.finBasis ℝ E) (trivializationAt E (TangentSpace I) α) (↑(CovariantDerivative.leviCivitaConnection I M)) k j k y

The contracted Christoffel symbols. In the chart frame e₁, …, eₙ at α, the derivative of the volume density ρ along eⱼ is ρ ∑ₖ Γᵏₖⱼ, where Γᵏᵢⱼ are the Christoffel symbols of the Levi-Civita connection in that frame; that is, ∂ⱼ log ρ = ∑ₖ Γᵏₖⱼ.

theorem TauCeti.chartVolumeDensity_mul_divergence {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 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (α : M) {y : M} (hy : y ∈ (trivializationAt E (TangentSpace I) α).baseSet) {X : (x : M) → TangentSpace I x} (hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) y) : chartVolumeDensity α y * Manifold.divergence I X y = ∑ k : Fin (Module.finrank ℝ E), ((d% fun (z : M) => chartVolumeDensity α z * (Bundle.Trivialization.localFrameCoeff I (trivializationAt E (TangentSpace I) α) (Module.finBasis ℝ E) k z) (X z)) y) (Riemannian.Tensor.chartLocalFrame α k y)

The divergence in a chart. Let ρ be the volume density in the chart frame e₁, …, eₙ at α, and let Xᵏ be the coefficients of the vector field X in that frame. At every point y of the chart domain where X is differentiable, ρ div X = ∑ₖ ∂ₖ (ρ Xᵏ), where ∂ₖ is the derivative along eₖ.