The Newtonian kernel in dimension at least three

For 3 ≤ n, this file defines the Newtonian kernel for the negative Laplacian on EuclideanSpace ℝ (Fin n):

Gₙ(x) = (n (n - 2) ωₙ)⁻¹ ‖x‖²⁻ⁿ,

where ωₙ is the volume of the Euclidean unit ball. It proves the full Fréchet derivative formula and the pointwise equation Δ Gₙ = 0 away from the pole, together with translated versions for a pole at an arbitrary point. The dimension-three specialization recovers the classical kernel 1 / (4π‖x‖).

The normalization and formulas follow Evans, Partial Differential Equations, Section 2.2. The distributional identity -Δ Gₙ = δ₀ is proved from the derivative formula here in TauCeti.Analysis.PDE.FundamentalSolution.Euclidean.DistributionalLaplacian.

Main declarations

• TauCeti.newtonianKernel: the normalized kernel in dimension n ≥ 3.
• TauCeti.hasFDerivAt_newtonianKernel: its derivative away from the origin.
• TauCeti.norm_fderiv_newtonianKernel: the ‖x‖ ^ (1 - n) operator norm of that derivative.
• TauCeti.laplacian_newtonianKernel: the pointwise equation Δ Gₙ = 0 away from the origin.
• TauCeti.harmonicAt_newtonianKernel_sub: harmonicity of the kernel with a translated pole.
• TauCeti.newtonianKernel_three: the familiar three-dimensional formula.

noncomputable def TauCeti.newtonianKernel (n : ℕ) (x : EuclideanSpace ℝ (Fin n)) : ℝ

The Newtonian kernel for the negative Laplacian on ℝⁿ.

For 3 ≤ n, this normalization is the fundamental solution, and the exponent 2 - n is negative. Lean's convention for a negative real power of zero makes the kernel take the value zero at the pole in these dimensions. Results that need the higher-dimensional regime state it as a hypothesis rather than carrying it in the definition.

Equations

• TauCeti.newtonianKernel n x = (↑n * (↑n - 2) * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * ‖x‖ ^ (2 - ↑n)

theorem TauCeti.newtonianKernel_def (n : ℕ) (x : EuclideanSpace ℝ (Fin n)) : newtonianKernel n x = (↑n * (↑n - 2) * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * ‖x‖ ^ (2 - ↑n)

The defining formula for the Newtonian kernel. The body of TauCeti.newtonianKernel is not @[expose]d, so this is the form in which other modules reach the definition.

@[simp]

theorem TauCeti.newtonianKernel_zero (n : ℕ) : newtonianKernel n 0 = 0

The totalized Newtonian kernel takes the value zero at its pole.

@[simp]

theorem TauCeti.newtonianKernel_map_linearIsometryEquiv (n : ℕ) (e : EuclideanSpace ℝ (Fin n) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n)) (x : EuclideanSpace ℝ (Fin n)) : newtonianKernel n (e x) = newtonianKernel n x

The Newtonian kernel is radial, hence invariant under orthogonal transformations.

theorem TauCeti.newtonianKernel_sub_comm (n : ℕ) (x a : EuclideanSpace ℝ (Fin n)) : newtonianKernel n (x - a) = newtonianKernel n (a - x)

The Newtonian kernel is symmetric under exchanging a point and its pole.

theorem TauCeti.newtonianKernel_smul (n : ℕ) (r : ℝ) (x : EuclideanSpace ℝ (Fin n)) : newtonianKernel n (r • x) = ‖r‖ ^ (2 - ↑n) * newtonianKernel n x

Real dilation scales the Newtonian kernel with radial homogeneity 2 - n.

theorem TauCeti.volume_real_unitBall_pos (n : ℕ) : 0 < MeasureTheory.volume.real (Metric.ball 0 1)

The Euclidean unit ball has positive real volume in every dimension.

theorem TauCeti.newtonianKernel_pos (n : ℕ) (hn : 3 ≤ n) {x : EuclideanSpace ℝ (Fin n)} (hx : x ≠ 0) : 0 < newtonianKernel n x

Away from the pole, the normalized Newtonian kernel is strictly positive.

theorem TauCeti.newtonianKernel_rpow_sq_lt (n : ℕ) (hn : n ≠ 2) (hn0 : 0 < n) {a b : ℝ} (ha : 0 < a) (hab : a < b) : (↑n * (↑n - 2) * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * b ^ ((2 - ↑n) / 2) < (↑n * (↑n - 2) * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * a ^ ((2 - ↑n) / 2)

The radial expression for the Newtonian kernel strictly decreases as the squared radius increases, in every nondegenerate positive dimension.

theorem TauCeti.newtonianKernel_lt_newtonianKernel_of_norm_lt (n : ℕ) (hn : n ≠ 2) {x y : EuclideanSpace ℝ (Fin n)} (hx : x ≠ 0) (h : ‖x‖ < ‖y‖) : newtonianKernel n y < newtonianKernel n x

In a positive dimension other than two, the Newtonian kernel strictly decreases with distance from the origin.

theorem TauCeti.hasFDerivAt_newtonianKernel (n : ℕ) (hn : n ≠ 2) {x : EuclideanSpace ℝ (Fin n)} (hx : x ≠ 0) : HasFDerivAt (newtonianKernel n) ((-(↑n * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * ‖x‖ ^ (-↑n)) • (innerSL ℝ) x) x

The Fréchet derivative of the Newtonian kernel away from its pole.

theorem TauCeti.fderiv_newtonianKernel (n : ℕ) (hn : n ≠ 2) {x : EuclideanSpace ℝ (Fin n)} (hx : x ≠ 0) : fderiv ℝ (newtonianKernel n) x = (-(↑n * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * ‖x‖ ^ (-↑n)) • (innerSL ℝ) x

The Fréchet derivative of the Newtonian kernel as a continuous linear functional.

theorem TauCeti.fderiv_newtonianKernel_apply (n : ℕ) (hn : n ≠ 2) {x : EuclideanSpace ℝ (Fin n)} (hx : x ≠ 0) (v : EuclideanSpace ℝ (Fin n)) : (fderiv ℝ (newtonianKernel n) x) v = -((↑n * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * ‖x‖ ^ (-↑n) * inner ℝ x v)

The derivative of the Newtonian kernel evaluated in a direction.

@[simp]

theorem TauCeti.norm_fderiv_newtonianKernel (n : ℕ) (hn : n ≠ 2) {x : EuclideanSpace ℝ (Fin n)} (hx : x ≠ 0) : ‖fderiv ℝ (newtonianKernel n) x‖ = (↑n * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * ‖x‖ ^ (1 - ↑n)

The operator norm of the derivative of the Newtonian kernel decays like ‖x‖ ^ (1 - n).

theorem TauCeti.contDiffAt_newtonianKernel (n : ℕ) {x : EuclideanSpace ℝ (Fin n)} (hx : x ≠ 0) : ContDiffAt ℝ 2 (newtonianKernel n) x

Away from its pole, the Newtonian kernel is twice continuously differentiable.

@[simp]

theorem TauCeti.laplacian_newtonianKernel (n : ℕ) {x : EuclideanSpace ℝ (Fin n)} (hx : x ≠ 0) : Laplacian.laplacian (newtonianKernel n) x = 0

The Newtonian kernel solves the homogeneous Laplace equation pointwise away from its pole.

theorem TauCeti.harmonicAt_newtonianKernel (n : ℕ) {x : EuclideanSpace ℝ (Fin n)} (hx : x ≠ 0) : InnerProductSpace.HarmonicAt (newtonianKernel n) x

The Newtonian kernel is harmonic at every point away from its pole at the origin.

theorem TauCeti.harmonicOnNhd_newtonianKernel (n : ℕ) : InnerProductSpace.HarmonicOnNhd (newtonianKernel n) {0}ᶜ

The Newtonian kernel is harmonic on the punctured Euclidean space.

theorem TauCeti.harmonicAt_newtonianKernel_sub (n : ℕ) {x a : EuclideanSpace ℝ (Fin n)} (hxa : x ≠ a) : InnerProductSpace.HarmonicAt (fun (y : EuclideanSpace ℝ (Fin n)) => newtonianKernel n (y - a)) x

A Newtonian kernel with pole at a is harmonic away from that pole.

theorem TauCeti.contDiffAt_newtonianKernel_sub (n : ℕ) {x a : EuclideanSpace ℝ (Fin n)} (hxa : x ≠ a) : ContDiffAt ℝ 2 (fun (y : EuclideanSpace ℝ (Fin n)) => newtonianKernel n (y - a)) x

A Newtonian kernel with pole at a is twice continuously differentiable away from a.

theorem TauCeti.hasFDerivAt_newtonianKernel_sub (n : ℕ) (hn : n ≠ 2) {x a : EuclideanSpace ℝ (Fin n)} (hxa : x ≠ a) : HasFDerivAt (fun (y : EuclideanSpace ℝ (Fin n)) => newtonianKernel n (y - a)) ((-(↑n * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * ‖x - a‖ ^ (-↑n)) • (innerSL ℝ) (x - a)) x

A Newtonian kernel with pole at a has the translated Fréchet derivative.

theorem TauCeti.fderiv_newtonianKernel_sub (n : ℕ) (hn : n ≠ 2) {x a : EuclideanSpace ℝ (Fin n)} (hxa : x ≠ a) : fderiv ℝ (fun (y : EuclideanSpace ℝ (Fin n)) => newtonianKernel n (y - a)) x = (-(↑n * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * ‖x - a‖ ^ (-↑n)) • (innerSL ℝ) (x - a)

The Fréchet derivative of a Newtonian kernel with pole at a.

theorem TauCeti.fderiv_newtonianKernel_sub_apply (n : ℕ) (hn : n ≠ 2) {x a : EuclideanSpace ℝ (Fin n)} (hxa : x ≠ a) (v : EuclideanSpace ℝ (Fin n)) : (fderiv ℝ (fun (y : EuclideanSpace ℝ (Fin n)) => newtonianKernel n (y - a)) x) v = -((↑n * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * ‖x - a‖ ^ (-↑n) * inner ℝ (x - a) v)

The derivative of the Newtonian kernel with a translated pole.

@[simp]

theorem TauCeti.norm_fderiv_newtonianKernel_sub (n : ℕ) (hn : n ≠ 2) {x a : EuclideanSpace ℝ (Fin n)} (hxa : x ≠ a) : ‖fderiv ℝ (fun (y : EuclideanSpace ℝ (Fin n)) => newtonianKernel n (y - a)) x‖ = (↑n * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * ‖x - a‖ ^ (1 - ↑n)

The operator norm of the derivative of a Newtonian kernel with pole at a.

@[simp]

theorem TauCeti.laplacian_newtonianKernel_sub (n : ℕ) {x a : EuclideanSpace ℝ (Fin n)} (hxa : x ≠ a) : Laplacian.laplacian (fun (y : EuclideanSpace ℝ (Fin n)) => newtonianKernel n (y - a)) x = 0

A translated Newtonian kernel solves the homogeneous Laplace equation away from its pole.

theorem TauCeti.harmonicOnNhd_newtonianKernel_sub (n : ℕ) (a : EuclideanSpace ℝ (Fin n)) : InnerProductSpace.HarmonicOnNhd (fun (x : EuclideanSpace ℝ (Fin n)) => newtonianKernel n (x - a)) {a}ᶜ

A Newtonian kernel with pole at a is harmonic on the complement of the pole.

theorem TauCeti.newtonianKernel_three (x : EuclideanSpace ℝ (Fin 3)) : newtonianKernel 3 x = (4 * Real.pi * ‖x‖)⁻¹

In dimension three the Newtonian kernel is the classical function 1 / (4π‖x‖).