Similarity invariance and pointwise estimates for the complex Poisson kernel

The Poisson kernel is unchanged when its center is translated to the origin and its arguments are multiplied by the inverse of a nonzero complex number. This normalized-coordinate identity transports formulas between centered unit disks and translated, rescaled disks, including the Green-kernel boundary derivative formula.

The file also collects elementary facts about the kernel on the circle: continuity in the boundary point, nonnegativity for poles inside the disk, and the far-field bound that drives recovery of boundary values by the Poisson integral.

theorem TauCeti.poissonKernel_inv_mul_sub {c a z q : ℂ} (hq : q ≠ 0) : poissonKernel 0 (q⁻¹ * (a - c)) (q⁻¹ * (z - c)) = poissonKernel c a z

Translating the center of the Poisson kernel to zero and multiplying by a nonzero complex number does not change its value.

theorem TauCeti.poissonKernel_nonneg_on_sphere {c w z : ℂ} {R : ℝ} (hw : w ∈ Metric.ball c |R|) (hz : z ∈ Metric.sphere c |R|) : 0 ≤ poissonKernel c w z

The Poisson kernel is nonnegative on a circle when its evaluation point lies inside.

theorem TauCeti.continuousOn_poissonKernel_sphere {c w : ℂ} {R : ℝ} (hw : w ∉ Metric.sphere c |R|) : ContinuousOn (poissonKernel c w) (Metric.sphere c |R|)

Off the circle, the Poisson kernel is continuous as a function of the boundary point.

theorem TauCeti.poissonKernel_le_of_le_dist {c w y : ℂ} {R d : ℝ} (hd : 0 < d) (hw : w ∈ Metric.closedBall c |R|) (hy : y ∈ Metric.sphere c |R|) (hdist : d ≤ dist w y) : poissonKernel c w y ≤ (R ^ 2 - ‖w - c‖ ^ 2) / d ^ 2

For a pole w in the closed disk and a boundary point y at distance at least d > 0 from w, the Poisson kernel is at most (R ^ 2 - ‖w - c‖ ^ 2) / d ^ 2. For fixed d this bound tends to zero as w approaches the circle.