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

Coordinate second differences and the trace Laplacian

For a function f : R^n -> R and a step h, the coordinate second-difference Laplacian is

Δ_h f(x) = h⁻² ∑ i, (f(x + h eᵢ) + f(x - h eᵢ) - 2 f(x)).

This file proves the facts about Δ_h needed to pass from viscosity to distributional subharmonicity:

• for a C² function χ with compact support, Δ_h χ → Δχ uniformly as h → 0, where Δχ = lapTrace χ is the trace of the second Fréchet derivative (exists_forall_abs_coordSecondDifference_sub_lapTrace_le);
• consequently ∫ w Δ_h χ → ∫ w Δχ for continuous w (tendsto_integral_mul_coordSecondDifference);
• the discrete integration by parts ∫ (Δ_h f) g = ∫ f (Δ_h g), a consequence of translation invariance of Lebesgue measure (integral_coordSecondDifference_mul).

noncomputable def ViscositySolns.lapTrace {n : ℕ} (χ : Point n → ℝ) (x : Point n) : ℝ

The trace Laplacian Δχ(x) = ∑ i, D²χ(x)(eᵢ, eᵢ), computed from the second Fréchet derivative of χ.

Equations

• ViscositySolns.lapTrace χ x = ∑ i : Fin n, ((fderiv ℝ (fderiv ℝ χ) x) (Pi.single i 1)) (Pi.single i 1)

def ViscositySolns.centralSecondDifference {n : ℕ} (f : Point n → ℝ) (v x : Point n) : ℝ

The central second difference f(x + v) + f(x - v) - 2 f(x).

Equations

• ViscositySolns.centralSecondDifference f v x = f (x + v) + f (x - v) - 2 * f x

noncomputable def ViscositySolns.coordSecondDifference {n : ℕ} (f : Point n → ℝ) (h : ℝ) (x : Point n) : ℝ

The coordinate second-difference Laplacian with step h: h⁻² ∑ i, (f(x + h eᵢ) + f(x - h eᵢ) - 2 f(x)).

Equations

• ViscositySolns.coordSecondDifference f h x = (h ^ 2)⁻¹ * ∑ i : Fin n, ViscositySolns.centralSecondDifference f (h • Pi.single i 1) x

theorem ViscositySolns.norm_single_one_le_one {n : ℕ} (i : Fin n) : ‖Pi.single i 1‖ ≤ 1

A one-dimensional second-order mean value estimate

theorem ViscositySolns.abs_central_second_difference_sub_le {g g' g'' : ℝ → ℝ} {a ε h : ℝ} (hh : 0 ≤ h) (hg : ∀ (t : ℝ), HasDerivAt g (g' t) t) (hg' : ∀ (t : ℝ), HasDerivAt g' (g'' t) t) (hbound : ∀ t ∈ Set.Icc (-h) h, |g'' t - a| ≤ ε) : |g h + g (-h) - 2 * g 0 - a * h ^ 2| ≤ 2 * ε * h ^ 2

If g'' stays within ε of a on [-h, h], then the central second difference of g is within 2 ε h² of a h².

Uniform convergence of second differences of test functions

theorem ViscositySolns.lapTrace_eq_zero_of_notMem_tsupport {n : ℕ} {χ : Point n → ℝ} {x : Point n} (hx : x ∉ tsupport χ) : lapTrace χ x = 0

The trace Laplacian of a function vanishes off its topological support.

theorem ViscositySolns.continuous_lapTrace {n : ℕ} {χ : Point n → ℝ} (hχ : ContDiff ℝ 2 χ) : Continuous (lapTrace χ)

The trace Laplacian of a C² function is continuous.

theorem ViscositySolns.hasCompactSupport_lapTrace {n : ℕ} {χ : Point n → ℝ} (hχc : HasCompactSupport χ) : HasCompactSupport (lapTrace χ)

The trace Laplacian of a C² function with compact support has compact support.

theorem ViscositySolns.dist_add_smul_single_le {n : ℕ} (x : Point n) (t : ℝ) (i : Fin n) : dist (x + t • Pi.single i 1) x ≤ |t|

theorem ViscositySolns.exists_forall_abs_coordSecondDifference_sub_lapTrace_le {n : ℕ} {χ : Point n → ℝ} (hχ : ContDiff ℝ 2 χ) (hχc : HasCompactSupport χ) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ (h : ℝ), 0 < h → h < δ → ∀ (x : Point n), |coordSecondDifference χ h x - lapTrace χ x| ≤ ε

For a C² function with compact support, the coordinate second differences converge uniformly to the trace Laplacian.

Supports and continuity of second differences

theorem ViscositySolns.continuous_coordSecondDifference {n : ℕ} {f : Point n → ℝ} (hf : Continuous f) (h : ℝ) : Continuous (coordSecondDifference f h)

theorem ViscositySolns.coordSecondDifference_eq_zero_of_notMem_cthickening {n : ℕ} {f : Point n → ℝ} {h r : ℝ} (hh : 0 ≤ h) (hhr : h ≤ r) {x : Point n} (hx : x ∉ Metric.cthickening r (tsupport f)) : coordSecondDifference f h x = 0

The second difference with step 0 ≤ h ≤ r vanishes outside the closed r-thickening of the topological support.

theorem ViscositySolns.integrable_of_continuous_of_forall_notMem_eq_zero {n : ℕ} {f : Point n → ℝ} (hf : Continuous f) {S : Set (Point n)} (hS : IsCompact S) (hzero : ∀ x ∉ S, f x = 0) : MeasureTheory.Integrable f MeasureTheory.volume

A continuous function whose support lies in a compact set is integrable.

theorem ViscositySolns.tendsto_integral_mul_coordSecondDifference {n : ℕ} {w χ : Point n → ℝ} (hw : Continuous w) (hχ : ContDiff ℝ 2 χ) (hχc : HasCompactSupport χ) : Filter.Tendsto (fun (h : ℝ) => ∫ (x : Point n), w x * coordSecondDifference χ h x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : Point n), w x * lapTrace χ x))

For continuous w and a C² function χ with compact support, ∫ w Δ_h χ → ∫ w Δχ as h → 0⁺.

Discrete integration by parts

theorem ViscositySolns.integral_centralSecondDifference_mul {n : ℕ} {f g : Point n → ℝ} (hf : Continuous f) (hg : Continuous g) (hgc : HasCompactSupport g) (v : Point n) : ∫ (x : Point n), centralSecondDifference f v x * g x = ∫ (x : Point n), f x * centralSecondDifference g v x

Translation invariance of Lebesgue measure moves a central second difference from one factor to the other.

theorem ViscositySolns.integral_coordSecondDifference_mul {n : ℕ} {f g : Point n → ℝ} (hf : Continuous f) (hg : Continuous g) (hgc : HasCompactSupport g) (h : ℝ) : ∫ (x : Point n), coordSecondDifference f h x * g x = ∫ (x : Point n), f x * coordSecondDifference g h x

Discrete integration by parts: ∫ (Δ_h f) g = ∫ f (Δ_h g) for continuous f and continuous compactly supported g.