Distributional Laplacian of the Green kernel of the unit ball

For a pole in the closed unit ball, the Green kernel is the Newtonian fundamental solution minus a correction harmonic throughout the ball. Thus its distributional negative Laplacian is the Dirac mass at the pole. This is the interior equation for the Dirichlet Green function; its zero boundary values are proved with the kernel construction.

This weak Green equation characterizes the kernel's interior response to a point source; see Evans, Partial Differential Equations, Section 2.2.

@[simp]

theorem TauCeti.integral_laplacian_mul_ballGreenKernel {n : ℕ} (hn : 3 ≤ n) {x : EuclideanSpace ℝ (Fin n)} (hx : ‖x‖ ≤ 1) (φ : TestFunction { carrier := Metric.ball 0 1, is_open' := ⋯ } ℝ ⊤) : ∫ (y : EuclideanSpace ℝ (Fin n)), Laplacian.laplacian (⇑φ) y * ballGreenKernel n x y = -φ x

The unit-ball Green kernel has distributional negative Laplacian equal to a Dirac mass at its pole. The test function is supported strictly inside the ball, so no boundary term appears.