The Dirichlet problem on a disk

The deepest ℂ-level analytic input to Radó's theorem: for continuous boundary data f on a circle, the Poisson/Schwarz integral produces a function that is harmonic inside the disk, continuous up to the boundary, with boundary values f. Mathlib's pinned version already provides the kernels (herglotzRieszKernel, poissonKernel in Mathlib/Analysis/Complex/Poisson.lean, with two-sided bounds) and the representation of an already harmonic function by its Poisson integral (Mathlib/Analysis/Complex/Harmonic/Poisson.lean); what is missing is the solution of the Dirichlet problem for arbitrary continuous boundary data: existence is proved in Rado/Complex/Poisson.lean (exists_harmonic_extension). The pooled LeanComplexAnalysis results poisson_integral_of_harmonicOn_unitDisc_continuousOn_closedUnitDisc and poisson_integral_of_harmonicOn_disc_continuousOn_closedDisc likewise assume an existing harmonic function and prove its representation; they do not construct a harmonic extension from arbitrary boundary data. This file packages that complementary existence result and derives the characterizations used by Perron's method:

• poissonExtension — a choice function packaging the solution, with API.
• harmonicOnNhd_iff_meanEqOn — harmonic ↔ continuous + mean-value property, on open sets (uniqueness direction via the comparison principle).
• HarmonicOnNhd.comp_analytic — harmonicity is preserved under holomorphic precomposition (via Re-of-holomorphic, both directions in Mathlib).
• SubMeanOn.le_poissonExtension_on — the comparison characterization of subharmonicity (Anghel–Stan Proposition 3, D1 ⇒ D3).

Here "harmonic" is Mathlib's InnerProductSpace.HarmonicOnNhd.

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

The solution of the Dirichlet problem on closedBall c R with boundary data f, extended by junk values off the closed disk and for illegal parameters.

Equations

• Rado.poissonExtension f c R = if h : 0 < R ∧ ContinuousOn f (Metric.sphere c R) then fun (z : ℂ) => if z ∈ Metric.closedBall c R then ⋯.choose z else f z else f

theorem Rado.poissonExtension_continuousOn {c : ℂ} {R : ℝ} {f : ℂ → ℝ} (hR : 0 < R) (hf : ContinuousOn f (Metric.sphere c R)) : ContinuousOn (poissonExtension f c R) (Metric.closedBall c R)

theorem Rado.poissonExtension_harmonicOnNhd {c : ℂ} {R : ℝ} {f : ℂ → ℝ} (hR : 0 < R) (hf : ContinuousOn f (Metric.sphere c R)) : InnerProductSpace.HarmonicOnNhd (poissonExtension f c R) (Metric.ball c R)

theorem Rado.poissonExtension_eqOn_sphere {c : ℂ} {R : ℝ} {f : ℂ → ℝ} (hR : 0 < R) (hf : ContinuousOn f (Metric.sphere c R)) : Set.EqOn (poissonExtension f c R) f (Metric.sphere c R)

theorem Rado.poissonExtension_eqOn_compl {c : ℂ} {R : ℝ} {f : ℂ → ℝ} (hR : 0 < R) (hf : ContinuousOn f (Metric.sphere c R)) : Set.EqOn (poissonExtension f c R) f (Metric.closedBall c R)ᶜ

theorem Rado.poissonExtension_mem_Icc {c : ℂ} {R : ℝ} {f : ℂ → ℝ} (hR : 0 < R) (hf : ContinuousOn f (Metric.sphere c R)) {m M : ℝ} (hfm : ∀ z ∈ Metric.sphere c R, f z ∈ Set.Icc m M) (z : ℂ) : z ∈ Metric.closedBall c R → poissonExtension f c R z ∈ Set.Icc m M

The Poisson extension takes values in any closed interval containing the boundary data (maximum principle packaging).

theorem Rado.HarmonicOnNhd.meanEqOn {u : ℂ → ℝ} {s : Set ℂ} (hu : InnerProductSpace.HarmonicOnNhd u s) : MeanEqOn u s

Harmonic functions satisfy the mean-value property on open sets.

theorem Rado.MeanEqOn.harmonicOnNhd {u : ℂ → ℝ} {s : Set ℂ} (hs : IsOpen s) (hu : MeanEqOn u s) : InnerProductSpace.HarmonicOnNhd u s

Continuous functions with the mean-value property on an open set are harmonic (Dirichlet uniqueness).

theorem Rado.HarmonicOnNhd.comp_analytic {u : ℂ → ℝ} {t : Set ℂ} (hu : InnerProductSpace.HarmonicOnNhd u t) (ht : IsOpen t) {φ : ℂ → ℂ} {s : Set ℂ} (hφ : AnalyticOnNhd ℂ φ s) (hmaps : Set.MapsTo φ s t) : InnerProductSpace.HarmonicOnNhd (u ∘ φ) s

Harmonicity is preserved by holomorphic precomposition.

theorem Rado.SubMeanOn.le_poissonExtension_on {g : ℂ → ℝ} {s : Set ℂ} (hg : SubMeanOn g s) {c : ℂ} {R : ℝ} (hR : 0 < R) (hsub : Metric.closedBall c R ⊆ s) (x : ℂ) : x ∈ Metric.closedBall c R → g x ≤ poissonExtension g c R x

Comparison characterization of subharmonicity (Anghel–Stan Prop. 3, D1 ⇒ D3): a sub-mean-value function is dominated on every closed disk by the Poisson extension of its own boundary values.