The Newtonian kernel is a fundamental solution of -Δ

For n ≥ 3, the Newtonian kernel Gₙ(x) = (n (n - 2) ωₙ)⁻¹ ‖x‖²⁻ⁿ on ℝⁿ satisfies the distributional identity -Δ Gₙ = δ₀: for every C² function f with compact support,

∫ x, Δ f x * Gₙ x = -f 0,

and, with the pole moved to a, ∫ x, Δ f x * Gₙ (x - a) = -f a.

The proof has two steps.

• The weak gradient. Integration by parts against Gₙ holds across the pole: for a C¹ function g with compact support, ∫ Gₙ ∂ᵥg = -∫ (∂ᵥGₙ) g. The kernel is replaced by the smooth regularizations C (‖x‖² + t) ^ ((2 - n) / 2), for which Mathlib's integration by parts applies, and t → 0⁺ by dominated convergence: both the regularized kernels and their derivatives are dominated by the kernel and its derivative. In particular Gₙ is weakly differentiable on every open set with weak derivative its classical one.
• The flux. Summing over an orthonormal basis turns ∫ Δ f Gₙ into -∫ ∇Gₙ · ∇f = (n ωₙ)⁻¹ ∫ ‖x‖⁻ⁿ f' x x, and the radial fundamental theorem of calculus TauCeti.integral_norm_rpow_neg_finrank_mul_fderiv_apply_self evaluates the latter integral as -(n ωₙ) f 0.

The statement and the normalization follow Evans, Partial Differential Equations, Section 2.2.1, Theorem 1, whose Green's-identity argument on the complement of a small ball is replaced here by the two steps above.

Main declarations

• TauCeti.integral_newtonianKernel_mul_fderiv_eq_neg_fderiv_mul: integration by parts against the Newtonian kernel.
• TauCeti.hasWeakFDerivOn_newtonianKernel: the classical derivative of the kernel is its weak derivative.
• TauCeti.integral_laplacian_mul_newtonianKernel: -Δ Gₙ = δ₀.
• TauCeti.integral_laplacian_mul_newtonianKernel_sub: the same identity with the pole at a.

theorem TauCeti.integral_newtonianKernel_mul_fderiv_eq_neg_fderiv_mul {n : ℕ} (hn : 3 ≤ n) {g : EuclideanSpace ℝ (Fin n) → ℝ} (hg : ContDiff ℝ 1 g) (hc : HasCompactSupport g) (v : EuclideanSpace ℝ (Fin n)) : ∫ (x : EuclideanSpace ℝ (Fin n)), newtonianKernel n x * (fderiv ℝ g x) v = -∫ (x : EuclideanSpace ℝ (Fin n)), (fderiv ℝ (newtonianKernel n) x) v * g x

Integration by parts against the Newtonian kernel. For n ≥ 3 and a C¹ function g with compact support, ∫ Gₙ ∂ᵥg = -∫ (∂ᵥGₙ) g, although Gₙ is singular at the origin.

theorem TauCeti.hasWeakFDerivOn_newtonianKernel {n : ℕ} (hn : 3 ≤ n) (Ω : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin n))) : HasWeakFDerivOn MeasureTheory.volume Ω (newtonianKernel n) (fderiv ℝ (newtonianKernel n))

The Newtonian kernel is weakly differentiable. For n ≥ 3, on every open set the classical derivative of Gₙ, which exists away from the origin, is a weak derivative of Gₙ.

theorem TauCeti.integral_laplacian_mul_newtonianKernel {n : ℕ} (hn : 3 ≤ n) {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : ContDiff ℝ 2 f) (hc : HasCompactSupport f) : ∫ (x : EuclideanSpace ℝ (Fin n)), Laplacian.laplacian f x * newtonianKernel n x = -f 0

The Newtonian kernel is a fundamental solution of -Δ. For n ≥ 3 and every C² function f with compact support on ℝⁿ, ∫ Δ f · Gₙ = -f 0; that is, -Δ Gₙ = δ₀ in the sense of distributions.

theorem TauCeti.integral_laplacian_mul_newtonianKernel_sub {n : ℕ} (hn : 3 ≤ n) {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : ContDiff ℝ 2 f) (hc : HasCompactSupport f) (a : EuclideanSpace ℝ (Fin n)) : ∫ (x : EuclideanSpace ℝ (Fin n)), Laplacian.laplacian f x * newtonianKernel n (x - a) = -f a

The Newtonian kernel with pole a is a fundamental solution of -Δ. For n ≥ 3 and every C² function f with compact support on ℝⁿ, ∫ Δ f · Gₙ(· - a) = -f a.