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

Viscosity subsolutions, supersolutions, and solutions

This file contains viscosity solution predicates, their test-function formulation, closed-semijet consequences, and solution-level negation duality.

theorem ViscositySolns.upperSemicontinuousOn_neg {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} (hu : UpperSemicontinuousOn u C) : LowerSemicontinuousOn (fun (x : Point n) => -u x) C

theorem ViscositySolns.lowerSemicontinuousOn_neg {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} (hu : LowerSemicontinuousOn u C) : UpperSemicontinuousOn (fun (x : Point n) => -u x) C

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

Viscosity subsolution of F = 0 on C, using superjets.

Equations

• ViscositySolns.ViscositySubsolution C F u = (UpperSemicontinuousOn u C ∧ ∀ x ∈ C, ∀ J ∈ ViscositySolns.Superjet C u x, F x (u x) J.gradient J.hessian ≤ 0)

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

Viscosity supersolution of F = 0 on C, using subjets.

Equations

• ViscositySolns.ViscositySupersolution C F u = (LowerSemicontinuousOn u C ∧ ∀ x ∈ C, ∀ J ∈ ViscositySolns.Subjet C u x, 0 ≤ F x (u x) J.gradient J.hessian)

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

The test-function formulation of viscosity subsolutions, using functions with a second-order expansion such that {y | u y <= φ y} is a relative neighborhood of the contact point in C.

Equations

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

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

The test-function formulation of viscosity supersolutions, using functions with a second-order expansion such that {y | φ y <= u y} is a relative neighborhood of the contact point in C.

Equations

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

theorem ViscositySolns.viscositySubsolution_iff_testFunctionSubsolution {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} : ViscositySubsolution C F u ↔ TestFunctionSubsolution C F u

The jet and abstract test-function formulations of subsolutions are equivalent.

theorem ViscositySolns.viscositySupersolution_iff_testFunctionSupersolution {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} : ViscositySupersolution C F u ↔ TestFunctionSupersolution C F u

The jet and abstract test-function formulations of supersolutions are equivalent.

theorem ViscositySolns.ViscositySubsolution.of_touchesAbove_hasSecondOrderExpansionWithin {n : ℕ} {C : Set (Point n)} {F : Operator n} {u φ : Point n → ℝ} {x : Point n} {J : Jet n} (hu : ViscositySubsolution C F u) (hx : x ∈ C) (htouch : TouchesAboveOn C u φ x) (hφ : HasSecondOrderExpansionWithin C φ x J) : F x (u x) J.gradient J.hessian ≤ 0

A viscosity subsolution satisfies the expected inequality for every touching test function with a second-order expansion.

theorem ViscositySolns.ViscositySupersolution.of_touchesBelow_hasSecondOrderExpansionWithin {n : ℕ} {C : Set (Point n)} {F : Operator n} {u φ : Point n → ℝ} {x : Point n} {J : Jet n} (hu : ViscositySupersolution C F u) (hx : x ∈ C) (htouch : TouchesBelowOn C u φ x) (hφ : HasSecondOrderExpansionWithin C φ x J) : 0 ≤ F x (u x) J.gradient J.hessian

A viscosity supersolution satisfies the expected inequality for every touching test function with a second-order expansion.

theorem ViscositySolns.ViscositySubsolution.closedSuperjet_le_of_isClosed {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} {x : Point n} {J : Jet n} (hu : ViscositySubsolution C F u) (hclosed : IsClosed {z : (Point n × ℝ) × Jet n | operatorGraphEval F z ≤ 0}) (hJ : J ∈ ClosedSuperjet C u x) : F x (u x) J.gradient J.hessian ≤ 0

theorem ViscositySolns.ViscositySupersolution.closedSubjet_nonneg_of_isClosed {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} {x : Point n} {J : Jet n} (hu : ViscositySupersolution C F u) (hclosed : IsClosed {z : (Point n × ℝ) × Jet n | 0 ≤ operatorGraphEval F z}) (hJ : J ∈ ClosedSubjet C u x) : 0 ≤ F x (u x) J.gradient J.hessian

theorem ViscositySolns.ViscositySubsolution.closedSuperjet_le_of_continuous {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} {x : Point n} {J : Jet n} (hu : ViscositySubsolution C F u) (hF : Continuous (operatorGraphEval F)) (hJ : J ∈ ClosedSuperjet C u x) : F x (u x) J.gradient J.hessian ≤ 0

theorem ViscositySolns.ViscositySubsolution.closedSuperjet_le_of_operatorContinuous {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} {x : Point n} {J : Jet n} (hu : ViscositySubsolution C F u) (hF : OperatorContinuous F) (hJ : J ∈ ClosedSuperjet C u x) : F x (u x) J.gradient J.hessian ≤ 0

theorem ViscositySolns.ViscositySupersolution.closedSubjet_nonneg_of_continuous {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} {x : Point n} {J : Jet n} (hu : ViscositySupersolution C F u) (hF : Continuous (operatorGraphEval F)) (hJ : J ∈ ClosedSubjet C u x) : 0 ≤ F x (u x) J.gradient J.hessian

theorem ViscositySolns.ViscositySupersolution.closedSubjet_nonneg_of_operatorContinuous {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} {x : Point n} {J : Jet n} (hu : ViscositySupersolution C F u) (hF : OperatorContinuous F) (hJ : J ∈ ClosedSubjet C u x) : 0 ≤ F x (u x) J.gradient J.hessian

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

Viscosity solution of F = 0 on C.

Equations

• ViscositySolns.ViscositySolution C F u = (ViscositySolns.ViscositySubsolution C F u ∧ ViscositySolns.ViscositySupersolution C F u)

theorem ViscositySolns.ViscositySolution.subsolution {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} (hu : ViscositySolution C F u) : ViscositySubsolution C F u

theorem ViscositySolns.ViscositySolution.supersolution {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} (hu : ViscositySolution C F u) : ViscositySupersolution C F u

theorem ViscositySolns.viscositySubsolution_neg_iff {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} : ViscositySubsolution C F u ↔ ViscositySupersolution C (negOperator F) fun (y : Point n) => -u y

Neg duality for subsolutions (CIL Remark 2.6): u is a viscosity subsolution of F = 0 if and only if -u is a viscosity supersolution of negOperator F = 0.

theorem ViscositySolns.viscositySupersolution_neg_iff {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} : ViscositySupersolution C F u ↔ ViscositySubsolution C (negOperator F) fun (y : Point n) => -u y

Neg duality for supersolutions: u is a viscosity supersolution of F = 0 if and only if -u is a viscosity subsolution of negOperator F = 0.

theorem ViscositySolns.viscositySolution_neg_iff {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} : ViscositySolution C F u ↔ ViscositySolution C (negOperator F) fun (y : Point n) => -u y

Neg duality for viscosity solutions: u solves F = 0 exactly when -u solves negOperator F = 0.