The planar Poisson integral: harmonicity and boundary values

The Poisson average of integrable real boundary data is harmonic in the disk. For continuous boundary data, it converges to the prescribed value as the interior point approaches the boundary. Together these facts solve the planar Dirichlet problem on a disk.

The Poisson integral is the real part of Mathlib's analytic Herglotz–Riesz integral. See L. C. Evans, Partial Differential Equations, Section 2.2.4.

noncomputable def TauCeti.planarPoissonIntegral (g : ℂ → ℝ) (c : ℂ) (R : ℝ) (w : ℂ) : ℝ

The Poisson average of real boundary data on the circle of radius R centered at c. For integrable data it is harmonic at points off the circle.

Equations

• TauCeti.planarPoissonIntegral g c R w = Real.circleAverage (poissonKernel c w • g) c R

theorem TauCeti.planarPoissonIntegral_def (g : ℂ → ℝ) (c : ℂ) (R : ℝ) (w : ℂ) : planarPoissonIntegral g c R w = Real.circleAverage (poissonKernel c w • g) c R

The Poisson integral agrees with the usual circle average of the Poisson kernel times the boundary data.

@[simp]

theorem TauCeti.planarPoissonIntegral_zero (c : ℂ) (R : ℝ) (w : ℂ) : planarPoissonIntegral (fun (x : ℂ) => 0) c R w = 0

The Poisson integral of zero boundary data is zero.

theorem TauCeti.planarPoissonIntegral_add {g₁ g₂ : ℂ → ℝ} {c : ℂ} {R : ℝ} {w : ℂ} (hg₁ : CircleIntegrable g₁ c R) (hg₂ : CircleIntegrable g₂ c R) (hw : w ∉ Metric.sphere c |R|) : planarPoissonIntegral (g₁ + g₂) c R w = planarPoissonIntegral g₁ c R w + planarPoissonIntegral g₂ c R w

The Poisson integral is additive in circle-integrable boundary data away from the circle.

@[simp]

theorem TauCeti.planarPoissonIntegral_smul (a : ℝ) (g : ℂ → ℝ) (c : ℂ) (R : ℝ) (w : ℂ) : planarPoissonIntegral (a • g) c R w = a • planarPoissonIntegral g c R w

The Poisson integral commutes with real scalar multiplication.

theorem TauCeti.planarPoissonIntegral_congr_sphere {g₁ g₂ : ℂ → ℝ} {c : ℂ} {R : ℝ} {w : ℂ} (h : Set.EqOn g₁ g₂ (Metric.sphere c |R|)) : planarPoissonIntegral g₁ c R w = planarPoissonIntegral g₂ c R w

Boundary data agreeing on the circle have the same Poisson integral.

theorem TauCeti.harmonicOnNhd_planarPoissonIntegral {g : ℂ → ℝ} {c : ℂ} {R : ℝ} (hg : CircleIntegrable g c R) : InnerProductSpace.HarmonicOnNhd (planarPoissonIntegral g c R) (Metric.sphere c |R|)ᶜ

The planar Poisson integral of circle-integrable data is harmonic away from the circle, in particular throughout the open disk.

@[simp]

theorem TauCeti.planarPoissonIntegral_const {c : ℂ} {R : ℝ} {w : ℂ} (hw : w ∈ Metric.ball c |R|) (a : ℝ) : planarPoissonIntegral (fun (x : ℂ) => a) c R w = a

The Poisson integral preserves constant boundary data at every point inside the disk. In particular, the Poisson kernel has circle average one there.

@[simp]

theorem TauCeti.circleAverage_poissonKernel {c : ℂ} {R : ℝ} {w : ℂ} (hw : w ∈ Metric.ball c |R|) : Real.circleAverage (poissonKernel c w) c R = 1

The Poisson kernel has circle average one at every point inside the disk.

theorem TauCeti.planarPoissonIntegral_sub_const {g : ℂ → ℝ} {c : ℂ} {R : ℝ} {w : ℂ} (hg : CircleIntegrable g c R) (hw : w ∈ Metric.ball c |R|) (a : ℝ) : planarPoissonIntegral g c R w - a = Real.circleAverage (fun (y : ℂ) => poissonKernel c w y * (g y - a)) c R

Inside the disk, subtracting a constant from the Poisson integral subtracts it from the boundary data under the kernel.

theorem TauCeti.planarPoissonIntegral_mono {g₁ g₂ : ℂ → ℝ} {c : ℂ} {R : ℝ} {w : ℂ} (hg₁ : CircleIntegrable g₁ c R) (hg₂ : CircleIntegrable g₂ c R) (hw : w ∈ Metric.ball c |R|) (hle : ∀ z ∈ Metric.sphere c |R|, g₁ z ≤ g₂ z) : planarPoissonIntegral g₁ c R w ≤ planarPoissonIntegral g₂ c R w

The Poisson integral preserves order between circle-integrable boundary data in the disk.

theorem TauCeti.planarPoissonIntegral_nonneg {g : ℂ → ℝ} {c : ℂ} {R : ℝ} {w : ℂ} (hw : w ∈ Metric.ball c |R|) (hnonneg : ∀ z ∈ Metric.sphere c |R|, 0 ≤ g z) : 0 ≤ planarPoissonIntegral g c R w

Nonnegative boundary data have a nonnegative Poisson integral in the disk.

theorem TauCeti.tendsto_planarPoissonIntegral {g : ℂ → ℝ} {c z : ℂ} {R : ℝ} (hg : ContinuousOn g (Metric.sphere c |R|)) (hz : z ∈ Metric.sphere c |R|) : Filter.Tendsto (planarPoissonIntegral g c R) (nhdsWithin z (Metric.ball c |R|)) (nhds (g z))

The Poisson integral of continuous boundary data converges to the prescribed value when its argument approaches a boundary point through the open disk.