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

Compact selection lemmas for stability arguments (CompactContact)

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

theorem ViscositySolns.ContinuousOn.upperSemicontinuousOn_real {n : ℕ} {C : Set (Point n)} {φ : Point n → ℝ} (hφ : ContinuousOn φ C) : UpperSemicontinuousOn φ C

A continuous function is upper semicontinuous on a set.

theorem ViscositySolns.ContinuousOn.lowerSemicontinuousOn_real {n : ℕ} {C : Set (Point n)} {φ : Point n → ℝ} (hφ : ContinuousOn φ C) : LowerSemicontinuousOn φ C

A continuous function is lower semicontinuous on a set.

theorem ViscositySolns.UpperSemicontinuousOn.sub_continuousOn {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} (hu : UpperSemicontinuousOn u C) (hφ : ContinuousOn φ C) : UpperSemicontinuousOn (fun (x : Point n) => u x - φ x) C

Subtracting a continuous perturbation preserves upper semicontinuity.

theorem ViscositySolns.LowerSemicontinuousOn.sub_continuousOn {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} (hu : LowerSemicontinuousOn u C) (hφ : ContinuousOn φ C) : LowerSemicontinuousOn (fun (x : Point n) => u x - φ x) C

Subtracting a continuous perturbation preserves lower semicontinuity.

theorem ViscositySolns.exists_isMaxOn_of_upperSemicontinuousOn_isCompact {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} (hne : K.Nonempty) (hK : IsCompact K) (hu : UpperSemicontinuousOn u K) : ∃ x ∈ K, IsMaxOn u K x

An upper semicontinuous function attains its maximum on a nonempty compact set.

theorem ViscositySolns.exists_isMinOn_of_lowerSemicontinuousOn_isCompact {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} (hne : K.Nonempty) (hK : IsCompact K) (hu : LowerSemicontinuousOn u K) : ∃ x ∈ K, IsMinOn u K x

A lower semicontinuous function attains its minimum on a nonempty compact set.

theorem ViscositySolns.exists_isMaxOn_sub_continuousOn_of_upperSemicontinuousOn_isCompact {n : ℕ} {K : Set (Point n)} {u φ : Point n → ℝ} (hne : K.Nonempty) (hK : IsCompact K) (hu : UpperSemicontinuousOn u K) (hφ : ContinuousOn φ K) : ∃ x ∈ K, IsMaxOn (fun (y : Point n) => u y - φ y) K x

Upper semicontinuous functions minus continuous perturbations attain maxima on nonempty compact sets.

theorem ViscositySolns.exists_isMinOn_sub_continuousOn_of_lowerSemicontinuousOn_isCompact {n : ℕ} {K : Set (Point n)} {u φ : Point n → ℝ} (hne : K.Nonempty) (hK : IsCompact K) (hu : LowerSemicontinuousOn u K) (hφ : ContinuousOn φ K) : ∃ x ∈ K, IsMinOn (fun (y : Point n) => u y - φ y) K x

Lower semicontinuous functions minus continuous perturbations attain minima on nonempty compact sets.

theorem ViscositySolns.exists_isLocalMaxOn_sub_continuousOn_of_upperSemicontinuousOn_isCompact {n : ℕ} {K : Set (Point n)} {u φ : Point n → ℝ} (hne : K.Nonempty) (hK : IsCompact K) (hu : UpperSemicontinuousOn u K) (hφ : ContinuousOn φ K) : ∃ x ∈ K, IsLocalMaxOn (fun (y : Point n) => u y - φ y) K x

The compact maximum selected above is also a local maximum on the compact set.

theorem ViscositySolns.exists_isLocalMinOn_sub_continuousOn_of_lowerSemicontinuousOn_isCompact {n : ℕ} {K : Set (Point n)} {u φ : Point n → ℝ} (hne : K.Nonempty) (hK : IsCompact K) (hu : LowerSemicontinuousOn u K) (hφ : ContinuousOn φ K) : ∃ x ∈ K, IsLocalMinOn (fun (y : Point n) => u y - φ y) K x

The compact minimum selected above is also a local minimum on the compact set.

theorem ViscositySolns.touchesAboveOn_of_isLocalMaxOn_sub {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} (hmax : IsLocalMaxOn (fun (y : Point n) => u y - φ y) C x) : TouchesAboveOn C u φ x

A local maximum of u - φ is exactly a touching from above of u by φ.

theorem ViscositySolns.touchesBelowOn_of_isLocalMinOn_sub {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} (hmin : IsLocalMinOn (fun (y : Point n) => u y - φ y) C x) : TouchesBelowOn C u φ x

A local minimum of u - φ is exactly a touching from below of u by φ.

theorem ViscositySolns.touchesAboveOn_of_isMaxOn_sub {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} (hmax : IsMaxOn (fun (y : Point n) => u y - φ y) C x) : TouchesAboveOn C u φ x

A global maximum of u - φ on C gives a touching from above on C.

theorem ViscositySolns.touchesBelowOn_of_isMinOn_sub {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} (hmin : IsMinOn (fun (y : Point n) => u y - φ y) C x) : TouchesBelowOn C u φ x

A global minimum of u - φ on C gives a touching from below on C.

theorem ViscositySolns.strict_isMaxOn_sub_quadraticModel_add_identity_of_forall_le_half {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} {x p : Point n} {X : Hessian n} {δ : ℝ} (hδ : 0 < δ) (hle : ∀ y ∈ K, u y ≤ quadraticModel x (u x) p (X + (δ / 2) • 1) y) (V : Set (Point n)) : V ∈ nhds x → ∃ η > 0, ∀ y ∈ K, y ∉ V → u y - quadraticModel x (u x) p (X + δ • 1) y ≤ u x - quadraticModel x (u x) p (X + δ • 1) x - η

If the half-size identity-Hessian perturbation supports u from above on K, then the full perturbation has strict contact from above on K.

theorem ViscositySolns.strict_isMinOn_sub_quadraticModel_sub_identity_of_forall_half_le {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} {x p : Point n} {X : Hessian n} {δ : ℝ} (hδ : 0 < δ) (hle : ∀ y ∈ K, quadraticModel x (u x) p (X - (δ / 2) • 1) y ≤ u y) (V : Set (Point n)) : V ∈ nhds x → ∃ η > 0, ∀ y ∈ K, y ∉ V → u x - quadraticModel x (u x) p (X - δ • 1) x + η ≤ u y - quadraticModel x (u x) p (X - δ • 1) y

If the half-size identity-Hessian perturbation supports u from below on K, then the full perturbation has strict contact from below on K.

theorem ViscositySolns.superjetGraph_of_isLocalMaxOn_sub_hasSecondOrderExpansionWithin {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} {J : Jet n} (hx : x ∈ C) (hmax : IsLocalMaxOn (fun (y : Point n) => u y - φ y) C x) (hφ : HasSecondOrderExpansionWithin C φ x J) : ((x, u x), J) ∈ SuperjetGraph C u

A selected local maximum contact gives a superjet graph point.

theorem ViscositySolns.subjetGraph_of_isLocalMinOn_sub_hasSecondOrderExpansionWithin {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} {J : Jet n} (hx : x ∈ C) (hmin : IsLocalMinOn (fun (y : Point n) => u y - φ y) C x) (hφ : HasSecondOrderExpansionWithin C φ x J) : ((x, u x), J) ∈ SubjetGraph C u

A selected local minimum contact gives a subjet graph point.

theorem ViscositySolns.superjetGraph_of_isMaxOn_sub_hasSecondOrderExpansionWithin {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} {J : Jet n} (hx : x ∈ C) (hmax : IsMaxOn (fun (y : Point n) => u y - φ y) C x) (hφ : HasSecondOrderExpansionWithin C φ x J) : ((x, u x), J) ∈ SuperjetGraph C u

A selected compact maximum contact gives a superjet graph point.

theorem ViscositySolns.subjetGraph_of_isMinOn_sub_hasSecondOrderExpansionWithin {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} {J : Jet n} (hx : x ∈ C) (hmin : IsMinOn (fun (y : Point n) => u y - φ y) C x) (hφ : HasSecondOrderExpansionWithin C φ x J) : ((x, u x), J) ∈ SubjetGraph C u

A selected compact minimum contact gives a subjet graph point.

theorem ViscositySolns.eventually_exists_superjetGraph_of_isLocalMaxOn_sub_hasSecondOrderExpansionWithin {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {φ : Point n → ℝ} {Jᵢ : ι → Jet n} {l : Filter ι} (h : ∀ᶠ (i : ι) in l, ∃ x ∈ C, IsLocalMaxOn (fun (y : Point n) => uᵢ i y - φ y) C x ∧ HasSecondOrderExpansionWithin C φ x (Jᵢ i)) : ∀ᶠ (i : ι) in l, ∃ x ∈ C, ((x, uᵢ i x), Jᵢ i) ∈ SuperjetGraph C (uᵢ i)

If the set of indices i for which there exists a local maximum contact between uᵢ i and a test function φ with second-order expansion Jᵢ i belongs to l, then the set of indices i for which there exists a corresponding superjet graph point belongs to l.

theorem ViscositySolns.eventually_exists_subjetGraph_of_isLocalMinOn_sub_hasSecondOrderExpansionWithin {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {φ : Point n → ℝ} {Jᵢ : ι → Jet n} {l : Filter ι} (h : ∀ᶠ (i : ι) in l, ∃ x ∈ C, IsLocalMinOn (fun (y : Point n) => uᵢ i y - φ y) C x ∧ HasSecondOrderExpansionWithin C φ x (Jᵢ i)) : ∀ᶠ (i : ι) in l, ∃ x ∈ C, ((x, uᵢ i x), Jᵢ i) ∈ SubjetGraph C (uᵢ i)

If the set of indices i for which there exists a local minimum contact between uᵢ i and a test function φ with second-order expansion Jᵢ i belongs to l, then the set of indices i for which there exists a corresponding subjet graph point belongs to l.

theorem ViscositySolns.eventually_exists_superjetGraph_of_isMaxOn_sub_hasSecondOrderExpansionWithin {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {φ : Point n → ℝ} {Jᵢ : ι → Jet n} {l : Filter ι} (h : ∀ᶠ (i : ι) in l, ∃ x ∈ C, IsMaxOn (fun (y : Point n) => uᵢ i y - φ y) C x ∧ HasSecondOrderExpansionWithin C φ x (Jᵢ i)) : ∀ᶠ (i : ι) in l, ∃ x ∈ C, ((x, uᵢ i x), Jᵢ i) ∈ SuperjetGraph C (uᵢ i)

If the set of indices i for which there exists a maximum point of uᵢ i - φ on C with second-order expansion Jᵢ i belongs to l, then the set of indices i for which there exists a corresponding superjet graph point belongs to l.

theorem ViscositySolns.eventually_exists_subjetGraph_of_isMinOn_sub_hasSecondOrderExpansionWithin {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {φ : Point n → ℝ} {Jᵢ : ι → Jet n} {l : Filter ι} (h : ∀ᶠ (i : ι) in l, ∃ x ∈ C, IsMinOn (fun (y : Point n) => uᵢ i y - φ y) C x ∧ HasSecondOrderExpansionWithin C φ x (Jᵢ i)) : ∀ᶠ (i : ι) in l, ∃ x ∈ C, ((x, uᵢ i x), Jᵢ i) ∈ SubjetGraph C (uᵢ i)

If the set of indices i for which there exists a minimum point of uᵢ i - φ on C with second-order expansion Jᵢ i belongs to l, then the set of indices i for which there exists a corresponding subjet graph point belongs to l.

theorem ViscositySolns.exists_mem_tailUnion_superjetGraph_of_eventually_exists_superjetGraph {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {Jᵢ : ι → Jet n} {l : Filter ι} [l.NeBot] (h : ∀ᶠ (i : ι) in l, ∃ x ∈ C, ((x, uᵢ i x), Jᵢ i) ∈ SuperjetGraph C (uᵢ i)) {A : Set ι} (hA : A ∈ l) : ∃ (z : (Point n × ℝ) × Jet n), z ∈ ⋃ i ∈ A, SuperjetGraph C (uᵢ i)

Assume that the set of indices i for which there exists x ∈ C with ((x, uᵢ i x), Jᵢ i) ∈ SuperjetGraph C (uᵢ i) belongs to the filter l. Then, for every set of indices A with A ∈ l, the union ⋃ i ∈ A, SuperjetGraph C (uᵢ i) is nonempty.

theorem ViscositySolns.exists_mem_tailUnion_subjetGraph_of_eventually_exists_subjetGraph {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {Jᵢ : ι → Jet n} {l : Filter ι} [l.NeBot] (h : ∀ᶠ (i : ι) in l, ∃ x ∈ C, ((x, uᵢ i x), Jᵢ i) ∈ SubjetGraph C (uᵢ i)) {A : Set ι} (hA : A ∈ l) : ∃ (z : (Point n × ℝ) × Jet n), z ∈ ⋃ i ∈ A, SubjetGraph C (uᵢ i)

Assume that the set of indices i for which there exists x ∈ C with ((x, uᵢ i x), Jᵢ i) ∈ SubjetGraph C (uᵢ i) belongs to the filter l. Then, for every set of indices A with A ∈ l, the union ⋃ i ∈ A, SubjetGraph C (uᵢ i) is nonempty.

theorem ViscositySolns.exists_mem_tailUnion_superjetGraph_of_eventually_exists_isMaxOn_sub {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {φ : Point n → ℝ} {Jᵢ : ι → Jet n} {l : Filter ι} [l.NeBot] (h : ∀ᶠ (i : ι) in l, ∃ x ∈ C, IsMaxOn (fun (y : Point n) => uᵢ i y - φ y) C x ∧ HasSecondOrderExpansionWithin C φ x (Jᵢ i)) {A : Set ι} (hA : A ∈ l) : ∃ (z : (Point n × ℝ) × Jet n), z ∈ ⋃ i ∈ A, SuperjetGraph C (uᵢ i)

Assume that the set of indices i for which there exists x ∈ C satisfying IsMaxOn (fun y => uᵢ i y - φ y) C x and HasSecondOrderExpansionWithin C φ x (Jᵢ i) belongs to the filter l. Then, for every set of indices A with A ∈ l, the union ⋃ i ∈ A, SuperjetGraph C (uᵢ i) contains a graph point.

theorem ViscositySolns.exists_mem_tailUnion_subjetGraph_of_eventually_exists_isMinOn_sub {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {φ : Point n → ℝ} {Jᵢ : ι → Jet n} {l : Filter ι} [l.NeBot] (h : ∀ᶠ (i : ι) in l, ∃ x ∈ C, IsMinOn (fun (y : Point n) => uᵢ i y - φ y) C x ∧ HasSecondOrderExpansionWithin C φ x (Jᵢ i)) {A : Set ι} (hA : A ∈ l) : ∃ (z : (Point n × ℝ) × Jet n), z ∈ ⋃ i ∈ A, SubjetGraph C (uᵢ i)

Assume that the set of indices i for which there exists x ∈ C satisfying IsMinOn (fun y => uᵢ i y - φ y) C x and HasSecondOrderExpansionWithin C φ x (Jᵢ i) belongs to the filter l. Then, for every set of indices A with A ∈ l, the union ⋃ i ∈ A, SubjetGraph C (uᵢ i) contains a graph point.

theorem ViscositySolns.tailClosureSuperjetGraph_of_tendsto_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} (hx : Filter.Tendsto xᵢ l (nhds x)) (hu : Filter.Tendsto (fun (i : ι) => uᵢ i (xᵢ i)) l (nhds (u 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

Selected compact maximum contacts whose graph triples converge give tail-closure membership for the limiting superjet triple.

theorem ViscositySolns.tailClosureSubjetGraph_of_tendsto_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} (hx : Filter.Tendsto xᵢ l (nhds x)) (hu : Filter.Tendsto (fun (i : ι) => uᵢ i (xᵢ i)) l (nhds (u 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

Selected compact minimum contacts whose graph triples converge give tail-closure membership for the limiting subjet triple.

theorem ViscositySolns.tailClosureSuperjetGraph_to_ambient_of_tendsto_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) (hx : Filter.Tendsto xᵢ l (nhds x)) (hu : Filter.Tendsto (fun (i : ι) => uᵢ i (xᵢ i)) l (nhds (u 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 xᵢ → x, uᵢ i (xᵢ i) → u 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_tendsto_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) (hx : Filter.Tendsto xᵢ l (nhds x)) (hu : Filter.Tendsto (fun (i : ι) => uᵢ i (xᵢ i)) l (nhds (u 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 xᵢ → x, uᵢ i (xᵢ i) → u 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.