Eq. (2.23) — Γ ∗ (Δf) = −f for f ∈ C_c^∞(ℝⁿ)

Proved

HunterPDE.Newtonian.newtonianPotential_laplacian

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

newtonian-potentialp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pdepoisson-equation

Let $n \ge 2$ and let $f \in C_c^\infty(\mathbb{R}^n)$ be smooth with compact support. Then the convolution of the Laplacian of $f$ with the fundamental solution recovers $-f$ :

\Gamma * (\Delta f) = -f, \qquad\text{i.e.}\qquad \int_{\mathbb{R}^n} \Gamma(x - y)\,\Delta f(y)\,dy = -f(x) \quad\text{for every } x \in \mathbb{R}^n.

This is the heart of the proof of Theorem 2.25: it represents a test function as the Newtonian potential of its own Laplacian.

Formalization Note. $\Delta$ is Mathlib's Laplacian on the inner-product space EuclideanSpace ℝ (Fin n) (the sum of pure second partial derivatives in an orthonormal basis). The statement first asserts that $y \mapsto \Gamma(x-y)\,\Delta f(y)$ is Lebesgue integrable for every $x$ , so the identity is between genuine integrals. "Smooth" is ContDiff ℝ ∞ (not ContDiff ℝ ⊤, which in this Mathlib means analytic), and compact support is HasCompactSupport.

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Newtonian_FundamentalSolution
import Definitions.Def_HunterPDE_Newtonian_NewtonianPotential

Formal statement

namespace HunterPDE.Newtonian

open MeasureTheory
open scoped ContDiff
open Laplacian

/-- Hunter, *Notes on PDEs*, p. 36, Eq. (2.23): for `f ∈ C_c^∞(ℝⁿ)`, `n ≥ 2`,
`Γ ∗ (Δf) = −f`, i.e. `∫ Γ(x − y) Δf(y) dy = −f(x)` for every `x`; the first conjunct records
that this integral is a genuine Lebesgue integral for every `x`. `Δ` is Mathlib's Laplacian
on the inner product space `EuclideanSpace ℝ (Fin n)` (the sum of the pure second partial
derivatives in any orthonormal basis). -/
theorem newtonianPotential_laplacian (n : ℕ) (hn : 2 ≤ n)
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f) :
    (∀ x, Integrable (fun y => fundamentalSolution n (x - y) * (Δ f) y)) ∧
      ∀ x, newtonianPotential n (Δ f) x = -f x := by sorry

end HunterPDE.Newtonian

Source

Hunter, Notes on Partial Differential Equations (revised 6/18/2014), p. 36, Eq. (2.23)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting.

$n$ is a natural number with $n \ge 2$ .
$f : \mathbb{R}^n \to \mathbb{R}$ is infinitely differentiable ( $C^\infty$ to every finite order) on all of $\mathbb{R}^n$ .
$f$ has compact support: the closure of $\{y : f(y) \ne 0\}$ is compact.

Symbols.

$\Delta f$ is the Laplacian of $f$ : at each point, the sum $\sum_k D^2 f(y)[b_k, b_k]$ of second derivatives along the vectors $b_k$ of an orthonormal basis of $\mathbb{R}^n$ .
$\Gamma_n$ is:
- for $n = 2$ , $\Gamma_2(z) = -\frac{1}{2\pi}\log|z|$ ;
- for $n \ge 3$ , $\Gamma_n(z) = \frac{1}{n(n-2)\alpha_n}|z|^{-(n-2)}$ ;
where $\alpha_n$ is the Lebesgue measure of the open unit ball, and $\Gamma_n(0) = 0$ by the conventions $\log 0 = 0$ and $1/0 = 0$ .

Assertion. The statement asserts both of the following.

Integrability. For every $x \in \mathbb{R}^n$ , the function $y \mapsto \Gamma_n(x-y)\,\Delta f(y)$ is Lebesgue integrable over $\mathbb{R}^n$ .
Identity. For every $x \in \mathbb{R}^n$ ,

\int_{\mathbb{R}^n} \Gamma_n(x-y)\,\Delta f(y)\,dy = -f(x).

Here the left side is the Newtonian potential of $\Delta f$ , the Lebesgue integral with respect to the standard volume measure. Part 1 ensures this integral is a genuine integral rather than the default value $0$ assigned to non-integrable functions.

Degenerate cases:

Excluded dimensions. $n \ge 2$ excludes $n = 0, 1$ .
Zero function. $f \equiv 0$ satisfies the hypotheses. Both conclusions then read $0 = 0$ and are integrability of the zero function.
Satisfiability. The hypotheses are satisfiable by nonzero smooth bump functions.
Undefined values. No value of $\Gamma_n$ other than $\Gamma_n(0) = 0$ is involved in a junk way, and that value sits on a single point $y = x$ .

Human review

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

View graph