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

Basic Dirichlet and Perron predicates

This file contains the small shared vocabulary for Perron's method. It is deliberately independent of the concrete comparison proof and of the Aleksandrov/Jensen analysis files: Perron's method takes comparison as an abstract hypothesis.

def ViscositySolns.BoundarySubsolutionOn {n : ℕ} (boundary : Set (Point n)) (g u : Point n → ℝ) : Prop

Boundary inequality for a Dirichlet subsolution.

Equations

• ViscositySolns.BoundarySubsolutionOn boundary g u = ∀ x ∈ boundary, u x ≤ g x

def ViscositySolns.BoundarySupersolutionOn {n : ℕ} (boundary : Set (Point n)) (g u : Point n → ℝ) : Prop

Boundary inequality for a Dirichlet supersolution.

Equations

• ViscositySolns.BoundarySupersolutionOn boundary g u = ∀ x ∈ boundary, g x ≤ u x

def ViscositySolns.BoundarySolutionOn {n : ℕ} (boundary : Set (Point n)) (g u : Point n → ℝ) : Prop

Boundary equality for a Dirichlet solution.

Equations

• ViscositySolns.BoundarySolutionOn boundary g u = Set.EqOn u g boundary

def ViscositySolns.DirichletSubsolutionOn {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g u : Point n → ℝ) : Prop

A viscosity subsolution with the Dirichlet boundary inequality and upper semicontinuity up to the boundary on C ∪ boundary.

The set C is the PDE domain used by the existing viscosity predicates, while boundary is kept separate so Section 4's strict boundary condition can be assembled without forcing a specific closure encoding.

Equations

• ViscositySolns.DirichletSubsolutionOn C boundary F g u = (ViscositySolns.ViscositySubsolution C F u ∧ ViscositySolns.BoundarySubsolutionOn boundary g u ∧ UpperSemicontinuousOn u (C ∪ boundary))

def ViscositySolns.DirichletSupersolutionOn {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g u : Point n → ℝ) : Prop

A viscosity supersolution with the Dirichlet boundary inequality and lower semicontinuity up to the boundary on C ∪ boundary.

Equations

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

def ViscositySolns.DirichletSolutionOn {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g u : Point n → ℝ) : Prop

A viscosity solution with equality on the Dirichlet boundary.

Equations

• ViscositySolns.DirichletSolutionOn C boundary F g u = (ViscositySolns.ViscositySolution C F u ∧ ViscositySolns.BoundarySolutionOn boundary g u)

theorem ViscositySolns.DirichletSubsolutionOn.viscosity {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u : Point n → ℝ} (hu : DirichletSubsolutionOn C boundary F g u) : ViscositySubsolution C F u

theorem ViscositySolns.DirichletSubsolutionOn.boundary {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u : Point n → ℝ} (hu : DirichletSubsolutionOn C boundary F g u) : BoundarySubsolutionOn boundary g u

theorem ViscositySolns.DirichletSubsolutionOn.upperSemicontinuousOn {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u : Point n → ℝ} (hu : DirichletSubsolutionOn C boundary F g u) : UpperSemicontinuousOn u (C ∪ boundary)

theorem ViscositySolns.DirichletSubsolutionOn.boundary_le {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u : Point n → ℝ} (hu : DirichletSubsolutionOn C boundary F g u) {x : Point n} (hx : x ∈ boundary) : u x ≤ g x

theorem ViscositySolns.ViscositySubsolution.congr_eqOn {n : ℕ} {C : Set (Point n)} {F : Operator n} {u v : Point n → ℝ} (hu : ViscositySubsolution C F u) (h : Set.EqOn u v C) : ViscositySubsolution C F v

theorem ViscositySolns.ViscositySupersolution.congr_eqOn {n : ℕ} {C : Set (Point n)} {F : Operator n} {u v : Point n → ℝ} (hu : ViscositySupersolution C F u) (h : Set.EqOn u v C) : ViscositySupersolution C F v

theorem ViscositySolns.DirichletSubsolutionOn.congr_eqOn {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u v : Point n → ℝ} (hu : DirichletSubsolutionOn C boundary F g u) (hC : Set.EqOn u v C) (hboundary : Set.EqOn u v boundary) : DirichletSubsolutionOn C boundary F g v

theorem ViscositySolns.DirichletSupersolutionOn.viscosity {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u : Point n → ℝ} (hu : DirichletSupersolutionOn C boundary F g u) : ViscositySupersolution C F u

theorem ViscositySolns.DirichletSupersolutionOn.boundary {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u : Point n → ℝ} (hu : DirichletSupersolutionOn C boundary F g u) : BoundarySupersolutionOn boundary g u

theorem ViscositySolns.DirichletSupersolutionOn.lowerSemicontinuousOn {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u : Point n → ℝ} (hu : DirichletSupersolutionOn C boundary F g u) : LowerSemicontinuousOn u (C ∪ boundary)

theorem ViscositySolns.DirichletSupersolutionOn.boundary_le {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u : Point n → ℝ} (hu : DirichletSupersolutionOn C boundary F g u) {x : Point n} (hx : x ∈ boundary) : g x ≤ u x

theorem ViscositySolns.DirichletSupersolutionOn.congr_eqOn {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u v : Point n → ℝ} (hu : DirichletSupersolutionOn C boundary F g u) (hC : Set.EqOn u v C) (hboundary : Set.EqOn u v boundary) : DirichletSupersolutionOn C boundary F g v

theorem ViscositySolns.DirichletSolutionOn.viscosity {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u : Point n → ℝ} (hu : DirichletSolutionOn C boundary F g u) : ViscositySolution C F u

theorem ViscositySolns.DirichletSolutionOn.boundary {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u : Point n → ℝ} (hu : DirichletSolutionOn C boundary F g u) : BoundarySolutionOn boundary g u

theorem ViscositySolns.DirichletSolutionOn.boundary_eq {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u : Point n → ℝ} (hu : DirichletSolutionOn C boundary F g u) {x : Point n} (hx : x ∈ boundary) : u x = g x

def ViscositySolns.DirichletComparisonPrinciple {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) : Prop

Abstract Dirichlet comparison principle used by Perron's method.

Concrete comparison theorems should later prove adapters into this predicate; the Perron proof itself should only consume this hypothesis.

Equations

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

structure ViscositySolns.DirichletBarrierPair {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) : Type

A lower and upper barrier pair for the Dirichlet problem, including the order relation needed to make the Perron class nonempty and bounded.

• lower : Point n → ℝ

  Lower Dirichlet barrier bounding the Perron family.

• upper : Point n → ℝ

  Upper Dirichlet barrier bounding the Perron family.

• lower_dirichlet : DirichletSubsolutionOn C boundary F g self.lower
• upper_dirichlet : DirichletSupersolutionOn C boundary F g self.upper
• lower_le_upper (x : Point n) : x ∈ C ∪ boundary → self.lower x ≤ self.upper x

def ViscositySolns.PerronClass {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g lower upper w : Point n → ℝ) : Prop

Membership in the Perron family between a lower and an upper barrier.

The pointwise envelope is formed from all such w.

Equations

• ViscositySolns.PerronClass C boundary F g lower upper w = (ViscositySolns.DirichletSubsolutionOn C boundary F g w ∧ (∀ x ∈ C ∪ boundary, lower x ≤ w x) ∧ ∀ x ∈ C ∪ boundary, w x ≤ upper x)

noncomputable def ViscositySolns.perronEnvelope {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g lower upper : Point n → ℝ) : Point n → ℝ

The pointwise Perron envelope of all admissible subsolutions.

Equations

• ViscositySolns.perronEnvelope C boundary F g lower upper x = sSup {r : ℝ | ∃ (w : ViscositySolns.Point n → ℝ), ViscositySolns.PerronClass C boundary F g lower upper w ∧ r = w x}

theorem ViscositySolns.PerronClass.dirichletSubsolution {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g lower upper w : Point n → ℝ} (hw : PerronClass C boundary F g lower upper w) : DirichletSubsolutionOn C boundary F g w

theorem ViscositySolns.PerronClass.lower_le {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g lower upper w : Point n → ℝ} (hw : PerronClass C boundary F g lower upper w) {x : Point n} (hx : x ∈ C ∪ boundary) : lower x ≤ w x

theorem ViscositySolns.PerronClass.le_upper {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g lower upper w : Point n → ℝ} (hw : PerronClass C boundary F g lower upper w) {x : Point n} (hx : x ∈ C ∪ boundary) : w x ≤ upper x

theorem ViscositySolns.DirichletBarrierPair.lower_mem_perronClass {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) : PerronClass C boundary F g B.lower B.upper B.lower