Boundary concentration of the Poisson kernel of the ball

For a point approaching the unit sphere from inside the ball, the Poisson kernel has vanishing integral on every part of the sphere a fixed positive distance from that point. This is the concentration estimate needed to recover continuous boundary data from the Poisson integral, once its total mass is known to be one.

The estimate is the elementary far-field half of the approximate-identity argument in L. C. Evans, Partial Differential Equations, Section 2.2.4.

theorem TauCeti.ballPoissonKernel_le_of_dist_le_half_of_le_dist {n : ℕ} {x z : EuclideanSpace ℝ (Fin n)} {delta : ℝ} (hdelta : 0 < delta) (hx : ‖x‖ ≤ 1) (hnear : dist x z ≤ delta / 2) {y : EuclideanSpace ℝ (Fin n)} (hfar : delta ≤ dist y z) : ballPoissonKernel n x y ≤ (1 - ‖x‖ ^ 2) / (↑n * MeasureTheory.volume.real (Metric.ball 0 1) * (delta / 2) ^ n)

Far from a boundary point z, the Poisson kernel is bounded by its vanishing numerator divided by a denominator depending only on the separation distance.

theorem TauCeti.tendsto_setIntegral_ballPoissonKernel_mul_away {n : ℕ} (f : ↑(Metric.sphere 0 1) → ℝ) {z : EuclideanSpace ℝ (Fin n)} (hz : ‖z‖ = 1) {delta : ℝ} (hdelta : 0 < delta) (hf : MeasureTheory.IntegrableOn f {y : ↑(Metric.sphere 0 1) | delta ≤ dist (↑y) z} MeasureTheory.volume.toSphere) : Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => ∫ (y : ↑(Metric.sphere 0 1)) in {y : ↑(Metric.sphere 0 1) | delta ≤ dist (↑y) z}, ballPoissonKernel n x ↑y * f y ∂MeasureTheory.volume.toSphere) (nhdsWithin z (Metric.ball 0 1)) (nhds 0)

The contribution of integrable boundary data from a fixed positive distance away from z vanishes in the Poisson integral as the pole approaches z from inside the ball.

theorem TauCeti.tendsto_setIntegral_ballPoissonKernel_away {n : ℕ} {z : EuclideanSpace ℝ (Fin n)} (hz : ‖z‖ = 1) {delta : ℝ} (hdelta : 0 < delta) : Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => ∫ (y : ↑(Metric.sphere 0 1)) in {y : ↑(Metric.sphere 0 1) | delta ≤ dist (↑y) z}, ballPoissonKernel n x ↑y ∂MeasureTheory.volume.toSphere) (nhdsWithin z (Metric.ball 0 1)) (nhds 0)

The mass of the unit-ball Poisson kernel outside a fixed boundary neighbourhood vanishes as the pole approaches the boundary point through the open ball.

theorem TauCeti.tendsto_setIntegral_ballPoissonKernel_mul_away_of_continuous {n : ℕ} (f : ↑(Metric.sphere 0 1) → ℝ) (hf : Continuous f) {z : EuclideanSpace ℝ (Fin n)} (hz : ‖z‖ = 1) {delta : ℝ} (hdelta : 0 < delta) : Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => ∫ (y : ↑(Metric.sphere 0 1)) in {y : ↑(Metric.sphere 0 1) | delta ≤ dist (↑y) z}, ballPoissonKernel n x ↑y * f y ∂MeasureTheory.volume.toSphere) (nhdsWithin z (Metric.ball 0 1)) (nhds 0)

The far-field Poisson integral of continuous boundary data vanishes as the pole approaches the boundary point through the open ball.