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

Algebraic comparison consequences after Ishii's lemma.

theorem ViscositySolns.exists_closedSemijet_inequalities_of_quadraticPenaltyIshiiConclusion {n : ℕ} {C : Set (Point n)} {F : Operator n} {u v : Point n → ℝ} {α : ℝ} {x y : Point n} (hu : ViscositySubsolution C F u) (hv : ViscositySupersolution C F v) (hF : OperatorContinuous F) (hI : QuadraticPenaltyIshiiConclusion C C u v α x y) : ∃ (X : Hessian n) (Y : Hessian n), { gradient := quadraticPenaltyGradientLeft α x y, hessian := X } ∈ ClosedSuperjet C u x ∧ { gradient := quadraticPenaltyGradientLeft α x y, hessian := Y } ∈ ClosedSubjet C v y ∧ IshiiMatrixRelation α x y X Y ∧ F x (u x) (quadraticPenaltyGradientLeft α x y) X ≤ 0 ∧ 0 ≤ F y (v y) (quadraticPenaltyGradientLeft α x y) Y

If the quadratic-penalty conclusion of Ishii's lemma holds at (x, y), then the corresponding closed superjet and closed subjet produce the viscosity inequalities for the same first-derivative vector α • (x - y).

theorem ViscositySolns.exists_nonnegative_operator_gap_of_quadraticPenaltyIshiiConclusion {n : ℕ} {C : Set (Point n)} {F : Operator n} {u v : Point n → ℝ} {α : ℝ} {x y : Point n} (hu : ViscositySubsolution C F u) (hv : ViscositySupersolution C F v) (hF : OperatorContinuous F) (hproper : Proper F) (hvyux : v y ≤ u x) (hI : QuadraticPenaltyIshiiConclusion C C u v α x y) : ∃ (X : Hessian n) (Y : Hessian n), IshiiMatrixRelation α x y X Y ∧ 0 ≤ F y (u x) (quadraticPenaltyGradientLeft α x y) Y - F x (u x) (quadraticPenaltyGradientLeft α x y) X

Assume the conclusion of Ishii's lemma at (x, y). If v y ≤ u x, then properness implies that the operator gap

F y (u x) (α • (x - y)) Y - F x (u x) (α • (x - y)) X

is nonnegative for the matrices supplied by the closed semijets.

theorem ViscositySolns.exists_operator_gap_bounds_of_quadraticPenaltyIshiiConclusion {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} {u v : Point n → ℝ} {α : ℝ} {x y : Point n} (hu : ViscositySubsolution C F u) (hv : ViscositySupersolution C F v) (hFcont : OperatorContinuous F) (hproper : Proper F) (hcomp : IshiiOperatorComparisonConditionOn C R F) (hα : 0 < α) (hx : x ∈ C) (hy : y ∈ C) (hr : u x ∈ R) (hvyux : v y ≤ u x) (hI : QuadraticPenaltyIshiiConclusion C C u v α x y) : ∃ (ω : ℝ → ℝ), ComparisonModulus ω ∧ ∃ (X : Hessian n) (Y : Hessian n), IshiiMatrixRelation α x y X Y ∧ 0 ≤ F y (u x) (quadraticPenaltyGradientLeft α x y) Y - F x (u x) (quadraticPenaltyGradientLeft α x y) X ∧ F y (u x) (quadraticPenaltyGradientLeft α x y) Y - F x (u x) (quadraticPenaltyGradientLeft α x y) X ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖)

Under the specialized structural condition, the same operator gap is bounded above by a comparison modulus. Thus the matrices supplied by Ishii's lemma satisfy both inequalities

0 ≤ gap and gap ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖).

theorem ViscositySolns.exists_strict_operator_gap_of_quadraticPenaltyIshiiConclusion {n : ℕ} {C : Set (Point n)} {F : Operator n} {u v : Point n → ℝ} {ε α : ℝ} {x y : Point n} (hu : StrictViscositySubsolution C F ε u) (hv : ViscositySupersolution C F v) (hF : OperatorContinuous F) (hproper : Proper F) (hvyux : v y ≤ u x) (hI : QuadraticPenaltyIshiiConclusion C C u v α x y) : ∃ (X : Hessian n) (Y : Hessian n), IshiiMatrixRelation α x y X Y ∧ ε ≤ F y (u x) (quadraticPenaltyGradientLeft α x y) Y - F x (u x) (quadraticPenaltyGradientLeft α x y) X

Assume the conclusion of Ishii's lemma at (x, y). If u is a strict subsolution with margin ε and v y ≤ u x, then properness implies that the operator gap

F y (u x) (α • (x - y)) Y - F x (u x) (α • (x - y)) X

is at least ε for the matrices supplied by the closed semijets.

theorem ViscositySolns.eventually_comparisonScale_pos_of_strict_eventually_isMaxOn {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {F : Operator n} {u v : Point n → ℝ} {ε : ℝ} {α : ι → ℝ} {x y : ι → Point n} (hu : StrictViscositySubsolution C F ε u) (hv : ViscositySupersolution C F v) (hFcont : OperatorContinuous F) (hproper : Proper F) (hIshii : QuadraticPenaltyIshiiLemmaOn C C u v) (hε : 0 < ε) (hdata : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ v (y i) ≤ u (x i) ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) : ∀ᶠ (i : ι) in l, 0 < α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖

Let ε > 0, let u be a strict subsolution with margin ε, and let v be a supersolution. Assume properness, operator continuity, and QuadraticPenaltyIshiiLemmaOn C C u v.

If, for all i in a set belonging to l, α i > 0, x i ∈ C, y i ∈ C, v (y i) ≤ u (x i), and (x i, y i) maximizes the doubled-variable objective on C × C, then, for all i in a set belonging to l,

0 < α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖.

Indeed, if the displayed quantity were zero for one of these indices, then x i = y i. Ishii's lemma would produce matrices X and Y with X ≤ Y. Degenerate ellipticity would make the corresponding operator difference nonpositive, contradicting the strict subsolution gap ε > 0.

theorem ViscositySolns.exists_strict_operator_gap_bounds_of_quadraticPenaltyIshiiConclusion {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} {u v : Point n → ℝ} {ε α : ℝ} {x y : Point n} (hu : StrictViscositySubsolution C F ε u) (hv : ViscositySupersolution C F v) (hFcont : OperatorContinuous F) (hproper : Proper F) (hcomp : IshiiOperatorComparisonConditionOn C R F) (hα : 0 < α) (hx : x ∈ C) (hy : y ∈ C) (hr : u x ∈ R) (hvyux : v y ≤ u x) (hI : QuadraticPenaltyIshiiConclusion C C u v α x y) : ∃ (ω : ℝ → ℝ), ComparisonModulus ω ∧ ∃ (X : Hessian n) (Y : Hessian n), IshiiMatrixRelation α x y X Y ∧ ε ≤ F y (u x) (quadraticPenaltyGradientLeft α x y) Y - F x (u x) (quadraticPenaltyGradientLeft α x y) X ∧ F y (u x) (quadraticPenaltyGradientLeft α x y) Y - F x (u x) (quadraticPenaltyGradientLeft α x y) X ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖)

With a strict subsolution margin ε, the matrices supplied by Ishii's lemma satisfy both inequalities

ε ≤ gap and gap ≤ ω (α * ‖x - y‖ ^ 2 + ‖x - y‖).

theorem ViscositySolns.not_eventually_strict_isMaxOn_doubledObjective_of_tendsto_scale {n : ℕ} {ι : Type u_1} {l : Filter ι} [l.NeBot] {C : Set (Point n)} {R : Set ℝ} {F : Operator n} {u v : Point n → ℝ} {ε : ℝ} {α : ι → ℝ} {x y : ι → Point n} (hu : StrictViscositySubsolution C F ε u) (hv : ViscositySupersolution C F v) (hFcont : OperatorContinuous F) (hproper : Proper F) (hcomp : IshiiOperatorComparisonConditionOn C R F) (hIshii : QuadraticPenaltyIshiiLemmaOn C C u v) (hε : 0 < ε) (hdata : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ u (x i) ∈ R ∧ v (y i) ≤ u (x i) ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) : ¬Filter.Tendsto (fun (i : ι) => α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖) l (nhdsWithin 0 (Set.Ioi 0))

Let ε > 0, let u be a strict subsolution with margin ε, and let v be a supersolution. Assume properness, operator continuity, the Ishii structural condition, and QuadraticPenaltyIshiiLemmaOn C C u v.

Let α i, x i, and y i be data indexed by a nontrivial filter l. Suppose that for all i in a set belonging to l:

• α i > 0;
• x i ∈ C and y i ∈ C;
• u (x i) ∈ R;
• v (y i) ≤ u (x i);
• (x i, y i) maximizes (x', y') ↦ u x' - v y' - (α i / 2) * ∑ j, (x' j - y' j)^2 on C × C.

Then the associated scales α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖ cannot converge to 0 through positive values along l.

theorem ViscositySolns.strictComparison_of_doubledVariableLocalizationAlong {n : ℕ} {ι : Type u_1} {l : Filter ι} [l.NeBot] {C : Set (Point n)} {R : Set ℝ} {F : Operator n} {u v : Point n → ℝ} {ε : ℝ} {α : ι → ℝ} {x y : ι → Point n} (hu : StrictViscositySubsolution C F ε u) (hv : ViscositySupersolution C F v) (hFcont : OperatorContinuous F) (hproper : Proper F) (hcomp : IshiiOperatorComparisonConditionOn C R F) (hIshii : QuadraticPenaltyIshiiLemmaOn C C u v) (hε : 0 < ε) (hloc : StrictDoubledVariableLocalizationAlongOn C R u v l α x y) : ComparisonConclusionOn C u v

Strict comparison conditional on the filter form of the doubled-variable localization hypothesis and on Ishii's lemma.

Assume ε > 0, u is a strict subsolution with margin ε, v is a supersolution, F is proper and continuous, and F satisfies the Ishii structural condition. Assume also QuadraticPenaltyIshiiLemmaOn C C u v.

If failure of u ≤ v somewhere on C produces doubled-variable maximum data along a nontrivial filter whose scales tend to 0 through positive values, then u ≤ v at every point of C.

theorem ViscositySolns.comparison_of_localizedStrictificationAlong {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} {u v : Point n → ℝ} (hproper : Proper F) (hFcont : OperatorContinuous F) (hcomp : IshiiOperatorComparisonConditionOn C R F) (hv : ViscositySupersolution C F v) (hstrictify : LocalizedStrictificationAlongOn C R F u v) : ComparisonConclusionOn C u v

Comparison from strictification and natural-number indexed doubled-variable localization on C.

In quantified mathematical form, assume F is proper and continuous, assume the Ishii structural condition on C and R, and assume that v is a viscosity supersolution on C. If, for every η > 0, there are ε > 0, a function w, and natural-number indexed selected doubled-variable data satisfying the conclusions in LocalizedStrictificationAlongOn C R F u v, then u x ≤ v x for every x ∈ C.

theorem ViscositySolns.comparison_of_constantShiftLocalizedStrictificationAlongData {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} {u v : Point n → ℝ} (hproper : Proper F) (hFcont : OperatorContinuous F) (hcomp : IshiiOperatorComparisonConditionOn C R F) (hu : ViscositySubsolution C F u) (hv : ViscositySupersolution C F v) (hdata : ConstantShiftLocalizedStrictificationAlongDataOn C R F u v) : ComparisonConclusionOn C u v

Natural-number indexed constant-shift data imply comparison for a fixed pair of functions.

In quantified mathematical form, assume:

• F is proper and continuous;
• F satisfies IshiiOperatorComparisonConditionOn C R F;
• u is a viscosity subsolution of F = 0 on C;
• v is a viscosity supersolution of F = 0 on C;
• for every η > 0, there exist δ > 0, ε > 0, and sequences α : ℕ -> ℝ, x y : ℕ -> ℝ^n satisfying the conditions in ConstantShiftLocalizedStrictificationAlongDataOn C R F u v.

Then u z ≤ v z for every z ∈ C.

theorem ViscositySolns.comparison_of_constantShiftLocalizedStrictificationAlongCore {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} {u v : Point n → ℝ} (hproper : Proper F) (hFcont : OperatorContinuous F) (hcomp : IshiiOperatorComparisonConditionOn C R F) (hu : ViscositySubsolution C F u) (hv : ViscositySupersolution C F v) (huR : ScalarRangeOn C R u) (hR : ClosedUnderSubNonneg R) (hIshii : QuadraticPenaltyIshiiLemmaOn C C u v) (hcore : ∀ (η : ℝ), 0 < η → ∃ (δ : ℝ) (ε : ℝ) (α : ℕ → ℝ) (x : ℕ → Point n) (y : ℕ → Point n), 0 < δ ∧ δ ≤ η ∧ 0 < ε ∧ UniformScalarDecreaseOn C F δ ε ∧ StrictDoubledVariableLocalizationAlongOn C R (fun (z : Point n) => u z - δ) v Filter.atTop α x y) : ComparisonConclusionOn C u v

Reduced natural-number indexed constant-shift data imply comparison for a fixed pair of functions.

In quantified mathematical form, suppose:

• F is proper and continuous;
• F satisfies IshiiOperatorComparisonConditionOn C R F;
• u is a viscosity subsolution of F = 0 on C;
• v is a viscosity supersolution of F = 0 on C;
• u x ∈ R for every x ∈ C;
• if r ∈ R and δ ≥ 0, then r - δ ∈ R;
• the quadratic-penalty Ishii lemma holds for u and v on C × C;
• for every η > 0, there exist δ > 0, ε > 0, and sequences α : ℕ -> ℝ, x y : ℕ -> ℝ^n such that δ ≤ η, UniformScalarDecreaseOn C F δ ε holds, and StrictDoubledVariableLocalizationAlongOn C R (fun z => u z - δ) v atTop α x y holds.

Then u z ≤ v z for every z ∈ C.

theorem ViscositySolns.properBoundaryComparisonStatementOn_of_localizedStrictificationAlongConstructor {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} (hconstruct : LocalizedBoundaryStrictificationAlongConstructorOn C R F) : ProperBoundaryComparisonStatementOn C R F

If the ordinary boundary-value hypotheses construct natural-number indexed localized strictification, then the boundary comparison statement on C follows.

In quantified mathematical form, assume F is proper and continuous and satisfies the Ishii structural condition on C and R. If, whenever C is nonempty and a pair u, v satisfies the ordinary boundary-value hypotheses on C, those hypotheses imply LocalizedStrictificationAlongOn C R F u v, then the ordinary boundary-value hypotheses imply u x ≤ v x for every x ∈ C.

theorem ViscositySolns.properBoundaryComparisonStatementOn_of_constantShiftAlongDataConstructor {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} (hconstruct : ConstantShiftBoundaryStrictificationAlongDataConstructorOn C R F) : ProperBoundaryComparisonStatementOn C R F

Natural-number indexed constant-shift boundary data imply the ordinary boundary comparison statement on C.

theorem ViscositySolns.properBoundaryComparisonStatementOn_of_constantShiftAlongCoreConstructor {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} (hR : ClosedUnderSubNonneg R) (hIshii : QuadraticPenaltyIshiiLemmaConstructorOn C) (hconstruct : ConstantShiftBoundaryStrictificationAlongCoreConstructorOn C R F) : ProperBoundaryComparisonStatementOn C R F

The reduced boundary-level constant-shift construction implies the ordinary boundary comparison statement.

In quantified mathematical form, assume:

• if r ∈ R and δ ≥ 0, then r - δ ∈ R;
• the quadratic-penalty Ishii lemma holds on C × C for every upper semicontinuous u and lower semicontinuous v;
• the remaining constant-shift construction in ConstantShiftBoundaryStrictificationAlongCoreConstructorOn C R F holds.

Then the ordinary boundary-value comparison target ProperBoundaryComparisonStatementOn C R F follows.

theorem ViscositySolns.properBoundaryComparisonStatementOn_traceSecondOrderOperator_of_constantShiftLocalization {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} {γ : ℝ} (hR : ClosedUnderSubNonneg R) (hIshii : QuadraticPenaltyIshiiLemmaConstructorOn C) (hγ : 0 < γ) (hcγ : ZerothCoefficientLowerBoundOn C c γ) (hconstruct : TraceConstantShiftBoundaryLocalizationAlongConstructorOn C R A b c f) : ProperBoundaryComparisonStatementOn C R (traceSecondOrderOperator A b c f)

Trace-form version of the reduced constant-shift boundary comparison criterion.

In quantified mathematical form, assume:

• if r ∈ R and δ ≥ 0, then r - δ ∈ R;
• the quadratic-penalty Ishii lemma holds on C × C for every upper semicontinuous u and lower semicontinuous v;
• 0 < γ and γ ≤ c x for every x ∈ C;
• the remaining trace-form localization construction in TraceConstantShiftBoundaryLocalizationAlongConstructorOn C R A b c f holds.

Then the ordinary boundary comparison target holds for traceSecondOrderOperator A b c f.