Divergence, Hessian, and Laplace–Beltrami operators #
This file introduces the pointwise Riemannian divergence as the trace of the Levi–Civita
covariant derivative, the scalar Hessian obtained by pairing that derivative of the gradient,
and the Laplace–Beltrami operator with the convention Δ = div ∘ grad. The orthonormal-basis
trace formula makes the relationship between the Laplacian and the Hessian explicit. The operator
laws include the Leibniz rule and the chain rule Δ (h ∘ f) = h'(f) Δ f + h''(f) |grad f|² for a
real function h, with its special case Δ (log f) = Δ f / f - |grad f|² / f². On a
finite-dimensional normed space whose metric is a field of bilinear forms g, the Hessian in
linear coordinates is D²f(u, v) - Df(Γ(u, v)) with Γ the Christoffel symbols of g. On a
finite-dimensional inner-product space, the operator agrees with Mathlib's
flat Laplacian. The Hessian conventions follow Lee, Introduction to Riemannian Manifolds,
Chapter 3.
The Riemannian divergence of a vector field, defined as the trace of its Levi–Civita covariant derivative.
Instances For
A C^(n + 1) vector field on a C^m Riemannian manifold with C^k metric has C^n
divergence when n + 2 ≤ m and n + 1 ≤ k.
The scalar Hessian of f, pairing the covariant derivative of its gradient with a second
tangent vector.
Instances For
The Hessian applied to a vector field and a differentiable vector field is the directional
derivative of the directional derivative of f, minus the derivative in the covariant derivative
direction.
The Hessian of a twice continuously differentiable function is symmetric for the Levi–Civita connection.
The Hessian divided by a nonvanishing function f: for the Levi-Civita connection D,
(Y f / f) (X f / f) + X (Y f / f) - (D_X Y) f / f = Hess f(X,Y) / f where f does not
vanish.
The Laplace–Beltrami operator, with the sign convention Δ = div ∘ grad.
Instances For
For a Laplace–Beltrami eigenfunction, the derivative of its Laplacian along its gradient is minus the eigenvalue times the squared gradient norm.
On a C^m manifold with a C^k Riemannian metric, the Laplace--Beltrami operator of a
C^(n + 2) function is C^n when n + 2 ≤ m and n + 1 ≤ k; like the flat Laplacian, it
loses two derivatives. The finite-regularity statement is useful when the operator is used under
an integral, where smoothness of the resulting scalar function must be supplied explicitly.
For a C¹ Riemannian metric, the Laplace--Beltrami operator of a C² function is
continuous.
The divergence of the zero vector field is zero.
Divergence is additive at a point where both vector fields are differentiable.
Divergence commutes with a real constant at a differentiability point of the field.
Product rule for the divergence at a point where f and X are differentiable:
divergence I (f • X) x = f x * divergence I X x + mvfderiv I f x (X x).
This is the pointwise input for integrating the Laplace--Beltrami operator by parts.
Divergence is additive over a finite family of vector fields, at a point where every field is differentiable.
The divergence vanishes off the topological support of a vector field, since the field is zero near such a point. No regularity of the field is needed.
The divergence of a compactly supported vector field is compactly supported.
The Laplace--Beltrami operator of a compactly supported function is compactly supported.
The Hessian of a constant function is zero.
The Hessian of the zero function is zero.
The Hessian is additive on twice continuously differentiable functions.
The Hessian commutes with multiplication of a C² function by a real constant.
The Laplace–Beltrami operator vanishes on constants.
The Laplace–Beltrami operator vanishes on the zero function.
The Laplace–Beltrami operator is additive on C² functions.
Leibniz rule for the Laplace--Beltrami operator. For twice continuously differentiable functions, the Laplacian of a product is the sum of the two scalar terms and twice the inner product of their gradients.
The Laplace–Beltrami operator commutes with real scalar multiplication on C² functions.
The Laplace–Beltrami operator commutes with negation on C² functions.
The Laplace–Beltrami operator is additive with respect to subtraction of C² functions.
Chain rule for the Laplace--Beltrami operator. If h is C² on an open set of real
numbers containing all values of a C² function f, then
Δ (h ∘ f) = h'(f) Δ f + h''(f) |grad f|².
The Laplace--Beltrami operator of the logarithm of a nowhere-vanishing C² function:
Δ (log f) = Δ f / f - |grad f|² / f².
In any orthonormal basis, the divergence is the sum of the diagonal inner products of the covariant derivative of the vector field.
The Laplace–Beltrami operator is the trace of the scalar Hessian in every orthonormal basis.
The squared trace of the Hessian is at most the dimension times its squared norm, expressed in any orthonormal basis. This includes dimension zero.
If the Hessian of f at x is c times the metric, then Δ f x = n c, where n is the
dimension.
Linear coordinates #
The Hessian in linear coordinates. On a finite-dimensional real normed space F whose
Riemannian metric is the field of bilinear forms g, differentiable at x, the Hessian of a
function f that is C² at x is Hess f(u, v) = D²f(u, v) - Df(Γ(u, v)), where Γ is
TauCeti.Manifold.christoffelSecondKind g. Tangent vectors are read in the model space through
tangentSpaceCastModel.
The flat model #
On a finite-dimensional real inner-product space with its standard metric, the Riemannian divergence is the trace of the ordinary Fréchet derivative.
On a finite-dimensional real inner-product space with its standard metric, the Riemannian Hessian is the second Fréchet derivative.
At a point x where ∇ f is differentiable, the Laplace–Beltrami operator of the standard
Riemannian metric equals Mathlib's flat Laplacian Δ f. This fixes the sign convention as
Δ = div ∘ grad.
For a function f with ContDiff ℝ 2 f on a finite-dimensional real inner product space,
the Laplace--Beltrami operator of the standard metric equals Mathlib's flat Laplacian Δ f at
every point (convention Δ = div ∘ grad).
If the installed fibre metric is the standard one, the Laplace–Beltrami operator is Mathlib's
flat Laplacian. This transports
laplaceBeltrami_eq_laplacian_of_differentiableAt_gradient along an equality of fibre metrics,
such as toRiemannianMetric_ofLE, which cannot be rewritten inside the instance-dependent
arguments.
The squared norm has constant flat Laplace--Beltrami operator.