Laplacian on $\mathbb R^n$

Definition

tegmark_laplacian

by Lucas · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicspde

For a function $f:\mathbb R^n\to\mathbb R$ and a point $x\in\mathbb R^n$ , the Laplacian is

\nabla^2 f(x)=\sum_{i=1}^n \frac{\partial^2 f}{\partial x_i^2}(x)=\sum_{i=1}^n D^2 f(x)(e_i,e_i),

where $e_1,\dots,e_n$ is the standard basis and $D^2 f(x)$ is the second Fréchet derivative.

It appears in the Poisson equation $\nabla^2\phi=\rho$ for the electrostatic or gravitational potential, in the wave and Klein–Gordon equations, and in Ásgeirsson's ultrahyperbolic equation.

Formalization Note $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). When $f$ is not twice differentiable at $x$ , Lean's derivative conventions give a junk value (typically $0$ ), so statements using the Laplacian must assume enough regularity themselves.

Definition code

import Mathlib

namespace TegmarkDimensionality

/-- The Laplacian `∇² f (x) = ∑ᵢ ∂²f/∂xᵢ² (x)` of a real function on `ℝⁿ`, written as the sum
of the pure second derivatives along the standard coordinate directions. -/
noncomputable def laplacian {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (x : EuclideanSpace ℝ (Fin n)) : ℝ :=
  ∑ i, iteratedFDeriv ℝ 2 f x ![EuclideanSpace.single i 1, EuclideanSpace.single i 1]

end TegmarkDimensionality

Source

M. Tegmark, *On the dimensionality of spacetime*, Class. Quantum Grav. 14 (1997) L69–L75, https://doi.org/10.1088/0264-9381/14/4/002, p. L70 (Poisson equation

\nabla^2\phi=\rho

)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source paper and of the intended meaning. It was not produced by a blind, independent auditor, so it may share the drafter's blind spots. Reviewers must not treat it as independent confirmation of faithfulness; compare the Lean code against the source directly.

For a natural number $n$ , a function $f:\mathbb R^n\to\mathbb R$ (Euclidean $n$ -space) and a point $x$ , the quantity $\nabla^2 f(x)$ is defined as

\nabla^2 f(x)=\sum_{i=1}^{n} D^2f(x)(e_i,e_i),

where $e_i$ is the $i$ -th standard unit vector and $D^2f(x)$ is the second iterated Fréchet derivative of $f$ at $x$ , viewed as a bilinear form. The derivative of a non-differentiable function is $0$ by convention, so $\nabla^2f(x)$ is a junk value, typically $0$ , when $f$ is not twice differentiable near $x$ . For $n=0$ the sum is empty and $\nabla^2 f=0$ .

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Laplacian on Rn\mathbb R^nRn

Laplacian on $\mathbb R^n$