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

Operator comparison condition for the Ishii matrix inequality (IshiiCondition)

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.

theorem ViscositySolns.comparisonModulus_zero : ComparisonModulus fun (_t : ℝ) => 0

The zero function is a comparison modulus.

def ViscositySolns.IshiiOperatorComparisonConditionOn {n : ℕ} (C : Set (Point n)) (R : Set ℝ) (F : Operator n) : Prop

Structural continuity condition with the matrix relation

-(3 * α) [I 0; 0 I] ≤ [X 0; 0 -Y] ≤ 3 [α I -α I; -α I α I].

Equations

• ViscositySolns.IshiiOperatorComparisonConditionOn C R F = ViscositySolns.OperatorComparisonConditionOn C R ViscositySolns.IshiiMatrixRelation F

theorem ViscositySolns.IshiiOperatorComparisonConditionOn.mono_scalar_set {n : ℕ} {C : Set (Point n)} {R S : Set ℝ} {F : Operator n} (hF : IshiiOperatorComparisonConditionOn C S F) (hRS : R ⊆ S) : IshiiOperatorComparisonConditionOn C R F

theorem ViscositySolns.IshiiOperatorComparisonConditionOn.mono_spatial_set {n : ℕ} {C D : Set (Point n)} {R : Set ℝ} {F : Operator n} (hF : IshiiOperatorComparisonConditionOn D R F) (hCD : C ⊆ D) : IshiiOperatorComparisonConditionOn C R F

theorem ViscositySolns.IshiiOperatorComparisonConditionOn.bound {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} (hF : IshiiOperatorComparisonConditionOn C R F) : ∃ (ω : ℝ → ℝ), ComparisonModulus ω ∧ ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → F y r (quadraticPenaltyGradientLeft α x y) Y - F x r (quadraticPenaltyGradientLeft α x y) X ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖)

Unpack the specialized structural condition.

If α > 0, x, y ∈ C, r ∈ R, and X, Y satisfy the Ishii block matrix inequality, then the operator difference is bounded by the comparison modulus.

theorem ViscositySolns.IshiiOperatorComparisonConditionOn.of_nonpositive_difference {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} (hF : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → F y r (quadraticPenaltyGradientLeft α x y) Y - F x r (quadraticPenaltyGradientLeft α x y) X ≤ 0) : IshiiOperatorComparisonConditionOn C R F

If the operator difference in the Ishii structural condition is always nonpositive, then the condition holds with the zero comparison modulus.

theorem ViscositySolns.IshiiOperatorComparisonConditionOn.of_norm_bound {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} {ω : ℝ → ℝ} (hω : ComparisonModulus ω) (hmono : Monotone ω) (hbound : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → F y r (quadraticPenaltyGradientLeft α x y) Y - F x r (quadraticPenaltyGradientLeft α x y) X ≤ ω ‖x - y‖) : IshiiOperatorComparisonConditionOn C R F

Let ω be a comparison modulus which is monotone on real numbers. Suppose that for every α > 0, every x, y ∈ C, every r ∈ R, and every X, Y satisfying IshiiMatrixRelation α x y X Y,

F y r (α • (x - y)) Y - F x r (α • (x - y)) X ≤ ω ‖x - y‖.

Then F satisfies the Ishii structural condition, because ‖x - y‖ ≤ α * ‖x - y‖ ^ 2 + ‖x - y‖.

theorem ViscositySolns.IshiiOperatorComparisonConditionOn.supOperator {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {C : Set (Point n)} {R : Set ℝ} {F : ι → Operator n} (hF : ∀ (a : ι), IshiiOperatorComparisonConditionOn C R (F a)) : IshiiOperatorComparisonConditionOn C R (ViscositySolns.supOperator F)

Let F a, for a in a nonempty finite type, be operators. If every F a satisfies the Ishii structural condition on C and R, then the pointwise supremum operator

(x, r, p, X) ↦ max_a F a x r p X

also satisfies the Ishii structural condition on C and R.

theorem ViscositySolns.IshiiOperatorComparisonConditionOn.supOperator_of_common_modulus {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {C : Set (Point n)} {R : Set ℝ} {F : ι → Operator n} {ω : ℝ → ℝ} (hω : ComparisonModulus ω) (hbound : ∀ (a : ι) (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → F a y r (quadraticPenaltyGradientLeft α x y) Y - F a x r (quadraticPenaltyGradientLeft α x y) X ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖)) : IshiiOperatorComparisonConditionOn C R (ViscositySolns.supOperator F)

Common-modulus version for finite pointwise suprema.

Suppose one comparison modulus ω bounds the Ishii operator difference for every branch F a. Then the pointwise supremum of the finite family F satisfies IshiiOperatorComparisonConditionOn C R.

theorem ViscositySolns.IshiiOperatorComparisonConditionOn.infOperator {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {C : Set (Point n)} {R : Set ℝ} {F : ι → Operator n} (hF : ∀ (a : ι), IshiiOperatorComparisonConditionOn C R (F a)) : IshiiOperatorComparisonConditionOn C R (ViscositySolns.infOperator F)

Let F a, for a in a nonempty finite type, be operators. If every F a satisfies the Ishii structural condition on C and R, then the pointwise infimum operator

(x, r, p, X) ↦ min_a F a x r p X

also satisfies the Ishii structural condition on C and R.

theorem ViscositySolns.IshiiOperatorComparisonConditionOn.infOperator_of_common_modulus {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {C : Set (Point n)} {R : Set ℝ} {F : ι → Operator n} {ω : ℝ → ℝ} (hω : ComparisonModulus ω) (hbound : ∀ (a : ι) (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → F a y r (quadraticPenaltyGradientLeft α x y) Y - F a x r (quadraticPenaltyGradientLeft α x y) X ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖)) : IshiiOperatorComparisonConditionOn C R (ViscositySolns.infOperator F)

Common-modulus version for finite pointwise infima.

Suppose one comparison modulus ω bounds the Ishii operator difference for every branch F a. Then the pointwise infimum of the finite family F satisfies IshiiOperatorComparisonConditionOn C R.

theorem ViscositySolns.IshiiOperatorComparisonConditionOn.addOperator {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F G : Operator n} (hF : IshiiOperatorComparisonConditionOn C R F) (hG : IshiiOperatorComparisonConditionOn C R G) : IshiiOperatorComparisonConditionOn C R (ViscositySolns.addOperator F G)

If two operators satisfy the Ishii structural comparison condition on the same set C and scalar set R, then their pointwise sum satisfies the same condition.

theorem ViscositySolns.IshiiOperatorComparisonConditionOn.smulOperator_nonneg {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} {a : ℝ} (ha : 0 ≤ a) (hF : IshiiOperatorComparisonConditionOn C R F) : IshiiOperatorComparisonConditionOn C R (smulOperator a F)

If an operator satisfies the Ishii structural comparison condition on C and R, then every nonnegative scalar multiple of it satisfies the same condition.

theorem ViscositySolns.IshiiOperatorComparisonConditionOn.constOperator {n : ℕ} (C : Set (Point n)) (R : Set ℝ) (c : ℝ) : IshiiOperatorComparisonConditionOn C R (ViscositySolns.constOperator c)

Every constant operator satisfies the Ishii structural comparison condition, for any spatial set and scalar set.

theorem ViscositySolns.ishiiOperatorComparisonConditionOn_of_independent_spatial_hessian {n : ℕ} (C : Set (Point n)) (R : Set ℝ) (G : ℝ → Point n → ℝ) : IshiiOperatorComparisonConditionOn C R fun (_x : Point n) (r : ℝ) (p : Point n) (_X : Hessian n) => G r p

An operator of the form F x r p X = G r p, with no dependence on the spatial variable x or Hessian variable X, satisfies the Ishii structural condition with the zero comparison modulus.

theorem ViscositySolns.ishiiOperatorComparisonConditionOn_of_independent_spatial_degenerateElliptic {n : ℕ} (C : Set (Point n)) (R : Set ℝ) (G : ℝ → Point n → Hessian n → ℝ) (hG : ∀ (r : ℝ) (p : Point n) (X Y : Hessian n), Y ≤ X → G r p X ≤ G r p Y) : IshiiOperatorComparisonConditionOn C R fun (_x : Point n) (r : ℝ) (p : Point n) (X : Hessian n) => G r p X

Let G r p X be independent of the spatial variable. Suppose that for every r, p, X, and Y, the implication Y ≤ X -> G r p X ≤ G r p Y holds. Then the operator F x r p X = G r p X satisfies the Ishii structural condition with the zero comparison modulus.

theorem ViscositySolns.ishiiOperatorComparisonConditionOn_zeroOrderOperator_of_norm_bound {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {g : Point n → ℝ → ℝ} {ω : ℝ → ℝ} (hω : ComparisonModulus ω) (hmono : Monotone ω) (hg : ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, g y r - g x r ≤ ω ‖x - y‖) : IshiiOperatorComparisonConditionOn C R (zeroOrderOperator g)

Let ω be a monotone comparison modulus. Suppose that for every x, y ∈ C and every r ∈ R,

g y r - g x r ≤ ω ‖x - y‖.

Then the zero-order operator F x r p X = g x r satisfies the Ishii structural condition.

theorem ViscositySolns.ishiiOperatorComparisonConditionOn_firstOrderOperator_of_bound {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {G : Point n → ℝ → Point n → ℝ} {ω : ℝ → ℝ} (hω : ComparisonModulus ω) (hG : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → G y r (quadraticPenaltyGradientLeft α x y) - G x r (quadraticPenaltyGradientLeft α x y) ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖)) : IshiiOperatorComparisonConditionOn C R (firstOrderOperator G)

Let G x r p be a first-order operator expression. Suppose that for every α > 0, every x, y ∈ C, every r ∈ R, and every X, Y satisfying IshiiMatrixRelation α x y X Y, one has

G y r (α • (x - y)) - G x r (α • (x - y)) ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖).

Then the first-order operator F x r p X = G x r p satisfies the Ishii structural condition.

theorem ViscositySolns.ishiiOperatorComparisonConditionOn_affineSecondOrderOperator_of_same_hessian_bound {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {G : Point n → Hessian n → ℝ} {b : Point n → Point n} {c f : Point n → ℝ} {ω : ℝ → ℝ} (hω : ComparisonModulus ω) (hG : ∀ z ∈ C, ∀ (X Y : Hessian n), Y ≤ X → G z X ≤ G z Y) (hbound : ∀ (α : ℝ), 0 < α → ∀ x ∈ C, ∀ y ∈ C, ∀ r ∈ R, ∀ (X Y : Hessian n), IshiiMatrixRelation α x y X Y → G y X + b y ⬝ᵥ quadraticPenaltyGradientLeft α x y + c y * r - f y - (G x X + b x ⬝ᵥ quadraticPenaltyGradientLeft α x y + c x * r - f x) ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖)) : IshiiOperatorComparisonConditionOn C R (affineSecondOrderOperator G b c f)

Let G x X + b x · p + c x * r - f x be an affine second-order operator. Assume:

1. for every z ∈ C, the Hessian contribution is antitone in the sense that Y ≤ X -> G z X ≤ G z Y;
2. for every α > 0, every x, y ∈ C, every r ∈ R, and every X, Y satisfying IshiiMatrixRelation α x y X Y, the same-Hessian coefficient difference satisfies

`(G y X + b y · (α • (x - y)) + c y * r - f y)

• (G x X + b x · (α • (x - y)) + c x * r - f x) ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖)`.

Then the affine second-order operator satisfies the Ishii structural condition. The proof uses IshiiMatrixRelation α x y X Y -> X ≤ Y to replace the Y Hessian in the left operator by the same Hessian X.

theorem ViscositySolns.ishiiOperatorComparisonConditionOn_const_traceSecondOrderOperator {n : ℕ} (C : Set (Point n)) (R : Set ℝ) {A : Hessian n} {b : Point n} {c f : ℝ} (hA : Matrix.PosSemidef A) : IshiiOperatorComparisonConditionOn C R (traceSecondOrderOperator (fun (_x : Point n) => A) (fun (_x : Point n) => b) (fun (_x : Point n) => c) fun (_x : Point n) => f)

Let A be a positive semidefinite real matrix. Then the constant-coefficient trace-form operator

F x r p X = -trace (A * X) + b · p + c * r - f

satisfies the Ishii structural condition with the zero comparison modulus.

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

Let ω be a comparison modulus. Suppose that:

1. for every z ∈ C, the matrix A z is positive semidefinite;
2. for every α > 0, every x, y ∈ C, every r ∈ R, and every X, Y satisfying IshiiMatrixRelation α x y X Y, the same-Hessian coefficient difference satisfies

`(-trace ((A y) * X) + b y · (α • (x - y)) + c y * r - f y)

• (-trace ((A x) * X) + b x · (α • (x - y)) + c x * r - f x) ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖)`.

Then the trace-form operator F z r p Z = -trace ((A z) * Z) + b z · p + c z * r - f z satisfies the Ishii structural condition. The proof uses IshiiMatrixRelation α x y X Y -> X ≤ Y and the positive semidefiniteness of A y to compare the Y-Hessian term with the X-Hessian term.