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

Perron barrier pairs for the Laplace operator

For a bounded open set C with a uniform exterior sphere condition and boundary data g that is L-Lipschitz on closure C for the Euclidean distance, we assemble a DirichletBarrierPair for -Δu = 0:

• the upper barrier is U_g = inf_{p ∈ P} (g x₀ + A Φ_p);
• the lower barrier is -U_{-g}, using that the Laplace operator equals its own negOperator.

Both barriers are continuous, attain the boundary data, and satisfy the Hölder-1/2 boundary modulus |B(x) - g(x₀)| ≤ K |x - x₀|^{1/2} with a constant K depending only on n, R, L and the diameter of C. When the frontier is empty we use the constant barriers 0.

theorem ViscositySolns.viscositySupersolution_laplaceOperator_const {n : ℕ} {C : Set (Point n)} (hCopen : IsOpen C) (a : ℝ) : ViscositySupersolution C laplaceOperator fun (x : Point n) => a

Constants are viscosity supersolutions of -Δu = 0 on open sets.

theorem ViscositySolns.viscositySubsolution_laplaceOperator_const {n : ℕ} {C : Set (Point n)} (hCopen : IsOpen C) (a : ℝ) : ViscositySubsolution C laplaceOperator fun (x : Point n) => a

Constants are viscosity subsolutions of -Δu = 0 on open sets.

theorem ViscositySolns.continuousOn_of_abs_sub_le_mul_sqrt_eucSq {n : ℕ} {S : Set (Point n)} {g : Point n → ℝ} {L : ℝ} (hg : ∀ x ∈ S, ∀ y ∈ S, |g x - g y| ≤ L * √(eucSq x y)) : ContinuousOn g S

A function that is L-Lipschitz for the Euclidean distance is continuous.

theorem ViscositySolns.exists_eucSq_le_of_isBounded {n : ℕ} {C : Set (Point n)} (hC : Bornology.IsBounded C) : ∃ (D : ℝ), ∀ x ∈ closure C, ∀ y ∈ closure C, eucSq x y ≤ D

Bounded sets have bounded squared Euclidean diameter.

theorem ViscositySolns.upperEnvelope_eq_of_continuous {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} (hu : Continuous u) {x : Point n} (hx : x ∈ closure C) : upperEnvelope C u x = u x

theorem ViscositySolns.lowerEnvelope_eq_of_continuous {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} (hu : Continuous u) {x : Point n} (hx : x ∈ closure C) : lowerEnvelope C u x = u x

noncomputable def ViscositySolns.laplaceBarrierCoeff (n : ℕ) (R D L : ℝ) : ℝ

The coefficient A = L / √c of the barrier branches.

Equations

• ViscositySolns.laplaceBarrierCoeff n R D L = L / √(ViscositySolns.laplaceBarrierLowerConst n R D)

noncomputable def ViscositySolns.laplaceBarrierModulus (n : ℕ) (R D L : ℝ) : ℝ

The Hölder-1/2 modulus constant K = A √(α (√D + R)).

Equations

• ViscositySolns.laplaceBarrierModulus n R D L = ViscositySolns.laplaceBarrierCoeff n R D L * √(ViscositySolns.laplaceBarrierRate n R * (√D + R))

theorem ViscositySolns.laplaceBarrierCoeff_nonneg {n : ℕ} {R D L : ℝ} (hL : 0 ≤ L) : 0 ≤ laplaceBarrierCoeff n R D L

theorem ViscositySolns.laplaceBarrierModulus_nonneg {n : ℕ} {R D L : ℝ} (hL : 0 ≤ L) : 0 ≤ laplaceBarrierModulus n R D L

theorem ViscositySolns.mul_sqrt_eucSq_le_coeff_mul_profile {n : ℕ} {C : Set (Point n)} {R D L : ℝ} (hR : 0 < R) (hD : ∀ x ∈ closure C, ∀ y ∈ closure C, eucSq x y ≤ D) (hL : 0 ≤ L) {p : Point n × Point n} (hp : p ∈ exteriorSphereParams C R) {x : Point n} (hx : x ∈ closure C) : L * √(eucSq x p.1) ≤ laplaceBarrierCoeff n R D L * laplaceBarrierProfile (laplaceBarrierRate n R) R p x

Each branch dominates the Lipschitz growth L |x - x₀| on closure C.

theorem ViscositySolns.laplaceUpperBarrier_properties {n : ℕ} {C : Set (Point n)} {R D L : ℝ} (hCopen : IsOpen C) (hCbdd : Bornology.IsBounded C) (hext : UniformExteriorSphereSq C R) (hD : ∀ x ∈ closure C, ∀ y ∈ closure C, eucSq x y ≤ D) (hL : 0 ≤ L) {x₀ : Point n} (hx₀ : x₀ ∈ frontier C) {h : Point n → ℝ} (hh : ∀ x ∈ closure C, ∀ y ∈ closure C, |h x - h y| ≤ L * √(eucSq x y)) : Continuous (laplaceUpperBarrier C R (laplaceBarrierCoeff n R D L) h) ∧ ViscositySupersolution C laplaceOperator (laplaceUpperBarrier C R (laplaceBarrierCoeff n R D L) h) ∧ (∀ z ∈ frontier C, laplaceUpperBarrier C R (laplaceBarrierCoeff n R D L) h z = h z) ∧ ∀ z ∈ frontier C, ∀ x ∈ closure C, laplaceUpperBarrier C R (laplaceBarrierCoeff n R D L) h x ≤ h z + laplaceBarrierModulus n R D L * √√(eucSq x z)

The properties of the upper barrier U_h for Lipschitz boundary data h.

theorem ViscositySolns.neg_laplaceUpperBarrier_neg_le {n : ℕ} {C : Set (Point n)} {R D L : ℝ} (hext : UniformExteriorSphereSq C R) (hD : ∀ x ∈ closure C, ∀ y ∈ closure C, eucSq x y ≤ D) (hL : 0 ≤ L) {x₀ : Point n} (hx₀ : x₀ ∈ frontier C) {g : Point n → ℝ} (hg : ∀ x ∈ closure C, ∀ y ∈ closure C, |g x - g y| ≤ L * √(eucSq x y)) {x : Point n} (hx : x ∈ closure C) : -laplaceUpperBarrier C R (laplaceBarrierCoeff n R D L) (fun (y : Point n) => -g y) x ≤ laplaceUpperBarrier C R (laplaceBarrierCoeff n R D L) g x

The lower barrier -U_{-g} lies below the upper barrier U_g on closure C.

theorem ViscositySolns.exists_laplace_barrierPair_of_uniformExteriorSphereSq {n : ℕ} {C : Set (Point n)} (hCopen : IsOpen C) (hCbdd : Bornology.IsBounded C) {R : ℝ} (hext : UniformExteriorSphereSq C R) (L : ℝ) (hL : 0 ≤ L) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (g : Point n → ℝ), (∀ x ∈ closure C, ∀ y ∈ closure C, |g x - g y| ≤ L * √(eucSq x y)) → ∃ (B : DirichletBarrierPair C (frontier C) laplaceOperator g), ContinuousOn B.lower (closure C) ∧ ContinuousOn B.upper (closure C) ∧ BoundaryLowerTraceOn C (frontier C) g B.lower ∧ BoundaryUpperTraceOn C (frontier C) g B.upper ∧ ∀ x₀ ∈ frontier C, ∀ x ∈ closure C, B.upper x ≤ g x₀ + K * √√(eucSq x x₀) ∧ g x₀ - K * √√(eucSq x x₀) ≤ B.lower x

Perron barriers for the Laplace operator under a uniform exterior sphere condition. Let C be a bounded open set satisfying the uniform exterior sphere condition with radius R, and let L ≥ 0. There is a constant K, depending only on n, R, L and the diameter of C, such that every g which is L-Lipschitz on closure C for the Euclidean distance admits a Dirichlet barrier pair for -Δu = 0 whose members are continuous on closure C, attain the boundary values g in the envelope sense, and satisfy the Hölder-1/2 boundary modulus |B(x) - g(x₀)| ≤ K |x - x₀|^{1/2}.