The distribution induced by the Euclidean Newtonian kernel

The totalized n-dimensional Newtonian kernel and its Fréchet derivative are locally integrable in every dimension: the kernel and derivative are zero in dimensions zero and two, the one-dimensional kernel is continuous, and the higher-dimensional singularities are integrable. This file packages that fact with Mathlib's canonical distribution induced by a locally integrable function. The resulting distribution is the object to which the distributional identity -Δ Gₙ = δ₀ applies.

The normalization and decay estimate are the standard ones from Evans, Partial Differential Equations, Section 2.2. The kernel and its derivative have locally integrable singularities; their local integrability is the input for the distributional identity -Δ Gₙ = δ₀, proved in TauCeti.Analysis.PDE.FundamentalSolution.Euclidean.DistributionalLaplacian.

Main declarations

• TauCeti.locallyIntegrable_newtonianKernel: local integrability of Gₙ.
• TauCeti.newtonianKernelDistribution: the distribution induced by Gₙ on all of Euclidean space in dimensions n ≥ 3.
• TauCeti.newtonianKernelDistribution_apply: its test-function pairing.

theorem TauCeti.locallyIntegrable_newtonianKernel (n : ℕ) : MeasureTheory.LocallyIntegrable (newtonianKernel n) MeasureTheory.volume

The Newtonian kernel is locally integrable in every dimension.

In dimensions zero and two it is identically zero; in dimension one the totalized kernel is continuous, and in dimensions at least three its radial singularity has order n - 2, strictly below the ambient dimension.

theorem TauCeti.locallyIntegrable_fderiv_newtonianKernel (n : ℕ) : MeasureTheory.LocallyIntegrable (fun (x : EuclideanSpace ℝ (Fin n)) => fderiv ℝ (newtonianKernel n) x) MeasureTheory.volume

The Fréchet derivative of the Newtonian kernel is locally integrable in every dimension.

In dimensions zero and two it is identically zero; in dimensions one and at least three its radial order is 1 - n, strictly below the ambient dimension.

noncomputable def TauCeti.newtonianKernelDistribution (n : ℕ) (_hn : 3 ≤ n) : Distribution ⊤ ℝ ⊤

The distribution induced by the Newtonian kernel on all of Euclidean space in dimensions n ≥ 3. The dimension hypothesis reserves this name for the higher-dimensional fundamental solution, since the totalized kernel formula is defined in every dimension.

Equations

• TauCeti.newtonianKernelDistribution n _hn = Distribution.ofFun ⊤ (TauCeti.newtonianKernel n) MeasureTheory.volume ⊤

@[simp]

theorem TauCeti.newtonianKernelDistribution_apply (n : ℕ) (hn : 3 ≤ n) (φ : TestFunction ⊤ ℝ ⊤) : (newtonianKernelDistribution n hn) φ = ∫ (x : EuclideanSpace ℝ (Fin n)), φ x • newtonianKernel n x

Evaluation of the Newtonian-kernel distribution on a smooth compactly supported test function.