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

Dirichlet comparison for the Laplace operator

The Laplace operator F(x,r,p,X) = - trace X is proper but has no strict monotonicity in the scalar variable, so the constant-shift comparison adapter does not apply to it directly. Instead we strictify a subsolution u by adding the quadratic penalty η (|y|² - K), whose Hessian 2η I makes u + η (|y|² - K) a strict subsolution with strictness 2 η n. Choosing K so that the penalty is at most -η on the compact closure keeps the boundary inequality, and letting η → 0 gives the comparison principle.

In dimension zero the principle fails (every function is a solution and the boundary is empty), so the positive-dimension hypothesis is necessary.

def ViscositySolns.laplaceOperator {n : ℕ} : Operator n

The Laplace operator F(x,r,p,X) = - trace X, i.e. the equation -Δu = 0.

Equations

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

@[simp]

theorem ViscositySolns.laplaceOperator_apply {n : ℕ} (x : Point n) (r : ℝ) (p : Point n) (X : Hessian n) : laplaceOperator x r p X = -Matrix.trace X

theorem ViscositySolns.proper_laplaceOperator {n : ℕ} : Proper laplaceOperator

theorem ViscositySolns.degenerateElliptic_laplaceOperator {n : ℕ} : DegenerateElliptic laplaceOperator

theorem ViscositySolns.operatorContinuous_laplaceOperator {n : ℕ} : OperatorContinuous laplaceOperator

theorem ViscositySolns.ishiiOperatorComparisonConditionOn_laplaceOperator {n : ℕ} (C : Set (Point n)) (R : Set ℝ) : IshiiOperatorComparisonConditionOn C R laplaceOperator

theorem ViscositySolns.negOperator_laplaceOperator {n : ℕ} : negOperator laplaceOperator = laplaceOperator

The Laplace operator is invariant under the sign duality negOperator.

noncomputable def ViscositySolns.laplacePenalty {n : ℕ} (η K : ℝ) : Point n → ℝ

The strictifying penalty y ↦ η (|y|² - K), written as a quadratic model.

Equations

• ViscositySolns.laplacePenalty η K y = ViscositySolns.quadraticModel 0 (-(η * K)) 0 ((2 * η) • 1) y

theorem ViscositySolns.laplacePenalty_apply {n : ℕ} (η K : ℝ) (y : Point n) : laplacePenalty η K y = η * (y ⬝ᵥ y - K)

theorem ViscositySolns.continuous_laplacePenalty {n : ℕ} (η K : ℝ) : Continuous (laplacePenalty η K)

theorem ViscositySolns.ViscositySubsolution.strict_add_laplacePenalty {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} (hu : ViscositySubsolution C laplaceOperator u) (η K : ℝ) : StrictViscositySubsolution C laplaceOperator (2 * η * ↑n) fun (y : Point n) => u y + laplacePenalty η K y

Adding the penalty η (|y|² - K) to a subsolution of -Δu = 0 produces a strict subsolution: every superjet (p, X) satisfies - trace X ≤ - 2 η n.

theorem ViscositySolns.dirichletComparisonPrinciple_laplaceOperator {n : ℕ} (hn : 0 < n) {C : Set (Point n)} [LocallyCompactSpace ↑C] (hCcompact : CompactClosure C) (g : Point n → ℝ) : DirichletComparisonPrinciple C (frontier C) laplaceOperator g

Dirichlet comparison for the Laplace operator on a domain with compact closure in positive dimension, with the topological frontier as the Dirichlet boundary.