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

Basic examples of proper operators

This file collects small reusable constructors for operators satisfying the monotonicity, continuity, and boundedness hypotheses used in the viscosity solution theory.

def ViscositySolns.constOperator {n : ℕ} (c : ℝ) : Operator n

The constant operator.

Equations

• ViscositySolns.constOperator c _x _r _p _X = c

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

Pointwise sum of two operators.

Equations

• ViscositySolns.addOperator F G x r p X = F x r p X + G x r p X

def ViscositySolns.smulOperator {n : ℕ} (a : ℝ) (F : Operator n) : Operator n

Scalar multiple of an operator.

Equations

• ViscositySolns.smulOperator a F x r p X = a * F x r p X

@[simp]

theorem ViscositySolns.constOperator_apply {n : ℕ} (c : ℝ) (x : Point n) (r : ℝ) (p : Point n) (X : Hessian n) : constOperator c x r p X = c

@[simp]

theorem ViscositySolns.addOperator_apply {n : ℕ} (F G : Operator n) (x : Point n) (r : ℝ) (p : Point n) (X : Hessian n) : addOperator F G x r p X = F x r p X + G x r p X

@[simp]

theorem ViscositySolns.smulOperator_apply {n : ℕ} (a : ℝ) (F : Operator n) (x : Point n) (r : ℝ) (p : Point n) (X : Hessian n) : smulOperator a F x r p X = a * F x r p X

theorem ViscositySolns.degenerateElliptic_of_independent_hessian {n : ℕ} (G : Point n → ℝ → Point n → ℝ) : DegenerateElliptic fun (x : Point n) (r : ℝ) (p : Point n) (_X : Hessian n) => G x r p

An operator independent of its Hessian argument is automatically degenerate elliptic.

theorem ViscositySolns.proper_of_independent_hessian {n : ℕ} (G : Point n → ℝ → Point n → ℝ) (hmono : ∀ (x p : Point n), Monotone fun (r : ℝ) => G x r p) : Proper fun (x : Point n) (r : ℝ) (p : Point n) (_X : Hessian n) => G x r p

An operator independent of its Hessian argument is proper when it is monotone in the scalar argument.

theorem ViscositySolns.proper_zero_operator {n : ℕ} : Proper fun (_x : Point n) (_r : ℝ) (_p : Point n) (_X : Hessian n) => 0

The zero operator is proper.

theorem ViscositySolns.degenerateElliptic_constOperator {n : ℕ} (c : ℝ) : DegenerateElliptic (constOperator c)

theorem ViscositySolns.proper_constOperator {n : ℕ} (c : ℝ) : Proper (constOperator c)

theorem ViscositySolns.DegenerateElliptic.add {n : ℕ} {F G : Operator n} (hF : DegenerateElliptic F) (hG : DegenerateElliptic G) : DegenerateElliptic (addOperator F G)

theorem ViscositySolns.Proper.add {n : ℕ} {F G : Operator n} (hF : Proper F) (hG : Proper G) : Proper (addOperator F G)

theorem ViscositySolns.DegenerateElliptic.smul_nonneg {n : ℕ} {F : Operator n} {a : ℝ} (ha : 0 ≤ a) (hF : DegenerateElliptic F) : DegenerateElliptic (smulOperator a F)

theorem ViscositySolns.Proper.smul_nonneg {n : ℕ} {F : Operator n} {a : ℝ} (ha : 0 ≤ a) (hF : Proper F) : Proper (smulOperator a F)

theorem ViscositySolns.operatorContinuous_constOperator {n : ℕ} (c : ℝ) : OperatorContinuous (constOperator c)

theorem ViscositySolns.OperatorContinuous.add {n : ℕ} {F G : Operator n} (hF : OperatorContinuous F) (hG : OperatorContinuous G) : OperatorContinuous (addOperator F G)

theorem ViscositySolns.OperatorContinuous.smul {n : ℕ} {F : Operator n} (a : ℝ) (hF : OperatorContinuous F) : OperatorContinuous (smulOperator a F)

theorem ViscositySolns.operatorLocallyBounded_constOperator {n : ℕ} (c : ℝ) : OperatorLocallyBounded (constOperator c)

theorem ViscositySolns.OperatorLocallyBounded.add {n : ℕ} {F G : Operator n} (hF : OperatorLocallyBounded F) (hG : OperatorLocallyBounded G) : OperatorLocallyBounded (addOperator F G)

theorem ViscositySolns.OperatorLocallyBounded.smul {n : ℕ} {F : Operator n} (a : ℝ) (hF : OperatorLocallyBounded F) : OperatorLocallyBounded (smulOperator a F)

theorem ViscositySolns.OperatorLocallyBoundedOn.add {n : ℕ} {S : Set ((Point n × ℝ) × Jet n)} {F G : Operator n} (hF : OperatorLocallyBoundedOn S F) (hG : OperatorLocallyBoundedOn S G) : OperatorLocallyBoundedOn S (addOperator F G)

theorem ViscositySolns.OperatorLocallyBoundedOn.smul {n : ℕ} {S : Set ((Point n × ℝ) × Jet n)} {F : Operator n} (a : ℝ) (hF : OperatorLocallyBoundedOn S F) : OperatorLocallyBoundedOn S (smulOperator a F)