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

Operator comparison condition for the Ishii matrix inequality (TraceForm)

Part of the specialization of the structural continuity condition for operators to the matrix relation used in the quadratic doubling-of-variables argument. Split from OperatorCondition.lean; see the umbrella module docstring.

def ViscositySolns.TraceSecondOrderComponentBoundsOn {n : ℕ} (C : Set (Point n)) (R : Set ℝ) (A : Point n → Hessian n) (b : Point n → Point n) (c f : Point n → ℝ) (ωA ωb ωc ωf : ℝ → ℝ) : Prop

The four component estimates for the trace-form operator

F z r p Z = -trace ((A z) * Z) + b z · p + c z * r - f z.

In quantified mathematical form, this predicate says that, for every α > 0, every x, y ∈ C, every r ∈ R, and every X, Y satisfying IshiiMatrixRelation α x y X Y, the trace, drift, zeroth-order, and source-term differences are respectively bounded above by the four comparison moduli evaluated at α * ‖x - y‖ ^ 2 + ‖x - y‖.

Equations

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

theorem ViscositySolns.TraceSecondOrderComponentBoundsOn.of_norm_bounds {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} {ωA ωb ωc ωf : ℝ → ℝ} (hmonoA : Monotone ωA) (hmonob : Monotone ωb) (hmonoc : Monotone ωc) (hmonof : Monotone ωf) (htrace : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → -(A y * X).trace - -(A x * X).trace ≤ ωA ‖x - y‖) (hb : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → b y ⬝ᵥ quadraticPenaltyGradientLeft α x y - b x ⬝ᵥ quadraticPenaltyGradientLeft α x y ≤ ωb ‖x - y‖) (hc : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → c y * r - c x * r ≤ ωc ‖x - y‖) (hf : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → f x - f y ≤ ωf ‖x - y‖) : TraceSecondOrderComponentBoundsOn C R A b c f ωA ωb ωc ωf

It is enough to prove the four trace-form component estimates with the moduli evaluated at ‖x - y‖, provided the four moduli are monotone.

Indeed, if α > 0, then ‖x - y‖ ≤ α * ‖x - y‖ ^ 2 + ‖x - y‖.

theorem ViscositySolns.ishiiOperatorComparisonConditionOn_traceSecondOrderOperator_of_component_bounds {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} {ωA ωb ωc ωf : ℝ → ℝ} (hωA : ComparisonModulus ωA) (hωb : ComparisonModulus ωb) (hωc : ComparisonModulus ωc) (hωf : ComparisonModulus ωf) (hA : ∀ z ∈ C, Matrix.PosSemidef (A z)) (htrace : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → -(A y * X).trace - -(A x * X).trace ≤ ωA (α * ‖x - y‖ ^ 2 + ‖x - y‖)) (hb : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → b y ⬝ᵥ quadraticPenaltyGradientLeft α x y - b x ⬝ᵥ quadraticPenaltyGradientLeft α x y ≤ ωb (α * ‖x - y‖ ^ 2 + ‖x - y‖)) (hc : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → c y * r - c x * r ≤ ωc (α * ‖x - y‖ ^ 2 + ‖x - y‖)) (hf : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → f x - f y ≤ ωf (α * ‖x - y‖ ^ 2 + ‖x - y‖)) : IshiiOperatorComparisonConditionOn C R (traceSecondOrderOperator A b c f)

Let A, b, c, and f define the trace-form operator

F z r p Z = -trace ((A z) * Z) + b z · p + c z * r - f z.

Suppose that A z is positive semidefinite for every z ∈ C. Suppose also that there are comparison moduli ωA, ωb, ωc, and ωf such that, for every α > 0, every x, y ∈ C, every r ∈ R, and every X, Y satisfying IshiiMatrixRelation α x y X Y, the following four inequalities hold, where s = α * ‖x - y‖ ^ 2 + ‖x - y‖:

• -trace ((A y) * X) - (-trace ((A x) * X)) ≤ ωA s;
• b y · (α • (x - y)) - b x · (α • (x - y)) ≤ ωb s;
• c y * r - c x * r ≤ ωc s;
• f x - f y ≤ ωf s.

Then F satisfies the Ishii structural condition on C and R.

theorem ViscositySolns.TraceSecondOrderComponentBoundsOn.ishiiOperatorComparisonConditionOn {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} {ωA ωb ωc ωf : ℝ → ℝ} (hωA : ComparisonModulus ωA) (hωb : ComparisonModulus ωb) (hωc : ComparisonModulus ωc) (hωf : ComparisonModulus ωf) (hA : ∀ z ∈ C, Matrix.PosSemidef (A z)) (hbounds : TraceSecondOrderComponentBoundsOn C R A b c f ωA ωb ωc ωf) : IshiiOperatorComparisonConditionOn C R (traceSecondOrderOperator A b c f)

Packaged form of ishiiOperatorComparisonConditionOn_traceSecondOrderOperator_of_component_bounds.

theorem ViscositySolns.ishiiOperatorComparisonConditionOn_traceSecondOrderOperator_of_component_norm_bounds {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} {ωA ωb ωc ωf : ℝ → ℝ} (hωA : ComparisonModulus ωA) (hωb : ComparisonModulus ωb) (hωc : ComparisonModulus ωc) (hωf : ComparisonModulus ωf) (hmonoA : Monotone ωA) (hmonob : Monotone ωb) (hmonoc : Monotone ωc) (hmonof : Monotone ωf) (hA : ∀ z ∈ C, Matrix.PosSemidef (A z)) (htrace : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → -(A y * X).trace - -(A x * X).trace ≤ ωA ‖x - y‖) (hb : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → b y ⬝ᵥ quadraticPenaltyGradientLeft α x y - b x ⬝ᵥ quadraticPenaltyGradientLeft α x y ≤ ωb ‖x - y‖) (hc : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → c y * r - c x * r ≤ ωc ‖x - y‖) (hf : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → f x - f y ≤ ωf ‖x - y‖) : IshiiOperatorComparisonConditionOn C R (traceSecondOrderOperator A b c f)

Direct trace-form constructor from component estimates stated at the distance scale ‖x - y‖.

Assume the four component differences of the trace-form operator are bounded above by monotone comparison moduli evaluated at ‖x - y‖. If A z is positive semidefinite for every z ∈ C, then the trace-form operator satisfies IshiiOperatorComparisonConditionOn C R.

structure ViscositySolns.TraceSecondOrderOperatorComparisonHypothesesOn {n : ℕ} (C : Set (Point n)) (R : Set ℝ) (A : Point n → Hessian n) (b : Point n → Point n) (c f : Point n → ℝ) : Type

Packaged hypotheses for a trace-form second-order operator on a spatial set C and scalar set R.

In quantified mathematical form, this structure consists of:

• four comparison moduli ωA, ωb, ωc, and ωf;
• positive semidefiniteness of A z for every point z;
• nonnegativity of c z for every point z;
• continuity of the trace-form operator;
• the four component estimates in TraceSecondOrderComponentBoundsOn C R.

These hypotheses imply properness, operator continuity, and IshiiOperatorComparisonConditionOn C R for traceSecondOrderOperator A b c f.

• ωA : ℝ → ℝ

  Comparison modulus for the second-order coefficient.

• ωb : ℝ → ℝ

  Comparison modulus for the drift coefficient.

• ωc : ℝ → ℝ

  Comparison modulus for the zero-order coefficient.

• ωf : ℝ → ℝ

  Comparison modulus for the source term.

• comparisonModulus_trace : ComparisonModulus self.ωA
• comparisonModulus_drift : ComparisonModulus self.ωb
• comparisonModulus_zeroth : ComparisonModulus self.ωc
• comparisonModulus_source : ComparisonModulus self.ωf
• positive_semidefinite (z : Point n) : Matrix.PosSemidef (A z)
• zeroth_nonnegative (z : Point n) : 0 ≤ c z
• operator_continuous : OperatorContinuous (traceSecondOrderOperator A b c f)
• component_bounds : TraceSecondOrderComponentBoundsOn C R A b c f self.ωA self.ωb self.ωc self.ωf

def ViscositySolns.TraceSecondOrderOperatorComparisonHypothesesOn.ofComponentBounds {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} {ωA ωb ωc ωf : ℝ → ℝ} (hωA : ComparisonModulus ωA) (hωb : ComparisonModulus ωb) (hωc : ComparisonModulus ωc) (hωf : ComparisonModulus ωf) (hA : ∀ (z : Point n), Matrix.PosSemidef (A z)) (hc : ∀ (z : Point n), 0 ≤ c z) (hcont : OperatorContinuous (traceSecondOrderOperator A b c f)) (hbounds : TraceSecondOrderComponentBoundsOn C R A b c f ωA ωb ωc ωf) : TraceSecondOrderOperatorComparisonHypothesesOn C R A b c f

Constructor for the packaged trace-form comparison hypotheses from component estimates stated at the comparison scale α * ‖x - y‖ ^ 2 + ‖x - y‖.

Equations

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

def ViscositySolns.TraceSecondOrderOperatorComparisonHypothesesOn.ofComponentNormBounds {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} {ωA ωb ωc ωf : ℝ → ℝ} (hωA : ComparisonModulus ωA) (hωb : ComparisonModulus ωb) (hωc : ComparisonModulus ωc) (hωf : ComparisonModulus ωf) (hmonoA : Monotone ωA) (hmonob : Monotone ωb) (hmonoc : Monotone ωc) (hmonof : Monotone ωf) (hA : ∀ (z : Point n), Matrix.PosSemidef (A z)) (hc_nonneg : ∀ (z : Point n), 0 ≤ c z) (hcont : OperatorContinuous (traceSecondOrderOperator A b c f)) (htrace : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → -(A y * X).trace - -(A x * X).trace ≤ ωA ‖x - y‖) (hb : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → b y ⬝ᵥ quadraticPenaltyGradientLeft α x y - b x ⬝ᵥ quadraticPenaltyGradientLeft α x y ≤ ωb ‖x - y‖) (hc : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → c y * r - c x * r ≤ ωc ‖x - y‖) (hf : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → f x - f y ≤ ωf ‖x - y‖) : TraceSecondOrderOperatorComparisonHypothesesOn C R A b c f

Constructor for the packaged trace-form comparison hypotheses from component estimates stated at the distance scale ‖x - y‖.

In quantified mathematical form, if the four moduli are monotone and each of the four component differences is bounded above by the corresponding modulus evaluated at ‖x - y‖, then the component estimates at α * ‖x - y‖ ^ 2 + ‖x - y‖ follow, and hence the packaged trace-form hypotheses hold.

Equations

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

def ViscositySolns.TraceSecondOrderOperatorComparisonHypothesesOn.ofBoundsAndContinuousSummands {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} {ωA ωb ωc ωf : ℝ → ℝ} (hωA : ComparisonModulus ωA) (hωb : ComparisonModulus ωb) (hωc : ComparisonModulus ωc) (hωf : ComparisonModulus ωf) (hA : ∀ (z : Point n), Matrix.PosSemidef (A z)) (hc_nonneg : ∀ (z : Point n), 0 ≤ c z) (hAcont : Continuous fun (z : (Point n × ℝ) × Jet n) => -(A z.1.1 * z.2.hessian).trace) (hbcont : Continuous fun (z : (Point n × ℝ) × Jet n) => b z.1.1 ⬝ᵥ z.2.gradient) (hccont : Continuous fun (z : (Point n × ℝ) × Jet n) => c z.1.1 * z.1.2) (hfcont : Continuous fun (z : (Point n × ℝ) × Jet n) => f z.1.1) (hbounds : TraceSecondOrderComponentBoundsOn C R A b c f ωA ωb ωc ωf) : TraceSecondOrderOperatorComparisonHypothesesOn C R A b c f

Constructor for the packaged trace-form comparison hypotheses from component estimates and continuity of the four graph-space summands.

In quantified mathematical form, the continuity hypotheses are continuity of the functions

• (x, r, p, X) ↦ -trace ((A x) * X);
• (x, r, p, X) ↦ b x · p;
• (x, r, p, X) ↦ c x * r;
• (x, r, p, X) ↦ f x.

Together with the component estimates at α * ‖x - y‖ ^ 2 + ‖x - y‖, these hypotheses construct TraceSecondOrderOperatorComparisonHypothesesOn C R A b c f.

Equations

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

def ViscositySolns.TraceSecondOrderOperatorComparisonHypothesesOn.ofNormBoundsAndContinuousSummands {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} {ωA ωb ωc ωf : ℝ → ℝ} (hωA : ComparisonModulus ωA) (hωb : ComparisonModulus ωb) (hωc : ComparisonModulus ωc) (hωf : ComparisonModulus ωf) (hmonoA : Monotone ωA) (hmonob : Monotone ωb) (hmonoc : Monotone ωc) (hmonof : Monotone ωf) (hA : ∀ (z : Point n), Matrix.PosSemidef (A z)) (hc_nonneg : ∀ (z : Point n), 0 ≤ c z) (hAcont : Continuous fun (z : (Point n × ℝ) × Jet n) => -(A z.1.1 * z.2.hessian).trace) (hbcont : Continuous fun (z : (Point n × ℝ) × Jet n) => b z.1.1 ⬝ᵥ z.2.gradient) (hccont : Continuous fun (z : (Point n × ℝ) × Jet n) => c z.1.1 * z.1.2) (hfcont : Continuous fun (z : (Point n × ℝ) × Jet n) => f z.1.1) (htrace : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → -(A y * X).trace - -(A x * X).trace ≤ ωA ‖x - y‖) (hb : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → b y ⬝ᵥ quadraticPenaltyGradientLeft α x y - b x ⬝ᵥ quadraticPenaltyGradientLeft α x y ≤ ωb ‖x - y‖) (hc : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → c y * r - c x * r ≤ ωc ‖x - y‖) (hf : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → f x - f y ≤ ωf ‖x - y‖) : TraceSecondOrderOperatorComparisonHypothesesOn C R A b c f

Constructor for the packaged trace-form comparison hypotheses from component estimates stated at the distance scale ‖x - y‖ and continuity of the four graph-space summands.

Equations

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

theorem ViscositySolns.TraceSecondOrderOperatorComparisonHypothesesOn.proper {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} (h : TraceSecondOrderOperatorComparisonHypothesesOn C R A b c f) : Proper (traceSecondOrderOperator A b c f)

theorem ViscositySolns.TraceSecondOrderOperatorComparisonHypothesesOn.ishiiOperatorComparisonConditionOn {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} (h : TraceSecondOrderOperatorComparisonHypothesesOn C R A b c f) : IshiiOperatorComparisonConditionOn C R (traceSecondOrderOperator A b c f)

theorem ViscositySolns.TraceSecondOrderOperatorComparisonHypothesesOn.ishii_supOperator {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {C : Set (Point n)} {R : Set ℝ} {A : ι → Point n → Hessian n} {b : ι → Point n → Point n} {c f : ι → Point n → ℝ} (h : (a : ι) → TraceSecondOrderOperatorComparisonHypothesesOn C R (A a) (b a) (c a) (f a)) : IshiiOperatorComparisonConditionOn C R (supOperator fun (a : ι) => traceSecondOrderOperator (A a) (b a) (c a) (f a))

Finite pointwise suprema of trace-form operators satisfy the Ishii structural condition when every branch satisfies the packaged trace-form hypotheses.

theorem ViscositySolns.TraceSecondOrderOperatorComparisonHypothesesOn.proper_supOperator {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {C : Set (Point n)} {R : Set ℝ} {A : ι → Point n → Hessian n} {b : ι → Point n → Point n} {c f : ι → Point n → ℝ} (h : (a : ι) → TraceSecondOrderOperatorComparisonHypothesesOn C R (A a) (b a) (c a) (f a)) : Proper (supOperator fun (a : ι) => traceSecondOrderOperator (A a) (b a) (c a) (f a))

Finite pointwise suprema of trace-form operators are proper when every branch satisfies the packaged trace-form hypotheses.

theorem ViscositySolns.TraceSecondOrderOperatorComparisonHypothesesOn.operatorContinuous_supOperator {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {C : Set (Point n)} {R : Set ℝ} {A : ι → Point n → Hessian n} {b : ι → Point n → Point n} {c f : ι → Point n → ℝ} (h : (a : ι) → TraceSecondOrderOperatorComparisonHypothesesOn C R (A a) (b a) (c a) (f a)) : OperatorContinuous (supOperator fun (a : ι) => traceSecondOrderOperator (A a) (b a) (c a) (f a))

Finite pointwise suprema of trace-form operators are continuous when every branch satisfies the packaged trace-form hypotheses.

theorem ViscositySolns.TraceSecondOrderOperatorComparisonHypothesesOn.ishii_infOperator {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {C : Set (Point n)} {R : Set ℝ} {A : ι → Point n → Hessian n} {b : ι → Point n → Point n} {c f : ι → Point n → ℝ} (h : (a : ι) → TraceSecondOrderOperatorComparisonHypothesesOn C R (A a) (b a) (c a) (f a)) : IshiiOperatorComparisonConditionOn C R (infOperator fun (a : ι) => traceSecondOrderOperator (A a) (b a) (c a) (f a))

Finite pointwise infima of trace-form operators satisfy the Ishii structural condition when every branch satisfies the packaged trace-form hypotheses.

theorem ViscositySolns.TraceSecondOrderOperatorComparisonHypothesesOn.proper_infOperator {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {C : Set (Point n)} {R : Set ℝ} {A : ι → Point n → Hessian n} {b : ι → Point n → Point n} {c f : ι → Point n → ℝ} (h : (a : ι) → TraceSecondOrderOperatorComparisonHypothesesOn C R (A a) (b a) (c a) (f a)) : Proper (infOperator fun (a : ι) => traceSecondOrderOperator (A a) (b a) (c a) (f a))

Finite pointwise infima of trace-form operators are proper when every branch satisfies the packaged trace-form hypotheses.

theorem ViscositySolns.TraceSecondOrderOperatorComparisonHypothesesOn.operatorContinuous_infOperator {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {C : Set (Point n)} {R : Set ℝ} {A : ι → Point n → Hessian n} {b : ι → Point n → Point n} {c f : ι → Point n → ℝ} (h : (a : ι) → TraceSecondOrderOperatorComparisonHypothesesOn C R (A a) (b a) (c a) (f a)) : OperatorContinuous (infOperator fun (a : ι) => traceSecondOrderOperator (A a) (b a) (c a) (f a))

Finite pointwise infima of trace-form operators are continuous when every branch satisfies the packaged trace-form hypotheses.