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

Compact selection for half-relaxed limits

This file proves the compact maximum and minimum selection statements used to approximate semijets of half-relaxed limits.

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

Assume the set of indices i such that xᵢ i ∈ K and IsMaxOn (fun y => uᵢ i y - φ y) K (xᵢ i) belongs to l. Then for every ε > 0 and every set of indices A with A ∈ l, there exists i ∈ A such that xᵢ i ∈ K and upperHalfRelaxedLimit uᵢ l C x - φ x - ε < uᵢ i (xᵢ i) - φ (xᵢ i).

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

Assume the set of indices i such that xᵢ i ∈ K and IsMinOn (fun y => uᵢ i y - φ y) K (xᵢ i) belongs to l. Then for every ε > 0 and every set of indices A with A ∈ l, there exists i ∈ A such that xᵢ i ∈ K and uᵢ i (xᵢ i) - φ (xᵢ i) < lowerHalfRelaxedLimit uᵢ l C x - φ x + ε.

theorem ViscositySolns.exists_isMaxOn_upperHalfRelaxedLimit_sub_test_sub_lt {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C K : 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φC : ContinuousWithinAt φ C x) (hφK : ContinuousOn φ K) (hKne : K.Nonempty) (hKcompact : IsCompact K) (hKnhds : K ∈ nhdsWithin x C) (husc : ∀ᶠ (i : ι) in l, UpperSemicontinuousOn (uᵢ i) K) {A : Set ι} (hA : A ∈ l) : ∃ i ∈ A, ∃ z ∈ K, IsMaxOn (fun (y : Point n) => uᵢ i y - φ y) K z ∧ upperHalfRelaxedLimit uᵢ l C x - φ x - ε < uᵢ i z - φ z

Assume K is nonempty and compact, φ is continuous on K, and the set of indices i for which uᵢ i is upper semicontinuous on K belongs to l. Then for every ε > 0 and every set of indices A with A ∈ l, there exist i ∈ A and z ∈ K such that IsMaxOn (fun y => uᵢ i y - φ y) K z and upperHalfRelaxedLimit uᵢ l C x - φ x - ε < uᵢ i z - φ z.

theorem ViscositySolns.exists_isMinOn_lt_lowerHalfRelaxedLimit_sub_test_add {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C K : 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φC : ContinuousWithinAt φ C x) (hφK : ContinuousOn φ K) (hKne : K.Nonempty) (hKcompact : IsCompact K) (hKnhds : K ∈ nhdsWithin x C) (hlsc : ∀ᶠ (i : ι) in l, LowerSemicontinuousOn (uᵢ i) K) {A : Set ι} (hA : A ∈ l) : ∃ i ∈ A, ∃ z ∈ K, IsMinOn (fun (y : Point n) => uᵢ i y - φ y) K z ∧ uᵢ i z - φ z < lowerHalfRelaxedLimit uᵢ l C x - φ x + ε

Assume K is nonempty and compact, φ is continuous on K, and the set of indices i for which uᵢ i is lower semicontinuous on K belongs to l. Then for every ε > 0 and every set of indices A with A ∈ l, there exist i ∈ A and z ∈ K such that IsMinOn (fun y => uᵢ i y - φ y) K z and uᵢ i z - φ z < lowerHalfRelaxedLimit uᵢ l C x - φ x + ε.

theorem ViscositySolns.exists_isMaxOn_mem_nhds_upperHalfRelaxedLimit_sub_test_sub_lt {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C K : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {ε : ℝ} (hε : 0 < ε) (hxC : x ∈ C) (hKne : K.Nonempty) (hKcompact : IsCompact K) (hKC : K ⊆ C) (hKnhds : K ∈ nhdsWithin x C) (hbddAbove : ∀ y ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hcobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφC : ContinuousOn φ C) (hφK : ContinuousOn φ K) (husc : ∀ᶠ (i : ι) in l, UpperSemicontinuousOn (uᵢ i) K) (hstrict : ∀ V ∈ nhds x, ∃ δ > 0, ∀ y ∈ K, y ∉ V → upperHalfRelaxedLimit uᵢ l C y - φ y ≤ upperHalfRelaxedLimit uᵢ l C x - φ x - δ) {A : Set ι} (hA : A ∈ l) {V : Set (Point n)} (hV : V ∈ nhds x) : ∃ i ∈ A, ∃ z ∈ K, z ∈ V ∧ IsMaxOn (fun (y : Point n) => uᵢ i y - φ y) K z ∧ upperHalfRelaxedLimit uᵢ l C x - φ x - ε < uᵢ i z - φ z

For a strict maximum contact of the upper half-relaxed limit on a compact set K, compact maximum points of uᵢ i - φ can be chosen in any prescribed neighborhood of the contact point.

More precisely, for every ε > 0, every set of indices A with A ∈ l, and every neighborhood V of x, there exist i ∈ A and z ∈ K ∩ V such that z is a maximum point of uᵢ i - φ on K and upperHalfRelaxedLimit uᵢ l C x - φ x - ε < uᵢ i z - φ z.

theorem ViscositySolns.exists_isMinOn_mem_nhds_lowerHalfRelaxedLimit_sub_test_add {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C K : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {ε : ℝ} (hε : 0 < ε) (hxC : x ∈ C) (hKne : K.Nonempty) (hKcompact : IsCompact K) (hKC : K ⊆ C) (hKnhds : K ∈ nhdsWithin x C) (hbddBelow : ∀ y ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hcobddAbove : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφC : ContinuousOn φ C) (hφK : ContinuousOn φ K) (hlsc : ∀ᶠ (i : ι) in l, LowerSemicontinuousOn (uᵢ i) K) (hstrict : ∀ V ∈ nhds x, ∃ δ > 0, ∀ y ∈ K, y ∉ V → lowerHalfRelaxedLimit uᵢ l C x - φ x + δ ≤ lowerHalfRelaxedLimit uᵢ l C y - φ y) {A : Set ι} (hA : A ∈ l) {V : Set (Point n)} (hV : V ∈ nhds x) : ∃ i ∈ A, ∃ z ∈ K, z ∈ V ∧ IsMinOn (fun (y : Point n) => uᵢ i y - φ y) K z ∧ uᵢ i z - φ z < lowerHalfRelaxedLimit uᵢ l C x - φ x + ε

For a strict minimum contact of the lower half-relaxed limit on a compact set K, compact minimum points of uᵢ i - φ can be chosen in any prescribed neighborhood of the contact point.

More precisely, for every ε > 0, every set of indices A with A ∈ l, and every neighborhood V of x, there exist i ∈ A and z ∈ K ∩ V such that z is a minimum point of uᵢ i - φ on K and uᵢ i z - φ z < lowerHalfRelaxedLimit uᵢ l C x - φ x + ε.

theorem ViscositySolns.exists_isMaxOn_mem_nhds_abs_sub_test_upperHalfRelaxedLimit_lt {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C K : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {ε : ℝ} (hε : 0 < ε) (hxC : x ∈ C) (hKne : K.Nonempty) (hKcompact : IsCompact K) (hKC : K ⊆ C) (hKnhds : K ∈ nhdsWithin x C) (hbddAbove : ∀ y ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hcobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφC : ContinuousOn φ C) (hφK : ContinuousOn φ K) (husc : ∀ᶠ (i : ι) in l, UpperSemicontinuousOn (uᵢ i) K) (hstrict : ∀ V ∈ nhds x, ∃ δ > 0, ∀ y ∈ K, y ∉ V → upperHalfRelaxedLimit uᵢ l C y - φ y ≤ upperHalfRelaxedLimit uᵢ l C x - φ x - δ) {A : Set ι} (hA : A ∈ l) {V : Set (Point n)} (hV : V ∈ nhds x) : ∃ i ∈ A, ∃ z ∈ K, z ∈ V ∧ IsMaxOn (fun (y : Point n) => uᵢ i y - φ y) K z ∧ |uᵢ i z - φ z - (upperHalfRelaxedLimit uᵢ l C x - φ x)| < ε

Assume that φ has strict maximum contact with upperHalfRelaxedLimit uᵢ l C at x on K. For every ε > 0, every A ∈ l, and every neighborhood V of x, there exist i ∈ A and z ∈ K ∩ V such that z maximizes uᵢ i - φ on K and |(uᵢ i z - φ z) - (upperHalfRelaxedLimit uᵢ l C x - φ x)| < ε.

theorem ViscositySolns.exists_isMinOn_mem_nhds_abs_sub_test_lowerHalfRelaxedLimit_lt {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C K : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {ε : ℝ} (hε : 0 < ε) (hxC : x ∈ C) (hKne : K.Nonempty) (hKcompact : IsCompact K) (hKC : K ⊆ C) (hKnhds : K ∈ nhdsWithin x C) (hbddBelow : ∀ y ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hcobddAbove : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφC : ContinuousOn φ C) (hφK : ContinuousOn φ K) (hlsc : ∀ᶠ (i : ι) in l, LowerSemicontinuousOn (uᵢ i) K) (hstrict : ∀ V ∈ nhds x, ∃ δ > 0, ∀ y ∈ K, y ∉ V → lowerHalfRelaxedLimit uᵢ l C x - φ x + δ ≤ lowerHalfRelaxedLimit uᵢ l C y - φ y) {A : Set ι} (hA : A ∈ l) {V : Set (Point n)} (hV : V ∈ nhds x) : ∃ i ∈ A, ∃ z ∈ K, z ∈ V ∧ IsMinOn (fun (y : Point n) => uᵢ i y - φ y) K z ∧ |uᵢ i z - φ z - (lowerHalfRelaxedLimit uᵢ l C x - φ x)| < ε

Assume that φ has strict minimum contact with lowerHalfRelaxedLimit uᵢ l C at x on K. For every ε > 0, every A ∈ l, and every neighborhood V of x, there exist i ∈ A and z ∈ K ∩ V such that z minimizes uᵢ i - φ on K and |(uᵢ i z - φ z) - (lowerHalfRelaxedLimit uᵢ l C x - φ x)| < ε.

theorem ViscositySolns.exists_isMaxOn_mem_nhds_abs_upperHalfRelaxedLimit_lt {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C K : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {ε : ℝ} (hε : 0 < ε) (hxC : x ∈ C) (hKne : K.Nonempty) (hKcompact : IsCompact K) (hKC : K ⊆ C) (hKnhds : K ∈ nhdsWithin x C) (hbddAbove : ∀ y ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hcobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφC : ContinuousOn φ C) (hφK : ContinuousOn φ K) (husc : ∀ᶠ (i : ι) in l, UpperSemicontinuousOn (uᵢ i) K) (hstrict : ∀ V ∈ nhds x, ∃ δ > 0, ∀ y ∈ K, y ∉ V → upperHalfRelaxedLimit uᵢ l C y - φ y ≤ upperHalfRelaxedLimit uᵢ l C x - φ x - δ) {A : Set ι} (hA : A ∈ l) {V : Set (Point n)} (hV : V ∈ nhds x) : ∃ i ∈ A, ∃ z ∈ K, z ∈ V ∧ K ∈ nhdsWithin z C ∧ IsMaxOn (fun (y : Point n) => uᵢ i y - φ y) K z ∧ |uᵢ i z - upperHalfRelaxedLimit uᵢ l C x| < ε

Assume that φ has strict maximum contact with upperHalfRelaxedLimit uᵢ l C at x on K and that K ∈ nhdsWithin x C. For every ε > 0, every A ∈ l, and every neighborhood V of x, there exist i ∈ A and z ∈ K ∩ V such that K ∈ nhdsWithin z C, z maximizes uᵢ i - φ on K, and |uᵢ i z - upperHalfRelaxedLimit uᵢ l C x| < ε.

theorem ViscositySolns.exists_isMinOn_mem_nhds_abs_lowerHalfRelaxedLimit_lt {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C K : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {ε : ℝ} (hε : 0 < ε) (hxC : x ∈ C) (hKne : K.Nonempty) (hKcompact : IsCompact K) (hKC : K ⊆ C) (hKnhds : K ∈ nhdsWithin x C) (hbddBelow : ∀ y ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hcobddAbove : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφC : ContinuousOn φ C) (hφK : ContinuousOn φ K) (hlsc : ∀ᶠ (i : ι) in l, LowerSemicontinuousOn (uᵢ i) K) (hstrict : ∀ V ∈ nhds x, ∃ δ > 0, ∀ y ∈ K, y ∉ V → lowerHalfRelaxedLimit uᵢ l C x - φ x + δ ≤ lowerHalfRelaxedLimit uᵢ l C y - φ y) {A : Set ι} (hA : A ∈ l) {V : Set (Point n)} (hV : V ∈ nhds x) : ∃ i ∈ A, ∃ z ∈ K, z ∈ V ∧ K ∈ nhdsWithin z C ∧ IsMinOn (fun (y : Point n) => uᵢ i y - φ y) K z ∧ |uᵢ i z - lowerHalfRelaxedLimit uᵢ l C x| < ε

Assume that φ has strict minimum contact with lowerHalfRelaxedLimit uᵢ l C at x on K and that K ∈ nhdsWithin x C. For every ε > 0, every A ∈ l, and every neighborhood V of x, there exist i ∈ A and z ∈ K ∩ V such that K ∈ nhdsWithin z C, z minimizes uᵢ i - φ on K, and |uᵢ i z - lowerHalfRelaxedLimit uᵢ l C x| < ε.

theorem ViscositySolns.exists_isMaxOn_hasSecondOrderExpansionWithin_mem_nhds_upperHalfRelaxedLimit {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C K : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {JAt : Point n → Jet n} (hxC : x ∈ C) (hKne : K.Nonempty) (hKcompact : IsCompact K) (hKC : K ⊆ C) (hKnhds : K ∈ nhdsWithin x C) (hbddAbove : ∀ y ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hcobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφC : ContinuousOn φ C) (hφK : ContinuousOn φ K) (hJAt : ContinuousWithinAt JAt K x) (hφexp : ∀ y ∈ K, HasSecondOrderExpansionWithin K φ y (JAt y)) (husc : ∀ᶠ (i : ι) in l, UpperSemicontinuousOn (uᵢ i) K) (hstrict : ∀ V ∈ nhds x, ∃ δ > 0, ∀ y ∈ K, y ∉ V → upperHalfRelaxedLimit uᵢ l C y - φ y ≤ upperHalfRelaxedLimit uᵢ l C x - φ x - δ) {A : Set ι} (hA : A ∈ l) {W : Set ((Point n × ℝ) × Jet n)} (hW : W ∈ nhds ((x, upperHalfRelaxedLimit uᵢ l C x), JAt x)) : ∃ i ∈ A, ∃ z ∈ K, ∃ (Jᵢ : Jet n), K ∈ nhdsWithin z C ∧ IsMaxOn (fun (y : Point n) => uᵢ i y - φ y) K z ∧ HasSecondOrderExpansionWithin K φ z Jᵢ ∧ ((z, uᵢ i z), Jᵢ) ∈ W

Let upperLimit x = upperHalfRelaxedLimit uᵢ l C x. Assume that φ has strict maximum contact with upperLimit at x on the compact set K, that K ⊆ C, and that K is a relative neighborhood of x in C. Let JAt be a function from points to jets such that JAt is continuous at x relative to K, and such that for every y ∈ K, the function φ has second-order expansion JAt y at y relative to K.

Then for every A ∈ l and every neighborhood W of ((x, upperLimit x), JAt x), there exist i ∈ A, z ∈ K, and the jet JAt z such that K ∈ nhdsWithin z C, z maximizes uᵢ i - φ on K, φ has second-order expansion JAt z at z relative to K, and ((z, uᵢ i z), JAt z) ∈ W.

theorem ViscositySolns.exists_isMinOn_hasSecondOrderExpansionWithin_mem_nhds_lowerHalfRelaxedLimit {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C K : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {JAt : Point n → Jet n} (hxC : x ∈ C) (hKne : K.Nonempty) (hKcompact : IsCompact K) (hKC : K ⊆ C) (hKnhds : K ∈ nhdsWithin x C) (hbddBelow : ∀ y ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hcobddAbove : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφC : ContinuousOn φ C) (hφK : ContinuousOn φ K) (hJAt : ContinuousWithinAt JAt K x) (hφexp : ∀ y ∈ K, HasSecondOrderExpansionWithin K φ y (JAt y)) (hlsc : ∀ᶠ (i : ι) in l, LowerSemicontinuousOn (uᵢ i) K) (hstrict : ∀ V ∈ nhds x, ∃ δ > 0, ∀ y ∈ K, y ∉ V → lowerHalfRelaxedLimit uᵢ l C x - φ x + δ ≤ lowerHalfRelaxedLimit uᵢ l C y - φ y) {A : Set ι} (hA : A ∈ l) {W : Set ((Point n × ℝ) × Jet n)} (hW : W ∈ nhds ((x, lowerHalfRelaxedLimit uᵢ l C x), JAt x)) : ∃ i ∈ A, ∃ z ∈ K, ∃ (Jᵢ : Jet n), K ∈ nhdsWithin z C ∧ IsMinOn (fun (y : Point n) => uᵢ i y - φ y) K z ∧ HasSecondOrderExpansionWithin K φ z Jᵢ ∧ ((z, uᵢ i z), Jᵢ) ∈ W

Let lowerLimit x = lowerHalfRelaxedLimit uᵢ l C x. Assume that φ has strict minimum contact with lowerLimit at x on the compact set K, that K ⊆ C, and that K is a relative neighborhood of x in C. Let JAt be a function from points to jets such that JAt is continuous at x relative to K, and such that for every y ∈ K, the function φ has second-order expansion JAt y at y relative to K.

Then for every A ∈ l and every neighborhood W of ((x, lowerLimit x), JAt x), there exist i ∈ A, z ∈ K, and the jet JAt z such that K ∈ nhdsWithin z C, z minimizes uᵢ i - φ on K, φ has second-order expansion JAt z at z relative to K, and ((z, uᵢ i z), JAt z) ∈ W.