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

Compact selection lemmas for stability arguments (LocallyUniformApproximation)

Part of the compact-extremum selection tools used in viscosity stability proofs. Split from Selection.lean; see the umbrella module docstring.

theorem ViscositySolns.tailClosureSuperjetGraph_of_locallyUniform_isMaxOn_sub_hasSecondOrderExpansionWithin {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {φ : Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {J : Jet n} {xᵢ : ι → Point n} {Jᵢ : ι → Jet n} (hlu : LocallyUniformTendstoOn uᵢ u l C) (hu : ContinuousWithinAt u C x) (hxC : x ∈ C) (hx : Filter.Tendsto xᵢ l (nhds x)) (hJ : Filter.Tendsto Jᵢ l (nhds J)) (hcontact : ∀ᶠ (i : ι) in l, xᵢ i ∈ C ∧ IsMaxOn (fun (y : Point n) => uᵢ i y - φ y) C (xᵢ i) ∧ HasSecondOrderExpansionWithin C φ (xᵢ i) (Jᵢ i)) : ((x, u x), J) ∈ TailClosureSuperjetGraph C uᵢ l

Under locally uniform convergence, selected compact maximum contacts whose points and jets converge give tail-closure membership for the limiting superjet triple.

theorem ViscositySolns.tailClosureSubjetGraph_of_locallyUniform_isMinOn_sub_hasSecondOrderExpansionWithin {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {φ : Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {J : Jet n} {xᵢ : ι → Point n} {Jᵢ : ι → Jet n} (hlu : LocallyUniformTendstoOn uᵢ u l C) (hu : ContinuousWithinAt u C x) (hxC : x ∈ C) (hx : Filter.Tendsto xᵢ l (nhds x)) (hJ : Filter.Tendsto Jᵢ l (nhds J)) (hcontact : ∀ᶠ (i : ι) in l, xᵢ i ∈ C ∧ IsMinOn (fun (y : Point n) => uᵢ i y - φ y) C (xᵢ i) ∧ HasSecondOrderExpansionWithin C φ (xᵢ i) (Jᵢ i)) : ((x, u x), J) ∈ TailClosureSubjetGraph C uᵢ l

Under locally uniform convergence, selected compact minimum contacts whose points and jets converge give tail-closure membership for the limiting subjet triple.

theorem ViscositySolns.tailClosureSuperjetGraph_to_ambient_of_locallyUniform_isMaxOn_sub {n : ℕ} {ι : Type u_1} {K C : Set (Point n)} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {φ : Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {J : Jet n} {xᵢ : ι → Point n} {Jᵢ : ι → Jet n} (hKC : K ⊆ C) (hlu : LocallyUniformTendstoOn uᵢ u l K) (hu : ContinuousWithinAt u K x) (hxK : x ∈ K) (hx : Filter.Tendsto xᵢ l (nhds x)) (hJ : Filter.Tendsto Jᵢ l (nhds J)) (hcontact : ∀ᶠ (i : ι) in l, xᵢ i ∈ K ∧ IsMaxOn (fun (y : Point n) => uᵢ i y - φ y) K (xᵢ i) ∧ HasSecondOrderExpansionWithin K φ (xᵢ i) (Jᵢ i)) (hKnhds : ∀ᶠ (i : ι) in l, K ∈ nhdsWithin (xᵢ i) C) : ((x, u x), J) ∈ TailClosureSuperjetGraph C uᵢ l

Let K ⊆ C. Suppose uᵢ converges locally uniformly to u on K, u is continuous within K at x, x ∈ K, xᵢ → x, and Jᵢ → J along l. Assume that the set of indices i for which xᵢ i ∈ K, IsMaxOn (fun y => uᵢ i y - φ y) K (xᵢ i), and HasSecondOrderExpansionWithin K φ (xᵢ i) (Jᵢ i) all hold belongs to l. Assume also that the set of indices i for which K ∈ nhdsWithin (xᵢ i) C belongs to l. Then ((x, u x), J) belongs to the tail closure of the superjet graphs on C.

theorem ViscositySolns.tailClosureSubjetGraph_to_ambient_of_locallyUniform_isMinOn_sub {n : ℕ} {ι : Type u_1} {K C : Set (Point n)} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {φ : Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {J : Jet n} {xᵢ : ι → Point n} {Jᵢ : ι → Jet n} (hKC : K ⊆ C) (hlu : LocallyUniformTendstoOn uᵢ u l K) (hu : ContinuousWithinAt u K x) (hxK : x ∈ K) (hx : Filter.Tendsto xᵢ l (nhds x)) (hJ : Filter.Tendsto Jᵢ l (nhds J)) (hcontact : ∀ᶠ (i : ι) in l, xᵢ i ∈ K ∧ IsMinOn (fun (y : Point n) => uᵢ i y - φ y) K (xᵢ i) ∧ HasSecondOrderExpansionWithin K φ (xᵢ i) (Jᵢ i)) (hKnhds : ∀ᶠ (i : ι) in l, K ∈ nhdsWithin (xᵢ i) C) : ((x, u x), J) ∈ TailClosureSubjetGraph C uᵢ l

Let K ⊆ C. Suppose uᵢ converges locally uniformly to u on K, u is continuous within K at x, x ∈ K, xᵢ → x, and Jᵢ → J along l. Assume that the set of indices i for which xᵢ i ∈ K, IsMinOn (fun y => uᵢ i y - φ y) K (xᵢ i), and HasSecondOrderExpansionWithin K φ (xᵢ i) (Jᵢ i) all hold belongs to l. Assume also that the set of indices i for which K ∈ nhdsWithin (xᵢ i) C belongs to l. Then ((x, u x), J) belongs to the tail closure of the subjet graphs on C.

theorem ViscositySolns.tailClosureSuperjetGraph_to_ambient_of_compactRelativeNeighborhood_isMaxOn_sub {n : ℕ} {ι : Type u_1} {K C : Set (Point n)} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {φ : Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {J : Jet n} {xᵢ : ι → Point n} {Jᵢ : ι → Jet n} (hK : CompactRelativeNeighborhood C x K) (hlu : LocallyUniformTendstoOn uᵢ u l K) (hu : ContinuousWithinAt u K x) (hx : Filter.Tendsto xᵢ l (nhds x)) (hJ : Filter.Tendsto Jᵢ l (nhds J)) (hcontact : ∀ᶠ (i : ι) in l, xᵢ i ∈ K ∧ IsMaxOn (fun (y : Point n) => uᵢ i y - φ y) K (xᵢ i) ∧ HasSecondOrderExpansionWithin K φ (xᵢ i) (Jᵢ i)) : ((x, u x), J) ∈ TailClosureSuperjetGraph C uᵢ l

Selected compact maximum contacts on a compact relative neighborhood give tail-closure membership over the ambient domain.

theorem ViscositySolns.tailClosureSubjetGraph_to_ambient_of_compactRelativeNeighborhood_isMinOn_sub {n : ℕ} {ι : Type u_1} {K C : Set (Point n)} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {φ : Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {J : Jet n} {xᵢ : ι → Point n} {Jᵢ : ι → Jet n} (hK : CompactRelativeNeighborhood C x K) (hlu : LocallyUniformTendstoOn uᵢ u l K) (hu : ContinuousWithinAt u K x) (hx : Filter.Tendsto xᵢ l (nhds x)) (hJ : Filter.Tendsto Jᵢ l (nhds J)) (hcontact : ∀ᶠ (i : ι) in l, xᵢ i ∈ K ∧ IsMinOn (fun (y : Point n) => uᵢ i y - φ y) K (xᵢ i) ∧ HasSecondOrderExpansionWithin K φ (xᵢ i) (Jᵢ i)) : ((x, u x), J) ∈ TailClosureSubjetGraph C uᵢ l

Selected compact minimum contacts on a compact relative neighborhood give tail-closure membership over the ambient domain.

theorem ViscositySolns.eventually_exists_isMaxOn_sub_continuousOn_of_upperSemicontinuousOn_isCompact {n : ℕ} {ι : Type u_1} {K : Set (Point n)} {uᵢ : ι → Point n → ℝ} {φ : Point n → ℝ} {l : Filter ι} (hne : K.Nonempty) (hK : IsCompact K) (husc : ∀ᶠ (i : ι) in l, UpperSemicontinuousOn (uᵢ i) K) (hφ : ContinuousOn φ K) : ∀ᶠ (i : ι) in l, ∃ x ∈ K, IsMaxOn (fun (y : Point n) => uᵢ i y - φ y) K x

Assume K is nonempty and compact, and φ is continuous on K. If the set of indices i for which uᵢ i is upper semicontinuous on K belongs to l, then the set of indices i for which there exists x ∈ K satisfying IsMaxOn (fun y => uᵢ i y - φ y) K x belongs to l.

theorem ViscositySolns.tendsto_argmax_sub_of_uniformTendstoOn_of_strict {n : ℕ} {ι : Type u_1} {K : Set (Point n)} {uᵢ : ι → Point n → ℝ} {u φ : Point n → ℝ} {l : Filter ι} {x₀ : Point n} {xᵢ : ι → Point n} (hunif : UniformTendstoOn uᵢ u l K) (hx₀ : x₀ ∈ K) (hargmax : ∀ᶠ (i : ι) in l, xᵢ i ∈ K ∧ IsMaxOn (fun (y : Point n) => uᵢ i y - φ y) K (xᵢ i)) (hstrict : ∀ V ∈ nhds x₀, ∃ δ > 0, ∀ y ∈ K, y ∉ V → u y - φ y ≤ u x₀ - φ x₀ - δ) : Filter.Tendsto xᵢ l (nhdsWithin x₀ K)

A strict compact maximizer of u - φ attracts compact maximizers of uᵢ - φ under uniform convergence on the compact set.

The strictness hypothesis is deliberately local-neighborhood shaped: outside each neighborhood of x₀, the value of u - φ on K is separated below its value at x₀ by a positive gap.

theorem ViscositySolns.tendsto_argmin_sub_of_uniformTendstoOn_of_strict {n : ℕ} {ι : Type u_1} {K : Set (Point n)} {uᵢ : ι → Point n → ℝ} {u φ : Point n → ℝ} {l : Filter ι} {x₀ : Point n} {xᵢ : ι → Point n} (hunif : UniformTendstoOn uᵢ u l K) (hx₀ : x₀ ∈ K) (hargmin : ∀ᶠ (i : ι) in l, xᵢ i ∈ K ∧ IsMinOn (fun (y : Point n) => uᵢ i y - φ y) K (xᵢ i)) (hstrict : ∀ V ∈ nhds x₀, ∃ δ > 0, ∀ y ∈ K, y ∉ V → u x₀ - φ x₀ + δ ≤ u y - φ y) : Filter.Tendsto xᵢ l (nhdsWithin x₀ K)

A strict compact minimizer of u - φ attracts compact minimizers of uᵢ - φ under uniform convergence on the compact set.

The strictness hypothesis is deliberately local-neighborhood shaped: outside each neighborhood of x₀, the value of u - φ on K is separated above its value at x₀ by a positive gap.

theorem ViscositySolns.tailClosureSuperjetGraph_to_ambient_of_compactRelativeNeighborhood_strict_exists_isMaxOn_sub {n : ℕ} {ι : Type u_1} {K C : Set (Point n)} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {φ : Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {JAt : Point n → Jet n} (hK : CompactRelativeNeighborhood C x K) (hlu : LocallyUniformTendstoOn uᵢ u l K) (hu : ContinuousWithinAt u K x) (hJ : ContinuousWithinAt JAt K x) (hφcont : ContinuousOn φ K) (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 → u y - φ y ≤ u x - φ x - δ) : ((x, u x), JAt x) ∈ TailClosureSuperjetGraph C uᵢ l

Compact relative neighborhood version of the strict maximum selection theorem.

The hypothesis hJ says that the jet assigned to the test function varies continuously at the contact point, and hφexp says this assigned jet is a second-order expansion of the test function at every selected point.

theorem ViscositySolns.tailClosureSubjetGraph_to_ambient_of_compactRelativeNeighborhood_strict_exists_isMinOn_sub {n : ℕ} {ι : Type u_1} {K C : Set (Point n)} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {φ : Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {JAt : Point n → Jet n} (hK : CompactRelativeNeighborhood C x K) (hlu : LocallyUniformTendstoOn uᵢ u l K) (hu : ContinuousWithinAt u K x) (hJ : ContinuousWithinAt JAt K x) (hφcont : ContinuousOn φ K) (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 → u x - φ x + δ ≤ u y - φ y) : ((x, u x), JAt x) ∈ TailClosureSubjetGraph C uᵢ l

Compact relative neighborhood version of the strict minimum selection theorem.

The hypothesis hJ says that the jet assigned to the test function varies continuously at the contact point, and hφexp says this assigned jet is a second-order expansion of the test function at every selected point.

theorem ViscositySolns.tailClosureSuperjetGraph_of_locallyUniform_superjet_hessian_add_identity {n : ℕ} {ι : Type u_1} {C : Set (Point n)} [LocallyCompactSpace ↑C] {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {J : Jet n} {δ : ℝ} (hlu : LocallyUniformTendstoOn uᵢ u l C) (hu : ContinuousWithinAt u C x) (hxC : x ∈ C) (husc : ∀ᶠ (i : ι) in l, UpperSemicontinuousOn (uᵢ i) C) (hδ : 0 < δ) (hJ : J ∈ Superjet C u x) : ((x, u x), { gradient := J.gradient, hessian := J.hessian + δ • 1 }) ∈ TailClosureSuperjetGraph C uᵢ l

Locally uniform approximation theorem with a positive identity-Hessian perturbation for superjets.

If J = (p, X) belongs to Superjet C u x, δ > 0, and uᵢ converges locally uniformly to u on C, then ((x, u x), (p, X + δ I)) belongs to TailClosureSuperjetGraph C uᵢ l. Equivalently, for every set of indices A with A ∈ l, this graph point lies in the closure of ⋃ i ∈ A, SuperjetGraph C (uᵢ i).

theorem ViscositySolns.tailClosureSubjetGraph_of_locallyUniform_subjet_hessian_sub_identity {n : ℕ} {ι : Type u_1} {C : Set (Point n)} [LocallyCompactSpace ↑C] {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {J : Jet n} {δ : ℝ} (hlu : LocallyUniformTendstoOn uᵢ u l C) (hu : ContinuousWithinAt u C x) (hxC : x ∈ C) (hlsc : ∀ᶠ (i : ι) in l, LowerSemicontinuousOn (uᵢ i) C) (hδ : 0 < δ) (hJ : J ∈ Subjet C u x) : ((x, u x), { gradient := J.gradient, hessian := J.hessian - δ • 1 }) ∈ TailClosureSubjetGraph C uᵢ l

Locally uniform approximation theorem with a negative identity-Hessian perturbation for subjets.

If J = (p, X) belongs to Subjet C u x, δ > 0, and uᵢ converges locally uniformly to u on C, then ((x, u x), (p, X - δ I)) belongs to TailClosureSubjetGraph C uᵢ l. Equivalently, for every set of indices A with A ∈ l, this graph point lies in the closure of ⋃ i ∈ A, SubjetGraph C (uᵢ i).

theorem ViscositySolns.tailClosureSuperjetGraph_of_locallyUniform_superjet {n : ℕ} {ι : Type u_1} {C : Set (Point n)} [LocallyCompactSpace ↑C] {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {J : Jet n} (hlu : LocallyUniformTendstoOn uᵢ u l C) (hu : ContinuousWithinAt u C x) (hxC : x ∈ C) (husc : ∀ᶠ (i : ι) in l, UpperSemicontinuousOn (uᵢ i) C) (hJ : J ∈ Superjet C u x) : ((x, u x), J) ∈ TailClosureSuperjetGraph C uᵢ l

Locally uniform approximation theorem for superjets, in tail-closure graph form.

If J ∈ Superjet C u x and uᵢ converges locally uniformly to u on C, then ((x, u x), J) ∈ TailClosureSuperjetGraph C uᵢ l. Equivalently, for every set of indices A with A ∈ l, this graph point lies in the closure of ⋃ i ∈ A, SuperjetGraph C (uᵢ i).

theorem ViscositySolns.tailClosureSubjetGraph_of_locallyUniform_subjet {n : ℕ} {ι : Type u_1} {C : Set (Point n)} [LocallyCompactSpace ↑C] {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {J : Jet n} (hlu : LocallyUniformTendstoOn uᵢ u l C) (hu : ContinuousWithinAt u C x) (hxC : x ∈ C) (hlsc : ∀ᶠ (i : ι) in l, LowerSemicontinuousOn (uᵢ i) C) (hJ : J ∈ Subjet C u x) : ((x, u x), J) ∈ TailClosureSubjetGraph C uᵢ l

Locally uniform approximation theorem for subjets, in tail-closure graph form.

If J ∈ Subjet C u x and uᵢ converges locally uniformly to u on C, then ((x, u x), J) ∈ TailClosureSubjetGraph C uᵢ l. Equivalently, for every set of indices A with A ∈ l, this graph point lies in the closure of ⋃ i ∈ A, SubjetGraph C (uᵢ i).