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

Compact and bounded Straszewicz cluster reductions

This module packages compact and bounded subdifferential versions of the Rockafellar exposed-point route, leaving the Straszewicz approximation input explicit.

theorem AleksandrovDifferentiability.mem_closure_convexHull_gradientClusterSet_of_compact_straszewicz_exposedCluster {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {domain sample : Set E} {u : E → ℝ} {y p : E} (hcompact : IsCompact {q : E | SubgradientOn domain u y q}) (hstrasz : Set.extremePoints ℝ {q : E | SubgradientOn domain u y q} ⊆ 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))

Compact subdifferential version of the Rockafellar exposed-point route.

For a compact subdifferential, Mathlib's Krein-Milman theorem reduces the closed-convex-hull representation to a Straszewicz-style hypothesis that extreme points are approximated by exposed points. If exposed subgradients are already known to lie in the gradient cluster closed convex hull, then every subgradient has the desired cluster-density conclusion.

theorem AleksandrovDifferentiability.mem_closure_convexHull_gradientClusterSet_of_compact_straszewiczClosure_exposedCluster {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {domain sample : Set E} {u : E → ℝ} {y p : E} (hcompact : IsCompact {q : E | SubgradientOn domain u y q}) (hstrasz : Set.extremePoints ℝ {q : E | SubgradientOn domain u y q} ⊆ closure (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))

Compact subdifferential version using the literal Straszewicz hypothesis that extreme points are limits of exposed points.

theorem AleksandrovDifferentiability.mem_closure_convexHull_gradientClusterSet_of_compact_mathlibStraszewicz_exposedCluster {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {domain sample : Set E} {u : E → ℝ} {y p : E} (hcompact : IsCompact {q : E | SubgradientOn domain u y q}) (hstrasz : Set.extremePoints ℝ {q : E | SubgradientOn domain u y q} ⊆ closure (Set.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))

Compact subdifferential version using a Mathlib-shaped literal Straszewicz hypothesis.

theorem AleksandrovDifferentiability.mem_closure_convexHull_gradientClusterSet_of_bounded_straszewicz_exposedCluster {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [ProperSpace E] {domain sample : Set E} {u : E → ℝ} {y p : E} (hbounded : Bornology.IsBounded {q : E | SubgradientOn domain u y q}) (hstrasz : Set.extremePoints ℝ {q : E | SubgradientOn domain u y q} ⊆ 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))

Bounded-subdifferential version of the compact Rockafellar exposed-point route.

In finite-dimensional source-cube applications, boundedness of the subdifferential is usually the available local input; properness of the ambient metric space turns that bounded closed subdifferential into a compact set.

theorem AleksandrovDifferentiability.mem_closure_convexHull_gradientClusterSet_of_bounded_straszewiczClosure_exposedCluster {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [ProperSpace E] {domain sample : Set E} {u : E → ℝ} {y p : E} (hbounded : Bornology.IsBounded {q : E | SubgradientOn domain u y q}) (hstrasz : Set.extremePoints ℝ {q : E | SubgradientOn domain u y q} ⊆ closure (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))

Bounded-subdifferential version using the literal Straszewicz closure hypothesis.

theorem AleksandrovDifferentiability.mem_closure_convexHull_gradientClusterSet_of_bounded_mathlibStraszewicz_exposedCluster {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [ProperSpace E] {domain sample : Set E} {u : E → ℝ} {y p : E} (hbounded : Bornology.IsBounded {q : E | SubgradientOn domain u y q}) (hstrasz : Set.extremePoints ℝ {q : E | SubgradientOn domain u y q} ⊆ closure (Set.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))

Bounded-subdifferential version using a Mathlib-shaped literal Straszewicz hypothesis.