The planar Green kernel on a disk

Translation and dilation carry the Green kernel of the complex unit disk to any disk of positive radius. The resulting kernel is harmonic away from its pole, positive in the disk, and zero on its boundary. Its singular part is the scaled planar Newtonian kernel; the difference is harmonic throughout the disk. These properties allow the kernel to be used in Green-potential representations on balls with arbitrary center and radius.

The normalization follows the standard method-of-images formula in Evans, Partial Differential Equations, Chapter 2, Section 2.2.

noncomputable def TauCeti.planarGreenKernelDisk (c : ℂ) (R : ℝ) (a z : ℂ) : ℝ

The Dirichlet Green kernel of the disk Metric.ball c R, obtained from the unit-disk kernel by the similarity z ↦ R⁻¹ • (z - c). The parameter R is intended to be positive.

Equations

• TauCeti.planarGreenKernelDisk c R a z = TauCeti.planarGreenKernel (R⁻¹ • (a - c)) (R⁻¹ • (z - c))

theorem TauCeti.planarGreenKernelDisk_def (c : ℂ) (R : ℝ) (a z : ℂ) : planarGreenKernelDisk c R a z = planarGreenKernel (R⁻¹ • (a - c)) (R⁻¹ • (z - c))

The disk kernel is the unit-disk kernel in normalized coordinates.

@[simp]

theorem TauCeti.planarGreenKernelDisk_zero_one (a z : ℂ) : planarGreenKernelDisk 0 1 a z = planarGreenKernel a z

The disk kernel specializes to the unit-disk kernel.

theorem TauCeti.harmonicAt_planarGreenKernelDisk {c a z : ℂ} {R : ℝ} (hR : 0 < R) (ha : ‖a - c‖ < R) (hz : ‖z - c‖ < R) (hza : z ≠ a) : InnerProductSpace.HarmonicAt (planarGreenKernelDisk c R a) z

The Green kernel is harmonic in the disk away from its pole.

@[simp]

theorem TauCeti.planarGreenKernelDisk_eq_zero_of_norm_sub_eq {c a z : ℂ} {R : ℝ} (hR : 0 < R) (hz : ‖z - c‖ = R) : planarGreenKernelDisk c R a z = 0

The Green kernel vanishes on the boundary circle of its disk.

theorem TauCeti.planarGreenKernelDisk_pos {c a z : ℂ} {R : ℝ} (hR : 0 < R) (ha : ‖a - c‖ < R) (hz : ‖z - c‖ < R) (hza : z ≠ a) : 0 < planarGreenKernelDisk c R a z

The Green kernel is strictly positive inside the disk away from its pole.

theorem TauCeti.harmonicAt_planarGreenKernelDisk_sub_newtonianKernel {c a z : ℂ} {R : ℝ} (hR : 0 < R) (ha : ‖a - c‖ < R) (hz : ‖z - c‖ < R) : InnerProductSpace.HarmonicAt (fun (w : ℂ) => planarGreenKernelDisk c R a w - planarNewtonianKernel (R⁻¹ • (w - a))) z

The difference between the disk Green kernel and its scaled Newtonian singularity is harmonic throughout the disk, including at the pole. The scale matters at the pole because the totalized logarithmic kernel has the assigned value zero there.

theorem TauCeti.differentiableAt_planarGreenKernelDisk_boundary {c a z : ℂ} {R : ℝ} (hR : 0 < R) (ha : ‖a - c‖ < R) (hz : ‖z - c‖ = R) : DifferentiableAt ℝ (planarGreenKernelDisk c R a) z

The Green kernel of a positive-radius disk is differentiable at a boundary point when its pole lies inside the disk.