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

Viscosity subharmonic functions are distributionally subharmonic

Let u be a continuous viscosity subsolution of -Δu = 0 on an open set C and let χ ≥ 0 be a C² function with compact support in C. We prove 0 ≤ ∫ Δχ · u.

The proof follows the sup-convolution route:

1. Replace u by its sup-convolution w = u^λ over a compact neighbourhood K of supp χ. The function w is continuous and λ-semiconvex, so its coordinate second differences are bounded below by -n λ.
2. By Aleksandrov's theorem w has a two-sided second-order jet (p, X) at almost every point. At such a point of supp χ, the superjet transfer lemma moves (p, X) to a superjet of u at a nearby maximizer, so trace X ≥ 0, and the second differences of w converge to trace X.
3. Fatou's lemma, applied to (Δ_h w + c) χ ≥ 0, together with the discrete integration by parts ∫ (Δ_h w) χ = ∫ w (Δ_h χ) and Δ_h χ → Δχ, gives 0 ≤ ∫ w Δχ (integral_mul_lapTrace_nonneg_of_ae_tendsto).
4. Since w → u uniformly on K as λ → ∞, 0 ≤ ∫ Δχ · u.

Fatou's lemma for second differences

theorem ViscositySolns.integral_mul_lapTrace_nonneg_of_ae_tendsto {n : ℕ} {w χ : Point n → ℝ} (hw : Continuous w) (hχ : ContDiff ℝ 2 χ) (hχc : HasCompactSupport χ) (hχ0 : 0 ≤ χ) {c : ℝ} (hlow : ∀ (h : ℝ), h ≠ 0 → ∀ (x : Point n), -c ≤ coordSecondDifference w h x) (hae : ∀ᵐ (x : Point n), x ∈ tsupport χ → ∃ (T : ℝ), 0 ≤ T ∧ Filter.Tendsto (fun (h : ℝ) => coordSecondDifference w h x) (nhdsWithin 0 {0}ᶜ) (nhds T)) : 0 ≤ ∫ (x : Point n), w x * lapTrace χ x

Fatou step. Let w be continuous with second differences bounded below, and suppose that at almost every point of supp χ the second differences of w converge to a nonnegative limit. Then 0 ≤ ∫ w Δχ for every nonnegative C² function χ with compact support.

Subsolutions of the Laplace equation

theorem ViscositySolns.superjet_eq_of_mem_nhds {n : ℕ} {C K : Set (Point n)} (hKC : K ⊆ C) {u : Point n → ℝ} {y : Point n} (hK : K ∈ nhds y) : Superjet K u y = Superjet C u y

Superjets relative to K and to a larger set C agree at every point of which K is a neighbourhood.

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

Viscosity subharmonic functions are distributionally subharmonic.

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