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

Compact and subsequence comparison bridges. (ConstantShiftBoundary)

Part of the compact and subsequence comparison bridge development. Split from Compact.lean; see the umbrella module docstring.

theorem ViscositySolns.strictComparison_of_eventually_maximizers_of_scaleEstimates {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 < ε) (huR : ScalarRangeOn C R u) (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) (hscale : DoubledVariableScaleEstimatesAlong l α x y) : ComparisonConclusionOn C u v

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

Let l be a filter on ι with NeBot l. Suppose there are functions α : ι -> R and x y : ι -> R^n such that, for all i in a set belonging to l, one has 0 < α i, x i ∈ C, y i ∈ C, and (x i, y i) maximizes (x', y') ↦ u x' - v y' - (α i / 2) * ∑ j, (x' j - y' j)^2 on C × C. Suppose also that DoubledVariableScaleEstimatesAlong l α x y holds and that u x ∈ R for every x ∈ C. Then u ≤ v on C.

theorem ViscositySolns.strictComparison_of_eventually_maximizers_of_scales {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 < ε) (huR : ScalarRangeOn C R u) (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) (hquad : Filter.Tendsto (fun (i : ι) => α i * ‖x i - y i‖ ^ 2) l (nhds 0)) (hdist : Filter.Tendsto (fun (i : ι) => ‖x i - y i‖) l (nhds 0)) : ComparisonConclusionOn C u v

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

Let l be a filter on ι with NeBot l. Suppose there are functions α : ι -> R and x y : ι -> R^n such that, for all i in a set belonging to l, one has 0 < α i, x i ∈ C, y i ∈ C, and (x i, y i) maximizes (x', y') ↦ u x' - v y' - (α i / 2) * ∑ j, (x' j - y' j)^2 on C × C. Suppose also that u x ∈ R for every x ∈ C, that α i * ‖x i - y i‖ ^ 2 -> 0 along l, and that ‖x i - y i‖ -> 0 along l. Then u ≤ v on C.

The theorem does not assume separately that {i | x i ≠ y i} belongs to l. If comparison failed, the strict subsolution inequality and Ishii's lemma would imply that 0 < α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖ for all i in a set belonging to l.

theorem ViscositySolns.strictComparison_of_eventually_maximizers_of_weightedDistanceSq {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 < ε) (huR : ScalarRangeOn C R u) (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) (hquad : Filter.Tendsto (fun (i : ι) => α i * ‖x i - y i‖ ^ 2) l (nhds 0)) (hαone : ∀ᶠ (i : ι) in l, 1 ≤ α i) : ComparisonConclusionOn C u v

Assume the hypotheses of strictComparison_of_eventually_maximizers_of_scaleEstimates. Instead of assuming DoubledVariableScaleEstimatesAlong l α x y directly, assume:

• α i * ‖x i - y i‖ ^ 2 -> 0 along l;
• {i | 1 ≤ α i} belongs to l.

Then u ≤ v on C.

theorem ViscositySolns.strictComparison_of_eventually_maximizers_of_weightedDistanceSq_atTop {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 < ε) (huR : ScalarRangeOn C R u) (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) (hquad : Filter.Tendsto (fun (i : ι) => α i * ‖x i - y i‖ ^ 2) l (nhds 0)) (hα : Filter.Tendsto α l Filter.atTop) : ComparisonConclusionOn C u v

Assume the hypotheses of strictComparison_of_eventually_maximizers_of_weightedDistanceSq, with the condition {i | 1 ≤ α i} ∈ l replaced by α i -> +∞ along l.

theorem ViscositySolns.strictComparison_of_shifted_closure_maximizers_of_tendsto_atTop {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} {x0 : Point n} (hboundary : BoundaryComparisonOn C u v) (hδ : 0 < δ) (hx0closure : x0 ∈ closure C) (hgap : v x0 < u x0 - δ) (hu : StrictViscositySubsolution C F ε fun (z : Point n) => u z - δ) (hv : ViscositySupersolution C F v) (hFcont : OperatorContinuous F) (hproper : Proper F) (hcomp : IshiiOperatorComparisonConditionOn C R F) (hIshii : QuadraticPenaltyIshiiLemmaOn C C (fun (z : Point n) => u z - δ) v) (hε : 0 < ε) (huR : ScalarRangeOn C R fun (z : Point n) => u z - δ) (husc : UpperSemicontinuousOn (fun (z : Point n) => u z - δ) (closure C)) (hvlsc : LowerSemicontinuousOn v (closure C)) (hx : Filter.Tendsto x l (nhdsWithin x0 (closure C))) (hy : Filter.Tendsto y l (nhdsWithin x0 (closure C))) (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ closure C ∧ y i ∈ closure C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective (fun (z : Point n) => u z - δ) v (α i) q) (closure C ×ˢ closure C) (x i, y i)) (hα : Filter.Tendsto α l Filter.atTop) : ComparisonConclusionOn C (fun (z : Point n) => u z - δ) v

Strict comparison from shifted doubled-variable maximizers selected on closure C × closure C.

In quantified mathematical form, assume u ≤ v on frontier C, δ > 0, x0 ∈ closure C, and v x0 < u x0 - δ. Suppose selected points x i, y i converge to x0 within closure C, and for all i in a set belonging to l, (x i, y i) maximizes

(x', y') ↦ u x' - δ - v y' - (α i / 2) * ∑ j, (x' j - y' j)^2

on closure C × closure C. If α i -> +∞, x ↦ u x - δ is a strict subsolution on C, v is a supersolution on C, the shifted function has values in R on C, and the operator hypotheses and Ishii lemma hold on C, then u x - δ ≤ v x for every x ∈ C.

theorem ViscositySolns.strictComparison_of_constantShift_boundary {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {F : Operator n} {u v : Point n → ℝ} {δ ε : ℝ} (hboundary : BoundaryComparisonOn C u v) (hδ : 0 < δ) (hu : StrictViscositySubsolution C F ε fun (z : Point n) => u z - δ) (hv : ViscositySupersolution C F v) (hFcont : OperatorContinuous F) (hproper : Proper F) (hcomp : IshiiOperatorComparisonConditionOn C R F) (hIshii : QuadraticPenaltyIshiiLemmaOn C C (fun (z : Point n) => u z - δ) v) (hε : 0 < ε) (huR : ScalarRangeOn C R fun (z : Point n) => u z - δ) (hCne : C.Nonempty) (hCcompact : CompactClosure C) (husc : UpperSemicontinuousOn (fun (z : Point n) => u z - δ) (closure C)) (hvlsc : LowerSemicontinuousOn v (closure C)) : ComparisonConclusionOn C (fun (z : Point n) => u z - δ) v

Strict boundary comparison for a fixed positive constant shift.

In quantified mathematical form, assume:

• u ≤ v on frontier C;
• δ > 0;
• x ↦ u x - δ is a strict subsolution on C;
• v is a supersolution on C;
• x ↦ u x - δ is upper semicontinuous on closure C;
• v is lower semicontinuous on closure C;
• closure C is compact;
• the operator hypotheses and the quadratic-penalty Ishii lemma hold on C.

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

The proof follows the comparison argument in CIL: if the conclusion failed, choose maximum points of the shifted doubled-variable functional on closure C × closure C for parameters tending to infinity. Compactness gives a convergent subsequence of the first coordinates, the doubled-variable estimate forces the second coordinates to have the same limit, boundary strictness places the limit in C, and the already-proved strict comparison contradiction applies.

theorem ViscositySolns.comparison_of_constantShift_boundary {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) (hboundary : BoundaryComparisonOn C u v) (huR : ScalarRangeOn C R u) (hR : ClosedUnderSubNonneg R) (hIshii : QuadraticPenaltyIshiiLemmaConstructorOn C) (hCne : C.Nonempty) (hCcompact : CompactClosure C) (hu : ViscositySubsolution C F u) (hv : ViscositySupersolution C F v) (husc : UpperSemicontinuousOn u (closure C)) (hvlsc : LowerSemicontinuousOn v (closure C)) (hdecrease : ∀ (η : ℝ), 0 < η → ∃ (δ : ℝ) (ε : ℝ), 0 < δ ∧ δ ≤ η ∧ 0 < ε ∧ UniformScalarDecreaseOn C F δ ε) : ComparisonConclusionOn C u v

Proper comparison from constant shifts, following the paper's strictification argument.

In quantified mathematical form, assume:

• u ≤ v on frontier C;
• u is a viscosity subsolution and v is a viscosity supersolution on C;
• u is upper semicontinuous and v is lower semicontinuous on closure C;
• closure C is compact;
• the operator hypotheses and the quadratic-penalty Ishii lemma constructor hold on C;
• the scalar set is closed under subtracting nonnegative constants;
• for every η > 0, there are δ and ε such that 0 < δ, δ ≤ η, 0 < ε, and F x (r - δ) p X ≤ F x r p X - ε for every x ∈ C, r, p, and X.

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

theorem ViscositySolns.comparison_of_constantShift_boundary_of_localized_jensen_aleksandrov {n : ℕ} (hJensen : JensenContactSetPositiveMeasureOnClosedBallTheorem (n + n)) (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem (n + n)) {C : Set (Point n)} [LocallyCompactSpace ↑C] {R : Set ℝ} {F : Operator n} {u v : Point n → ℝ} (hproper : Proper F) (hFcont : OperatorContinuous F) (hcomp : IshiiOperatorComparisonConditionOn C R F) (hboundary : BoundaryComparisonOn C u v) (huR : ScalarRangeOn C R u) (hR : ClosedUnderSubNonneg R) (hCne : C.Nonempty) (hCcompact : CompactClosure C) (hu : ViscositySubsolution C F u) (hv : ViscositySupersolution C F v) (husc : UpperSemicontinuousOn u (closure C)) (hvlsc : LowerSemicontinuousOn v (closure C)) (hdecrease : ∀ (η : ℝ), 0 < η → ∃ (δ : ℝ) (ε : ℝ), 0 < δ ∧ δ ≤ η ∧ 0 < ε ∧ UniformScalarDecreaseOn C F δ ε) : ComparisonConclusionOn C u v

Non-strict boundary comparison from the constant-shift argument, with the quadratic-penalty Ishii lemma constructor supplied by the localized Jensen and Aleksandrov analytic inputs.

In quantified mathematical form, assume the localized Jensen contact-set theorem and the localized Aleksandrov second-differentiability theorem in dimension n + n, and assume the relative topology on C is locally compact. If F is proper and continuous, F satisfies the Ishii operator comparison condition on C and R, u ≤ v on frontier C, u x ∈ R for every x ∈ C, R is closed under subtracting nonnegative constants, C is nonempty, closure C is compact, u is a viscosity subsolution, v is a viscosity supersolution, u is upper semicontinuous on closure C, v is lower semicontinuous on closure C, and every positive η has a positive constant shift which makes the subsolution inequality strict, then u x ≤ v x for every x ∈ C.

theorem ViscositySolns.comparison_of_constantShift_boundary_of_aleksandrov {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem (n + n)) {C : Set (Point n)} [LocallyCompactSpace ↑C] {R : Set ℝ} {F : Operator n} {u v : Point n → ℝ} (hproper : Proper F) (hFcont : OperatorContinuous F) (hcomp : IshiiOperatorComparisonConditionOn C R F) (hboundary : BoundaryComparisonOn C u v) (huR : ScalarRangeOn C R u) (hR : ClosedUnderSubNonneg R) (hCne : C.Nonempty) (hCcompact : CompactClosure C) (hu : ViscositySubsolution C F u) (hv : ViscositySupersolution C F v) (husc : UpperSemicontinuousOn u (closure C)) (hvlsc : LowerSemicontinuousOn v (closure C)) (hdecrease : ∀ (η : ℝ), 0 < η → ∃ (δ : ℝ) (ε : ℝ), 0 < δ ∧ δ ≤ η ∧ 0 < ε ∧ UniformScalarDecreaseOn C F δ ε) : ComparisonConclusionOn C u v

Non-strict boundary comparison from the constant-shift argument follows from the localized Aleksandrov second-differentiability theorem in dimension n + n, because the localized Jensen contact-set theorem has already been proved.

theorem ViscositySolns.comparison_of_constantShift_boundary_proof {n : ℕ} {C : Set (Point n)} [LocallyCompactSpace ↑C] {R : Set ℝ} {F : Operator n} {u v : Point n → ℝ} (hproper : Proper F) (hFcont : OperatorContinuous F) (hcomp : IshiiOperatorComparisonConditionOn C R F) (hboundary : BoundaryComparisonOn C u v) (huR : ScalarRangeOn C R u) (hR : ClosedUnderSubNonneg R) (hCne : C.Nonempty) (hCcompact : CompactClosure C) (hu : ViscositySubsolution C F u) (hv : ViscositySupersolution C F v) (husc : UpperSemicontinuousOn u (closure C)) (hvlsc : LowerSemicontinuousOn v (closure C)) (hdecrease : ∀ (η : ℝ), 0 < η → ∃ (δ : ℝ) (ε : ℝ), 0 < δ ∧ δ ≤ η ∧ 0 < ε ∧ UniformScalarDecreaseOn C F δ ε) : ComparisonConclusionOn C u v

Compact-domain comparison with the analytic Jensen and Aleksandrov inputs discharged.

theorem ViscositySolns.comparison_of_constantShiftClosureMaximizerData {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) (hboundary : BoundaryComparisonOn C u v) (hu : ViscositySubsolution C F u) (hv : ViscositySupersolution C F v) (hdata : ConstantShiftClosureMaximizerDataOn C R F u v) : ComparisonConclusionOn C u v

Constant-shift data stated using maximizers on closure C × closure C 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;
• u ≤ v on frontier C;
• for every η > 0, there are δ, ε, α, x, y, and x0 satisfying the conditions in ConstantShiftClosureMaximizerDataOn C R F u v.

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

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

If the ordinary boundary-value hypotheses construct constant-shift data stated using maximizers on closure C × closure C, then the ordinary boundary comparison statement on C follows.