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

Second differences of semiconvex functions and sup-convolutions

This file collects the pointwise facts about the compact sup-convolution

w(ξ) = sup { u(x) - (λ / 2) |x - ξ|² | x ∈ K }

used in the proof that viscosity subharmonic functions are distributionally subharmonic:

• a λ-semiconvex function has coordinate second differences bounded below by -n λ (neg_mul_le_coordSecondDifference_of_coordinateSemiconvexOn);
• at a point where a function has a two-sided second-order jet (p, X), its coordinate second differences converge to trace X (tendsto_coordSecondDifference_of_hasSecondOrderJet);
• maximizers in the definition of w(η) lie within O(λ^{-1/2}) of η (dist_lt_of_isMaxOn_supConvolutionKernel), so w converges to u uniformly on K as λ → ∞ (exists_lambda_abs_compactSupConvolution_sub_le).

Semiconvexity bounds second differences from below

theorem ViscositySolns.neg_mul_dotProduct_le_centralSecondDifference_of_coordinateSemiconvexOn {n : ℕ} {lambda : ℝ} {f : Point n → ℝ} (hf : CoordinateSemiconvexOn lambda Set.univ f) (v x : Point n) : -(lambda * v ⬝ᵥ v) ≤ centralSecondDifference f v x

A λ-semiconvex function has central second differences bounded below by -λ |v|².

theorem ViscositySolns.dotProduct_smul_single_self {n : ℕ} (h : ℝ) (i : Fin n) : h • Pi.single i 1 ⬝ᵥ h • Pi.single i 1 = h ^ 2

theorem ViscositySolns.neg_mul_le_coordSecondDifference_of_coordinateSemiconvexOn {n : ℕ} {lambda : ℝ} {f : Point n → ℝ} (hf : CoordinateSemiconvexOn lambda Set.univ f) {h : ℝ} (hh : h ≠ 0) (x : Point n) : -(↑n * lambda) ≤ coordSecondDifference f h x

A λ-semiconvex function has coordinate second differences bounded below by -n λ.

Second differences at points with a second-order jet

theorem ViscositySolns.tendsto_coordSecondDifference_of_hasSecondOrderJet {n : ℕ} {f : Point n → ℝ} {x p : Point n} {X : Hessian n} (hJ : HasSecondOrderJet f x p X) : Filter.Tendsto (fun (h : ℝ) => coordSecondDifference f h x) (nhdsWithin 0 {0}ᶜ) (nhds (Matrix.trace X))

If (p, X) is a two-sided second-order jet of f at x, then the coordinate second differences of f at x converge to trace X.

Localization and uniform approximation for sup-convolutions

theorem ViscositySolns.supConvolutionKernel_self {n : ℕ} (lambda : ℝ) (u : Point n → ℝ) (η : Point n) : supConvolutionKernel lambda u η η = u η

theorem ViscositySolns.dist_lt_of_isMaxOn_supConvolutionKernel {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} {lambda M δ : ℝ} (hδ : 0 < δ) (hlam : 4 * (M + 1) ≤ lambda * δ ^ 2) (hM : ∀ z ∈ K, |u z| ≤ M) {η y : Point n} (hη : η ∈ K) (hy : y ∈ K) (hmax : IsMaxOn (fun (z : Point n) => supConvolutionKernel lambda u η z) K y) : dist y η < δ

Maximizers in the sup-convolution are close to the base point: if 4 (M + 1) ≤ λ δ² and |u| ≤ M on K, then every maximizer y ∈ K of the kernel at a base point η ∈ K satisfies dist y η < δ.

theorem ViscositySolns.le_compactSupConvolution_of_isCompact {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} {lambda : ℝ} (hKne : K.Nonempty) (hK : IsCompact K) (hu : UpperSemicontinuousOn u K) {η : Point n} (hη : η ∈ K) : u η ≤ compactSupConvolution lambda K u η

The compact sup-convolution dominates u on K.

theorem ViscositySolns.exists_lambda_abs_compactSupConvolution_sub_le {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} (hKne : K.Nonempty) (hK : IsCompact K) (hu : ContinuousOn u K) {M : ℝ} (hM : ∀ z ∈ K, |u z| ≤ M) {ε δ₀ : ℝ} (hε : 0 < ε) (hδ₀ : 0 < δ₀) : ∃ lambda > 0, 4 * (M + 1) ≤ lambda * δ₀ ^ 2 ∧ ∀ η ∈ K, |compactSupConvolution lambda K u η - u η| ≤ ε

Uniform approximation by sup-convolutions: if u is continuous on the compact set K with |u| ≤ M there, then for every ε > 0 and every δ₀ > 0 there is λ > 0 with 4 (M + 1) ≤ λ δ₀² and |w_λ - u| ≤ ε on K.