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

Trace-form linear second-order operators

This file records the standard trace-form Hessian contribution

X ↦ - trace ((A x) * X).

In the usual elliptic case, A x is positive semidefinite for every x. The matrix lemma connecting that hypothesis to monotonicity is kept as a separate future theorem: if A x is positive semidefinite and Y ≤ X, then - trace ((A x) * X) ≤ - trace ((A x) * Y).

def ViscositySolns.traceHessianContribution {n : ℕ} (A : Point n → Hessian n) (x : Point n) (X : Hessian n) : ℝ

The Hessian contribution - trace ((A x) * X).

Equations

• ViscositySolns.traceHessianContribution A x X = -(A x * X).trace

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

The linear second-order operator - trace ((A x) * X) + b x · p + c x * r - f x.

Equations

• ViscositySolns.traceSecondOrderOperator A b c f = ViscositySolns.affineSecondOrderOperator (ViscositySolns.traceHessianContribution A) b c f

@[simp]

theorem ViscositySolns.traceHessianContribution_apply {n : ℕ} (A : Point n → Hessian n) (x : Point n) (X : Hessian n) : traceHessianContribution A x X = -(A x * X).trace

@[simp]

theorem ViscositySolns.traceSecondOrderOperator_apply {n : ℕ} (A : Point n → Hessian n) (b : Point n → Point n) (c f : Point n → ℝ) (x : Point n) (r : ℝ) (p : Point n) (X : Hessian n) : traceSecondOrderOperator A b c f x r p X = -(A x * X).trace + b x ⬝ᵥ p + c x * r - f x

theorem ViscositySolns.degenerateElliptic_traceSecondOrderOperator {n : ℕ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} (hA : ∀ (x : Point n) (X Y : Hessian n), Y ≤ X → -(A x * X).trace ≤ -(A x * Y).trace) : DegenerateElliptic (traceSecondOrderOperator A b c f)

If for every x, X, and Y, the implication Y ≤ X -> - trace ((A x) * X) ≤ - trace ((A x) * Y) holds, then the trace-form operator is degenerate elliptic.

theorem ViscositySolns.proper_traceSecondOrderOperator {n : ℕ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} (hA : ∀ (x : Point n) (X Y : Hessian n), Y ≤ X → -(A x * X).trace ≤ -(A x * Y).trace) (hc : ∀ (x : Point n), 0 ≤ c x) : Proper (traceSecondOrderOperator A b c f)

If the trace-form Hessian contribution is antitone in the Loewner order and 0 ≤ c x for every x, then the trace-form operator is proper.

theorem ViscositySolns.operatorContinuous_traceSecondOrderOperator {n : ℕ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} (hA : Continuous fun (z : (Point n × ℝ) × Jet n) => -(A z.1.1 * z.2.hessian).trace) (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 (traceSecondOrderOperator A b c f)

Continuity of the trace-form operator follows from continuity of the trace-form Hessian summand and the other affine summands.

theorem ViscositySolns.trace_mul_nonneg_of_posSemidef {n : ℕ} {A B : Hessian n} (hA : Matrix.PosSemidef A) (hB : Matrix.PosSemidef B) : 0 ≤ (A * B).trace

If A and B are positive semidefinite real matrices, then 0 ≤ trace (A * B).

theorem ViscositySolns.trace_mul_antitone_of_posSemidef {n : ℕ} {A : Hessian n} (hA : Matrix.PosSemidef A) (X Y : Hessian n) : Y ≤ X → -(A * X).trace ≤ -(A * Y).trace

If A is positive semidefinite and Y ≤ X, then the trace-form Hessian contribution is antitone: - trace (A * X) ≤ - trace (A * Y).

theorem ViscositySolns.degenerateElliptic_traceSecondOrderOperator_of_posSemidef {n : ℕ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} (hA : ∀ (x : Point n), Matrix.PosSemidef (A x)) : DegenerateElliptic (traceSecondOrderOperator A b c f)

If A x is positive semidefinite for every x, then the trace-form operator is degenerate elliptic.

theorem ViscositySolns.proper_traceSecondOrderOperator_of_posSemidef {n : ℕ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} (hA : ∀ (x : Point n), Matrix.PosSemidef (A x)) (hc : ∀ (x : Point n), 0 ≤ c x) : Proper (traceSecondOrderOperator A b c f)

If A x is positive semidefinite and 0 ≤ c x for every x, then the trace-form operator is proper.

theorem ViscositySolns.trace_diagonal_mul_antitone_of_nonneg {n : ℕ} {a : Fin n → ℝ} (ha : ∀ (i : Fin n), 0 ≤ a i) (X Y : Hessian n) : Y ≤ X → -(Matrix.diagonal a * X).trace ≤ -(Matrix.diagonal a * Y).trace

For a diagonal coefficient matrix with nonnegative diagonal entries, the trace-form Hessian contribution is antitone in the Loewner order: if Y ≤ X, then - trace ((diagonal a) * X) ≤ - trace ((diagonal a) * Y).

theorem ViscositySolns.degenerateElliptic_traceSecondOrderOperator_diagonal {n : ℕ} {a : Point n → Fin n → ℝ} {b : Point n → Point n} {c f : Point n → ℝ} (ha : ∀ (x : Point n) (i : Fin n), 0 ≤ a x i) : DegenerateElliptic (traceSecondOrderOperator (fun (x : Point n) => Matrix.diagonal (a x)) b c f)

The trace-form operator with a diagonal nonnegative Hessian coefficient is degenerate elliptic.

theorem ViscositySolns.proper_traceSecondOrderOperator_diagonal {n : ℕ} {a : Point n → Fin n → ℝ} {b : Point n → Point n} {c f : Point n → ℝ} (ha : ∀ (x : Point n) (i : Fin n), 0 ≤ a x i) (hc : ∀ (x : Point n), 0 ≤ c x) : Proper (traceSecondOrderOperator (fun (x : Point n) => Matrix.diagonal (a x)) b c f)

The trace-form operator with a diagonal nonnegative Hessian coefficient and 0 ≤ c x is proper.