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

Pointwise exposed subgradient cluster bridges

This module contains the pointwise exposed-point reduction and the filter/ray wrappers turning Rockafellar exposed-face outer semicontinuity into membership in the gradient cluster hull.

theorem AleksandrovDifferentiability.mem_closure_convexHull_gradientClusterSet_of_exposedPoint_reduction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {domain sample : Set E} {u : E → ℝ} {y p : E} (hrepr : ∀ ⦃r : E⦄, SubgradientOn domain u y r → r ∈ closure ((convexHull ℝ) (exposedPoints {q : E | SubgradientOn domain u y q}))) (hexposed_cluster : ∀ ⦃r : E⦄, r ∈ exposedPoints {q : E | SubgradientOn domain u y q} → r ∈ closure ((convexHull ℝ) (HasSubgradientLinearizationOnAt.GradientClusterSet (differentiabilitySetOn sample u) (gradient u) y))) (hp : SubgradientOn domain u y p) : p ∈ closure ((convexHull ℝ) (HasSubgradientLinearizationOnAt.GradientClusterSet (differentiabilitySetOn sample u) (gradient u) y))

Rockafellar-style exposed-point reduction for the local subgradient cluster-density conclusion at one point.

This theorem intentionally keeps the two hard finite-dimensional convex-analysis inputs visible: first, that the subdifferential is contained in the closed convex hull of its exposed points; second, that every exposed subgradient is a cluster limit of nearby gradients.

theorem AleksandrovDifferentiability.exposedSubgradient_mem_closure_convexHull_gradientClusterSet_of_eventually_norm_sub_lt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {domain sample : Set E} {u : E → ℝ} {y p : E} (hne : (nhdsWithin y (differentiabilitySetOn sample u)).NeBot) (_hexposed : p ∈ exposedPoints {q : E | SubgradientOn domain u y q}) (hgradient : ∀ ε > 0, ∀ᶠ (w : E) in nhdsWithin y (differentiabilitySetOn sample u), ‖gradient u w - p‖ < ε) : p ∈ closure ((convexHull ℝ) (HasSubgradientLinearizationOnAt.GradientClusterSet (differentiabilitySetOn sample u) (gradient u) y))

An exposed subgradient belongs to the gradient cluster closed convex hull once nearby differentiability gradients converge to it along the sampling filter.

This is the final filter/metric packaging of Rockafellar's exposed-point argument. The hard analytic input is the norm convergence hypothesis, which is supplied in Rockafellar 25.6 by directional outer semicontinuity and the fact that the exposed face is the singleton {p}.

theorem AleksandrovDifferentiability.exposedSubgradient_mem_closure_convexHull_gradientClusterSet_of_eventually_mem_thickening {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {domain sample : Set E} {u : E → ℝ} {y p normal : E} (hne : (nhdsWithin y (differentiabilitySetOn sample u)).NeBot) (hexposed : ExposesPoint {q : E | SubgradientOn domain u y q} normal p) (houter : ∀ ε > 0, ∀ᶠ (w : E) in nhdsWithin y (differentiabilitySetOn sample u), gradient u w ∈ normThickening (exposedFace {q : E | SubgradientOn domain u y q} normal) ε) : p ∈ closure ((convexHull ℝ) (HasSubgradientLinearizationOnAt.GradientClusterSet (differentiabilitySetOn sample u) (gradient u) y))

Exposed-subgradient cluster membership from the outer-semicontinuity shape used by Rockafellar.

The hypothesis says that for every ε > 0, nearby differentiability gradients lie in the ε-thickening of the exposed face selected by normal. If normal exposes p, that exposed face is {p}, so the previous metric bridge applies.

theorem AleksandrovDifferentiability.exposedSubgradient_mem_closure_convexHull_gradientClusterSet_of_tendsto_norm_sub_lt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {ι : Type u_2} {l : Filter ι} {domain sample : Set E} {u : E → ℝ} {y p : E} {φ : ι → E} (hne : l.NeBot) (hφ : Filter.Tendsto φ l (nhdsWithin y (differentiabilitySetOn sample u))) (_hexposed : p ∈ exposedPoints {q : E | SubgradientOn domain u y q}) (hgradient : ∀ ε > 0, ∀ᶠ (a : ι) in l, ‖gradient u (φ a) - p‖ < ε) : p ∈ closure ((convexHull ℝ) (HasSubgradientLinearizationOnAt.GradientClusterSet (differentiabilitySetOn sample u) (gradient u) y))

Exposed-subgradient cluster membership from convergence along an auxiliary approach filter.

This is the filter form closest to Rockafellar's exposed-point proof: one constructs differentiability points approaching y in the exposing direction, and proves that their gradients converge to the exposed subgradient. The approach map only has to tend to y through the differentiability set; it need not be the full ambient 𝓝[D] y filter.

theorem AleksandrovDifferentiability.exposedSubgradient_mem_closure_convexHull_gradientClusterSet_of_tendsto_mem_thickening {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {ι : Type u_2} {l : Filter ι} {domain sample : Set E} {u : E → ℝ} {y p normal : E} {φ : ι → E} (hne : l.NeBot) (hφ : Filter.Tendsto φ l (nhdsWithin y (differentiabilitySetOn sample u))) (hexposed : ExposesPoint {q : E | SubgradientOn domain u y q} normal p) (houter : ∀ ε > 0, ∀ᶠ (a : ι) in l, gradient u (φ a) ∈ normThickening (exposedFace {q : E | SubgradientOn domain u y q} normal) ε) : p ∈ closure ((convexHull ℝ) (HasSubgradientLinearizationOnAt.GradientClusterSet (differentiabilitySetOn sample u) (gradient u) y))

Directional/filter version of the exposed-face outer-semicontinuity bridge.

Instead of requiring all sufficiently nearby differentiability gradients to lie near the exposed face, it is enough to have one nontrivial approach filter through the differentiability set along which the outer-semicontinuity estimate holds.

theorem AleksandrovDifferentiability.exposedSubgradient_mem_closure_convexHull_gradientClusterSet_of_ray_thickening {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {ι : Type u_2} {l : Filter ι} {domain sample : Set E} {u : E → ℝ} {y p normal : E} {φ : ι → E} {ε : ι → ℝ} (hne : l.NeBot) (hnormal : ‖normal‖ = 1) (hε : Filter.Tendsto ε l (nhds 0)) (hεpos : ∀ᶠ (a : ι) in l, 0 < ε a) (hmem : ∀ᶠ (a : ι) in l, φ a ∈ differentiabilitySetOn sample u) (hclose : ∀ᶠ (a : ι) in l, ‖φ a - (y + ε a • normal)‖ ≤ ε a ^ 2) (hexposed : ExposesPoint {q : E | SubgradientOn domain u y q} normal p) (houter : Filter.Tendsto (fun (a : ι) => ‖φ a - y‖⁻¹ • (φ a - y)) l (nhds normal) → ∀ δ > 0, ∀ᶠ (a : ι) in l, gradient u (φ a) ∈ normThickening (exposedFace {q : E | SubgradientOn domain u y q} normal) δ) : p ∈ closure ((convexHull ℝ) (HasSubgradientLinearizationOnAt.GradientClusterSet (differentiabilitySetOn sample u) (gradient u) y))

Source-ray version of Rockafellar's exposed-subgradient bridge.

This is the wrapper closest to the printed proof of Theorem 25.6. The differentiability samples φ a are chosen within ε a ^ 2 of the ray point y + ε a • normal, with ε a -> 0 and ε a > 0 eventually. The already-proved ray lemmas supply both the approach through the differentiability set and the normalized-direction convergence required by directional outer semicontinuity.