The Green kernel of a Euclidean half-space

The method of images gives a Dirichlet Green kernel for the half-space on the positive side of a hyperplane. Reflect the pole through the hyperplane and subtract its Newtonian kernel. The reflected pole lies outside the half-space, so the correction is harmonic inside, while the two kernels agree on the boundary. The construction works for any unit normal vector. In dimension n = 2, the underlying newtonianKernel is degenerate; the Green-kernel interpretation here is for n = 1 or n ≥ 3.

The normalization follows Evans, Partial Differential Equations, Section 2.2.4.

noncomputable def TauCeti.halfSpaceGreenKernel (n : ℕ) (v : { w : EuclideanSpace ℝ (Fin n) // ‖w‖ = 1 }) (x y : EuclideanSpace ℝ (Fin n)) : ℝ

The method-of-images Dirichlet Green kernel for the half-space with unit inward normal v, evaluated at the pole x and variable y. The Newtonian normalization gives a genuine Green kernel for n = 1 or n ≥ 3; at n = 2 the Newtonian kernel is degenerate.

Equations

• TauCeti.halfSpaceGreenKernel n v x y = TauCeti.newtonianKernel n (y - x) - TauCeti.newtonianKernel n (y - (ℝ ∙ ↑v)ᗮ.reflection x)

theorem TauCeti.halfSpaceGreenKernel_def {n : ℕ} (v : { w : EuclideanSpace ℝ (Fin n) // ‖w‖ = 1 }) (x y : EuclideanSpace ℝ (Fin n)) : halfSpaceGreenKernel n v x y = newtonianKernel n (y - x) - newtonianKernel n (y - (ℝ ∙ ↑v)ᗮ.reflection x)

The method-of-images formula for the half-space Green kernel.

theorem TauCeti.halfSpaceGreenKernel_comm {n : ℕ} (v : { w : EuclideanSpace ℝ (Fin n) // ‖w‖ = 1 }) (x y : EuclideanSpace ℝ (Fin n)) : halfSpaceGreenKernel n v x y = halfSpaceGreenKernel n v y x

The image Green kernel is symmetric in its pole and variable.

@[simp]

theorem TauCeti.halfSpaceGreenKernel_eq_zero_of_inner_eq_zero_right {n : ℕ} {v : { w : EuclideanSpace ℝ (Fin n) // ‖w‖ = 1 }} (x : EuclideanSpace ℝ (Fin n)) {y : EuclideanSpace ℝ (Fin n)} (hy : inner ℝ (↑v) y = 0) : halfSpaceGreenKernel n v x y = 0

The Green kernel vanishes when its variable is on the bounding hyperplane.

@[simp]

theorem TauCeti.halfSpaceGreenKernel_eq_zero_of_inner_eq_zero_left {n : ℕ} {v : { w : EuclideanSpace ℝ (Fin n) // ‖w‖ = 1 }} {x : EuclideanSpace ℝ (Fin n)} (hx : inner ℝ (↑v) x = 0) (y : EuclideanSpace ℝ (Fin n)) : halfSpaceGreenKernel n v x y = 0

The Green kernel also vanishes when its pole lies on the bounding hyperplane.

theorem TauCeti.halfSpaceGreenKernel_pos {n : ℕ} (hn : n ≠ 2) {v : { w : EuclideanSpace ℝ (Fin n) // ‖w‖ = 1 }} {x y : EuclideanSpace ℝ (Fin n)} (hx : 0 < inner ℝ (↑v) x) (hy : 0 < inner ℝ (↑v) y) (hxy : y ≠ x) : 0 < halfSpaceGreenKernel n v x y

Outside dimension two, the half-space Green kernel is positive at distinct interior points.

theorem TauCeti.harmonicAt_halfSpaceGreenKernel {n : ℕ} {v : { w : EuclideanSpace ℝ (Fin n) // ‖w‖ = 1 }} {x y : EuclideanSpace ℝ (Fin n)} (hxy : y ≠ x) (hxy' : y ≠ (ℝ ∙ ↑v)ᗮ.reflection x) : InnerProductSpace.HarmonicAt (halfSpaceGreenKernel n v x) y

The Green kernel is harmonic away from its pole and the reflected pole.

theorem TauCeti.harmonicOnNhd_halfSpaceGreenKernel {n : ℕ} {v : { w : EuclideanSpace ℝ (Fin n) // ‖w‖ = 1 }} {x : EuclideanSpace ℝ (Fin n)} (hx : 0 < inner ℝ (↑v) x) : InnerProductSpace.HarmonicOnNhd (halfSpaceGreenKernel n v x) ({y : EuclideanSpace ℝ (Fin n) | 0 < inner ℝ (↑v) y} \ {x})

The Green kernel is harmonic throughout the punctured positive half-space.

theorem TauCeti.harmonicAt_halfSpaceGreenKernel_left {n : ℕ} {v : { w : EuclideanSpace ℝ (Fin n) // ‖w‖ = 1 }} {x y : EuclideanSpace ℝ (Fin n)} (hxy : x ≠ y) (hxy' : x ≠ (ℝ ∙ ↑v)ᗮ.reflection y) : InnerProductSpace.HarmonicAt (fun (z : EuclideanSpace ℝ (Fin n)) => halfSpaceGreenKernel n v z y) x

The Green kernel is harmonic in its pole away from the variable point and its reflection.

noncomputable def TauCeti.halfSpacePoissonKernel (n : ℕ) (v : { w : EuclideanSpace ℝ (Fin n) // ‖w‖ = 1 }) (x y : EuclideanSpace ℝ (Fin n)) : ℝ

The Poisson kernel for the half-space with unit inward normal v. Its boundary normalization is 2 ⟪v,x⟫ / (n ωₙ ‖y-x‖ⁿ), where ωₙ is the volume of the unit ball.

Equations

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

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

The defining formula for the half-space Poisson kernel.

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

The usual quotient form of the half-space Poisson kernel.

theorem TauCeti.halfSpacePoissonKernel_pos {n : ℕ} {v : { w : EuclideanSpace ℝ (Fin n) // ‖w‖ = 1 }} {x y : EuclideanSpace ℝ (Fin n)} (hx : 0 < inner ℝ (↑v) x) (hxy : y ≠ x) : 0 < halfSpacePoissonKernel n v x y

The half-space Poisson kernel is positive for an interior pole and a distinct point.

theorem TauCeti.hasFDerivAt_halfSpaceGreenKernel {n : ℕ} (hn : n ≠ 2) {v : { w : EuclideanSpace ℝ (Fin n) // ‖w‖ = 1 }} {x y : EuclideanSpace ℝ (Fin n)} (hxy : y ≠ x) (hyref : y ≠ (ℝ ∙ ↑v)ᗮ.reflection x) : HasFDerivAt (halfSpaceGreenKernel n v x) ((-(↑n * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * ‖y - x‖ ^ (-↑n)) • (innerSL ℝ) (y - x) - (-(↑n * MeasureTheory.volume.real (Metric.ball 0 1))⁻¹ * ‖y - (ℝ ∙ ↑v)ᗮ.reflection x‖ ^ (-↑n)) • (innerSL ℝ) (y - (ℝ ∙ ↑v)ᗮ.reflection x)) y

The Fréchet derivative of the half-space Green kernel away from its two poles.

theorem TauCeti.fderiv_halfSpaceGreenKernel_normal {n : ℕ} (hn : n ≠ 2) {v : { w : EuclideanSpace ℝ (Fin n) // ‖w‖ = 1 }} {x y : EuclideanSpace ℝ (Fin n)} (hxy : y ≠ x) (hy : inner ℝ (↑v) y = 0) : (fderiv ℝ (halfSpaceGreenKernel n v x) y) (-↑v) = -halfSpacePoissonKernel n v x y

On the boundary, the derivative in the negative normal direction of the Green kernel is the negative Poisson kernel.