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

Smooth test-function characterization of viscosity solutions

This file proves the classical CIL Section 2 equivalence between the semijet definition of viscosity sub- and supersolutions and the smooth test-function formulation: on an open domain, for an operator that is continuous in the Hessian argument and depends on it only through its symmetric part, u is a viscosity subsolution if and only if u is upper semicontinuous and F (x, u x, Dφ x, D²φ x) <= 0 whenever φ is a C² function such that u - φ has a local maximum at x relative to the domain.

The forward direction localizes the Taylor bridge of ViscositySolns.TestFunctions.Solutions to a ball. The converse applies the test-function inequality to the epsilon-inflated quadratic models quadraticModel x (u x) p (symHessian X + ε • 1) and passes to the limit ε → 0 using the continuity of the operator in the Hessian slot.

Main definitions and results

• SmoothTestFunctionSubsolution, SmoothTestFunctionSupersolution: the classical smooth test-function formulations, phrased with ContDiff and mathlib's canonical fderiv data at the contact point.
• viscositySubsolution_iff_smoothTestFunctionSubsolution
• viscositySupersolution_iff_smoothTestFunctionSupersolution

The smooth test-function formulations

def ViscositySolns.SmoothTestFunctionSubsolution {n : ℕ} (C : Set (Point n)) (F : Operator n) (u : Point n → ℝ) : Prop

The classical smooth test-function formulation of viscosity subsolutions: u is upper semicontinuous, and the operator inequality holds at every point where a globally C² test function touches u from above, evaluated on the coordinate gradient and Hessian extracted from mathlib's canonical first and second Fréchet derivatives at the contact point.

Equations

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

def ViscositySolns.SmoothTestFunctionSupersolution {n : ℕ} (C : Set (Point n)) (F : Operator n) (u : Point n → ℝ) : Prop

The classical smooth test-function formulation of viscosity supersolutions: u is lower semicontinuous, and the operator inequality holds at every point where a globally C² test function touches u from below.

Equations

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

Smoothness and derivatives of the quadratic model

theorem ViscositySolns.quadraticModel_eq_frechetSecondOrderModel {n : ℕ} (x0 : Point n) (r : ℝ) (p : Point n) (X : Hessian n) : quadraticModel x0 r p X = frechetSecondOrderModel x0 r (gradientLinearMap p) (hessianBilinearMap X)

The quadratic model is the Fréchet second-order model of its jet data.

theorem ViscositySolns.contDiff_frechetSecondOrderModel {n : ℕ} (x0 : Point n) (r : ℝ) (Dφ : Point n →L[ℝ] ℝ) (D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ) : ContDiff ℝ 2 (frechetSecondOrderModel x0 r Dφ D2φ)

The Fréchet second-order model is a C² function of the base point.

theorem ViscositySolns.hasFDerivAt_frechetSecondOrderModel {n : ℕ} (x0 : Point n) (r : ℝ) (Dφ : Point n →L[ℝ] ℝ) (D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ) (hD2φ : IsSymmetricBilinear D2φ) (x : Point n) : HasFDerivAt (frechetSecondOrderModel x0 r Dφ D2φ) (Dφ + D2φ (x - x0)) x

Global version of the model derivative: for a symmetric bilinear second derivative, the Fréchet quadratic model has derivative Dφ + D²φ (x - x₀) at every point.

theorem ViscositySolns.fderiv_quadraticModel_center {n : ℕ} (x0 : Point n) (r : ℝ) (p : Point n) {X : Hessian n} (hX : IsSymmetricBilinear (hessianBilinearMap X)) : fderiv ℝ (quadraticModel x0 r p X) x0 = gradientLinearMap p

The canonical first derivative of a quadratic model at its center point.

theorem ViscositySolns.fderiv_fderiv_quadraticModel_center {n : ℕ} (x0 : Point n) (r : ℝ) (p : Point n) {X : Hessian n} (hX : IsSymmetricBilinear (hessianBilinearMap X)) : fderiv ℝ (fderiv ℝ (quadraticModel x0 r p X)) x0 = hessianBilinearMap X

The canonical second derivative of a quadratic model at its center point.

Symmetric Hessians and their bilinear maps

theorem ViscositySolns.isSymmetricBilinear_hessianBilinearMap {n : ℕ} {X : Hessian n} (hX : ∀ (i j : Fin n), X i j = X j i) : IsSymmetricBilinear (hessianBilinearMap X)

The bilinear map of an entrywise-symmetric coordinate Hessian is symmetric.

theorem ViscositySolns.symHessian_add_smul_one_symm {n : ℕ} (X : Hessian n) (c : ℝ) (i j : Fin n) : (symHessian X + c • 1) i j = (symHessian X + c • 1) j i

The symmetric part of a Hessian, shifted by a multiple of the identity, is entrywise symmetric.

theorem ViscositySolns.quadraticModel_add_smul_one {n : ℕ} (x0 : Point n) (r : ℝ) (p : Point n) (X : Hessian n) (c : ℝ) (x : Point n) : quadraticModel x0 r p (X + c • 1) x = quadraticModel x0 r p X x + c / 2 * (x - x0) ⬝ᵥ (x - x0)

Shifting the Hessian of a quadratic model by c • 1 adds the coordinate quadratic form c / 2 * <x - x0, x - x0>.

theorem ViscositySolns.quadraticModel_center {n : ℕ} (x0 : Point n) (r : ℝ) (p : Point n) (X : Hessian n) : quadraticModel x0 r p X x0 = r

The value of a quadratic model at its center point.

Eventual bounds from semijet remainders

theorem ViscositySolns.SemijetRemainder.eventually_abs_le {n : ℕ} {C : Set (Point n)} {x0 : Point n} {rho : Point n → ℝ} (hρ : SemijetRemainder C x0 rho) {c : ℝ} (hc : 0 < c) : ∀ᶠ (x : Point n) in nhdsWithin x0 C, |rho x| ≤ c * ‖x - x0‖ ^ 2

A semijet remainder is eventually dominated in absolute value by any positive multiple of the squared distance to the base point.

The forward direction: subsolutions satisfy the smooth inequality

theorem ViscositySolns.hasSecondOrderExpansionWithin_of_contDiff_two_isOpen {n : ℕ} {C : Set (Point n)} {φ : Point n → ℝ} {x0 : Point n} {J : Jet n} (hC : IsOpen C) (hx0 : x0 ∈ C) (hφ : ContDiff ℝ 2 φ) (hDφ : fderiv ℝ φ x0 = J.toFirstDerivative) (hD2φ : fderiv ℝ (fderiv ℝ φ) x0 = J.toSecondDerivative) : HasSecondOrderExpansionWithin C φ x0 J

On an open domain, a globally C² function has the abstract second-order expansion associated to its canonical global fderiv data.

theorem ViscositySolns.ViscositySubsolution.smoothTestFunctionSubsolution {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} (hu : ViscositySubsolution C F u) (hC : IsOpen C) : SmoothTestFunctionSubsolution C F u

On an open domain, a viscosity subsolution satisfies the smooth test-function inequality for the canonical global derivative data of any C² function touching it from above.

theorem ViscositySolns.ViscositySupersolution.smoothTestFunctionSupersolution {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} (hu : ViscositySupersolution C F u) (hC : IsOpen C) : SmoothTestFunctionSupersolution C F u

On an open domain, a viscosity supersolution satisfies the smooth test-function inequality for the canonical global derivative data of any C² function touching it from below.

The converse direction: the epsilon-inflated quadratic model

theorem ViscositySolns.smooth_test_key_subsolution {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} {x : Point n} {J : Jet n} (h : ∀ y ∈ C, ∀ (φ : Point n → ℝ), ContDiff ℝ 2 φ → TouchesAboveOn C u φ y → F y (u y) (linearMapGradient (fderiv ℝ φ y)) (bilinearMapHessian (fderiv ℝ (fderiv ℝ φ) y)) ≤ 0) (hx : x ∈ C) (hJ : J ∈ Superjet C u x) {ε : ℝ} (hε : 0 < ε) : F x (u x) J.gradient (symHessian J.hessian + ε • 1) ≤ 0

Core computation for the converse: applying the smooth test-function inequality of a subsolution candidate to the inflated quadratic model quadraticModel x (u x) J.gradient (symHessian J.hessian + ε • 1) yields the operator inequality at the shifted symmetric Hessian.

theorem ViscositySolns.smooth_test_key_supersolution {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} {x : Point n} {J : Jet n} (h : ∀ y ∈ C, ∀ (φ : Point n → ℝ), ContDiff ℝ 2 φ → TouchesBelowOn C u φ y → 0 ≤ F y (u y) (linearMapGradient (fderiv ℝ φ y)) (bilinearMapHessian (fderiv ℝ (fderiv ℝ φ) y))) (hx : x ∈ C) (hJ : J ∈ Subjet C u x) {ε : ℝ} (hε : 0 < ε) : 0 ≤ F x (u x) J.gradient (symHessian J.hessian + -ε • 1)

Core computation for the converse (supersolution side): the smooth test-function inequality applied to the deflated quadratic model yields the operator inequality at the shifted symmetric Hessian.

theorem ViscositySolns.ViscositySubsolution.of_smoothTestFunctionSubsolution {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} (hFcont : ∀ (x : Point n) (r : ℝ) (p : Point n), Continuous fun (X : Hessian n) => F x r p X) (hFsym : HessianSymmetricInvariant F) (h : SmoothTestFunctionSubsolution C F u) : ViscositySubsolution C F u

The converse direction for subsolutions: on any domain, the smooth test-function formulation implies the semijet formulation, provided the operator is continuous in the Hessian argument and depends on it only through its symmetric part.

theorem ViscositySolns.ViscositySupersolution.of_smoothTestFunctionSupersolution {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} (hFcont : ∀ (x : Point n) (r : ℝ) (p : Point n), Continuous fun (X : Hessian n) => F x r p X) (hFsym : HessianSymmetricInvariant F) (h : SmoothTestFunctionSupersolution C F u) : ViscositySupersolution C F u

The converse direction for supersolutions: the smooth test-function formulation implies the semijet formulation, provided the operator is continuous in the Hessian argument and depends on it only through its symmetric part.

The characterizations

theorem ViscositySolns.viscositySubsolution_iff_smoothTestFunctionSubsolution {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} (hC : IsOpen C) (hFcont : ∀ (x : Point n) (r : ℝ) (p : Point n), Continuous fun (X : Hessian n) => F x r p X) (hFsym : HessianSymmetricInvariant F) : ViscositySubsolution C F u ↔ SmoothTestFunctionSubsolution C F u

CIL Section 2, smooth test-function characterization of subsolutions: on an open domain, for an operator continuous in the Hessian argument and depending on it only through its symmetric part, the semijet and smooth test-function formulations of viscosity subsolutions coincide.

theorem ViscositySolns.viscositySupersolution_iff_smoothTestFunctionSupersolution {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} (hC : IsOpen C) (hFcont : ∀ (x : Point n) (r : ℝ) (p : Point n), Continuous fun (X : Hessian n) => F x r p X) (hFsym : HessianSymmetricInvariant F) : ViscositySupersolution C F u ↔ SmoothTestFunctionSupersolution C F u

CIL Section 2, smooth test-function characterization of supersolutions: on an open domain, for an operator continuous in the Hessian argument and depending on it only through its symmetric part, the semijet and smooth test-function formulations of viscosity supersolutions coincide.