Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Stability under finite maxima and minima #
This file proves the first finite lattice stability results for viscosity solutions: maxima of subsolutions and minima of supersolutions.
theorem
ViscositySolns.ViscositySubsolution.max
{n : ℕ}
{C : Set (Point n)}
{F : Operator n}
{u v : Point n → ℝ}
(hu : ViscositySubsolution C F u)
(hv : ViscositySubsolution C F v)
:
ViscositySubsolution C F fun (y : Point n) => Max.max (u y) (v y)
The pointwise maximum of two viscosity subsolutions of the same equation is a viscosity subsolution. No properness hypothesis is needed for this finite same-operator statement, because every contact point has an active branch with the same value.
theorem
ViscositySolns.ViscositySupersolution.min
{n : ℕ}
{C : Set (Point n)}
{F : Operator n}
{u v : Point n → ℝ}
(hu : ViscositySupersolution C F u)
(hv : ViscositySupersolution C F v)
:
ViscositySupersolution C F fun (y : Point n) => Min.min (u y) (v y)
The pointwise minimum of two viscosity supersolutions of the same equation is a viscosity supersolution.