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

Exterior-sphere barriers for the Laplace operator

Let C be a bounded open set satisfying the uniform exterior sphere condition with radius R, and let g be L-Lipschitz on closure C for the Euclidean distance. We build a Perron barrier pair for -Δu = 0 with boundary data g.

Parameter set. P consists of all pairs (x₀, y) with x₀ ∈ frontier C and y the centre of an admissible exterior sphere of radius R at x₀. It is compact, and using all admissible centres avoids choosing y continuously.

Profile. For p = (x₀, y) ∈ P let c = (x₀ + y)/2 and τ(x) = |x - c|² - R²/4. On closure C one has τ ≥ |x - x₀|²/2 and τ ≤ |x - x₀|² + R |x - x₀|. The profile is Φ_p(x) = √(1 - exp (-α τ(x))) with α = 2 (n + 1) / R², which is comparable to |x - x₀| from below and to |x - x₀|^{1/2} from above.

Upper barrier. U_g(x) = inf_{p ∈ P} (g x₀ + A Φ_p(x)). At a point of C the infimum is attained at some p̂; by concavity of the square root, the branch at p̂ lies below the exponential radial function W = const - k exp (-α τ), which touches it at the point and has nonpositive Laplacian because 2 α |x - c|² ≥ n + 1. Hence every subjet of U_g has nonnegative -trace.

Lower barrier. -U_{-g}, using that the Laplace operator is self-dual.

The parameter set

def ViscositySolns.exteriorSphereParams {n : ℕ} (C : Set (Point n)) (R : ℝ) : Set (Point n × Point n)

Frontier points of C together with all admissible exterior-sphere centres.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ViscositySolns.sphereMidpoint {n : ℕ} (p : Point n × Point n) : Point n

The midpoint (x₀ + y) / 2 of a frontier point and a sphere centre.

Equations

• ViscositySolns.sphereMidpoint p = (1 / 2) • (p.1 + p.2)

theorem ViscositySolns.isClosed_exteriorSphereParams {n : ℕ} (C : Set (Point n)) (R : ℝ) : IsClosed (exteriorSphereParams C R)

theorem ViscositySolns.isCompact_exteriorSphereParams {n : ℕ} {C : Set (Point n)} (hCbdd : Bornology.IsBounded C) (R : ℝ) : IsCompact (exteriorSphereParams C R)

theorem ViscositySolns.nonempty_exteriorSphereParams {n : ℕ} {C : Set (Point n)} {R : ℝ} (hext : UniformExteriorSphereSq C R) {x₀ : Point n} (hx₀ : x₀ ∈ frontier C) : ∃ (y : Point n), (x₀, y) ∈ exteriorSphereParams C R

theorem ViscositySolns.half_eucSq_le_eucSq_sphereMidpoint {n : ℕ} {C : Set (Point n)} {R : ℝ} {p : Point n × Point n} (hp : p ∈ exteriorSphereParams C R) {x : Point n} (hx : x ∈ closure C) : eucSq x p.1 / 2 ≤ eucSq x (sphereMidpoint p) - R ^ 2 / 4

The squared distance from the midpoint, shifted by R²/4, controls |x - x₀|²/2 from above on closure C.

theorem ViscositySolns.eucSq_sphereMidpoint_le {n : ℕ} {C : Set (Point n)} {R : ℝ} (hR : 0 < R) {p : Point n × Point n} (hp : p ∈ exteriorSphereParams C R) (x : Point n) : eucSq x (sphereMidpoint p) - R ^ 2 / 4 ≤ eucSq x p.1 + R * √(eucSq x p.1)

theorem ViscositySolns.eucSq_sphereMidpoint_self {n : ℕ} {C : Set (Point n)} {R : ℝ} {p : Point n × Point n} (hp : p ∈ exteriorSphereParams C R) : eucSq p.1 (sphereMidpoint p) = R ^ 2 / 4

The barrier profile

noncomputable def ViscositySolns.laplaceBarrierRate (n : ℕ) (R : ℝ) : ℝ

The exponential rate α = 2 (n + 1) / R² of the barrier profile.

Equations

• ViscositySolns.laplaceBarrierRate n R = 2 * (↑n + 1) / R ^ 2

theorem ViscositySolns.laplaceBarrierRate_pos {n : ℕ} {R : ℝ} (hR : 0 < R) : 0 < laplaceBarrierRate n R

theorem ViscositySolns.two_mul_laplaceBarrierRate_mul {n : ℕ} {R : ℝ} (hR : 0 < R) : 2 * laplaceBarrierRate n R * (R ^ 2 / 4) = ↑n + 1

noncomputable def ViscositySolns.laplaceBarrierProfile {n : ℕ} (α R : ℝ) (p : Point n × Point n) (x : Point n) : ℝ

The profile Φ_p(x) = √(1 - exp (-α (|x - c_p|² - R²/4))).

Equations

• ViscositySolns.laplaceBarrierProfile α R p x = √(1 - Real.exp (-(α * (ViscositySolns.eucSq x (ViscositySolns.sphereMidpoint p) - R ^ 2 / 4))))

theorem ViscositySolns.Continuous.laplaceBarrierProfile {n : ℕ} {X : Type u_1} [TopologicalSpace X] (α R : ℝ) {f : X → Point n × Point n} {h : X → Point n} (hf : Continuous f) (hh : Continuous h) : Continuous fun (t : X) => ViscositySolns.laplaceBarrierProfile α R (f t) (h t)

theorem ViscositySolns.laplaceBarrierProfile_self {n : ℕ} {C : Set (Point n)} {R α : ℝ} {p : Point n × Point n} (hp : p ∈ exteriorSphereParams C R) : laplaceBarrierProfile α R p p.1 = 0

theorem ViscositySolns.sqrt_mul_sqrt_le_sqrt_one_sub_exp {α T τ e : ℝ} (hα : 0 < α) (hτ : e / 2 ≤ τ) (hτT : τ ≤ T) (he : 0 ≤ e) : √(α * Real.exp (-(α * T)) / 2) * √e ≤ √(1 - Real.exp (-(α * τ)))

theorem ViscositySolns.sqrt_one_sub_exp_le_sqrt_mul_sqrt {α R Δ δ τ : ℝ} (hα : 0 ≤ α) (hR : 0 ≤ R) (hδ : 0 ≤ δ) (hδΔ : δ ≤ Δ) (hτ : τ ≤ δ ^ 2 + R * δ) : √(1 - Real.exp (-(α * τ))) ≤ √(α * (Δ + R)) * √δ

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

The lower constant c with √c |x - x₀| ≤ Φ_p(x) on closure C.

Equations

• ViscositySolns.laplaceBarrierLowerConst n R D = ViscositySolns.laplaceBarrierRate n R * Real.exp (-(ViscositySolns.laplaceBarrierRate n R * (D + R * √D))) / 2

theorem ViscositySolns.laplaceBarrierLowerConst_pos {n : ℕ} {R : ℝ} (hR : 0 < R) (D : ℝ) : 0 < laplaceBarrierLowerConst n R D

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

The profile grows at least linearly in the Euclidean distance to x₀.

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

The profile is Hölder-1/2 in the Euclidean distance to x₀.

The upper barrier

noncomputable def ViscositySolns.laplaceBarrierBranch {n : ℕ} (R A : ℝ) (g : Point n → ℝ) (p : Point n × Point n) (x : Point n) : ℝ

One branch g x₀ + A Φ_p of the upper barrier.

Equations

• ViscositySolns.laplaceBarrierBranch R A g p x = g p.1 + A * ViscositySolns.laplaceBarrierProfile (ViscositySolns.laplaceBarrierRate n R) R p x

noncomputable def ViscositySolns.laplaceUpperBarrier {n : ℕ} (C : Set (Point n)) (R A : ℝ) (g : Point n → ℝ) (x : Point n) : ℝ

The upper barrier U_g = inf_{p ∈ P} (g x₀ + A Φ_p).

Equations

• One or more equations did not get rendered due to their size.

theorem ViscositySolns.continuousOn_laplaceBarrierBranch {n : ℕ} {C : Set (Point n)} {R A : ℝ} {g : Point n → ℝ} (hgc : ContinuousOn g (closure C)) (x : Point n) : ContinuousOn (fun (p : Point n × Point n) => laplaceBarrierBranch R A g p x) (exteriorSphereParams C R)

theorem ViscositySolns.continuous_laplaceUpperBarrier {n : ℕ} {C : Set (Point n)} {R A : ℝ} {g : Point n → ℝ} (hCbdd : Bornology.IsBounded C) (hgc : ContinuousOn g (closure C)) : Continuous (laplaceUpperBarrier C R A g)

theorem ViscositySolns.laplaceUpperBarrier_le {n : ℕ} {C : Set (Point n)} {R A : ℝ} {g : Point n → ℝ} (hCbdd : Bornology.IsBounded C) (hgc : ContinuousOn g (closure C)) {p : Point n × Point n} (hp : p ∈ exteriorSphereParams C R) (x : Point n) : laplaceUpperBarrier C R A g x ≤ laplaceBarrierBranch R A g p x

theorem ViscositySolns.le_laplaceUpperBarrier {n : ℕ} {C : Set (Point n)} {R A : ℝ} {g : Point n → ℝ} {x₀ : Point n} (hx₀ : x₀ ∈ frontier C) (hext : UniformExteriorSphereSq C R) {b : ℝ} (x : Point n) (hb : ∀ p ∈ exteriorSphereParams C R, b ≤ laplaceBarrierBranch R A g p x) : b ≤ laplaceUpperBarrier C R A g x

theorem ViscositySolns.exists_laplaceUpperBarrier_eq {n : ℕ} {C : Set (Point n)} {R A : ℝ} {g : Point n → ℝ} (hCbdd : Bornology.IsBounded C) (hgc : ContinuousOn g (closure C)) {x₀ : Point n} (hx₀ : x₀ ∈ frontier C) (hext : UniformExteriorSphereSq C R) (x : Point n) : ∃ p ∈ exteriorSphereParams C R, laplaceBarrierBranch R A g p x = laplaceUpperBarrier C R A g x

theorem ViscositySolns.add_mul_sqrt_one_sub_le {gp A e₀ e : ℝ} (hA : 0 ≤ A) (he₀ : e₀ < 1) (he : e ≤ 1) : gp + A * √(1 - e) ≤ gp + A * √(1 - e₀) + A / (2 * √(1 - e₀)) * e₀ - A / (2 * √(1 - e₀)) * e

Scalar form of the touching inequality: by concavity of √, the branch gp + A √(1 - e) lies below the affine function of e tangent at e₀.

theorem ViscositySolns.viscositySupersolution_laplaceUpperBarrier {n : ℕ} {C : Set (Point n)} {R A : ℝ} {g : Point n → ℝ} (hCopen : IsOpen C) (hCbdd : Bornology.IsBounded C) (hext : UniformExteriorSphereSq C R) (hA : 0 ≤ A) (hgc : ContinuousOn g (closure C)) {x₀ : Point n} (hx₀ : x₀ ∈ frontier C) : ViscositySupersolution C laplaceOperator (laplaceUpperBarrier C R A g)

The upper barrier is a viscosity supersolution of -Δu = 0 on C.