Finite-annulus integration by parts for the cancelled Newtonian Hessian

Proved

HunterPDE.Newtonian.cancelled_hessian_annulus_identity

by Mazecto · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

integration-by-partsnewtonian-potentialpde

Let $n\ge2$ , let $f\in C_c^2(\mathbb R^n)$ , and suppose its support is contained in $B_R(x)$ , where $0<r<R$ . Write $\Gamma$ for the Newtonian fundamental solution, $A=B_R(x)\setminus\overline B_r(x)$ and

B_{ij}(R)=R^{n-1}\int_{S^{n-1}}\partial_i\Gamma(-R\omega)\omega_j\,dS(\omega).

For coordinate indices $i,j$ , define the inner error

E_{ij}(r)=r^{n-1}\int_{S^{n-1}}\left[\Gamma(-r\omega)\partial_jf(x+r\omega)\omega_i+\partial_i\Gamma(-r\omega)(f(x+r\omega)-f(x))\omega_j\right]dS(\omega).

Then the exact finite-radius identity is

\int_A\partial_{ij}\Gamma(x-y)(f(y)-f(x))\,dy=\int_A\Gamma(x-y)\partial_{ij}f(y)\,dy+f(x)B_{ij}(R)+E_{ij}(r).

This separates integration by parts on a regular annulus from the estimates at the singularity, and applies at every positive inner radius below the outer radius.

Preamble

import Definitions.Def_HunterPDE_Newtonian_FundamentalSolution
import Definitions.Def_HunterPDE_Newtonian_PartialDeriv
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.MeasureTheory.Integral.Bochner.Set
import Mathlib.MeasureTheory.Constructions.HaarToSphere
open MeasureTheory HunterPDE.Newtonian Filter
open scoped ContDiff Topology

Formal statement

theorem HunterPDE.Newtonian.cancelled_hessian_annulus_identity
    (n : ℕ) (hn : 2 ≤ n) (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f)
    (x : EuclideanSpace ℝ (Fin n)) (R r : ℝ) (hR : 0 < R)
    (hr : 0 < r) (hrR : r < R) (hsupp : tsupport f ⊆ Metric.ball x R) (i j : Fin n) :
    (∫ y in Metric.ball x R \ Metric.closedBall x r,
      secondPartial (fundamentalSolution n) i j (x - y) * (f y - f x)) =
    (∫ y in Metric.ball x R \ Metric.closedBall x r,
      fundamentalSolution n (x - y) * secondPartial f i j y)
    + f x * (R ^ (n - 1) *
      (∫ (w : Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1),
        partialDeriv (fundamentalSolution n) i (-(R • w.1)) * w.1 j ∂volume.toSphere))
    + r ^ (n - 1) *
      (∫ (w : Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1),
        fundamentalSolution n (-(r • w.1)) * partialDeriv f j (x + r • w.1) * w.1 i
        + partialDeriv (fundamentalSolution n) i (-(r • w.1)) *
          (f (x + r • w.1) - f x) * w.1 j ∂volume.toSphere) := by sorry

Source

Hunter, Notes on Partial Differential Equations, revised 6/18/2014, https://www.math.ucdavis.edu/~hunter/pdes/ch2.pdf, printed pp. 37–38, Eqs. (2.27)–(2.28) and subsequent inner-boundary estimates; finite-radius identity and quantitative C1 formulation.

View graph