Documentation

TauCeti.Analysis.PDE.GreenFunction.Planar

The Green kernel of the planar unit disk #

This file constructs the Dirichlet Green kernel of the complex unit disk from the logarithmic Newtonian kernel. For a pole a in the disk, the reflected logarithmic term has no singularity in the disk. Subtracting it from the Newtonian kernel gives a function harmonic away from a and zero on the unit circle.

The kernel is the basic ingredient for representing solutions of the planar Dirichlet problem by Green potentials. Its normalization agrees with planarNewtonianKernel, hence with the negative-Laplacian convention used by the fundamental-solution development.

The construction is the standard method-of-images formula; see Evans, Partial Differential Equations, Chapter 2, Section 2.2.

Main declarations #

source
noncomputable def TauCeti.planarGreenKernel (a z : ℂ) :
ℝ

The Dirichlet Green kernel of the complex unit disk, with pole a.

For ‖a‖ < 1, the second term is harmonic throughout the disk. Thus the first term supplies the Newtonian singularity at a, while the difference vanishes on the unit circle.

Equations
Instances For
    source
    theorem TauCeti.planarGreenKernel_def (a z : ℂ) :
    planarGreenKernel a z = planarNewtonianKernel (z - a) - planarNewtonianKernel (1 - (starRingEnd ℂ) a * z)

    The defining formula for the planar Green kernel.

    source
    theorem TauCeti.differentiableAt_planarGreenKernel {a z : ℂ} (hza : z - a ≠ 0) (hca : 1 - (starRingEnd ℂ) a * z ≠ 0) :
    DifferentiableAt ℝ (planarGreenKernel a) z

    The planar Green kernel is differentiable wherever neither of its logarithmic arguments vanishes.

    source
    theorem TauCeti.differentiableAt_planarGreenKernel_boundary {a z : ℂ} (ha : ‖a‖ < 1) (hz : ‖z‖ = 1) :
    DifferentiableAt ℝ (planarGreenKernel a) z

    The planar Green kernel is differentiable at a boundary point of the unit disk when its pole lies inside the disk.

    source
    theorem TauCeti.harmonicAt_planarGreenKernel {a z : ℂ} (ha : ‖a‖ < 1) (hz : ‖z‖ < 1) (hza : z ≠ a) :
    InnerProductSpace.HarmonicAt (planarGreenKernel a) z

    Away from its pole, the planar Green kernel is harmonic inside the unit disk.

    source
    theorem TauCeti.harmonicAt_planarGreenKernel_sub_newtonianKernel {a z : ℂ} (ha : ‖a‖ < 1) (hz : ‖z‖ < 1) :
    InnerProductSpace.HarmonicAt (fun (w : ℂ) => planarGreenKernel a w - planarNewtonianKernel (w - a)) z

    The difference between the planar Green kernel and its Newtonian singular term is harmonic throughout the unit disk.

    source
    theorem TauCeti.planarGreenKernel_pos {a z : ℂ} (ha : ‖a‖ < 1) (hz : ‖z‖ < 1) (hza : z ≠ a) :
    0 < planarGreenKernel a z

    Away from its pole, the planar Green kernel is positive inside the unit disk.

    source
    @[simp]
    theorem TauCeti.planarGreenKernel_eq_zero_of_norm_eq_one {a z : ℂ} (hz : ‖z‖ = 1) :
    planarGreenKernel a z = 0

    The planar Green kernel satisfies the homogeneous Dirichlet boundary condition on the unit circle.