Planar Poisson kernels and the Euclidean ball kernel

The outward radial derivative of the Dirichlet Green kernel on a planar disk is the negative of Mathlib's Poisson kernel, divided by 2π, when the radius is parametrized from zero to one. This identifies the boundary term in Green's representation formula with the existing Poisson kernel, both on the unit disk and after translation and dilation.

The file also reconciles the two-dimensional specialization of the Euclidean-ball Poisson kernel with Mathlib's complex kernel. Consequently its circle average is normalized at every pole in the disk, and it gives the Poisson representation of harmonic functions with respect to arc length on the unit circle.

The normalization follows Evans, Partial Differential Equations, Chapter 2, §2.2.

theorem TauCeti.hasDerivAt_planarGreenKernel_radial {a z : ℂ} (ha : ‖a‖ < 1) (hz : ‖z‖ = 1) : HasDerivAt (fun (t : ℝ) => planarGreenKernel a (t • z)) (-poissonKernel 0 a z / (2 * Real.pi)) 1

On the boundary of the unit disk, the outward radial derivative of the Green kernel with pole a is the negative of the Poisson kernel divided by 2π.

@[simp]

theorem TauCeti.fderiv_planarGreenKernel_normal {a z : ℂ} (ha : ‖a‖ < 1) (hz : ‖z‖ = 1) : (fderiv ℝ (planarGreenKernel a) z) z = -poissonKernel 0 a z / (2 * Real.pi)

The spatial derivative of the unit-disk Green kernel on the outward unit normal equals the negative Poisson kernel divided by 2π.

theorem TauCeti.hasDerivAt_planarGreenKernelDisk_radial {c a z : ℂ} {R : ℝ} (hR : 0 < R) (ha : ‖a - c‖ < R) (hz : ‖z - c‖ = R) : HasDerivAt (fun (t : ℝ) => planarGreenKernelDisk c R a (c + t • (z - c))) (-poissonKernel c a z / (2 * Real.pi)) 1

On the boundary of any positive-radius disk, the derivative of the Green kernel along the radius from the center to the boundary point is the negative of Mathlib's Poisson kernel divided by 2π. The derivative uses the dimensionless radial parameter t; the unit outward normal derivative is obtained by dividing by the disk radius.

@[simp]

theorem TauCeti.fderiv_planarGreenKernelDisk_normal {c a z : ℂ} {R : ℝ} (hR : 0 < R) (ha : ‖a - c‖ < R) (hz : ‖z - c‖ = R) : (fderiv ℝ (planarGreenKernelDisk c R a) z) ((↑R)⁻¹ * (z - c)) = -poissonKernel c a z / (2 * Real.pi * R)

The spatial derivative of the disk Green kernel on the outward unit normal is the negative Poisson kernel divided by 2πR.

Compatibility with the Euclidean-ball Poisson kernel

theorem TauCeti.ballPoissonKernel_two_repr {a z : ℂ} (hz : ‖z‖ = 1) : 2 * Real.pi * ballPoissonKernel 2 (Complex.orthonormalBasisOneI.repr a) (Complex.orthonormalBasisOneI.repr z) = poissonKernel 0 a z

In two dimensions, the Euclidean-ball Poisson kernel, transported along the standard orthonormal coordinates of ℂ, is Mathlib's Poisson kernel divided by the circumference 2π of the unit circle.

theorem TauCeti.circleAverage_ballPoissonKernel_two_fun_smul_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℂ → E) {a : ℂ} : Real.circleAverage (fun (z : ℂ) => ballPoissonKernel 2 (Complex.orthonormalBasisOneI.repr a) (Complex.orthonormalBasisOneI.repr z) • f z) 0 1 = (2 * Real.pi)⁻¹ • Real.circleAverage (fun (z : ℂ) => poissonKernel 0 a z • f z) 0 1

Scaling by the two-dimensional ball Poisson kernel under circleAverage is (2π)⁻¹ times scaling by Mathlib's Poisson kernel. This form applies to arbitrary vector-valued boundary data; no harmonicity or integrability hypothesis is needed for the identity.

theorem TauCeti.circleAverage_ballPoissonKernel_two_fun_mul {f : ℂ → ℝ} {a : ℂ} (hf : InnerProductSpace.HarmonicContOnCl f (Metric.ball 0 1)) (ha : ‖a‖ < 1) : Real.circleAverage (fun (z : ℂ) => ballPoissonKernel 2 (Complex.orthonormalBasisOneI.repr a) (Complex.orthonormalBasisOneI.repr z) * f z) 0 1 = (2 * Real.pi)⁻¹ * f a

The two-dimensional ball Poisson kernel represents a function harmonic on the open unit disk and continuous on its closure by integration against arc length on the unit circle. Since circleAverage is normalized by 2π, the right side carries the reciprocal factor.

theorem TauCeti.circleAverage_ballPoissonKernel_two {a : ℂ} (ha : ‖a‖ < 1) : Real.circleAverage (fun (z : ℂ) => ballPoissonKernel 2 (Complex.orthonormalBasisOneI.repr a) (Complex.orthonormalBasisOneI.repr z)) 0 1 = (2 * Real.pi)⁻¹

The circle average of the two-dimensional ball Poisson kernel is (2π)⁻¹; equivalently, its integral against arc length on the unit circle is one.