Existence for the Dirichlet problem on a disk

For continuous boundary data f on the circle sphere c R, the Schwarz integral

schwarzIntegral f c R w = ⨍ z, herglotzRieszKernel c w z * f z

is holomorphic in w on ball c R; its real part is the Poisson integral of f, which tends to f ζ₀ as w → ζ₀ ∈ sphere c R (positive kernel, unit mass, approximate identity). Together: exists_harmonic_extension, the solution of the Dirichlet problem (Anghel–Stan "Poisson integral formula"; Rainer/Forster Theorem 22.3; Hubbard's use in §1.2).

Mathlib anchors (pinned commit 905b9581):

• herglotzRieszKernel, poissonKernel, poissonKernel_eq_re_herglotzRieszKernel, re_herglotzRieszKernel_le, le_re_herglotzRieszKernel (Mathlib/Analysis/Complex/Poisson.lean); conventions: in poissonKernel c w z, w is the interior point, z the circle variable.
• DiffContOnCl.circleAverage_poissonKernel_smul: for f holomorphic on the ball and continuous up to the closure, ⨍ z, poissonKernel c w z • f z = f w — applied to f = 1 this gives the unit-mass identity.
• Real.circleAverage API (Mathlib/MeasureTheory/Integral/CircleAverage.lean), circleMap, intervalIntegral differentiation under the integral (intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_deriv_le).
• AnalyticAt.harmonicAt_re, InnerProductSpace.HarmonicAt (Mathlib/Analysis/InnerProductSpace/Harmonic/, Mathlib/Analysis/Complex/Harmonic/).

noncomputable def Rado.schwarzIntegral (f : ℂ → ℝ) (c : ℂ) (R : ℝ) (w : ℂ) : ℂ

The Schwarz integral of boundary data f on sphere c R, evaluated at the interior point w.

Equations

• Rado.schwarzIntegral f c R w = Real.circleAverage (fun (z : ℂ) => herglotzRieszKernel c w z * ↑(f z)) c R

theorem Rado.poissonKernel_pos {c w z : ℂ} {R : ℝ} (hw : w ∈ Metric.ball c R) (hz : z ∈ Metric.sphere c R) : 0 < poissonKernel c w z

Positivity of the Poisson kernel for interior w, boundary z.

theorem Rado.poissonKernel_continuousOn_sphere {c w : ℂ} {R : ℝ} (hw : w ∈ Metric.ball c R) : ContinuousOn (poissonKernel c w) (Metric.sphere c R)

The Poisson kernel is continuous on the circle, for a fixed interior point.

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

Unit mass of the Poisson kernel.

theorem Rado.eventually_poissonKernel_le_of_dist {c : ℂ} {R : ℝ} {ζ₀ : ℂ} (hζ₀ : ζ₀ ∈ Metric.sphere c R) (hR : 0 < R) {δ ε : ℝ} (hδ : 0 < δ) (hε : 0 < ε) : ∀ᶠ (w : ℂ) in nhdsWithin ζ₀ (Metric.ball c R), ∀ z ∈ Metric.sphere c R, δ ≤ dist z ζ₀ → poissonKernel c w z ≤ ε

Uniform smallness of the Poisson kernel away from the boundary singularity: for z at distance ≥ δ from ζ₀ ∈ sphere c R, the kernel at z becomes uniformly ≤ ε as the interior point w approaches ζ₀.

theorem Rado.schwarzIntegral_differentiableOn {f : ℂ → ℝ} {c : ℂ} {R : ℝ} (hR : 0 < R) (hf : ContinuousOn f (Metric.sphere c R)) : DifferentiableOn ℂ (schwarzIntegral f c R) (Metric.ball c R)

The Schwarz integral is holomorphic in the interior variable (differentiation under the integral).

theorem Rado.re_schwarzIntegral {f : ℂ → ℝ} {c : ℂ} {R : ℝ} {w : ℂ} (hR : 0 < R) (hf : ContinuousOn f (Metric.sphere c R)) (hw : w ∈ Metric.ball c R) : (schwarzIntegral f c R w).re = Real.circleAverage (fun (z : ℂ) => poissonKernel c w z • f z) c R

The real part of the Schwarz integral is the Poisson integral.

theorem Rado.tendsto_re_schwarzIntegral {f : ℂ → ℝ} {c : ℂ} {R : ℝ} (hR : 0 < R) (hf : ContinuousOn f (Metric.sphere c R)) {ζ₀ : ℂ} (hζ₀ : ζ₀ ∈ Metric.sphere c R) : Filter.Tendsto (fun (w : ℂ) => (schwarzIntegral f c R w).re) (nhdsWithin ζ₀ (Metric.ball c R)) (nhds (f ζ₀))

Boundary attainment: the Poisson integral of continuous boundary data tends to the data at each boundary point (approximate-identity argument, using positivity, unit mass and off-singularity smallness of the kernel).

theorem Rado.exists_harmonic_extension {c : ℂ} {R : ℝ} (hR : 0 < R) {f : ℂ → ℝ} (hf : ContinuousOn f (Metric.sphere c R)) : ∃ (u : ℂ → ℝ), ContinuousOn u (Metric.closedBall c R) ∧ InnerProductSpace.HarmonicOnNhd u (Metric.ball c R) ∧ Set.EqOn u f (Metric.sphere c R)

Solution of the Dirichlet problem on a disk. Every continuous function on a circle extends to a function continuous on the closed disk and harmonic inside.