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

Norm thickenings and cluster tools

This module contains the open norm-thickening API and general cluster-point lemmas used in the Rockafellar directional outer-semicontinuity argument.

def AleksandrovDifferentiability.normThickening {E : Type u_1} [NormedAddCommGroup E] (s : Set E) (ε : ℝ) : Set E

Open norm-thickening of a set.

This is the project-local version of the set A + ε B appearing in Rockafellar's directional outer semicontinuity theorem: a point lies in normThickening A ε if it is within norm-distance < ε of some point of A.

Equations

• AleksandrovDifferentiability.normThickening s ε = {x : E | ∃ a ∈ s, ‖x - a‖ < ε}

theorem AleksandrovDifferentiability.isOpen_normThickening {E : Type u_1} [NormedAddCommGroup E] (s : Set E) (ε : ℝ) : IsOpen (normThickening s ε)

The project-local open norm thickening is open.

theorem AleksandrovDifferentiability.subset_normThickening_self {E : Type u_1} [NormedAddCommGroup E] {s : Set E} {ε : ℝ} (hε : 0 < ε) : s ⊆ normThickening s ε

A set is contained in every positive norm thickening of itself.

theorem AleksandrovDifferentiability.normThickening_mem_nhdsSet {E : Type u_1} [NormedAddCommGroup E] (s : Set E) {ε : ℝ} (hε : 0 < ε) : normThickening s ε ∈ nhdsSet s

Every positive norm thickening is a neighborhood of the thickened set.

theorem AleksandrovDifferentiability.IsCompact.eventually_mem_normThickening_of_forall_mapClusterPt {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} {l : Filter ι} {K target : Set E} {f : ι → E} (hK : IsCompact K) (hmem : ∀ᶠ (i : ι) in l, f i ∈ K) (hcluster : ∀ q ∈ K, MapClusterPt q l f → q ∈ target) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (i : ι) in l, f i ∈ normThickening target ε

Compact cluster-point criterion for eventual membership in norm thickenings.

If f is eventually contained in a compact set K, and every cluster value of f in K belongs to target, then f is eventually contained in every positive norm-thickening of target. This is the abstract compactness/contradiction step in Rockafellar's directional outer-semicontinuity argument.

theorem AleksandrovDifferentiability.MapClusterPt.prod_of_tendsto {ι : Type u_2} {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] {l : Filter ι} {u : ι → X} {v : ι → Y} {x : X} {y : Y} (hu : MapClusterPt x l u) (hv : Filter.Tendsto v l (nhds y)) : MapClusterPt (x, y) l fun (i : ι) => (u i, v i)

Pair a map-cluster point with an ordinary limit along the same filter.

theorem AleksandrovDifferentiability.le_of_tendsto_of_mapClusterPt_of_eventually_le {ι : Type u_2} {l : Filter ι} {f g : ι → ℝ} {a b : ℝ} (hf : Filter.Tendsto f l (nhds a)) (hg : MapClusterPt b l g) (hle : f ≤ᶠ[l] g) : a ≤ b

An eventual scalar inequality passes to a limit on the left and a cluster point on the right.

theorem AleksandrovDifferentiability.le_of_mapClusterPt_of_tendsto_of_eventually_le {ι : Type u_2} {l : Filter ι} {f g : ι → ℝ} {a b : ℝ} (hf : MapClusterPt a l f) (hg : Filter.Tendsto g l (nhds b)) (hle : f ≤ᶠ[l] g) : a ≤ b

An eventual scalar inequality passes to a cluster point on the left and a limit on the right.

theorem AleksandrovDifferentiability.SubgradientOn.of_mapClusterPt_of_continuousAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {l : Filter ι} {s : Set E} {u : E → ℝ} {x p : E} {xs ps : ι → E} (hx : x ∈ s) (hxs : Filter.Tendsto xs l (nhds x)) (hps : MapClusterPt p l ps) (hu : ContinuousAt u x) (hsub : ∀ᶠ (i : ι) in l, SubgradientOn s u (xs i) (ps i)) : SubgradientOn s u x p

Closed-graph form of the subgradient inequality for cluster points.

This is the cluster-point analogue of SubgradientOn.of_tendsto: the slopes ps i need only cluster at p, while the base points xs i converge to x.