Corollary 2.27 — ∂ᵢⱼu(x) = ∫_{B_R(x)} ∂ᵢⱼΓ(x−y)[f(y)−f(x)] dy − (1/n) f(x) δᵢⱼ

Proved

HunterPDE.Newtonian.secondPartial_newtonianPotential_ball

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

newtonian-potentialp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pdesingular-integrals

Let $n \ge 2$ , $f \in C_c^\infty(\mathbb{R}^n)$ and $u = \Gamma * f$ . Let $x \in \mathbb{R}^n$ and let $B_R(x)$ be an open ball centered at $x$ containing the support of $f$ . Then for all indices $i, j$

\partial_{ij} u(x) = \int_{B_R(x)} \partial_{ij}\Gamma(x - y)\,\bigl[f(y) - f(x)\bigr]\,dy - \frac{1}{n} f(x)\,\delta_{ij},

where $\partial_{ij}\Gamma(x - y)$ is the second partial derivative of $\Gamma$ evaluated at $x - y$ and $\delta_{ij}$ is the Kronecker delta. The kernel $\partial_{ij}\Gamma$ is not locally integrable, and the subtraction of $f(x)$ is what makes the integral converge; this representation is the input to the Hölder estimate, Theorem 2.28.

Formalization Note. Indices are 0-based. The statement asserts, as a first conjunct, that $y \mapsto \partial_{ij}\Gamma(x-y)[f(y)-f(x)]$ is Lebesgue integrable on $B_R(x)$ (an absolutely convergent integral, as the book's proof uses), and then the identity. The support is the closed support tsupport f, and $R > 0$ .

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Newtonian_FundamentalSolution
import Definitions.Def_HunterPDE_Newtonian_NewtonianPotential
import Definitions.Def_HunterPDE_Newtonian_PartialDeriv

Formal statement

namespace HunterPDE.Newtonian

open MeasureTheory
open scoped ContDiff

/-- Hunter, *Notes on PDEs*, p. 39, Corollary 2.27: if `f ∈ C_c^∞(ℝⁿ)` (`n ≥ 2`) and
`u = Γ ∗ f`, then for every `x` and every open ball `B_R(x)` centered at `x` that contains the
support of `f`,
`∂ᵢⱼu(x) = ∫_{B_R(x)} ∂ᵢⱼΓ(x − y) [f(y) − f(x)] dy − (1/n) f(x) δᵢⱼ`.
Here `∂ᵢⱼΓ(x − y)` is the second partial derivative of `Γ` evaluated at `x − y`; the integrand
is Lebesgue integrable on the ball (asserted as the first conjunct, as the proof of Theorem 2.26
states). Indices are 0-based. -/
theorem secondPartial_newtonianPotential_ball (n : ℕ) (hn : 2 ≤ n)
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f)
    (x : EuclideanSpace ℝ (Fin n)) (R : ℝ) (hR : 0 < R)
    (hsupp : tsupport f ⊆ Metric.ball x R) (i j : Fin n) :
    IntegrableOn (fun y => secondPartial (fundamentalSolution n) i j (x - y) * (f y - f x))
        (Metric.ball x R) ∧
      secondPartial (newtonianPotential n f) i j x =
        (∫ y in Metric.ball x R, secondPartial (fundamentalSolution n) i j (x - y) * (f y - f x))
          - 1 / (n : ℝ) * f x * (if i = j then 1 else 0) := by sorry

end HunterPDE.Newtonian

Source

Hunter, Notes on Partial Differential Equations (revised 6/18/2014), p. 39, Corollary 2.27, Eq. (2.29)

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$ ) with compact support.
$x \in \mathbb{R}^n$ is a point.
$R$ is a real number with $R > 0$ .
The closed support $\overline{\{f \ne 0\}}$ is contained in the open ball $B_R(x) = \{y : |y - x| < R\}$ .
$i, j \in \{0, \dots, n-1\}$ are coordinate indices.

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$ .
$u(z) = \int_{\mathbb{R}^n}\Gamma_n(z-y)f(y)\,dy$ is the Newtonian potential. It is a Lebesgue integral, taken to be $0$ where the integrand is not integrable.
For any function $g$ :
- $\partial_j g(z)$ is the Fréchet derivative of $g$ at $z$ applied to the standard basis vector $e_j$ , and is $0$ where $g$ is not differentiable.
- $\partial_{ij} g(z) = \partial_i(\partial_j g)(z)$ : differentiate in direction $j$ first, then in direction $i$ . The outer derivative is taken of the everywhere-defined function $\partial_j g$ , including its zero junk values.

Assertion. The statement asserts both of the following.

Integrability. The function $y \mapsto \partial_{ij}\Gamma_n(x-y)\,\big(f(y) - f(x)\big)$ is Lebesgue integrable on the ball $B_R(x)$ .
Formula.

\partial_{ij} u(x) = \int_{B_R(x)} \partial_{ij}\Gamma_n(x-y)\,\big(f(y)-f(x)\big)\,dy \;-\; \frac{1}{n}\, f(x)\,\delta_{ij},

where $\delta_{ij}$ is $1$ if $i = j$ and $0$ otherwise.

Degenerate cases:

Excluded dimensions. $n \ge 2$ excludes $n = 0, 1$ .
The point $y = x$ . In the integrand, $\partial_{ij}\Gamma_n(x - y)$ at $y = x$ is the value produced by the derivative conventions at $0$ , possibly the junk value $0$ . This is a single point of measure zero.
Satisfiability of the support hypothesis. For any such $f$ and any $x$ , a sufficiently large $R$ satisfies it. If $f \equiv 0$ , every $R > 0$ works, and both sides of the formula are $0$ .
Choice of $R$ . The statement quantifies over every admissible $R$ . So it asserts that the right-hand side takes the same value for all such radii.
Symmetry. The statement is made separately for each ordered pair $(i, j)$ . No symmetry of $\partial_{ij}$ is assumed.

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