The Green kernel and the Poisson kernel of the Euclidean unit ball

This file constructs the Dirichlet Green kernel of the unit ball of ℝⁿ by the method of images. For a pole x in the ball, the corrector

φˣ(y) = Φ(‖x‖ (y - x*)), with x* = x / ‖x‖²,

is the Newtonian kernel Φ with its pole at the reflection of x through the unit sphere, rescaled so that it agrees with Φ(y - x) on the sphere. It is harmonic away from the reflected pole, in particular on a neighbourhood of the closed ball, so the Green kernel

G(x, y) = Φ(y - x) - φˣ(y)

is harmonic in y away from the pole and vanishes for ‖y‖ = 1. The corrector is written through the identity ‖‖x‖ y - x / ‖x‖‖² = ‖x‖² ‖y‖² - 2 ⟪x, y⟫ + 1, whose right-hand side is defined at x = 0 as well, where the corrector is the constant value of Φ on the unit sphere.

The outward normal derivative of G(x, ·) on the unit sphere is the negative of the Poisson kernel of the ball,

K(x, y) = (1 - ‖x‖²) / (n ωₙ ‖x - y‖ⁿ),

where ωₙ is the volume of the unit ball. This is the boundary term of Green's representation formula on the ball, and the kernel of the Poisson integral solving the Dirichlet problem for the Laplacian there. For a boundary point y, the identity 1 - ‖x‖² = -(2 ⟪y, x - y⟫ + ‖x - y‖²) writes K(·, y) as a combination of the dipole ⟪y, x - y⟫ ‖x - y‖⁻ⁿ and the radial power ‖x - y‖^(2 - n), both harmonic away from y; so K(·, y) is harmonic in its pole away from y, in every dimension.

The kernel is normalized for the negative Laplacian, as TauCeti.newtonianKernel is. In dimension two that kernel vanishes identically, so the planar case is instead TauCeti.planarGreenKernel, built from the logarithmic kernel.

Main declarations

• TauCeti.ballGreenCorrector: the reflected Newtonian kernel correcting the boundary values.
• TauCeti.harmonicOnNhd_ballGreenCorrector: harmonicity of the corrector inside the ball.
• TauCeti.ballGreenKernel: the Dirichlet Green kernel of the unit ball.
• TauCeti.ballGreenKernel_comm: symmetry of the Green kernel in its two arguments.
• TauCeti.harmonicAt_ballGreenKernel: harmonicity in y away from the pole.
• TauCeti.ballGreenKernel_eq_zero_of_norm_eq_one_left, TauCeti.ballGreenKernel_eq_zero_of_norm_eq_one_right: vanishing when either argument lies on the unit sphere.
• TauCeti.ballGreenKernel_pos: positivity inside the ball outside dimension two.
• TauCeti.ballPoissonKernel: the Poisson kernel of the unit ball.
• TauCeti.contDiffOn_ballPoissonKernel: joint smoothness of the Poisson kernel off the diagonal.
• TauCeti.harmonicAt_ballPoissonKernel_left, TauCeti.harmonicOnNhd_ballPoissonKernel_left: for a boundary point y, the Poisson kernel is harmonic in its pole away from y.
• TauCeti.fderiv_ballGreenKernel_normal: the outward normal derivative of the Green kernel on the unit sphere is the negative Poisson kernel.

References

• L. C. Evans, Partial Differential Equations, Section 2.2.4 (Green's function for a ball).
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Section 2.5.

Reflection through the unit sphere

theorem TauCeti.norm_sq_norm_smul_sub_inv_norm_smul {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} (hx : x ≠ 0) (y : F) : ‖‖x‖ • y - ‖x‖⁻¹ • x‖ ^ 2 = ‖x‖ ^ 2 * ‖y‖ ^ 2 - 2 * inner ℝ x y + 1

The squared length of ‖x‖ • y - x / ‖x‖, which is ‖x‖ ‖y - x*‖ for the reflection x* = x / ‖x‖² of x through the unit sphere. The right-hand side is a polynomial in x and y, defined at x = 0 as well.

theorem TauCeti.one_sub_norm_mul_norm_sq_le {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) : (1 - ‖x‖ * ‖y‖) ^ 2 ≤ ‖x‖ ^ 2 * ‖y‖ ^ 2 - 2 * inner ℝ x y + 1

The reflection polynomial ‖x‖² ‖y‖² - 2 ⟪x, y⟫ + 1 is at least (1 - ‖x‖ ‖y‖)².

theorem TauCeti.norm_sq_mul_norm_sq_sub_two_mul_inner_add_one_pos {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x y : F} (h : ‖x‖ * ‖y‖ ≠ 1) : 0 < ‖x‖ ^ 2 * ‖y‖ ^ 2 - 2 * inner ℝ x y + 1

The reflection polynomial is positive unless ‖x‖ ‖y‖ = 1; in particular it is positive whenever one of x, y lies in the open unit ball and the other in the closed one.

theorem TauCeti.norm_sub_sq_eq_of_norm_eq_one {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) {y : F} (hy : ‖y‖ = 1) : ‖y - x‖ ^ 2 = ‖x‖ ^ 2 * ‖y‖ ^ 2 - 2 * inner ℝ x y + 1

On the unit sphere, the reflection polynomial is the squared distance to the pole.

The corrector

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

The corrector of the Green kernel of the unit ball with pole x: the Newtonian kernel with its pole at the reflection x / ‖x‖² of x through the unit sphere, dilated by ‖x‖ so that it matches the Newtonian kernel with pole x on the sphere. It is written through the reflection polynomial ‖x‖² ‖y‖² - 2 ⟪x, y⟫ + 1, so at x = 0 it is the constant value of the Newtonian kernel on the unit sphere rather than a separate case.

Equations

• TauCeti.ballGreenCorrector n x y = (↑n * (↑n - 2) * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * (‖x‖ ^ 2 * ‖y‖ ^ 2 - 2 * inner ℝ x y + 1) ^ ((2 - ↑n) / 2)

theorem TauCeti.ballGreenCorrector_def {n : ℕ} (x y : EuclideanSpace ℝ (Fin n)) : ballGreenCorrector n x y = (↑n * (↑n - 2) * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * (‖x‖ ^ 2 * ‖y‖ ^ 2 - 2 * inner ℝ x y + 1) ^ ((2 - ↑n) / 2)

The defining formula for the corrector.

theorem TauCeti.ballGreenCorrector_comm {n : ℕ} (x y : EuclideanSpace ℝ (Fin n)) : ballGreenCorrector n x y = ballGreenCorrector n y x

The corrector is symmetric in the pole and the variable.

theorem TauCeti.ballGreenCorrector_eq_newtonianKernel {n : ℕ} {x : EuclideanSpace ℝ (Fin n)} (hx : x ≠ 0) (y : EuclideanSpace ℝ (Fin n)) : ballGreenCorrector n x y = newtonianKernel n (‖x‖ • y - ‖x‖⁻¹ • x)

Away from the pole x = 0, the corrector is the Newtonian kernel evaluated at ‖x‖ • y - x / ‖x‖, that is, the method-of-images formula Φ(‖x‖ (y - x*)).

@[simp]

theorem TauCeti.ballGreenCorrector_zero_left {n : ℕ} (y : EuclideanSpace ℝ (Fin n)) : ballGreenCorrector n 0 y = (↑n * (↑n - 2) * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹

At the pole x = 0, the corrector is the constant value of the Newtonian kernel on the unit sphere.

@[simp]

theorem TauCeti.ballGreenCorrector_zero_right {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) : ballGreenCorrector n x 0 = (↑n * (↑n - 2) * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹

At the center y = 0, the corrector is the constant value of the Newtonian kernel on the unit sphere.

@[simp]

theorem TauCeti.ballGreenCorrector_eq_newtonianKernel_sub_of_norm_eq_one_right {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) {y : EuclideanSpace ℝ (Fin n)} (hy : ‖y‖ = 1) : ballGreenCorrector n x y = newtonianKernel n (y - x)

For y on the unit sphere, the corrector agrees with the Newtonian kernel with pole x.

@[simp]

theorem TauCeti.ballGreenCorrector_eq_newtonianKernel_sub_of_norm_eq_one_left {n : ℕ} {x : EuclideanSpace ℝ (Fin n)} (hx : ‖x‖ = 1) (y : EuclideanSpace ℝ (Fin n)) : ballGreenCorrector n x y = newtonianKernel n (y - x)

For a pole x on the unit sphere, the corrector agrees with the Newtonian kernel with pole x.

theorem TauCeti.harmonicAt_ballGreenCorrector {n : ℕ} {x y : EuclideanSpace ℝ (Fin n)} (h : 0 < ‖x‖ ^ 2 * ‖y‖ ^ 2 - 2 * inner ℝ x y + 1) : InnerProductSpace.HarmonicAt (ballGreenCorrector n x) y

The corrector is harmonic in y wherever the reflection polynomial ‖x‖² ‖y‖² - 2 ⟪x, y⟫ + 1 is positive, that is, away from the reflected pole x / ‖x‖²; by norm_sq_mul_norm_sq_sub_two_mul_inner_add_one_pos this holds wherever ‖x‖ ‖y‖ ≠ 1, in particular on a neighbourhood of the closed unit ball when the pole x lies in the open ball.

theorem TauCeti.harmonicOnNhd_ballGreenCorrector {n : ℕ} {x : EuclideanSpace ℝ (Fin n)} (hx : ‖x‖ ≤ 1) : InnerProductSpace.HarmonicOnNhd (ballGreenCorrector n x) ↑{ carrier := Metric.ball 0 1, is_open' := ⋯ }

The reflected-pole corrector is harmonic throughout the open unit ball whenever the pole lies in the closed unit ball.

theorem TauCeti.hasFDerivAt_ballGreenCorrector {n : ℕ} (hn : n ≠ 2) {x y : EuclideanSpace ℝ (Fin n)} (h : 0 < ‖x‖ ^ 2 * ‖y‖ ^ 2 - 2 * inner ℝ x y + 1) : HasFDerivAt (ballGreenCorrector n x) ((-(↑n * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * (‖x‖ ^ 2 * ‖y‖ ^ 2 - 2 * inner ℝ x y + 1) ^ (-↑n / 2)) • (‖x‖ ^ 2 • (innerSL ℝ) y - (innerSL ℝ) x)) y

The Fréchet derivative of the corrector in y, wherever the reflection polynomial ‖x‖² ‖y‖² - 2 ⟪x, y⟫ + 1 is positive.

The Green kernel

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

The Dirichlet Green kernel of the Euclidean unit ball with pole x: the Newtonian kernel with pole x, corrected by the reflected kernel so that the difference vanishes on the unit sphere. For a pole in the open ball it is harmonic in y away from x.

Equations

• TauCeti.ballGreenKernel n x y = TauCeti.newtonianKernel n (y - x) - TauCeti.ballGreenCorrector n x y

theorem TauCeti.ballGreenKernel_def {n : ℕ} (x y : EuclideanSpace ℝ (Fin n)) : ballGreenKernel n x y = newtonianKernel n (y - x) - ballGreenCorrector n x y

The defining formula for the Green kernel of the unit ball.

theorem TauCeti.ballGreenKernel_comm {n : ℕ} (x y : EuclideanSpace ℝ (Fin n)) : ballGreenKernel n x y = ballGreenKernel n y x

The Green kernel of the unit ball is symmetric in the pole and the variable.

@[simp]

theorem TauCeti.ballGreenKernel_eq_zero_of_norm_eq_one_right {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) {y : EuclideanSpace ℝ (Fin n)} (hy : ‖y‖ = 1) : ballGreenKernel n x y = 0

The Green kernel of the unit ball vanishes for y on the unit sphere.

@[simp]

theorem TauCeti.ballGreenKernel_eq_zero_of_norm_eq_one_left {n : ℕ} {x : EuclideanSpace ℝ (Fin n)} (hx : ‖x‖ = 1) (y : EuclideanSpace ℝ (Fin n)) : ballGreenKernel n x y = 0

The Green kernel of the unit ball vanishes for a pole x on the unit sphere.

theorem TauCeti.harmonicAt_ballGreenKernel {n : ℕ} {x y : EuclideanSpace ℝ (Fin n)} (hxy : y ≠ x) (h : 0 < ‖x‖ ^ 2 * ‖y‖ ^ 2 - 2 * inner ℝ x y + 1) : InnerProductSpace.HarmonicAt (ballGreenKernel n x) y

The Green kernel of the unit ball is harmonic in y away from the pole, wherever the reflection polynomial ‖x‖² ‖y‖² - 2 ⟪x, y⟫ + 1 is positive.

theorem TauCeti.harmonicOnNhd_ballGreenKernel {n : ℕ} {x : EuclideanSpace ℝ (Fin n)} (hx : ‖x‖ < 1) : InnerProductSpace.HarmonicOnNhd (ballGreenKernel n x) (Metric.ball 0 1 \ {x})

For a pole in the open unit ball, the Green kernel is harmonic on the punctured ball.

theorem TauCeti.ballGreenKernel_pos {n : ℕ} (hn : n ≠ 2) {x y : EuclideanSpace ℝ (Fin n)} (hx : ‖x‖ < 1) (hy : ‖y‖ < 1) (hxy : y ≠ x) : 0 < ballGreenKernel n x y

Outside dimension two, the Green kernel of the unit ball is positive inside the ball away from the pole.

theorem TauCeti.hasFDerivAt_ballGreenKernel {n : ℕ} (hn : n ≠ 2) {x y : EuclideanSpace ℝ (Fin n)} (hxy : y ≠ x) (h : 0 < ‖x‖ ^ 2 * ‖y‖ ^ 2 - 2 * inner ℝ x y + 1) : HasFDerivAt (ballGreenKernel n x) ((-(↑n * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * ‖y - x‖ ^ (-↑n)) • (innerSL ℝ) (y - x) - (-(↑n * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * (‖x‖ ^ 2 * ‖y‖ ^ 2 - 2 * inner ℝ x y + 1) ^ (-↑n / 2)) • (‖x‖ ^ 2 • (innerSL ℝ) y - (innerSL ℝ) x)) y

The Fréchet derivative of the Green kernel of the unit ball in y, away from the pole and wherever the reflection polynomial ‖x‖² ‖y‖² - 2 ⟪x, y⟫ + 1 is positive.

The Poisson kernel

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

The Poisson kernel of the Euclidean unit ball,

K(x, y) = (1 - ‖x‖²) / (n ωₙ ‖x - y‖ⁿ),

for x in the ball and y on the unit sphere; ωₙ is the volume of the unit ball. It is the negative outward normal derivative of the Green kernel ballGreenKernel n x on the sphere.

Equations

• TauCeti.ballPoissonKernel n x y = (1 - ‖x‖ ^ 2) / (↑n * MeasureTheory.volume.real (Metric.ball 0 1) * ‖x - y‖ ^ n)

theorem TauCeti.ballPoissonKernel_def {n : ℕ} (x y : EuclideanSpace ℝ (Fin n)) : ballPoissonKernel n x y = (1 - ‖x‖ ^ 2) / (↑n * MeasureTheory.volume.real (Metric.ball 0 1) * ‖x - y‖ ^ n)

The defining formula for the Poisson kernel of the unit ball.

theorem TauCeti.ballPoissonKernel_pos {n : ℕ} {x y : EuclideanSpace ℝ (Fin n)} (hx : ‖x‖ < 1) (hxy : x ≠ y) : 0 < ballPoissonKernel n x y

The Poisson kernel of the unit ball is positive for a pole in the open ball and any other point.

theorem TauCeti.ballPoissonKernel_pos_on_sphere {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) (hx : ‖x‖ < 1) (y : ↑(Metric.sphere 0 1)) : 0 < ballPoissonKernel n x ↑y

The Poisson kernel with a pole in the open ball is positive on the unit sphere.

theorem TauCeti.continuous_ballPoissonKernel_on_sphere {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) (hx : ‖x‖ ≠ 1) : Continuous fun (y : ↑(Metric.sphere 0 1)) => ballPoissonKernel n x ↑y

The Poisson kernel is continuous as a function of the boundary point when its pole lies off the unit sphere.

theorem TauCeti.contDiffOn_ballPoissonKernel {n : ℕ} {k : WithTop ℕ∞} : ContDiffOn ℝ k (fun (p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)) => ballPoissonKernel n p.1 p.2) {p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) | p.1 ≠ p.2}

The Poisson kernel of the unit ball is smooth, jointly in the pole and the boundary variable, away from the diagonal.

theorem TauCeti.integrableOn_ballPoissonKernel {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) (hx : ‖x‖ ≠ 1) (s : Set ↑(Metric.sphere 0 1)) : MeasureTheory.IntegrableOn (fun (y : ↑(Metric.sphere 0 1)) => ballPoissonKernel n x ↑y) s MeasureTheory.volume.toSphere

The Poisson kernel is integrable over any subset of the sphere when its pole lies off the sphere.

theorem TauCeti.harmonicAt_ballPoissonKernel_left {n : ℕ} {x y : EuclideanSpace ℝ (Fin n)} (hy : ‖y‖ = 1) (hxy : x ≠ y) : InnerProductSpace.HarmonicAt (fun (z : EuclideanSpace ℝ (Fin n)) => ballPoissonKernel n z y) x

For a point y of the unit sphere, the Poisson kernel x ↦ K(x, y) is harmonic in its pole x away from y, in particular throughout the open unit ball.

theorem TauCeti.harmonicOnNhd_ballPoissonKernel_left {n : ℕ} {y : EuclideanSpace ℝ (Fin n)} (hy : ‖y‖ = 1) : InnerProductSpace.HarmonicOnNhd (fun (z : EuclideanSpace ℝ (Fin n)) => ballPoissonKernel n z y) {y}ᶜ

For a point y of the unit sphere, the Poisson kernel x ↦ K(x, y) is harmonic on the complement of {y}.

theorem TauCeti.fderiv_ballGreenKernel_normal {n : ℕ} (hn : n ≠ 2) {x y : EuclideanSpace ℝ (Fin n)} (hx : ‖x‖ ≠ 1) (hy : ‖y‖ = 1) : (fderiv ℝ (ballGreenKernel n x) y) y = -ballPoissonKernel n x y

The Poisson kernel is the normal derivative of the Green kernel. On the unit sphere, the derivative of the Green kernel with pole x off the sphere, taken in the direction of the outward unit normal y, is the negative of the Poisson kernel.

theorem TauCeti.hasDerivAt_ballGreenKernel_radial {n : ℕ} (hn : n ≠ 2) {x y : EuclideanSpace ℝ (Fin n)} (hx : ‖x‖ ≠ 1) (hy : ‖y‖ = 1) : HasDerivAt (fun (t : ℝ) => ballGreenKernel n x (t • y)) (-ballPoissonKernel n x y) 1

The radial derivative of the Green kernel of the unit ball at a boundary point y, along the ray from the center through y, is the negative of the Poisson kernel.