The integrated Bochner identity

For a compactly supported smooth real function on a σ-compact boundaryless Riemannian manifold,

∫ (|Hess f|² + Ric(grad f, grad f)) dV = ∫ (Δ f)² dV.

Here Δ = div grad is TauCeti.Manifold.laplaceBeltrami; squaring makes the right side identical for the nonnegative Laplacian. The measure is the canonical TauCeti.riemannianVolume. Compact support replaces compactness of the manifold; no orientation, completeness, connectedness or positive dimension is needed.

The Hessian norm is written in arbitrary pointwise orthonormal bases. The bases need not vary continuously: the pointwise Bochner formula identifies the combined Hessian–Ricci integrand with an integrable scalar expression. In particular the integral is not justified by an unproved regularity assumption on a chosen frame. This identity is the energy equality underlying the sharp scalar eigenvalue estimate.

The proof uses laplaceBeltrami_norm_sq_mgradient and Green's first identity integral_mul_laplaceBeltrami.

References

• P. Petersen, Riemannian Geometry, 3rd ed., Springer GTM 171 (2016), Chapter 9 (the Bochner technique).

theorem TauCeti.Manifold.integrable_sum_hessian_sq_add_ricci {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] [T2Space M] [IsManifold I (↑⊤) M] [MeasurableSpace M] [BorelSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {f : M → ℝ} {ι : Type u_4} [Fintype ι] [LindelofSpace M] (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hfc : HasCompactSupport f) (b : (x : M) → OrthonormalBasis ι ℝ (TangentSpace I x)) : MeasureTheory.Integrable (fun (x : M) => ∑ i : ι, ∑ j : ι, hessian I f x ((b x) i) ((b x) j) ^ 2 + (((CovariantDerivative.leviCivitaConnection I M).ricciTensor x) (mgradient I f x)) (mgradient I f x)) (riemannianVolume I M)

The combined Hessian–Ricci integrand is integrable for a compactly supported smooth function. The pointwise orthonormal bases may be chosen without any regularity assumption.

theorem TauCeti.Manifold.integral_sum_hessian_sq_add_ricci {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] [T2Space M] [IsManifold I (↑⊤) M] [I.Boundaryless] [MeasurableSpace M] [BorelSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {f : M → ℝ} {ι : Type u_4} [Fintype ι] [SigmaCompactSpace M] (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hfc : HasCompactSupport f) (b : (x : M) → OrthonormalBasis ι ℝ (TangentSpace I x)) : ∫ (x : M), ∑ i : ι, ∑ j : ι, hessian I f x ((b x) i) ((b x) j) ^ 2 + (((CovariantDerivative.leviCivitaConnection I M).ricciTensor x) (mgradient I f x)) (mgradient I f x) ∂riemannianVolume I M = ∫ (x : M), laplaceBeltrami I f x ^ 2 ∂riemannianVolume I M

The integrated Bochner identity. For a compactly supported smooth function on a boundaryless manifold, ∫ (|Hess f|² + Ric(grad f, grad f)) = ∫ (Δ f)². Both integrands are integrable, and the identity holds in every pointwise orthonormal basis.