Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

The Dirichlet problem for harmonic functions

Let U ⊆ ℝᵈ be a bounded open set satisfying a uniform exterior sphere condition, for instance a bounded C² domain (uniformExteriorSphere_of_contDiff_levelSet). For Lipschitz data g there is a classical harmonic function h ∈ C(Ū) ∩ C²(U) with h = g on ∂U, and the boundary modulus of continuity depends only on U and the Lipschitz constant.

The proof is an application of the CIL Perron method:

1. exterior-sphere barriers (exists_laplace_barrierPair_of_uniformExteriorSphereSq) give a Dirichlet barrier pair with a Hölder-1/2 boundary modulus;
2. the Perron theorem with the Laplace comparison principle (exists_laplace_dirichlet_of_barrierPair) gives a viscosity solution that is continuous on Ū and attains g;
3. a continuous viscosity solution of -Δu = 0 is weakly harmonic (integral_lapTrace_mul_eq_zero_of_viscositySolution_laplace), hence smooth and classically harmonic by Weyl's lemma (Analysis.weyl_of_weaklyHarmonicOn).

The modulus is ϖ t = K √t.

theorem ViscositySolns.dirichlet_harmonic_modulus_of_uniformExteriorSphere {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hext : UniformExteriorSphere U) (L : NNReal) : ∃ (ϖ : ℝ → ℝ), Filter.Tendsto ϖ (nhdsWithin 0 (Set.Ici 0)) (nhds 0) ∧ ∀ (g : EuclideanSpace ℝ (Fin d) → ℝ), LipschitzOnWith L g (closure U) → ∃ (h : EuclideanSpace ℝ (Fin d) → ℝ), ContinuousOn h (closure U) ∧ ContDiffOn ℝ 2 h U ∧ (∀ x ∈ U, Laplacian.laplacian h x = 0) ∧ (∀ x ∈ frontier U, h x = g x) ∧ ∀ x₀ ∈ frontier U, ∀ x ∈ closure U, |h x - g x₀| ≤ ϖ ‖x - x₀‖

Existence for the harmonic Dirichlet problem on a bounded open set with a uniform exterior sphere condition, with a boundary modulus of continuity that is uniform over Lipschitz data with a fixed constant. No size bound on the data is needed.