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

Affine linear operator forms

This file contains reusable declarations for operators that are affine in the unknown r, the gradient p, and the Hessian X.

The Hessian contribution is represented by a function G x X. Concrete trace-form linear elliptic operators can later instantiate G; the monotonicity theorems in this file only require the standard antitonicity condition in the Hessian variable.

def ViscositySolns.affineSecondOrderOperator {n : ℕ} (G : Point n → Hessian n → ℝ) (b : Point n → Point n) (c f : Point n → ℝ) : Operator n

An affine second-order operator of the form G x X + b x · p + c x * r - f x.

Equations

• ViscositySolns.affineSecondOrderOperator G b c f x r p X = G x X + b x ⬝ᵥ p + c x * r - f x

@[simp]

theorem ViscositySolns.affineSecondOrderOperator_apply {n : ℕ} (G : Point n → Hessian n → ℝ) (b : Point n → Point n) (c f : Point n → ℝ) (x : Point n) (r : ℝ) (p : Point n) (X : Hessian n) : affineSecondOrderOperator G b c f x r p X = G x X + b x ⬝ᵥ p + c x * r - f x

theorem ViscositySolns.degenerateElliptic_affineSecondOrderOperator {n : ℕ} {G : Point n → Hessian n → ℝ} {b : Point n → Point n} {c f : Point n → ℝ} (hG : ∀ (x : Point n) (X Y : Hessian n), Y ≤ X → G x X ≤ G x Y) : DegenerateElliptic (affineSecondOrderOperator G b c f)

If the Hessian contribution G x X is antitone in X, then the affine operator is degenerate elliptic.

theorem ViscositySolns.proper_affineSecondOrderOperator {n : ℕ} {G : Point n → Hessian n → ℝ} {b : Point n → Point n} {c f : Point n → ℝ} (hG : ∀ (x : Point n) (X Y : Hessian n), Y ≤ X → G x X ≤ G x Y) (hc : ∀ (x : Point n), 0 ≤ c x) : Proper (affineSecondOrderOperator G b c f)

If the Hessian contribution is antitone in X and 0 ≤ c x for every x, then the affine operator is proper.

theorem ViscositySolns.operatorContinuous_affineSecondOrderOperator {n : ℕ} {G : Point n → Hessian n → ℝ} {b : Point n → Point n} {c f : Point n → ℝ} (hG : Continuous fun (z : (Point n × ℝ) × Jet n) => G z.1.1 z.2.hessian) (hb : Continuous fun (z : (Point n × ℝ) × Jet n) => b z.1.1 ⬝ᵥ z.2.gradient) (hc : Continuous fun (z : (Point n × ℝ) × Jet n) => c z.1.1 * z.1.2) (hf : Continuous fun (z : (Point n × ℝ) × Jet n) => f z.1.1) : OperatorContinuous (affineSecondOrderOperator G b c f)

Continuity of an affine second-order operator follows from continuity of its four graph-space summands.

def ViscositySolns.firstOrderOperator {n : ℕ} (G : Point n → ℝ → Point n → ℝ) : Operator n

A first-order operator, independent of its Hessian argument.

Equations

• ViscositySolns.firstOrderOperator G x r p _X = G x r p

@[simp]

theorem ViscositySolns.firstOrderOperator_apply {n : ℕ} (G : Point n → ℝ → Point n → ℝ) (x : Point n) (r : ℝ) (p : Point n) (X : Hessian n) : firstOrderOperator G x r p X = G x r p

theorem ViscositySolns.degenerateElliptic_firstOrderOperator {n : ℕ} (G : Point n → ℝ → Point n → ℝ) : DegenerateElliptic (firstOrderOperator G)

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

theorem ViscositySolns.operatorContinuous_firstOrderOperator {n : ℕ} {G : Point n → ℝ → Point n → ℝ} (hG : Continuous fun (z : (Point n × ℝ) × Jet n) => G z.1.1 z.1.2 z.2.gradient) : OperatorContinuous (firstOrderOperator G)

Continuity of a first-order operator follows from continuity of its graph-space expression.

def ViscositySolns.zeroOrderOperator {n : ℕ} (g : Point n → ℝ → ℝ) : Operator n

A zero-order operator, independent of gradient and Hessian arguments.

Equations

• ViscositySolns.zeroOrderOperator g x r _p _X = g x r

@[simp]

theorem ViscositySolns.zeroOrderOperator_apply {n : ℕ} (g : Point n → ℝ → ℝ) (x : Point n) (r : ℝ) (p : Point n) (X : Hessian n) : zeroOrderOperator g x r p X = g x r

theorem ViscositySolns.degenerateElliptic_zeroOrderOperator {n : ℕ} (g : Point n → ℝ → ℝ) : DegenerateElliptic (zeroOrderOperator g)

theorem ViscositySolns.proper_zeroOrderOperator {n : ℕ} {g : Point n → ℝ → ℝ} (hmono : ∀ (x : Point n), Monotone fun (r : ℝ) => g x r) : Proper (zeroOrderOperator g)

theorem ViscositySolns.operatorContinuous_zeroOrderOperator {n : ℕ} {g : Point n → ℝ → ℝ} (hg : Continuous fun (z : (Point n × ℝ) × Jet n) => g z.1.1 z.1.2) : OperatorContinuous (zeroOrderOperator g)

Continuity of a zero-order operator follows from continuity of its graph-space expression.