Flux of the Newtonian kernel in Euclidean space

For every dimension n ≠ 0 and n ≠ 2, this file computes the outward normal derivative of the normalized Newtonian kernel on a sphere. Integrating against the canonical measure on the unit sphere, with the radial surface Jacobian, gives total flux -1 through every sphere centered at the pole. This is the boundary form of the normalization in the distributional identity -Δ Gₙ = δ₀. The case n = 2 is excluded because the normalization of newtonianKernel degenerates there. The logarithmic planar kernel is developed separately on ℂ as planarNewtonianKernel in TauCeti.Analysis.PDE.FundamentalSolution.Flux.

The measure volume.toSphere is Mathlib's polar-coordinate surface measure. Its total mass is n times the volume of the Euclidean unit ball.

Main declarations

• TauCeti.fderiv_newtonianKernel_sub_apply_sphere_normal: the outward normal derivative on a sphere.
• TauCeti.integral_fderiv_newtonianKernel_sub_sphere_normal: the total sphere flux is -1.

@[simp]

theorem TauCeti.fderiv_newtonianKernel_sub_apply_sphere_normal (n : ℕ) (hn2 : n ≠ 2) {a : EuclideanSpace ℝ (Fin n)} {r : ℝ} (hr : 0 < r) (u : ↑(Metric.sphere 0 1)) : (fderiv ℝ (fun (y : EuclideanSpace ℝ (Fin n)) => newtonianKernel n (y - a)) (a + r • ↑u)) ↑u = -((↑n * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * r ^ (1 - ↑n))

On the sphere of radius r centered at its pole, the outward normal derivative of the Newtonian kernel is constant and equals -(n ωₙ)⁻¹ r^(1-n).

theorem TauCeti.integral_fderiv_newtonianKernel_sub_sphere_normal (n : ℕ) (hn0 : n ≠ 0) (hn2 : n ≠ 2) {a : EuclideanSpace ℝ (Fin n)} {r : ℝ} (hr : 0 < r) : r ^ (↑n - 1) * ∫ (u : ↑(Metric.sphere 0 1)), (fderiv ℝ (fun (y : EuclideanSpace ℝ (Fin n)) => newtonianKernel n (y - a)) (a + r • ↑u)) ↑u ∂MeasureTheory.volume.toSphere = -1

The outward flux of the Newtonian kernel through any sphere centered at its pole is -1. The factor r ^ ((n : ℝ) - 1) is the surface Jacobian for radial scaling from the unit sphere.