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

Viscosity harmonic functions are weakly harmonic

A continuous viscosity solution u of the Laplace equation -Δu = 0 on an open set C satisfies ∫ Δχ · u = 0 for every smooth test function χ with compact support in C (integral_lapTrace_mul_eq_zero_of_viscositySolution_laplace).

The subsolution half gives ∫ Δχ · u ≥ 0 for χ ≥ 0 (integral_lapTrace_mul_nonneg_of_viscositySubsolution_laplace). Since the Laplace operator is odd, -u is again a subsolution when u is a supersolution, which gives the reverse inequality. A general test function is the difference χ = (χ + M θ) - M θ of two nonnegative ones, where θ is a smooth cutoff equal to 1 on supp χ and M ≥ sup |χ|.

Algebra of the trace Laplacian

theorem ViscositySolns.lapTrace_sub {n : ℕ} {χ ψ : Point n → ℝ} (hχ : ContDiff ℝ 2 χ) (hψ : ContDiff ℝ 2 ψ) (x : Point n) : lapTrace (fun (y : Point n) => χ y - ψ y) x = lapTrace χ x - lapTrace ψ x

The trace Laplacian is additive on differences of C² functions.

theorem ViscositySolns.integrable_lapTrace_mul {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} (hcont : ContinuousOn u C) {χ : Point n → ℝ} (hχ : ContDiff ℝ 2 χ) (hχc : HasCompactSupport χ) (hχC : tsupport χ ⊆ C) : MeasureTheory.Integrable (fun (x : Point n) => lapTrace χ x * u x) MeasureTheory.volume

For u continuous on C and χ continuous with compact support in C, the product Δχ · u is integrable.

Supersolutions and nonnegative test functions

theorem ViscositySolns.integral_lapTrace_mul_nonpos_of_viscositySupersolution_laplace {n : ℕ} {C : Set (Point n)} (hC : IsOpen C) {u : Point n → ℝ} (hu : ViscositySupersolution C laplaceOperator u) (hcont : ContinuousOn u C) {χ : Point n → ℝ} (hχ : ContDiff ℝ 2 χ) (hχc : HasCompactSupport χ) (hχC : tsupport χ ⊆ C) (hχ0 : 0 ≤ χ) : ∫ (x : Point n), lapTrace χ x * u x ≤ 0

If u is a continuous viscosity supersolution of -Δu = 0 on an open set C, then ∫ Δχ · u ≤ 0 for every nonnegative C² function χ with compact support in C.

theorem ViscositySolns.integral_lapTrace_mul_eq_zero_of_viscositySolution_laplace_of_nonneg {n : ℕ} {C : Set (Point n)} (hC : IsOpen C) {u : Point n → ℝ} (hu : ViscositySolution C laplaceOperator u) (hcont : ContinuousOn u C) {χ : Point n → ℝ} (hχ : ContDiff ℝ 2 χ) (hχc : HasCompactSupport χ) (hχC : tsupport χ ⊆ C) (hχ0 : 0 ≤ χ) : ∫ (x : Point n), lapTrace χ x * u x = 0

A continuous viscosity solution of -Δu = 0 annihilates Δχ for every nonnegative C² test function χ with compact support in C.

General test functions

theorem ViscositySolns.exists_contDiff_cutoff {n : ℕ} {C K₀ : Set (Point n)} (hC : IsOpen C) (hK₀ : IsCompact K₀) (hK₀C : K₀ ⊆ C) : ∃ (θ : Point n → ℝ), ContDiff ℝ (↑⊤) θ ∧ HasCompactSupport θ ∧ tsupport θ ⊆ C ∧ (∀ (x : Point n), 0 ≤ θ x) ∧ ∀ x ∈ K₀, θ x = 1

A smooth cutoff: for a compact set K₀ inside an open set C, there is a smooth θ : R^n → [0, 1] with compact support in C and θ = 1 on K₀.

theorem ViscositySolns.integral_lapTrace_mul_eq_zero_of_viscositySolution_laplace {n : ℕ} {C : Set (Point n)} (hC : IsOpen C) {u : Point n → ℝ} (hu : ViscositySolution C laplaceOperator u) (hcont : ContinuousOn u C) {χ : Point n → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχc : HasCompactSupport χ) (hχC : tsupport χ ⊆ C) : ∫ (x : Point n), lapTrace χ x * u x = 0

Viscosity harmonic functions are weakly harmonic.

If u is a continuous viscosity solution of the Laplace equation -Δu = 0 on an open set C, then ∫ Δχ · u = 0 for every smooth χ with compact support in C, where Δχ = lapTrace χ = ∑ i, D²χ(eᵢ, eᵢ).