Laplace–Beltrami operator

DefinitionLaplace–Beltrami operator#✓fully proved

The Laplace-Beltrami operator applied to f : M → ℝ at x: Δf(x) is the metric trace ∑ i, hessian I f x (e i) (e i) over the orthonormal basis e = stdOrthonormalBasis ℝ (TangentSpace I x), the same basis convention as Manifold.scalarCurvature. For the textbook Hessian, which is bilinear, this trace does not depend on the orthonormal basis; the regularity caveat of Manifold.hessian applies here unchanged.

Sign convention Δf = tr_g ∇²f, the convention Δ = div ∘ grad under which Δ is the sum ∑ ∂²/∂x_i² on Euclidean space and Δ(‖x‖²) = 2n; the operator -Δ is then the nonnegative one, and the opposite sign convention is also common. Reference with the same conventions: Lee, Introduction to Riemannian Manifolds (2nd ed., GTM 176).

Mathlib's flat Laplacian is Laplacian.laplacian (instance InnerProductSpace.instLaplacian, notation Δ after open Laplacian): the trace of the second derivative over an orthonormal basis of a finite-dimensional real inner product space. On the model space 𝓘(ℝ, F), under DifferentiableAt ℝ (fderiv ℝ f) x, this operator agrees with Mathlib's Δ (same orthonormal-basis trace, same sign); see laplacian_vectorSpace_eq_laplacian for the proved agreement. What is new here is the manifold operator itself.

def laplacian (f : M → ℝ) (x : M) : ℝ :=
  ∑ i, hessian I f x (stdOrthonormalBasis ℝ (TangentSpace I x) i)
    (stdOrthonormalBasis ℝ (TangentSpace I x) i)

Uses 1 · Used by 4

Statement usesCovariant Hessian

Used byLaplacian of the Gaussian potential · Laplacian of the squared norm · Laplacian on a vector space as a sum of second directional derivatives · The Laplacian on a vector space is the flat Laplacian at twice-differentiable points

TheoremLaplacian on a vector space as a sum of second directional derivatives#✓fully proved

Let \(F\) be a finite-dimensional real inner product space of dimension \(n\) with its standard Riemannian metric, let \(f : F \to \mathbb{R}\) and \(x \in F\), and let \(e_1, \dots, e_n\) be the orthonormal basis of the tangent space \(T_xF\) used in the definition of the Laplacian, viewed as vectors of \(F\). For each \(i\) let \(g_i(y) = Df(y)(e_i)\), where \(D\) denotes the Fréchet derivative. Then the Laplacian of \(f\) at \(x\) is \(\Delta f(x) = \sum_{i=1}^{n} Dg_i(x)(e_i)\). No differentiability of \(f\) is assumed; a Fréchet derivative that does not exist is taken to be \(0\).

When \(Df\) is differentiable at \(x\), the right side is the flat Laplacian \(\sum_i D^2 f(x)(e_i, e_i)\) of \(f\) at \(x\).

theorem laplacian_vectorSpace {F : Type*} [NormedAddCommGroup F]
    [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (f : F → ℝ) (x : F) :
    laplacian 𝓘(ℝ, F) f x =
      ∑ i, fderiv ℝ (fun y => fderiv ℝ f y
        ((NormedSpace.fromTangentSpace x)
          (stdOrthonormalBasis ℝ (TangentSpace 𝓘(ℝ, F) x) i))) x
        ((NormedSpace.fromTangentSpace x)
          (stdOrthonormalBasis ℝ (TangentSpace 𝓘(ℝ, F) x) i))

Uses 3 · Used by 1

Statement usesLaplace–Beltrami operator

Proof usesCovariant Hessian · The Hessian on Euclidean space as an iterated directional derivative

Used byThe Laplacian on a vector space is the flat Laplacian at twice-differentiable points

TheoremThe Laplacian on a vector space is the flat Laplacian at twice-differentiable points#✓fully proved

Let \(F\) be a finite-dimensional real inner product space with its standard Riemannian metric, let \(f : F \to \mathbb{R}\) and \(x \in F\), and let \(Df\) denote the Fréchet derivative of \(f\), taken to be \(0\) at points where \(f\) is not differentiable. Suppose \(Df\) is differentiable at \(x\), with derivative \(D^2 f(x)\) there. Then the Laplacian \(\Delta f(x)\) equals \(\sum_i D^2 f(x)(b_i, b_i)\) for any orthonormal basis \((b_i)\) of \(F\), the flat Laplacian of \(f\) at \(x\).

Without the hypothesis the two can differ: \(D^2 f(x)\) is taken to be \(0\) when \(Df\) is not differentiable at \(x\), while \(\Delta f(x)\) is the sum, over the vectors \(v\) of the orthonormal basis used in its definition, of the derivative at \(x\) in direction \(v\) of the function \(y \mapsto Df(y)(v)\).

theorem laplacian_vectorSpace_eq_laplacian {F : Type*} [NormedAddCommGroup F]
    [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (f : F → ℝ) (x : F)
    (h : DifferentiableAt ℝ (fderiv ℝ f) x) :
    laplacian 𝓘(ℝ, F) f x = Δ f x

Uses 5

Statement usesLaplace–Beltrami operator

Proof usesCovariant Hessian · The Hessian on Euclidean space as an iterated directional derivative · The Hessian on Euclidean space is the second derivative · Laplacian on a vector space as a sum of second directional derivatives

TheoremLaplacian of the squared norm#✓fully proved

Let \(F\) be a finite-dimensional real inner product space of dimension \(n\) with its standard Riemannian metric. For every \(x \in F\), the Laplacian of the function \(y \mapsto \|y\|^2\) at \(x\) is \(2n\).

The Hessian of \(\|\cdot\|^2\) is \(2\langle \cdot, \cdot \rangle\), so each of its diagonal entries in an orthonormal basis is \(2\).

theorem laplacian_norm_sq {F : Type*} [NormedAddCommGroup F]
    [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (x : F) :
    laplacian 𝓘(ℝ, F) (fun x => ‖x‖ ^ 2) x
      = 2 * (Module.finrank ℝ F : ℝ)

Uses 4

Statement usesLaplace–Beltrami operator

Proof usesCovariant Hessian · The Hessian on Euclidean space is the second derivative · Second derivative of the squared norm

TheoremLaplacian of the Gaussian potential#✓fully proved

Let \(F\) be a finite-dimensional real inner product space of dimension \(n\) with its standard Riemannian metric. For every real number \(a\) and every \(x \in F\), the Laplacian of the function \(y \mapsto \frac{a}{2}\|y\|^2\) at \(x\) is \(a \cdot n\).

This function is the potential of the Gaussian gradient Ricci soliton; each diagonal entry of its Hessian in an orthonormal basis is \(a\).

theorem laplacian_gaussian {F : Type*} [NormedAddCommGroup F]
    [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (a : ℝ) (x : F) :
    laplacian 𝓘(ℝ, F) (fun x => (a / 2) * ‖x‖ ^ 2) x
      = a * (Module.finrank ℝ F : ℝ)

Uses 4

Statement usesLaplace–Beltrami operator

Proof usesCovariant Hessian · The Hessian on Euclidean space is the second derivative · Second derivative of the squared norm

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.