The Bochner formula for functions

For a smooth function f on a Riemannian manifold with Levi-Civita connection ∇, the Bochner formula is

½ Δ |grad f|² = |Hess f|² + ⟨grad f, grad Δ f⟩ + Ric(grad f, grad f),

where Δ = div ∘ grad is TauCeti.Manifold.laplaceBeltrami and |Hess f|² = ∑ᵢⱼ Hess f(eᵢ, eⱼ)² in an orthonormal basis eᵢ. With the nonnegative Laplacian Δ⁺ = -Δ it reads Δ⁺ |df|² + 2 |Hess f|² + 2 Ric(grad f, grad f) = 2 ⟨df, d Δ⁺ f⟩. The statement is pointwise: it needs neither compactness nor completeness, and it holds in every dimension, including zero and one. Integrated over a closed manifold it is the source of the Lichnerowicz eigenvalue estimate and of Bochner's vanishing theorems.

The formula combines three local identities for the gradient G = grad f, all stated with the second covariant derivative ∇²G(u, v) = ∇_u ∇_V G - ∇_{∇_u V} G (CovariantDerivative.secondCovariantDerivative).

• For every smooth vector field X, metric compatibility gives Hess |X|²(u, v) = 2 ⟨∇²X(u, v), X⟩ + 2 ⟨∇_u X, ∇_v X⟩; tracing gives the first term.
• Since Hess f(v, w) = ⟨∇_v G, w⟩ is symmetric, so is w ↦ ⟨∇²G(u, v), w⟩ in (v, w): the third covariant derivative of f is symmetric in its last two slots.
• The Ricci identity ∇²G(u, v) - ∇²G(v, u) = R(u, v) G moves the traced direction past the free one, and the trace of ∇_w Hess f is d(Δ f)(w) (CovariantDerivative.IsMetricCompatible.mvfderiv_bilinFormTrace). Together they give the contracted identity ∑ᵢ ⟨∇²G(eᵢ, eᵢ), w⟩ = d(Δ f)(w) + Ric(w, G), which says that the rough Laplacian of grad f is grad Δ f + Ric(grad f).

The first two identities, TauCeti.Manifold.hessian_norm_sq and TauCeti.Manifold.inner_secondCovariantDerivative_mgradient_comm, hold for every smooth function and live with the other Hessian identities.

Main results

• TauCeti.Manifold.sum_inner_secondCovariantDerivative_mgradient_self: the contracted Ricci identity ∑ᵢ ⟨∇²(grad f)(eᵢ, eᵢ), w⟩ = d(Δ f)(w) + Ric(w, grad f).
• TauCeti.Manifold.laplaceBeltrami_norm_sq_mgradient: the Bochner formula.

References

• P. Petersen, Riemannian Geometry, 3rd ed., Springer GTM 171 (2016), Chapter 9 (the Bochner technique).
• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 7 (the Ricci identities).

theorem TauCeti.Manifold.sum_inner_secondCovariantDerivative_mgradient_self {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (x : M) {ι : Type u_4} [Fintype ι] (b : OrthonormalBasis ι ℝ (TangentSpace I x)) (w : TangentSpace I x) : ∑ i : ι, inner ℝ ((((CovariantDerivative.leviCivitaConnection I M).secondCovariantDerivative (CovariantDerivative.leviCivitaConnection I M) (mgradient I f) x) (b i)) (b i)) w = (d% (laplaceBeltrami I f) x) w + (((CovariantDerivative.leviCivitaConnection I M).ricciTensor x) w) (mgradient I f x)

The contracted Ricci identity for the gradient. In every orthonormal basis eᵢ of the tangent space at x, ∑ᵢ ⟪∇²(grad f)(eᵢ, eᵢ), w⟫ = d(Δ f)(w) + Ric(w, grad f), where Δ = div ∘ grad is TauCeti.Manifold.laplaceBeltrami. Equivalently, the rough Laplacian of grad f is grad Δ f + Ric(grad f).

theorem TauCeti.Manifold.laplaceBeltrami_norm_sq_mgradient {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (x : M) {ι : Type u_4} [Fintype ι] (b : OrthonormalBasis ι ℝ (TangentSpace I x)) : laplaceBeltrami I (fun (y : M) => ‖mgradient I f y‖ ^ 2) x = 2 * ∑ i : ι, ∑ j : ι, hessian I f x (b i) (b j) ^ 2 + 2 * (d% (laplaceBeltrami I f) x) (mgradient I f x) + 2 * (((CovariantDerivative.leviCivitaConnection I M).ricciTensor x) (mgradient I f x)) (mgradient I f x)

The Bochner formula. For a smooth function f and every orthonormal basis eᵢ of the tangent space at x, Δ |grad f|² = 2 ∑ᵢⱼ Hess f(eᵢ, eⱼ)² + 2 d(Δ f)(grad f) + 2 Ric(grad f, grad f), where Δ = div ∘ grad is TauCeti.Manifold.laplaceBeltrami and Ric is the Ricci tensor of the Levi-Civita connection. For the nonnegative Laplacian Δ⁺ = -Δ this is Δ⁺ |df|² + 2 |Hess f|² + 2 Ric(grad f, grad f) = 2 ⟨df, d Δ⁺ f⟩.