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

Core declarations for proper comparison.

def ViscositySolns.ComparisonConclusionOn {n : ℕ} (C : Set (Point n)) (u v : Point n → ℝ) : Prop

Interior comparison conclusion on a set C: for every x ∈ C, u x ≤ v x.

Boundary hypotheses and compactness/localization hypotheses are not included in this predicate; they will appear in the theorem that proves it.

Equations

• ViscositySolns.ComparisonConclusionOn C u v = ∀ x ∈ C, u x ≤ v x

theorem ViscositySolns.ComparisonConclusionOn.mono_spatial_set {n : ℕ} {C D : Set (Point n)} {u v : Point n → ℝ} (h : ComparisonConclusionOn D u v) (hCD : C ⊆ D) : ComparisonConclusionOn C u v

def ViscositySolns.ScalarRangeOn {n : ℕ} (C : Set (Point n)) (R : Set ℝ) (u : Point n → ℝ) : Prop

Scalar range condition on a set C: for every x ∈ C, the value u x belongs to the scalar set R.

Equations

• ViscositySolns.ScalarRangeOn C R u = ∀ x ∈ C, u x ∈ R

def ViscositySolns.ClosedUnderSubNonneg (R : Set ℝ) : Prop

A scalar set is closed under subtracting nonnegative constants.

In quantified mathematical form, this predicate says: if r ∈ R and 0 ≤ δ, then r - δ ∈ R.

Equations

• ViscositySolns.ClosedUnderSubNonneg R = ∀ r ∈ R, ∀ (δ : ℝ), 0 ≤ δ → r - δ ∈ R

def ViscositySolns.ValueBoundedOn {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) : Prop

Boundedness of a real-valued function on a set C: there exist real numbers m and M such that, for every x ∈ C, m ≤ u x and u x ≤ M.

Equations

• ViscositySolns.ValueBoundedOn C u = ∃ (m : ℝ) (M : ℝ), ∀ x ∈ C, m ≤ u x ∧ u x ≤ M

def ViscositySolns.ValueUpperBoundedOn {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) : Prop

Upper boundedness of a real-valued function on a set C: there exists a real number M such that, for every x ∈ C, u x ≤ M.

Equations

• ViscositySolns.ValueUpperBoundedOn C u = ∃ (M : ℝ), ∀ x ∈ C, u x ≤ M

def ViscositySolns.ValueLowerBoundedOn {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) : Prop

Lower boundedness of a real-valued function on a set C: there exists a real number m such that, for every x ∈ C, m ≤ u x.

Equations

• ViscositySolns.ValueLowerBoundedOn C u = ∃ (m : ℝ), ∀ x ∈ C, m ≤ u x

theorem ViscositySolns.ValueBoundedOn.of_isMinOn_isMaxOn {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {xmin xmax : Point n} (hmin : IsMinOn u C xmin) (hmax : IsMaxOn u C xmax) : ValueBoundedOn C u

If u has a minimum and a maximum on C, then u is bounded above and below on C.

theorem ViscositySolns.ValueUpperBoundedOn.of_isMaxOn {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {xmax : Point n} (hmax : IsMaxOn u C xmax) : ValueUpperBoundedOn C u

If u has a maximum on C, then u is bounded above on C.

theorem ViscositySolns.ValueLowerBoundedOn.of_isMinOn {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {xmin : Point n} (hmin : IsMinOn u C xmin) : ValueLowerBoundedOn C u

If u has a minimum on C, then u is bounded below on C.

theorem ViscositySolns.ValueUpperBoundedOn.of_upperSemicontinuousOn_isCompact {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} (hCne : C.Nonempty) (hCcompact : IsCompact C) (husc : UpperSemicontinuousOn u C) : ValueUpperBoundedOn C u

If C is nonempty and compact and u is upper semicontinuous on C, then u is bounded above on C.

theorem ViscositySolns.ValueLowerBoundedOn.of_lowerSemicontinuousOn_isCompact {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} (hCne : C.Nonempty) (hCcompact : IsCompact C) (hlsc : LowerSemicontinuousOn u C) : ValueLowerBoundedOn C u

If C is nonempty and compact and u is lower semicontinuous on C, then u is bounded below on C.

theorem ViscositySolns.ValueBoundedOn.of_lower_upperSemicontinuousOn_isCompact {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} (hCne : C.Nonempty) (hCcompact : IsCompact C) (hlsc : LowerSemicontinuousOn u C) (husc : UpperSemicontinuousOn u C) : ValueBoundedOn C u

If C is nonempty and compact, u is lower semicontinuous on C, and u is upper semicontinuous on C, then u is bounded above and below on C.

theorem ViscositySolns.ValueBoundedOn.of_continuousOn_isCompact {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} (hCne : C.Nonempty) (hCcompact : IsCompact C) (hu : ContinuousOn u C) : ValueBoundedOn C u

If C is nonempty and compact and u is continuous on C, then u is bounded above and below on C.

def ViscositySolns.BoundaryComparisonOn {n : ℕ} (C : Set (Point n)) (u v : Point n → ℝ) : Prop

Boundary comparison on a set C: for every x in the topological frontier of C, u x ≤ v x.

Equations

• ViscositySolns.BoundaryComparisonOn C u v = ∀ x ∈ frontier C, u x ≤ v x

theorem ViscositySolns.BoundaryComparisonOn.sub_const_lt_on_frontier {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {δ : ℝ} (hboundary : BoundaryComparisonOn C u v) (hδ : 0 < δ) (x : Point n) : x ∈ frontier C → u x - δ < v x

If u ≤ v on frontier C and δ > 0, then u - δ < v on frontier C.

In quantified mathematical form, for every x ∈ frontier C, u x - δ < v x.

theorem ViscositySolns.mem_interior_of_mem_closure_of_not_mem_frontier {n : ℕ} {C : Set (Point n)} {x : Point n} (hxclosure : x ∈ closure C) (hxfrontier : x ∉ frontier C) : x ∈ interior C

If x ∈ closure C and x ∉ frontier C, then x ∈ interior C.

theorem ViscositySolns.mem_of_mem_closure_of_not_mem_frontier {n : ℕ} {C : Set (Point n)} {x : Point n} (hxclosure : x ∈ closure C) (hxfrontier : x ∉ frontier C) : x ∈ C

If x ∈ closure C and x ∉ frontier C, then x ∈ C.

theorem ViscositySolns.BoundaryComparisonOn.mem_of_mem_closure_of_shifted_gap {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {δ : ℝ} {x : Point n} (hboundary : BoundaryComparisonOn C u v) (hδ : 0 < δ) (hxclosure : x ∈ closure C) (hgap : v x < u x - δ) : x ∈ C

Assume u ≤ v on frontier C and δ > 0. If x ∈ closure C and v x < u x - δ, then x ∈ C.

theorem ViscositySolns.eventually_mem_of_tendsto_of_mem_interior {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {x : ι → Point n} {x0 : Point n} (hx0 : x0 ∈ interior C) (hx : Filter.Tendsto x l (nhds x0)) : ∀ᶠ (i : ι) in l, x i ∈ C

If x0 ∈ interior C and x i -> x0, then x i ∈ C for all i in a set belonging to the filter.

theorem ViscositySolns.eventually_pair_mem_of_tendsto_of_mem_interior {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {x y : ι → Point n} {x0 : Point n} (hx0 : x0 ∈ interior C) (hx : Filter.Tendsto x l (nhds x0)) (hy : Filter.Tendsto y l (nhds x0)) : ∀ᶠ (i : ι) in l, x i ∈ C ∧ y i ∈ C

If x0 ∈ interior C, x i -> x0, and y i -> x0, then x i ∈ C and y i ∈ C for all i in a set belonging to the filter.

theorem ViscositySolns.BoundaryComparisonOn.eventually_pair_mem_of_tendsto_of_shifted_gap {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point 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 - δ) (hx : Filter.Tendsto x l (nhds x0)) (hy : Filter.Tendsto y l (nhds x0)) : ∀ᶠ (i : ι) in l, x i ∈ C ∧ y i ∈ C

Assume u ≤ v on frontier C and δ > 0. If x0 ∈ closure C, v x0 < u x0 - δ, x i -> x0, and y i -> x0, then x i ∈ C and y i ∈ C for all i in a set belonging to the filter.

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

Compact-closure condition on a set C: the closure of C is compact.

Equations

• ViscositySolns.CompactClosure C = IsCompact (closure C)

theorem ViscositySolns.CompactClosure.isCompact_closure {n : ℕ} {C : Set (Point n)} (hC : CompactClosure C) : IsCompact (closure C)

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

The boundary, scalar-range, and compactness assumptions used by the first boundary-value comparison target.

Equations

• ViscositySolns.BoundaryComparisonHypothesesOn C R u v = (ViscositySolns.BoundaryComparisonOn C u v ∧ ViscositySolns.ScalarRangeOn C R u ∧ ViscositySolns.CompactClosure C)

def ViscositySolns.StrictDoubledVariableLocalizationAlongOn {n : ℕ} {ι : Type u_1} (C : Set (Point n)) (R : Set ℝ) (u v : Point n → ℝ) (l : Filter ι) (α : ι → ℝ) (x y : ι → Point n) : Prop

The doubled-variable localization hypothesis in the filter form used by the standard comparison proof.

Let ι be an index type with a filter l, and let α i, x i, and y i be data depending on i. This predicate says: if there exists z ∈ C such that v z < u z, then the following two statements hold.

First, for all i in a set belonging to the filter l, α i > 0, x i ∈ C, y i ∈ C, u (x i) ∈ R, v (y i) ≤ u (x i), and (x i, y i) maximizes (x', y') ↦ u x' - v y' - (α i / 2) * ∑ j, (x' j - y' j)^2 on C × C.

Second, the real numbers

α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖

converge to 0 through positive values along l.

Equations

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

def ViscositySolns.DoubledVariableScaleEstimatesAlong {n : ℕ} {ι : Type u_1} (l : Filter ι) (α : ι → ℝ) (x y : ι → Point n) : Prop

For functions α : ι -> R and x y : ι -> R^n and a filter l on ι, this predicate is the conjunction of the following three statements:

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

Together with 0 < α i for all i in a set belonging to l, these statements imply that α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖ tends to 0 through positive values along l.

Equations

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

theorem ViscositySolns.eventually_pos_of_tendsto_atTop {ι : Type u_1} {l : Filter ι} {α : ι → ℝ} (hα : Filter.Tendsto α l Filter.atTop) : ∀ᶠ (i : ι) in l, 0 < α i

Let α i be real numbers indexed by a filter l. If α i -> +∞ along l, then {i | 0 < α i} belongs to l.

theorem ViscositySolns.eventually_one_le_of_tendsto_atTop {ι : Type u_1} {l : Filter ι} {α : ι → ℝ} (hα : Filter.Tendsto α l Filter.atTop) : ∀ᶠ (i : ι) in l, 1 ≤ α i

Let α i be real numbers indexed by a filter l. If α i -> +∞ along l, then {i | 1 ≤ α i} belongs to l.

theorem ViscositySolns.ScalarRangeOn.mono_spatial_set {n : ℕ} {C D : Set (Point n)} {R : Set ℝ} {u : Point n → ℝ} (hu : ScalarRangeOn D R u) (hCD : C ⊆ D) : ScalarRangeOn C R u

theorem ViscositySolns.ScalarRangeOn.mono_scalar_set {n : ℕ} {C : Set (Point n)} {R S : Set ℝ} {u : Point n → ℝ} (hu : ScalarRangeOn C R u) (hRS : R ⊆ S) : ScalarRangeOn C S u

theorem ViscositySolns.ScalarRangeOn.univ {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) : ScalarRangeOn C Set.univ u

For every function u, the scalar range condition holds with scalar set Set.univ.

In quantified mathematical form, for every x ∈ C, u x ∈ Set.univ.

theorem ViscositySolns.ClosedUnderSubNonneg.univ : ClosedUnderSubNonneg Set.univ

The set of all real numbers is closed under subtracting nonnegative constants.

theorem ViscositySolns.ClosedUnderSubNonneg.Iic (a : ℝ) : ClosedUnderSubNonneg (Set.Iic a)

An upper closed ray is closed under subtracting nonnegative constants.

In quantified mathematical form, if r ≤ a and 0 ≤ δ, then r - δ ≤ a.

theorem ViscositySolns.ClosedUnderSubNonneg.Iio (a : ℝ) : ClosedUnderSubNonneg (Set.Iio a)

An upper open ray is closed under subtracting nonnegative constants.

In quantified mathematical form, if r < a and 0 ≤ δ, then r - δ < a.

theorem ViscositySolns.ScalarRangeOn.sub_const_of_closedUnderSubNonneg {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {u : Point n → ℝ} {δ : ℝ} (hu : ScalarRangeOn C R u) (hR : ClosedUnderSubNonneg R) (hδ : 0 ≤ δ) : ScalarRangeOn C R fun (x : Point n) => u x - δ

If the scalar set is closed under subtracting nonnegative constants, then subtracting a nonnegative constant preserves scalar range.

In quantified mathematical form, if u x ∈ R for every x ∈ C, if 0 ≤ δ, and if r ∈ R implies r - δ ∈ R, then u x - δ ∈ R for every x ∈ C.

theorem ViscositySolns.ValueBoundedOn.mono_spatial_set {n : ℕ} {C D : Set (Point n)} {u : Point n → ℝ} (hu : ValueBoundedOn D u) (hCD : C ⊆ D) : ValueBoundedOn C u

theorem ViscositySolns.BoundaryComparisonHypothesesOn.boundary {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {u v : Point n → ℝ} (h : BoundaryComparisonHypothesesOn C R u v) : BoundaryComparisonOn C u v

theorem ViscositySolns.BoundaryComparisonHypothesesOn.scalarRange {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {u v : Point n → ℝ} (h : BoundaryComparisonHypothesesOn C R u v) : ScalarRangeOn C R u

theorem ViscositySolns.BoundaryComparisonHypothesesOn.compactClosure {n : ℕ} {C : Set (Point n)} {R : Set ℝ} {u v : Point n → ℝ} (h : BoundaryComparisonHypothesesOn C R u v) : CompactClosure C