Theorem 2.25 — the Newtonian potential u = Γ ∗ f is C^∞ and solves −Δu = f

Proved

HunterPDE.Newtonian.newtonianPotential_poisson

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$ , let $f \in C_c^\infty(\mathbb{R}^n)$ , and let $u = \Gamma * f$ be its Newtonian potential, where $\Gamma$ is the fundamental solution (2.12). Then $u \in C^\infty(\mathbb{R}^n)$ and $u$ solves Poisson's equation

-\Delta u = f \quad\text{in } \mathbb{R}^n.

This is the existence half of the theory of Poisson's equation on the whole space and the starting point for the regularity estimates of this mission.

Formalization Note. The statement has three conjuncts: for every $x$ the integrand $y \mapsto \Gamma(x-y) f(y)$ is Lebesgue integrable (so $u(x)$ is a genuine integral, not Lean's default value $0$ for a non-integrable function), $u$ is ContDiff ℝ ∞, and $-\Delta u(x) = f(x)$ for every $x$ . The integrability conjunct makes explicit what the book's definition of $\Gamma * f$ presupposes.

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. 34, Theorem 2.25: if `f ∈ C_c^∞(ℝⁿ)` (`n ≥ 2`) and
`u = Γ ∗ f` with `Γ` the fundamental solution (2.12), then `u ∈ C^∞(ℝⁿ)` and `−Δu = f`
(2.16). The first conjunct records that the convolution integral `∫ Γ(x − y) f(y) dy` defining
`u(x)` is a genuine Lebesgue integral for every `x` (so `u` is not the Bochner junk value `0`).
`ContDiff ℝ ∞` is `C^∞` (not `ContDiff ℝ ⊤`, which is analyticity in this Mathlib). -/
theorem newtonianPotential_poisson (n : ℕ) (hn : 2 ≤ n)
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f) :
    (∀ x, Integrable (fun y => fundamentalSolution n (x - y) * f y)) ∧
      ContDiff ℝ ∞ (newtonianPotential n f) ∧
      ∀ x, -(Δ (newtonianPotential n f)) x = f x := by sorry

end HunterPDE.Newtonian

Source

Hunter, Notes on Partial Differential Equations (revised 6/18/2014), p. 34, Theorem 2.25

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$ : continuously differentiable to every finite order, not analytic) on all of $\mathbb{R}^n$ .
$f$ has compact support: the closure of $\{f \ne 0\}$ is compact.

Symbols.

$\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$ .
$u$ is the Newtonian potential

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

a Lebesgue integral over $\mathbb{R}^n$ that would be $0$ at any $x$ where the integrand is not integrable.

$\Delta u$ is the Laplacian of $u$ : the sum of second derivatives of $u$ along an orthonormal basis.

Assertion. The statement asserts three things.

Integrability. For every $x$ , the function $y \mapsto \Gamma_n(x-y)f(y)$ is Lebesgue integrable over $\mathbb{R}^n$ .
Smoothness. $u$ is infinitely differentiable ( $C^\infty$ ) on all of $\mathbb{R}^n$ .
Poisson equation. For every $x \in \mathbb{R}^n$ ,

-\Delta u(x) = f(x).

Degenerate cases:

Excluded dimensions. $n \ge 2$ excludes $n = 0, 1$ .
Zero function. $f \equiv 0$ satisfies the hypotheses, gives $u \equiv 0$ , and then all three conclusions hold trivially.
Default integral value. Part 1 rules out the default- $0$ value of the integral for every $x$ .
The origin. The value $\Gamma_n(0) = 0$ enters only at the 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