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

The Perron solution of the Laplace Dirichlet problem

On a bounded open set C ⊆ Point n with 0 < n, a Dirichlet barrier pair for -Δ whose barriers are continuous on closure C and attain the data g as boundary traces produces, through the CIL Perron theorem PerronMethodExistenceTheorem.strictBoundary and the Laplace comparison principle, a viscosity solution w of -Δw = 0 on C that is continuous on closure C, equals g on frontier C, and lies between the barriers.

theorem ViscositySolns.upperEnvelope_eq_of_continuousOn_closure {n : ℕ} {C : Set (Point n)} {f : Point n → ℝ} (hf : ContinuousOn f (closure C)) {x : Point n} (hx : x ∈ closure C) : upperEnvelope C f x = f x

The limsup along 𝓝[C] x of a function continuous on closure C is its value.

theorem ViscositySolns.lowerEnvelope_eq_of_continuousOn_closure {n : ℕ} {C : Set (Point n)} {f : Point n → ℝ} (hf : ContinuousOn f (closure C)) {x : Point n} (hx : x ∈ closure C) : lowerEnvelope C f x = f x

The liminf along 𝓝[C] x of a function continuous on closure C is its value.

theorem ViscositySolns.isBoundedUnder_le_of_continuousOn_closure {n : ℕ} {C : Set (Point n)} (hC : Bornology.IsBounded C) {f : Point n → ℝ} (hf : ContinuousOn f (closure C)) (x : Point n) : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) f

theorem ViscositySolns.isBoundedUnder_ge_of_continuousOn_closure {n : ℕ} {C : Set (Point n)} (hC : Bornology.IsBounded C) {f : Point n → ℝ} (hf : ContinuousOn f (closure C)) (x : Point n) : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) f

theorem ViscositySolns.exists_laplace_dirichlet_of_barrierPair {n : ℕ} (hn : 0 < n) {C : Set (Point n)} (hCopen : IsOpen C) (hCbdd : Bornology.IsBounded C) {g : Point n → ℝ} (B : DirichletBarrierPair C (frontier C) laplaceOperator g) (hlower : ContinuousOn B.lower (closure C)) (hupper : ContinuousOn B.upper (closure C)) (hlowerTrace : BoundaryLowerTraceOn C (frontier C) g B.lower) (hupperTrace : BoundaryUpperTraceOn C (frontier C) g B.upper) : ∃ (w : Point n → ℝ), ViscositySolution C laplaceOperator w ∧ ContinuousOn w (closure C) ∧ (∀ x ∈ frontier C, w x = g x) ∧ ∀ x ∈ closure C, B.lower x ≤ w x ∧ w x ≤ B.upper x

Perron existence for the Laplace Dirichlet problem from continuous barriers. The solution is continuous up to the boundary, attains g on frontier C, and is squeezed between the barriers on closure C.