The divergence theorem on a manifold without boundary

On a smooth manifold without boundary with a C¹ Riemannian metric, the divergence of a compactly supported C¹ vector field has integral zero against the Riemannian volume:

∫ div X dV = 0.

Integrating the product rule div (f X) = f div X + df(X) then gives the integration-by-parts formulas for the divergence and the Laplace–Beltrami operator Δ = div ∘ grad:

∫ f div X dV = -∫ df(X) dV, ∫ f Δg dV = -∫ ⟪grad f, grad g⟫ dV, ∫ f Δg dV = ∫ (Δf) g dV.

These identities underlie the energy (weak) formulation of second-order operators on closed manifolds. No orientation is used: the measure is the orientation-free TauCeti.riemannianVolume.

Main results

• TauCeti.Manifold.integral_divergence_eq_zero: the divergence theorem ∫ div X dV = 0.
• TauCeti.Manifold.integral_laplaceBeltrami_eq_zero: ∫ Δf dV = 0 for a compactly supported C² function f.
• TauCeti.Manifold.integral_mul_divergence, TauCeti.Manifold.integral_mul_divergence_of_hasCompactSupport_right: ∫ f div X dV = -∫ df(X) dV when f or X has compact support.
• TauCeti.Manifold.integral_mul_laplaceBeltrami: Green's first identity ∫ f Δg dV = -∫ ⟪grad f, grad g⟫ dV.
• TauCeti.Manifold.integral_mul_laplaceBeltrami_right_eq_left: Green's second identity ∫ f Δg dV = ∫ (Δf) g dV.
• TauCeti.Manifold.integrable_divergence: the divergence of a compactly supported C¹ field is integrable.

Implementation notes

The proof is chart by chart. In the chart at α, with chart frame e₁, …, eₙ, volume density ρ and frame coefficients Xᵏ, the coordinate formula ρ div X = ∑ₖ ∂ₖ (ρ Xᵏ) (TauCeti.chartVolumeDensity_mul_divergence) turns the integral of the divergence of a field supported in the chart into a sum of integrals of partial derivatives of compactly supported C¹ functions on the model space, each of which vanishes. A smooth partition of unity subordinate to the chart sources reduces a general compactly supported field to finitely many such fields; this is where the manifold is assumed smooth, while the metric need only be C¹.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 16 (the divergence theorem, Theorem 16.32, and Green's identities).
• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 2 (the divergence and the Riemannian density).

theorem TauCeti.Manifold.integrable_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] {X : (x : M) → TangentSpace I x} [MeasurableSpace M] [BorelSpace M] [LindelofSpace M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (hX : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, X x⟩) (hc : HasCompactSupport X) : MeasureTheory.Integrable (divergence I X) (riemannianVolume I M)

The divergence of a compactly supported C¹ vector field is integrable against the Riemannian volume.

theorem TauCeti.Manifold.integral_divergence_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [SigmaCompactSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [MeasurableSpace M] [BorelSpace M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {X : (x : M) → TangentSpace I x} (hX : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, X x⟩) (hc : HasCompactSupport X) : ∫ (x : M), divergence I X x ∂riemannianVolume I M = 0

The divergence theorem on a manifold without boundary: the divergence of a compactly supported C¹ vector field has integral zero against the Riemannian volume.

theorem TauCeti.Manifold.integral_mul_divergence {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [SigmaCompactSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [MeasurableSpace M] [BorelSpace M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {X : (x : M) → TangentSpace I x} {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 1 f) (hfc : HasCompactSupport f) (hX : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, X x⟩) : ∫ (x : M), f x * divergence I X x ∂riemannianVolume I M = -∫ (x : M), (d% f x) (X x) ∂riemannianVolume I M

Integration by parts for the divergence: for a compactly supported C¹ function f and a C¹ vector field X on a manifold without boundary, ∫ f div X dV = -∫ df(X) dV.

theorem TauCeti.Manifold.integral_mul_divergence_of_hasCompactSupport_right {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [SigmaCompactSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [MeasurableSpace M] [BorelSpace M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {X : (x : M) → TangentSpace I x} {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 1 f) (hX : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, X x⟩) (hXc : HasCompactSupport X) : ∫ (x : M), f x * divergence I X x ∂riemannianVolume I M = -∫ (x : M), (d% f x) (X x) ∂riemannianVolume I M

Integration by parts for the divergence, for a compactly supported field: for a C¹ function f and a compactly supported C¹ vector field X on a manifold without boundary, ∫ f div X dV = -∫ df(X) dV.

theorem TauCeti.Manifold.integral_laplaceBeltrami_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [SigmaCompactSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [MeasurableSpace M] [BorelSpace M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) (hfc : HasCompactSupport f) : ∫ (x : M), laplaceBeltrami I f x ∂riemannianVolume I M = 0

The Laplace--Beltrami operator of a compactly supported C² function on a manifold without boundary has integral zero against the Riemannian volume.

theorem TauCeti.Manifold.integral_mul_laplaceBeltrami {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [SigmaCompactSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [MeasurableSpace M] [BorelSpace M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {f g : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 1 f) (hfc : HasCompactSupport f) (hg : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 g) : ∫ (x : M), f x * laplaceBeltrami I g x ∂riemannianVolume I M = -∫ (x : M), inner ℝ (mgradient I f x) (mgradient I g x) ∂riemannianVolume I M

Green's first identity on a manifold without boundary: for a compactly supported C¹ function f and a C² function g, ∫ f Δg dV = -∫ ⟪grad f, grad g⟫ dV.

theorem TauCeti.Manifold.integral_norm_sq_mgradient_eq_mul_integral_sq_of_laplaceBeltrami_eq_neg_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [SigmaCompactSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [MeasurableSpace M] [BorelSpace M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {f : M → ℝ} {lam : ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) (hfc : HasCompactSupport f) (heig : ∀ (x : M), laplaceBeltrami I f x = -lam * f x) : ∫ (x : M), ‖mgradient I f x‖ ^ 2 ∂riemannianVolume I M = lam * ∫ (x : M), f x ^ 2 ∂riemannianVolume I M

The energy identity for a compactly supported C² eigenfunction of the scalar Laplacian on a manifold without boundary, using the convention Δf = -λ f.

theorem TauCeti.Manifold.integral_mul_laplaceBeltrami_right_eq_left {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [SigmaCompactSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [MeasurableSpace M] [BorelSpace M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {f g : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) (hfc : HasCompactSupport f) (hg : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 g) : ∫ (x : M), f x * laplaceBeltrami I g x ∂riemannianVolume I M = ∫ (x : M), laplaceBeltrami I f x * g x ∂riemannianVolume I M

Green's second identity on a manifold without boundary: for a compactly supported C² function f and a C² function g, ∫ f Δg dV = ∫ (Δf) g dV.