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

Basic half-relaxed limit definitions and estimates

This file contains the definitions of upper and lower half-relaxed limits and basic estimates derived from the limsup and liminf definitions.

def ViscositySolns.halfRelaxedFilter {n : ℕ} {ι : Type u_1} (l : Filter ι) (C : Set (Point n)) (x : Point n) : Filter (ι × Point n)

The product filter used in the definition of half-relaxed limits.

Membership in this product filter means the following: a set of pairs contains A × V for some A ∈ l and some V ∈ nhdsWithin x C. Thus the index is restricted by the filter l, while the spatial variable is restricted to a relative neighborhood of x in C.

Equations

• ViscositySolns.halfRelaxedFilter l C x = l ×ˢ nhdsWithin x C

def ViscositySolns.halfRelaxedValue {n : ℕ} {ι : Type u_1} (uᵢ : ι → Point n → ℝ) (q : ι × Point n) : ℝ

The scalar value whose limsup/liminf defines the half-relaxed limits.

Equations

• ViscositySolns.halfRelaxedValue uᵢ q = uᵢ q.1 q.2

noncomputable def ViscositySolns.upperHalfRelaxedLimit {n : ℕ} {ι : Type u_1} (uᵢ : ι → Point n → ℝ) (l : Filter ι) (C : Set (Point n)) (x : Point n) : ℝ

The upper half-relaxed limit \bar u(x) = limsup_{i, y -> x, y ∈ C} u_i(y).

Equations

• ViscositySolns.upperHalfRelaxedLimit uᵢ l C x = Filter.limsup (ViscositySolns.halfRelaxedValue uᵢ) (ViscositySolns.halfRelaxedFilter l C x)

noncomputable def ViscositySolns.lowerHalfRelaxedLimit {n : ℕ} {ι : Type u_1} (uᵢ : ι → Point n → ℝ) (l : Filter ι) (C : Set (Point n)) (x : Point n) : ℝ

The lower half-relaxed limit \underline u(x) = liminf_{i, y -> x, y ∈ C} u_i(y).

Equations

• ViscositySolns.lowerHalfRelaxedLimit uᵢ l C x = Filter.liminf (ViscositySolns.halfRelaxedValue uᵢ) (ViscositySolns.halfRelaxedFilter l C x)

theorem ViscositySolns.halfRelaxedFilter_def {n : ℕ} {ι : Type u_1} (l : Filter ι) (C : Set (Point n)) (x : Point n) : halfRelaxedFilter l C x = l ×ˢ nhdsWithin x C

theorem ViscositySolns.upperHalfRelaxedLimit_def {n : ℕ} {ι : Type u_1} (uᵢ : ι → Point n → ℝ) (l : Filter ι) (C : Set (Point n)) (x : Point n) : upperHalfRelaxedLimit uᵢ l C x = Filter.limsup (fun (q : ι × Point n) => uᵢ q.1 q.2) (l ×ˢ nhdsWithin x C)

theorem ViscositySolns.lowerHalfRelaxedLimit_def {n : ℕ} {ι : Type u_1} (uᵢ : ι → Point n → ℝ) (l : Filter ι) (C : Set (Point n)) (x : Point n) : lowerHalfRelaxedLimit uᵢ l C x = Filter.liminf (fun (q : ι × Point n) => uᵢ q.1 q.2) (l ×ˢ nhdsWithin x C)

theorem ViscositySolns.upperHalfRelaxedLimit_congr {n : ℕ} {ι : Type u_1} {uᵢ vᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} (h : ∀ᶠ (q : ι × Point n) in halfRelaxedFilter l C x, halfRelaxedValue uᵢ q = halfRelaxedValue vᵢ q) : upperHalfRelaxedLimit uᵢ l C x = upperHalfRelaxedLimit vᵢ l C x

If uᵢ q.1 q.2 = vᵢ q.1 q.2 for all pairs q = (i, y) in some member of halfRelaxedFilter l C x, then the two upper half-relaxed limits at x are equal.

theorem ViscositySolns.lowerHalfRelaxedLimit_congr {n : ℕ} {ι : Type u_1} {uᵢ vᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} (h : ∀ᶠ (q : ι × Point n) in halfRelaxedFilter l C x, halfRelaxedValue uᵢ q = halfRelaxedValue vᵢ q) : lowerHalfRelaxedLimit uᵢ l C x = lowerHalfRelaxedLimit vᵢ l C x

If uᵢ q.1 q.2 = vᵢ q.1 q.2 for all pairs q = (i, y) in some member of halfRelaxedFilter l C x, then the two lower half-relaxed limits at x are equal.

theorem ViscositySolns.upperHalfRelaxedLimit_congr_of_eventually_eqOn {n : ℕ} {ι : Type u_1} {uᵢ vᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} (h : ∀ᶠ (i : ι) in l, Set.EqOn (uᵢ i) (vᵢ i) C) : upperHalfRelaxedLimit uᵢ l C x = upperHalfRelaxedLimit vᵢ l C x

If the set of indices i for which uᵢ i and vᵢ i agree at every point of C belongs to l, then the two upper half-relaxed limits at x are equal.

theorem ViscositySolns.lowerHalfRelaxedLimit_congr_of_eventually_eqOn {n : ℕ} {ι : Type u_1} {uᵢ vᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} (h : ∀ᶠ (i : ι) in l, Set.EqOn (uᵢ i) (vᵢ i) C) : lowerHalfRelaxedLimit uᵢ l C x = lowerHalfRelaxedLimit vᵢ l C x

If the set of indices i for which uᵢ i and vᵢ i agree at every point of C belongs to l, then the two lower half-relaxed limits at x are equal.

theorem ViscositySolns.upperHalfRelaxedLimit_le_of_eventually_leOn {n : ℕ} {ι : Type u_1} {uᵢ vᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} (h : ∀ᶠ (i : ι) in l, ∀ y ∈ C, uᵢ i y ≤ vᵢ i y) (hu : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hv : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue vᵢ)) : upperHalfRelaxedLimit uᵢ l C x ≤ upperHalfRelaxedLimit vᵢ l C x

Assume the set of indices i such that ∀ y ∈ C, uᵢ i y <= vᵢ i y belongs to l. Under the boundedness hypotheses needed to evaluate real-valued limsup, the upper half-relaxed limit of uᵢ at x is at most the upper half-relaxed limit of vᵢ at x.

theorem ViscositySolns.lowerHalfRelaxedLimit_le_of_eventually_leOn {n : ℕ} {ι : Type u_1} {uᵢ vᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} (h : ∀ᶠ (i : ι) in l, ∀ y ∈ C, uᵢ i y ≤ vᵢ i y) (hu : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hv : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue vᵢ)) : lowerHalfRelaxedLimit uᵢ l C x ≤ lowerHalfRelaxedLimit vᵢ l C x

Assume the set of indices i such that ∀ y ∈ C, uᵢ i y <= vᵢ i y belongs to l. Under the boundedness hypotheses needed to evaluate real-valued liminf, the lower half-relaxed limit of uᵢ at x is at most the lower half-relaxed limit of vᵢ at x.

theorem ViscositySolns.eventually_mem_halfRelaxedFilter_of_mem {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {x : Point n} {S : Set (ι × Point n)} (hS : S ∈ halfRelaxedFilter l C x) : ∀ᶠ (z : Point n) in nhdsWithin x C, S ∈ halfRelaxedFilter l C z

Events for the half-relaxed product filter at x remain events for the half-relaxed product filter at all nearby points z ∈ C.

More explicitly: if S ∈ l ×ˢ nhdsWithin x C, then the set of points z such that S ∈ l ×ˢ nhdsWithin z C belongs to nhdsWithin x C.

theorem ViscositySolns.upperSemicontinuousOn_upperHalfRelaxedLimit {n : ℕ} {ι : Type u_1} (uᵢ : ι → Point n → ℝ) (l : Filter ι) (C : Set (Point n)) (hbddAbove : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hcobddBelow : ∀ x ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) : UpperSemicontinuousOn (upperHalfRelaxedLimit uᵢ l C) C

Upper semicontinuity of the upper half-relaxed limit, with the boundedness hypotheses needed by real-valued limsup.

theorem ViscositySolns.lowerSemicontinuousOn_lowerHalfRelaxedLimit {n : ℕ} {ι : Type u_1} (uᵢ : ι → Point n → ℝ) (l : Filter ι) (C : Set (Point n)) (hbddBelow : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hcobddAbove : ∀ x ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) : LowerSemicontinuousOn (lowerHalfRelaxedLimit uᵢ l C) C

Lower semicontinuity of the lower half-relaxed limit, with the boundedness hypotheses needed by real-valued liminf.

theorem ViscositySolns.eventually_forall_lt_of_isCompact_upperHalfRelaxedLimit_lt {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C E : Set (Point n)} {a b : ℝ} (hEcompact : IsCompact E) (hEC : E ⊆ C) (hbddAbove : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hub : ∀ x ∈ E, upperHalfRelaxedLimit uᵢ l C x < a) (hab : a < b) : ∀ᶠ (i : ι) in l, ∀ y ∈ E, uᵢ i y < b

Compact upper bound from strict upper half-relaxed bounds.

Assume E is compact, E ⊆ C, and upperHalfRelaxedLimit uᵢ l C x < a for every x ∈ E. Then for every b > a, the set of indices i for which uᵢ i y < b for all y ∈ E belongs to l.

theorem ViscositySolns.eventually_forall_lt_of_lt_isCompact_lowerHalfRelaxedLimit {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C E : Set (Point n)} {a b : ℝ} (hEcompact : IsCompact E) (hEC : E ⊆ C) (hbddBelow : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hlb : ∀ x ∈ E, a < lowerHalfRelaxedLimit uᵢ l C x) (hba : b < a) : ∀ᶠ (i : ι) in l, ∀ y ∈ E, b < uᵢ i y

Compact lower bound from strict lower half-relaxed bounds.

Assume E is compact, E ⊆ C, and a < lowerHalfRelaxedLimit uᵢ l C x for every x ∈ E. Then for every b < a, the set of indices i for which b < uᵢ i y for all y ∈ E belongs to l.

theorem ViscositySolns.eventually_sub_test_lt_of_upperHalfRelaxedLimit_sub_test_lt {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {a b : ℝ} (hbddAbove : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφ : ContinuousWithinAt φ C x) (hlt : upperHalfRelaxedLimit uᵢ l C x - φ x < a) (hab : a < b) : ∀ᶠ (q : ι × Point n) in halfRelaxedFilter l C x, uᵢ q.1 q.2 - φ q.2 < b

If the upper half-relaxed limit satisfies upperHalfRelaxedLimit uᵢ l C x - φ x < a, then the approximating values uᵢ i y - φ y satisfy the following filter statement for every b > a: the set of pairs (i, y) such that uᵢ i y - φ y < b belongs to halfRelaxedFilter l C x.

theorem ViscositySolns.eventually_lt_sub_test_of_lt_lowerHalfRelaxedLimit_sub_test {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {a b : ℝ} (hbddBelow : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφ : ContinuousWithinAt φ C x) (hlt : a < lowerHalfRelaxedLimit uᵢ l C x - φ x) (hba : b < a) : ∀ᶠ (q : ι × Point n) in halfRelaxedFilter l C x, b < uᵢ q.1 q.2 - φ q.2

If the lower half-relaxed limit satisfies a < lowerHalfRelaxedLimit uᵢ l C x - φ x, then the approximating values uᵢ i y - φ y satisfy the following filter statement for every b < a: the set of pairs (i, y) such that b < uᵢ i y - φ y belongs to halfRelaxedFilter l C x.

theorem ViscositySolns.eventually_forall_sub_test_lt_of_isCompact_upperHalfRelaxedLimit_sub_test_lt {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C E : Set (Point n)} {φ : Point n → ℝ} {a b : ℝ} (hEcompact : IsCompact E) (hEC : E ⊆ C) (hbddAbove : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφ : ∀ x ∈ E, ContinuousWithinAt φ C x) (hub : ∀ x ∈ E, upperHalfRelaxedLimit uᵢ l C x - φ x < a) (hab : a < b) : ∀ᶠ (i : ι) in l, ∀ y ∈ E, uᵢ i y - φ y < b

Compact upper bound for uᵢ - φ from strict upper half-relaxed test bounds.

Assume E is compact, E ⊆ C, and upperHalfRelaxedLimit uᵢ l C x - φ x < a for every x ∈ E. If a < b, then the set of indices i for which uᵢ i y - φ y < b for all y ∈ E belongs to l.

theorem ViscositySolns.eventually_forall_lt_sub_test_of_lt_isCompact_lowerHalfRelaxedLimit_sub_test {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C E : Set (Point n)} {φ : Point n → ℝ} {a b : ℝ} (hEcompact : IsCompact E) (hEC : E ⊆ C) (hbddBelow : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφ : ∀ x ∈ E, ContinuousWithinAt φ C x) (hlb : ∀ x ∈ E, a < lowerHalfRelaxedLimit uᵢ l C x - φ x) (hba : b < a) : ∀ᶠ (i : ι) in l, ∀ y ∈ E, b < uᵢ i y - φ y

Compact lower bound for uᵢ - φ from strict lower half-relaxed test bounds.

Assume E is compact, E ⊆ C, and a < lowerHalfRelaxedLimit uᵢ l C x - φ x for every x ∈ E. If b < a, then the set of indices i for which b < uᵢ i y - φ y for all y ∈ E belongs to l.

theorem ViscositySolns.frequently_lt_upperHalfRelaxedLimit {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} {a : ℝ} (hcobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (ha : a < upperHalfRelaxedLimit uᵢ l C x) : ∃ᶠ (q : ι × Point n) in halfRelaxedFilter l C x, a < halfRelaxedValue uᵢ q

If a < upperHalfRelaxedLimit uᵢ l C x, then every member of halfRelaxedFilter l C x intersects the set of pairs (i, y) satisfying a < uᵢ i y.

theorem ViscositySolns.frequently_lowerHalfRelaxedLimit_lt {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} {a : ℝ} (hcobddAbove : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (ha : lowerHalfRelaxedLimit uᵢ l C x < a) : ∃ᶠ (q : ι × Point n) in halfRelaxedFilter l C x, halfRelaxedValue uᵢ q < a

If lowerHalfRelaxedLimit uᵢ l C x < a, then every member of halfRelaxedFilter l C x intersects the set of pairs (i, y) satisfying uᵢ i y < a.

theorem ViscositySolns.exists_upperHalfRelaxedLimit_sub_lt {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} {ε : ℝ} (hε : 0 < ε) (hcobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) {A : Set ι} (hA : A ∈ l) {V : Set (Point n)} (hV : V ∈ nhdsWithin x C) : ∃ i ∈ A, ∃ y ∈ V, upperHalfRelaxedLimit uᵢ l C x - ε < uᵢ i y

For every ε > 0, every set of indices A with A ∈ l, and every V ∈ nhdsWithin x C, there exist i ∈ A and y ∈ V such that upperHalfRelaxedLimit uᵢ l C x - ε < uᵢ i y.

theorem ViscositySolns.exists_lt_lowerHalfRelaxedLimit_add {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} {ε : ℝ} (hε : 0 < ε) (hcobddAbove : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) {A : Set ι} (hA : A ∈ l) {V : Set (Point n)} (hV : V ∈ nhdsWithin x C) : ∃ i ∈ A, ∃ y ∈ V, uᵢ i y < lowerHalfRelaxedLimit uᵢ l C x + ε

For every ε > 0, every set of indices A with A ∈ l, and every V ∈ nhdsWithin x C, there exist i ∈ A and y ∈ V such that uᵢ i y < lowerHalfRelaxedLimit uᵢ l C x + ε.

theorem ViscositySolns.frequently_lt_upperHalfRelaxedLimit_sub_test {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {ε : ℝ} (hε : 0 < ε) (hcobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφ : ContinuousWithinAt φ C x) : ∃ᶠ (q : ι × Point n) in halfRelaxedFilter l C x, upperHalfRelaxedLimit uᵢ l C x - φ x - ε < uᵢ q.1 q.2 - φ q.2

After subtracting a continuous test function, the approximating family has the following lower selection property: for every ε > 0, every member of halfRelaxedFilter l C x intersects the set of pairs (i, y) satisfying upperHalfRelaxedLimit uᵢ l C x - φ x - ε < uᵢ i y - φ y.

theorem ViscositySolns.frequently_lowerHalfRelaxedLimit_sub_test_lt {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {ε : ℝ} (hε : 0 < ε) (hcobddAbove : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφ : ContinuousWithinAt φ C x) : ∃ᶠ (q : ι × Point n) in halfRelaxedFilter l C x, uᵢ q.1 q.2 - φ q.2 < lowerHalfRelaxedLimit uᵢ l C x - φ x + ε

After subtracting a continuous test function, the approximating family has the following upper selection property: for every ε > 0, every member of halfRelaxedFilter l C x intersects the set of pairs (i, y) satisfying uᵢ i y - φ y < lowerHalfRelaxedLimit uᵢ l C x - φ x + ε.

theorem ViscositySolns.exists_upperHalfRelaxedLimit_sub_test_sub_lt {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {ε : ℝ} (hε : 0 < ε) (hcobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφ : ContinuousWithinAt φ C x) {A : Set ι} (hA : A ∈ l) {V : Set (Point n)} (hV : V ∈ nhdsWithin x C) : ∃ i ∈ A, ∃ y ∈ V, upperHalfRelaxedLimit uᵢ l C x - φ x - ε < uᵢ i y - φ y

For every ε > 0, every set of indices A with A ∈ l, and every V ∈ nhdsWithin x C, there exist i ∈ A and y ∈ V such that upperHalfRelaxedLimit uᵢ l C x - φ x - ε < uᵢ i y - φ y.

theorem ViscositySolns.exists_lt_lowerHalfRelaxedLimit_sub_test_add {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {ε : ℝ} (hε : 0 < ε) (hcobddAbove : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφ : ContinuousWithinAt φ C x) {A : Set ι} (hA : A ∈ l) {V : Set (Point n)} (hV : V ∈ nhdsWithin x C) : ∃ i ∈ A, ∃ y ∈ V, uᵢ i y - φ y < lowerHalfRelaxedLimit uᵢ l C x - φ x + ε

For every ε > 0, every set of indices A with A ∈ l, and every V ∈ nhdsWithin x C, there exist i ∈ A and y ∈ V such that uᵢ i y - φ y < lowerHalfRelaxedLimit uᵢ l C x - φ x + ε.