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

Proper and degenerate elliptic operators

This file contains the basic monotonicity hypotheses for fully nonlinear second-order operators, together with small operator-level constructions used by the solution theory.

def ViscositySolns.DegenerateElliptic {n : ℕ} (F : Operator n) : Prop

Degenerate ellipticity: F is antitone in the Hessian variable for the Loewner order on matrices. This is condition (0.2) in CIL.

Equations

• ViscositySolns.DegenerateElliptic F = ∀ (x : ViscositySolns.Point n) (r : ℝ) (p : ViscositySolns.Point n) (X Y : ViscositySolns.Hessian n), Y ≤ X → F x r p X ≤ F x r p Y

def ViscositySolns.HessianSymmetricInvariant {n : ℕ} (F : Operator n) : Prop

The operator only depends on the symmetric part of its Hessian argument.

Classical viscosity equations are evaluated on symmetric Hessians; this predicate records that an operator written on all coordinate matrices ignores the skew-symmetric part.

Equations

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

def ViscositySolns.Proper {n : ℕ} (F : Operator n) : Prop

Properness: F is nondecreasing in the scalar variable and degenerate elliptic. This packages the two monotonicity assumptions in CIL condition (0.1).

Equations

• ViscositySolns.Proper F = ((∀ (x p : ViscositySolns.Point n) (X : ViscositySolns.Hessian n) {r s : ℝ}, r ≤ s → F x r p X ≤ F x s p X) ∧ ViscositySolns.DegenerateElliptic F)

theorem ViscositySolns.Proper.mono_value {n : ℕ} {F : Operator n} (hF : Proper F) (x p : Point n) (X : Hessian n) {r s : ℝ} (hrs : r ≤ s) : F x r p X ≤ F x s p X

theorem ViscositySolns.Proper.degenerateElliptic {n : ℕ} {F : Operator n} (hF : Proper F) : DegenerateElliptic F

def ViscositySolns.operatorGraphEval {n : ℕ} (F : Operator n) (z : (Point n × ℝ) × Jet n) : ℝ

Evaluate a second-order operator on a point of the closed-semijet graph space.

Equations

• ViscositySolns.operatorGraphEval F z = F z.1.1 z.1.2 z.2.gradient z.2.hessian

def ViscositySolns.negOperator {n : ℕ} (F : Operator n) : Operator n

The negated operator: negOperator F x r p X = -F x (-r) (-p) (-X).

This is the operator for which -u is a supersolution whenever u is a subsolution of F = 0; it encodes the symmetry principle of CIL Remark 2.6.

Equations

• ViscositySolns.negOperator F x r p X = -F x (-r) (-p) (-X)

@[simp]

theorem ViscositySolns.negOperator_negOperator {n : ℕ} (F : Operator n) : negOperator (negOperator F) = F