The Ricci identity for the Hessian

For a smooth function φ on a Riemannian manifold, the Hessian Hess φ(u, v) = ⟪∇_u grad φ, v⟫ (TauCeti.Manifold.hessian) is symmetric, but its covariant derivative is not: the third covariant derivative of φ commutes in its last two slots only up to curvature. With

(∇_Z Hess φ)(X, Y) = Z (Hess φ(X, Y)) - Hess φ(∇_Z X, Y) - Hess φ(X, ∇_Z Y)

and the curvature convention R(u, v) w = ∇_u ∇_v w - ∇_v ∇_u w - ∇_[u,v] w, the identity is

(∇_Z Hess φ)(X, Y) - (∇_Y Hess φ)(X, Z) = ⟪R(Z, Y) grad φ, X⟫.

It is the Ricci identity ∇²σ(u, v) - ∇²σ(v, u) = R(u, v) σ (CovariantDerivative.secondCovariantDerivative_sub_swap_of_isTorsionFree) for σ = grad φ, transported to the Hessian by metric compatibility and the symmetry of Hess φ. It is the commutation rule for third derivatives of functions used in the conformal transformation law of the Cotton tensor and in Bochner-type formulas.

The identity is stated on smooth vector fields, since the covariant derivative of the Hessian is evaluated through them.

The module also records two Hessian identities used in the Bochner formula. Metric compatibility gives Hess |X|²(u, v) = 2 ⟪∇²X(u, v), X⟫ + 2 ⟪∇_u X, ∇_v X⟫ for every smooth vector field X, where ∇²X(u, v) = ∇_u ∇_V X - ∇_{∇_u V} X is the second covariant derivative. Pairing ∇²(grad φ)(u, v) with w gives (∇_u Hess φ)(v, w), so since Hess φ is symmetric, the third covariant derivative of φ is symmetric in its last two slots.

Main results

• TauCeti.Manifold.mvfderiv_hessian_sub_swap: the Ricci identity for the Hessian.
• TauCeti.Manifold.hessian_norm_sq: the Hessian of the squared length of a smooth vector field.
• TauCeti.Manifold.inner_secondCovariantDerivative_mgradient_eq_mvfderiv_hessian: pairing the second covariant derivative of grad φ with a vector field is the covariant derivative of the Hessian.
• TauCeti.Manifold.inner_secondCovariantDerivative_mgradient_comm: the third covariant derivative of a smooth function is symmetric in its last two slots.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 7 (the Ricci identities).

theorem TauCeti.Manifold.mvfderiv_hessian_sub_swap {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] {φ : M → ℝ} (hφ : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) φ) {X Y Z : (x : M) → TangentSpace I x} (hX : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X x⟩) (hY : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y x⟩) (hZ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) (x : M) : ((d% fun (y : M) => hessian I φ y (X y) (Y y)) x) (Z x) - ((d% fun (y : M) => hessian I φ y (X y) (Z y)) x) (Y x) - hessian I φ x ((↑(CovariantDerivative.leviCivitaConnection I M) X x) (Z x)) (Y x) - hessian I φ x (X x) ((↑(CovariantDerivative.leviCivitaConnection I M) Y x) (Z x)) + hessian I φ x ((↑(CovariantDerivative.leviCivitaConnection I M) X x) (Y x)) (Z x) + hessian I φ x (X x) ((↑(CovariantDerivative.leviCivitaConnection I M) Z x) (Y x)) = inner ℝ (((((CovariantDerivative.leviCivitaConnection I M).curvatureTensor x) (Z x)) (Y x)) (mgradient I φ x)) (X x)

The Ricci identity for the Hessian. For a smooth function φ and smooth vector fields X, Y, Z, the covariant derivative of Hess φ is symmetric in its last two slots up to curvature: (∇_Z Hess φ)(X, Y) - (∇_Y Hess φ)(X, Z) = ⟪R(Z, Y) grad φ, X⟫, where (∇_Z Hess φ)(X, Y) = Z (Hess φ(X, Y)) - Hess φ(∇_Z X, Y) - Hess φ(X, ∇_Z Y) and ∇ is the Levi-Civita connection.

theorem TauCeti.Manifold.hessian_norm_sq {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] {X : (x : M) → TangentSpace I x} (hX : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X x⟩) (x : M) (u v : TangentSpace I x) : hessian I (fun (y : M) => ‖X y‖ ^ 2) x u v = 2 * inner ℝ ((((CovariantDerivative.leviCivitaConnection I M).secondCovariantDerivative (CovariantDerivative.leviCivitaConnection I M) X x) u) v) (X x) + 2 * inner ℝ ((↑(CovariantDerivative.leviCivitaConnection I M) X x) u) ((↑(CovariantDerivative.leviCivitaConnection I M) X x) v)

The Hessian of the squared length of a vector field. For a smooth vector field X, Hess |X|²(u, v) = 2 ⟪∇²X(u, v), X⟫ + 2 ⟪∇_u X, ∇_v X⟫, where ∇ is the Levi-Civita connection and ∇²X(u, v) = ∇_u ∇_V X - ∇_{∇_u V} X, for any smooth vector field V with V x = v, is its second covariant derivative.

theorem TauCeti.Manifold.inner_secondCovariantDerivative_mgradient_eq_mvfderiv_hessian {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] {φ : M → ℝ} (hφ : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) φ) {V W : (x : M) → TangentSpace I x} (hV : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, V x⟩) {x : M} (hW : (MDiffAt fun (x : M) => ⟨x, W x⟩) x) (u : TangentSpace I x) : inner ℝ ((((CovariantDerivative.leviCivitaConnection I M).secondCovariantDerivative (CovariantDerivative.leviCivitaConnection I M) (mgradient I φ) x) u) (V x)) (W x) = ((d% fun (y : M) => hessian I φ y (V y) (W y)) x) u - hessian I φ x ((↑(CovariantDerivative.leviCivitaConnection I M) V x) u) (W x) - hessian I φ x (V x) ((↑(CovariantDerivative.leviCivitaConnection I M) W x) u)

Pairing the second covariant derivative of grad φ with a vector field is the covariant derivative of the Hessian: for smooth vector fields V and W, ⟪∇²(grad φ)(u, V), W⟫ = u (Hess φ(V, W)) - Hess φ(∇_u V, W) - Hess φ(V, ∇_u W), where ∇ is the Levi-Civita connection.

theorem TauCeti.Manifold.inner_secondCovariantDerivative_mgradient_comm {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] {φ : M → ℝ} (hφ : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) φ) (x : M) (u v w : TangentSpace I x) : inner ℝ ((((CovariantDerivative.leviCivitaConnection I M).secondCovariantDerivative (CovariantDerivative.leviCivitaConnection I M) (mgradient I φ) x) u) v) w = inner ℝ ((((CovariantDerivative.leviCivitaConnection I M).secondCovariantDerivative (CovariantDerivative.leviCivitaConnection I M) (mgradient I φ) x) u) w) v

The third covariant derivative of a smooth function is symmetric in its last two slots: ⟪∇²(grad φ)(u, v), w⟫ = ⟪∇²(grad φ)(u, w), v⟫, since it is the covariant derivative of the symmetric Hessian.