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

Compact neighborhoods for local stability

This file packages compact neighborhood hypotheses used by stability arguments.

There are two levels. CompactRelativeNeighborhood records the compact relative neighborhoods used directly in the paper: compact subsets K ⊆ C which are neighborhoods of x inside C. CompactLocalization is stronger: it adds the convexity and differentiability hypotheses consumed by the smooth selection lemmas.

structure ViscositySolns.CompactRelativeNeighborhood {n : ℕ} (C : Set (Point n)) (x : Point n) (K : Set (Point n)) : Prop

A compact relative neighborhood of x inside C.

This means that K is a compact subset of C, x ∈ K, and K ∈ nhdsWithin x C. Equivalently, K contains the intersection of C with some neighborhood of x. No convexity or ambient-interior assumption is included.

• subset : K ⊆ C
• mem_nhdsWithin : K ∈ nhdsWithin x C
• point_mem : x ∈ K
• nonempty : K.Nonempty
• isCompact : IsCompact K

theorem ViscositySolns.CompactRelativeNeighborhood.eventually_mem_nhdsWithin {n : ℕ} {C K : Set (Point n)} {x : Point n} (hK : CompactRelativeNeighborhood C x K) {ι : Type u_1} {xᵢ : ι → Point n} {l : Filter ι} (hx : Filter.Tendsto xᵢ l (nhds x)) (hmem : ∀ᶠ (i : ι) in l, xᵢ i ∈ C) : ∀ᶠ (i : ι) in l, K ∈ nhdsWithin (xᵢ i) C

theorem ViscositySolns.CompactRelativeNeighborhood.nhdsWithin_eq {n : ℕ} {C K : Set (Point n)} {x : Point n} (hK : CompactRelativeNeighborhood C x K) : nhdsWithin x K = nhdsWithin x C

theorem ViscositySolns.exists_nhds_forall_mem_nhdsWithin {n : ℕ} {C K : Set (Point n)} {x : Point n} (hK : K ∈ nhdsWithin x C) : ∃ U ∈ nhds x, ∀ z ∈ U, z ∈ C → K ∈ nhdsWithin z C

If K is a relative neighborhood of x in C, then every point of C in some ordinary neighborhood of x also has K as a relative neighborhood in C.

structure ViscositySolns.CompactLocalization {n : ℕ} (C : Set (Point n)) (x : Point n) (K : Set (Point n)) : Prop

Compact localizing data for a point x in a domain C.

The smooth selected-contact stability lemmas consume exactly these shape hypotheses for the compact set K: compactness, convexity, unique differentiability, and the condition that all points of K lie in the closure of its interior.

• subset : K ⊆ C
• mem_nhdsWithin : K ∈ nhdsWithin x C
• point_mem : x ∈ K
• nonempty : K.Nonempty
• isCompact : IsCompact K
• convex : Convex ℝ K
• uniqueDiffOn : UniqueDiffOn ℝ K
• subset_closure_interior : K ⊆ closure (interior K)

theorem ViscositySolns.CompactLocalization.toCompactRelativeNeighborhood {n : ℕ} {C K : Set (Point n)} {x : Point n} (hK : CompactLocalization C x K) : CompactRelativeNeighborhood C x K

theorem ViscositySolns.CompactLocalization.eventually_mem_nhdsWithin {n : ℕ} {C K : Set (Point n)} {x : Point n} (hK : CompactLocalization C x K) {ι : Type u_1} {xᵢ : ι → Point n} {l : Filter ι} (hx : Filter.Tendsto xᵢ l (nhds x)) (hmem : ∀ᶠ (i : ι) in l, xᵢ i ∈ C) : ∀ᶠ (i : ι) in l, K ∈ nhdsWithin (xᵢ i) C

theorem ViscositySolns.compactRelativeNeighborhood_inter_closedBall {n : ℕ} {C : Set (Point n)} {x : Point n} {r : ℝ} (hxC : x ∈ C) (hr : 0 < r) (hcompact : IsCompact (C ∩ Metric.closedBall x r)) : CompactRelativeNeighborhood C x (C ∩ Metric.closedBall x r)

The compact relative neighborhood used in the CIL proof: intersect the domain with a positive-radius closed ball around the point. Compactness is kept as an explicit hypothesis, as it is supplied by local compactness in the paper.

theorem ViscositySolns.exists_isCompact_inter_closedBall_of_locallyCompactSpace {n : ℕ} {C : Set (Point n)} [LocallyCompactSpace ↑C] {x : Point n} (hxC : x ∈ C) : ∃ r > 0, IsCompact (C ∩ Metric.closedBall x r)

If C is locally compact in its relative topology, then around each point of C there is a positive-radius closed ball whose intersection with C is compact.

theorem ViscositySolns.exists_inter_closedBall_compactRelativeNeighborhood {n : ℕ} {C : Set (Point n)} {x : Point n} (hxC : x ∈ C) (h : ∃ r > 0, IsCompact (C ∩ Metric.closedBall x r)) : ∃ r > 0, CompactRelativeNeighborhood C x (C ∩ Metric.closedBall x r)

If a positive radius gives a compact intersection with a closed ball, then it gives a compact relative neighborhood.

theorem ViscositySolns.exists_inter_closedBall_compactRelativeNeighborhood_of_locallyCompactSpace {n : ℕ} {C : Set (Point n)} [LocallyCompactSpace ↑C] {x : Point n} (hxC : x ∈ C) : ∃ r > 0, CompactRelativeNeighborhood C x (C ∩ Metric.closedBall x r)

Local compactness of the relative topology on C supplies the compact relative closed-ball neighborhoods used in the paper.

theorem ViscositySolns.exists_inter_closedBall_compactRelativeNeighborhood_subset_of_mem_nhdsWithin {n : ℕ} {C P : Set (Point n)} [LocallyCompactSpace ↑C] {x : Point n} (hxC : x ∈ C) (hP : P ∈ nhdsWithin x C) : ∃ r > 0, CompactRelativeNeighborhood C x (C ∩ Metric.closedBall x r) ∧ C ∩ Metric.closedBall x r ⊆ P

Given any relative neighborhood P of x in C, local compactness lets us choose a positive-radius closed-ball relative neighborhood contained in P.

The conclusion gives r > 0, K = C ∩ closedBall x r, CompactRelativeNeighborhood C x K, and K ⊆ P. The compactness of K is obtained from local compactness of the relative topology on C at x.

theorem ViscositySolns.compactLocalization_closedBall {n : ℕ} {C : Set (Point n)} {x : Point n} {r : ℝ} (hr : 0 < r) (hball : Metric.closedBall x r ⊆ C) : CompactLocalization C x (Metric.closedBall x r)

theorem ViscositySolns.exists_closedBall_compactLocalization {n : ℕ} {C : Set (Point n)} {x : Point n} (hC : C ∈ nhds x) : ∃ r > 0, CompactLocalization C x (Metric.closedBall x r)

At an interior point of a domain, a sufficiently small closed ball supplies all compact localizing hypotheses used by the smooth stability selection lemmas.