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

Strictification and theorem-shaped hypotheses for proper comparison.

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

The theorem-shaped proposition for the proper comparison result with the operator hypotheses already formalized in this repository.

The predicate extraHypotheses u v is reserved for the boundary, boundedness, and localization assumptions required by the global comparison proof. With those assumptions, every upper semicontinuous viscosity subsolution u and every lower semicontinuous viscosity supersolution v should satisfy u ≤ v on C.

Equations

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

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

The theorem-shaped proposition for the first boundary-value comparison target.

It says that, under properness, operator continuity, the Ishii structural condition, boundary comparison on frontier C, the scalar-range condition u x ∈ R for x ∈ C, and compactness of closure C, every viscosity subsolution u is bounded above by every viscosity supersolution v on C.

Equations

• ViscositySolns.ProperBoundaryComparisonStatementOn C R F = ViscositySolns.ProperComparisonStatementOn C R F (ViscositySolns.BoundaryComparisonHypothesesOn C R)

theorem ViscositySolns.ProperBoundaryComparisonStatementOn.unfold {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} (h : ProperBoundaryComparisonStatementOn C R F) : Proper F → OperatorContinuous F → IshiiOperatorComparisonConditionOn C R F → ∀ (u v : Point n → ℝ), BoundaryComparisonOn C u v → ScalarRangeOn C R u → CompactClosure C → ViscositySubsolution C F u → ViscositySupersolution C F v → ComparisonConclusionOn C u v

theorem ViscositySolns.ProperBoundaryComparisonStatementOn.unfold_univScalar {n : ℕ} {C : Set (Point n)} {F : Operator n} (h : ProperBoundaryComparisonStatementOn C Set.univ F) : Proper F → OperatorContinuous F → IshiiOperatorComparisonConditionOn C Set.univ F → ∀ (u v : Point n → ℝ), BoundaryComparisonOn C u v → CompactClosure C → ViscositySubsolution C F u → ViscositySupersolution C F v → ComparisonConclusionOn C u v

Unbounded-scalar version of ProperBoundaryComparisonStatementOn.

In quantified mathematical form, if the scalar set is all real numbers, then the scalar-range condition is automatic: for every x ∈ C, u x ∈ Set.univ.

theorem ViscositySolns.not_eventually_strict_le_modulus_of_tendsto_nhdsWithin_Ioi {ι : Type u_1} {l : Filter ι} [l.NeBot] {ω : ℝ → ℝ} {ε : ℝ} {t : ι → ℝ} (hω : ComparisonModulus ω) (hε : 0 < ε) (ht : Filter.Tendsto t l (nhdsWithin 0 (Set.Ioi 0))) : ¬∀ᶠ (i : ι) in l, ε ≤ ω (t i)

Let ω be a comparison modulus and let ε > 0. Let t i be a family of real numbers which converges to 0 through positive values along a nontrivial filter l. Then it is impossible that ε ≤ ω (t i) holds for all i in a set belonging to l.

def ViscositySolns.StrictViscositySubsolution {n : ℕ} (C : Set (Point n)) (F : Operator n) (ε : ℝ) (u : Point n → ℝ) : Prop

Strict viscosity subsolution with margin ε: for every superjet, the viscosity inequality is F x (u x) p X ≤ -ε.

Equations

• ViscositySolns.StrictViscositySubsolution C F ε u = (UpperSemicontinuousOn u C ∧ ∀ x ∈ C, ∀ J ∈ ViscositySolns.Superjet C u x, F x (u x) J.gradient J.hessian ≤ -ε)

theorem ViscositySolns.StrictViscositySubsolution.upperSemicontinuousOn {n : ℕ} {C : Set (Point n)} {F : Operator n} {ε : ℝ} {u : Point n → ℝ} (hu : StrictViscositySubsolution C F ε u) : UpperSemicontinuousOn u C

theorem ViscositySolns.StrictViscositySubsolution.closedSuperjet_le_neg_of_operatorContinuous {n : ℕ} {C : Set (Point n)} {F : Operator n} {ε : ℝ} {u : Point n → ℝ} {x : Point n} {J : Jet n} (hu : StrictViscositySubsolution C F ε u) (hF : OperatorContinuous F) (hJ : J ∈ ClosedSuperjet C u x) : F x (u x) J.gradient J.hessian ≤ -ε

theorem ViscositySolns.StrictViscositySubsolution.to_viscositySubsolution {n : ℕ} {C : Set (Point n)} {F : Operator n} {ε : ℝ} {u : Point n → ℝ} (hu : StrictViscositySubsolution C F ε u) (hε : 0 ≤ ε) : ViscositySubsolution C F u

def ViscositySolns.UniformScalarDecreaseOn {n : ℕ} (C : Set (Point n)) (F : Operator n) (δ ε : ℝ) : Prop

Uniform decrease of the operator under a fixed downward shift in the scalar unknown.

In quantified mathematical form, UniformScalarDecreaseOn C F δ ε means: for every x ∈ C, every scalar r, every first-derivative vector p, and every Hessian matrix X,

F x (r - δ) p X ≤ F x r p X - ε.

Equations

• ViscositySolns.UniformScalarDecreaseOn C F δ ε = ∀ x ∈ C, ∀ (r : ℝ) (p : ViscositySolns.Point n) (X : ViscositySolns.Hessian n), F x (r - δ) p X ≤ F x r p X - ε

def ViscositySolns.ZerothCoefficientLowerBoundOn {n : ℕ} (C : Set (Point n)) (c : Point n → ℝ) (γ : ℝ) : Prop

A positive lower bound for the zeroth-order coefficient on C.

In quantified mathematical form, ZerothCoefficientLowerBoundOn C c γ means: for every x ∈ C, one has γ ≤ c x.

Equations

• ViscositySolns.ZerothCoefficientLowerBoundOn C c γ = ∀ x ∈ C, γ ≤ c x

theorem ViscositySolns.uniformScalarDecreaseOn_traceSecondOrderOperator {n : ℕ} {C : Set (Point n)} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} {δ ε : ℝ} (hcδ : ∀ x ∈ C, ε ≤ c x * δ) : UniformScalarDecreaseOn C (traceSecondOrderOperator A b c f) δ ε

Trace-form operators satisfy the uniform scalar-decrease condition when the zeroth-order coefficient gives the required decrease.

In quantified mathematical form, if ε ≤ c x * δ for every x ∈ C, then

F x (r - δ) p X ≤ F x r p X - ε

for F = traceSecondOrderOperator A b c f.

theorem ViscositySolns.uniformScalarDecreaseOn_traceSecondOrderOperator_of_zeroth_lower_bound {n : ℕ} {C : Set (Point n)} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} {δ γ : ℝ} (hδ : 0 ≤ δ) (hcγ : ZerothCoefficientLowerBoundOn C c γ) : UniformScalarDecreaseOn C (traceSecondOrderOperator A b c f) δ (γ * δ)

Trace-form operators satisfy the uniform scalar-decrease condition with margin γ * δ when 0 ≤ δ and γ ≤ c x for every x ∈ C.

In quantified mathematical form, if 0 ≤ δ and γ ≤ c x for every x ∈ C, then for every x ∈ C, scalar r, vector p, and matrix X,

F x (r - δ) p X ≤ F x r p X - γ * δ

for F = traceSecondOrderOperator A b c f.

theorem ViscositySolns.ViscositySubsolution.strict_sub_const_of_uniformScalarDecrease {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} {δ ε : ℝ} (hu : ViscositySubsolution C F u) (hdec : UniformScalarDecreaseOn C F δ ε) : StrictViscositySubsolution C F ε fun (y : Point n) => u y - δ

A non-strict viscosity subsolution becomes a strict viscosity subsolution after a constant downward shift, provided the operator decreases uniformly under that scalar shift.

In quantified mathematical form, if u is a viscosity subsolution on C and F x (r - δ) p X ≤ F x r p X - ε for every x ∈ C, r, p, and X, then x ↦ u x - δ is a strict viscosity subsolution with margin ε on C.

def ViscositySolns.CompactClosureStrictificationOn {n : ℕ} (C : Set (Point n)) (R : Set ℝ) (F : Operator n) (u v : Point n → ℝ) : Prop

Strictification data on the compact closure of C.

In quantified mathematical form, this predicate says that, for every real number η > 0, there exist a real number ε > 0 and a function w such that:

• the quadratic-penalty conclusion of Ishii's lemma is available for w and v on closure C;
• w is a strict viscosity subsolution with margin ε on closure C;
• w x ∈ R for every x ∈ closure C;
• u x ≤ w x + η for every x ∈ C.

This is the limiting bridge from non-strict comparison for u to strict comparison for nearby functions w.

Equations

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

def ViscositySolns.LocalizedStrictificationAlongOn {n : ℕ} (C : Set (Point n)) (R : Set ℝ) (F : Operator n) (u v : Point n → ℝ) : Prop

Localized strictification using natural-number indexed doubled-variable data.

In quantified mathematical form, this predicate says that, for every real number η > 0, there exist a real number ε > 0, a function w, functions α : ℕ -> ℝ and x y : ℕ -> ℝ^n, such that:

• the quadratic-penalty Ishii lemma holds for w and v on C × C;
• w is a strict viscosity subsolution with margin ε on C;
• w x ∈ R for every x ∈ C;
• if there exists z ∈ C with v z < w z, then the selected doubled-variable data α, x, and y satisfy the filter-form localization statement StrictDoubledVariableLocalizationAlongOn along atTop;
• u x ≤ w x + η for every x ∈ C.

This formulation is the one used by compact selection and subsequence arguments: the parameters and selected points are indexed by natural numbers, and the relevant convergence is expressed along atTop.

Equations

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

def ViscositySolns.ConstantShiftLocalizedStrictificationAlongDataOn {n : ℕ} (C : Set (Point n)) (R : Set ℝ) (F : Operator n) (u v : Point n → ℝ) : Prop

Constant-shift data sufficient for natural-number indexed localized strictification.

In quantified mathematical form, this predicate says that, for every real number η > 0, there exist real numbers δ and ε, functions α : ℕ -> ℝ and x y : ℕ -> ℝ^n, such that:

• 0 < δ and δ ≤ η;
• 0 < ε;
• F x (r - δ) p X ≤ F x r p X - ε for every x ∈ C, scalar r, first-derivative vector p, and Hessian matrix X;
• the quadratic-penalty Ishii lemma holds for x ↦ u x - δ and v on C × C;
• u x - δ ∈ R for every x ∈ C;
• the selected data α, x, and y satisfy StrictDoubledVariableLocalizationAlongOn C R (fun x => u x - δ) v atTop α x y.

Equations

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

def ViscositySolns.ConstantShiftClosureMaximizerDataOn {n : ℕ} (C : Set (Point n)) (R : Set ℝ) (F : Operator n) (u v : Point n → ℝ) : Prop

Constant-shift data stated directly in terms of maximizers selected on closure C × closure C.

In quantified mathematical form, this predicate says that, for every real number η > 0, there exist real numbers δ and ε, functions α : ℕ -> ℝ and x y : ℕ -> ℝ^n, and a point x0 : ℝ^n, such that:

• 0 < δ and δ ≤ η;
• 0 < ε;
• F x (r - δ) p X ≤ F x r p X - ε for every x ∈ C, scalar r, first-derivative vector p, and Hessian matrix X;
• the quadratic-penalty Ishii lemma holds for x ↦ u x - δ and v on C × C;
• u x - δ ∈ R for every x ∈ C;
• x0 ∈ closure C and v x0 < u x0 - δ;
• x ↦ u x - δ is upper semicontinuous on closure C;
• v is lower semicontinuous on closure C;
• x i -> x0 and y i -> x0 within closure C as i -> ∞;
• for all i in a set belonging to atTop, 0 < α i, x i ∈ closure C, y i ∈ closure C, and (x i, y i) maximizes (x', y') ↦ u x' - δ - v y' - (α i / 2) * ∑ j, (x' j - y' j)^2 on closure C × closure C;
• α i -> +∞ as i -> ∞.

Equations

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

theorem ViscositySolns.constantShiftLocalizedStrictificationAlongDataOn_of_core_unshiftedIshii {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} {u v : Point n → ℝ} (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 (x : Point n) => u x - δ) v Filter.atTop α x y) : ConstantShiftLocalizedStrictificationAlongDataOn C R F u v

Natural-number indexed constant-shift strictification data with scalar range and shifted Ishii hypotheses derived from unshifted hypotheses.

In quantified mathematical form, suppose:

• u x ∈ R for every x ∈ C;
• if r ∈ R and 0 ≤ δ, then r - δ ∈ R;
• the quadratic-penalty Ishii lemma holds on C × C for u and v;
• for every η > 0 there exist real numbers δ and ε and functions α : ℕ -> ℝ, x y : ℕ -> ℝ^n such that 0 < δ, δ ≤ η, 0 < ε, UniformScalarDecreaseOn C F δ ε holds, and StrictDoubledVariableLocalizationAlongOn C R (fun x => u x - δ) v atTop α x y holds.

Then ConstantShiftLocalizedStrictificationAlongDataOn C R F u v holds.

theorem ViscositySolns.localizedStrictificationAlongOn_of_constantShiftData {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} {u v : Point n → ℝ} (hu : ViscositySubsolution C F u) (hdata : ConstantShiftLocalizedStrictificationAlongDataOn C R F u v) : LocalizedStrictificationAlongOn C R F u v

Natural-number indexed constant-shift data give localized strictification in the filter form.

In quantified mathematical form, if u is a viscosity subsolution on C and for every η > 0 the natural-number indexed constant-shift data above are available, then LocalizedStrictificationAlongOn C R F u v holds, with strictified functions of the form x ↦ u x - δ.

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

A constructor for natural-number indexed constant-shift localized strictification data from the ordinary boundary-value comparison hypotheses.

In quantified mathematical form, this predicate says that, whenever C is nonempty and u, v satisfy the boundary comparison, scalar-range, compact-closure, subsolution, and supersolution hypotheses on C, then the natural-number indexed constant-shift data in ConstantShiftLocalizedStrictificationAlongDataOn C R F u v hold.

Equations

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

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

A constructor for constant-shift data stated in terms of maximizers selected on closure C × closure C.

In quantified mathematical form, this predicate says that, whenever C is nonempty and u, v satisfy the boundary comparison, scalar-range, compact-closure, subsolution, and supersolution hypotheses on C, then ConstantShiftClosureMaximizerDataOn C R F u v holds.

Equations

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

def ViscositySolns.QuadraticPenaltyIshiiLemmaConstructorOn {n : ℕ} (C : Set (Point n)) : Prop

The theorem-form hypothesis that supplies the quadratic-penalty Ishii lemma on one spatial set.

In quantified mathematical form, this says: for every pair of functions u, v, if u is upper semicontinuous on C and v is lower semicontinuous on C, then QuadraticPenaltyIshiiLemmaOn C C u v holds.

Equations

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

theorem ViscositySolns.QuadraticPenaltyIshiiLemmaConstructorOn.of_localized_jensen_aleksandrov {n : ℕ} (hJensen : JensenContactSetPositiveMeasureOnClosedBallTheorem (n + n)) (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem (n + n)) {C : Set (Point n)} [LocallyCompactSpace ↑C] : QuadraticPenaltyIshiiLemmaConstructorOn C

The localized Jensen and Aleksandrov analytic inputs supply the quadratic-penalty Ishii lemma constructor on a locally compact set.

In quantified mathematical form, if the relative topology on C is locally compact, then for every upper semicontinuous u on C and every lower semicontinuous v on C, the quadratic-penalty Ishii lemma holds on C × C, provided the localized Jensen contact-set theorem and localized Aleksandrov second-differentiability theorem are available in dimension n + n.

theorem ViscositySolns.QuadraticPenaltyIshiiLemmaConstructorOn.of_aleksandrov {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem (n + n)) {C : Set (Point n)} [LocallyCompactSpace ↑C] : QuadraticPenaltyIshiiLemmaConstructorOn C

The quadratic-penalty Ishii lemma constructor follows from the localized Aleksandrov second-differentiability theorem in dimension n + n, because the localized Jensen contact-set theorem has already been proved.

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

The remaining constant-shift construction after scalar range and Ishii's lemma have been separated out.

In quantified mathematical form, this predicate says that, whenever C is nonempty and u, v satisfy the boundary comparison, scalar-range, compact-closure, subsolution, and supersolution hypotheses on C, then for every η > 0 there exist real numbers δ, ε and sequences α : ℕ -> ℝ, x y : ℕ -> ℝ^n such that:

• 0 < δ and δ ≤ η;
• 0 < ε;
• UniformScalarDecreaseOn C F δ ε holds;
• StrictDoubledVariableLocalizationAlongOn C R (fun z => u z - δ) v atTop α x y holds.

Equations

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

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

The remaining trace-form constant-shift construction after the positive zeroth-order lower bound has supplied the strict subsolution margin.

In quantified mathematical form, this predicate says that, whenever C is nonempty and u, v satisfy the boundary comparison, scalar-range, compact-closure, subsolution, and supersolution hypotheses for traceSecondOrderOperator A b c f on C, then for every η > 0 there exist δ > 0 and sequences α : ℕ -> ℝ, x y : ℕ -> ℝ^n such that δ ≤ η and

StrictDoubledVariableLocalizationAlongOn C R (fun z => u z - δ) v atTop α x y

holds.

Equations

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

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

The trace-form constant-shift construction stated directly in terms of maximizers selected on closure C × closure C.

In quantified mathematical form, this predicate says that, whenever C is nonempty and u, v satisfy the boundary comparison, scalar-range, compact-closure, subsolution, and supersolution hypotheses for traceSecondOrderOperator A b c f on C, then for every η > 0 there exist δ > 0, sequences α : ℕ -> ℝ, x y : ℕ -> ℝ^n, and a point x0 : ℝ^n such that:

• δ ≤ η;
• x0 ∈ closure C and v x0 < u x0 - δ;
• x ↦ u x - δ is upper semicontinuous on closure C;
• v is lower semicontinuous on closure C;
• x i -> x0 and y i -> x0 within closure C as i -> ∞;
• for all i in a set belonging to atTop, (x i, y i) maximizes (x', y') ↦ u x' - δ - v y' - (α i / 2) * ∑ j, (x' j - y' j)^2 on closure C × closure C, with 0 < α i, x i ∈ closure C, and y i ∈ closure C;
• α i -> +∞ as i -> ∞.

The shifted scalar range, shifted Ishii lemma, and strict scalar decrease are supplied separately by ClosedUnderSubNonneg R, QuadraticPenaltyIshiiLemmaConstructorOn C, and a positive lower bound for the zeroth-order coefficient.

Equations

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

theorem ViscositySolns.constantShiftBoundaryStrictificationAlongCoreConstructorOn_traceSecondOrderOperator {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {A : Point n → Hessian n} {b : Point n → Point n} {c f : Point n → ℝ} {γ : ℝ} (hγ : 0 < γ) (hcγ : ZerothCoefficientLowerBoundOn C c γ) (hconstruct : TraceConstantShiftBoundaryLocalizationAlongConstructorOn C R A b c f) : ConstantShiftBoundaryStrictificationAlongCoreConstructorOn C R (traceSecondOrderOperator A b c f)

For trace-form operators, a positive lower bound on the zeroth-order coefficient reduces the constant-shift core constructor to the remaining doubled-variable localization construction.

In quantified mathematical form, assume 0 < γ, γ ≤ c x for every x ∈ C, and TraceConstantShiftBoundaryLocalizationAlongConstructorOn C R A b c f. Then ConstantShiftBoundaryStrictificationAlongCoreConstructorOn C R (traceSecondOrderOperator A b c f) holds.

theorem ViscositySolns.constantShiftBoundaryClosureMaximizerDataConstructorOn_traceSecondOrderOperator {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 : TraceConstantShiftBoundaryClosureMaximizerConstructorOn C R A b c f) : ConstantShiftBoundaryClosureMaximizerDataConstructorOn C R (traceSecondOrderOperator A b c f)

For trace-form operators, the closure-maximizer construction, together with the scalar-range and Ishii declarations and a positive lower bound for the zeroth-order coefficient, gives the generic closure-maximizer data constructor.

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

The reduced boundary-level constant-shift construction implies the constant-shift strictification data constructor.

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 full natural-number indexed constant-shift strictification data are available for every pair satisfying the ordinary boundary-value hypotheses.

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

A constructor for natural-number indexed localized strictification from the ordinary boundary-value comparison hypotheses.

In quantified mathematical form, this predicate says that, whenever C is nonempty and u, v satisfy the boundary comparison, scalar-range, compact-closure, subsolution, and supersolution hypotheses on C, then LocalizedStrictificationAlongOn C R F u v holds.

Equations

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

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

Natural-number indexed constant-shift boundary data construct natural-number indexed localized strictification from the ordinary boundary-value hypotheses.

def ViscositySolns.StrictifiedBoundaryComparisonHypothesesOn {n : ℕ} (C : Set (Point n)) (R : Set ℝ) (F : Operator n) (u v : Point n → ℝ) : Prop

Boundary comparison hypotheses together with the additional data needed to apply compact-closure strictification.

In quantified mathematical form, this predicate consists of:

• C is nonempty;
• u x ≤ v x for every x ∈ frontier C;
• u x ∈ R for every x ∈ C;
• closure C is compact;
• v is a viscosity supersolution on closure C;
• CompactClosureStrictificationOn C R F u v.

The last condition is the remaining analytic bridge from the non-strict subsolution hypothesis to strict comparison on closure C.

Equations

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

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

The theorem-shaped proposition for boundary comparison after strictification has been supplied.

In quantified mathematical form, this says: if F is proper, continuous, and satisfies the Ishii structural condition on closure C and R, then every pair of functions satisfying StrictifiedBoundaryComparisonHypothesesOn satisfies u x ≤ v x for every x ∈ C.

Equations

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

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

Boundary comparison statement whose structural condition is stated on closure C.

In quantified mathematical form, this says: under properness, operator continuity, IshiiOperatorComparisonConditionOn (closure C) R F, boundary comparison on frontier C, the scalar-range condition on C, compactness of closure C, and the non-strict viscosity subsolution and supersolution hypotheses on C, one has u x ≤ v x for every x ∈ C.

Equations

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

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

A constructor for the strictified boundary hypotheses from the ordinary boundary-value comparison hypotheses.

In quantified mathematical form, this predicate says that, whenever C is nonempty and u, v satisfy the boundary comparison, scalar-range, compact-closure, subsolution, and supersolution hypotheses on C, then the strictified hypotheses needed by StrictifiedBoundaryComparisonStatementOn hold.

Equations

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

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

Reduced constructor for the analytic data in the strictified boundary hypotheses.

In quantified mathematical form, this says that, under the ordinary boundary-value hypotheses on C, one can prove both:

• v is a viscosity supersolution on closure C;
• CompactClosureStrictificationOn C R F u v.

Together with the ordinary boundary comparison, scalar-range, compactness, and nonemptiness hypotheses, these two conclusions imply StrictifiedBoundaryComparisonHypothesesOn C R F u v.

Equations

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

theorem ViscositySolns.compactClosureBoundaryStrictificationConstructorOn_of_dataConstructor {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} (hdata : CompactClosureStrictificationDataConstructorOn C R F) : CompactClosureBoundaryStrictificationConstructorOn C R F

The reduced analytic data constructor supplies the full strictified boundary hypotheses.

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

The theorem-shaped proposition for strict comparison conditional on Ishii's lemma.

In quantified mathematical form, this says: assume F is proper, continuous, and satisfies IshiiOperatorComparisonConditionOn C R F. Let ε > 0. For every pair of functions u, v, assume:

• the additional hypotheses extraHypotheses u v;
• QuadraticPenaltyIshiiLemmaOn C C u v;
• u is a strict viscosity subsolution with margin ε;
• v is a viscosity supersolution;
• u x ∈ R for every x ∈ C.

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

Equations

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

def ViscositySolns.CompactStrictComparisonHypothesesOn {n : ℕ} (C : Set (Point n)) (_u _v : Point n → ℝ) : Prop

Compactness hypotheses for strict comparison on a fixed set C.

In quantified mathematical form, this predicate says that C is nonempty and compact. It does not impose any additional condition on the particular functions u and v.

Equations

• ViscositySolns.CompactStrictComparisonHypothesesOn C _u _v = (C.Nonempty ∧ IsCompact C)