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

Local Rockafellar cluster-density assembly

This module turns compact or bounded subdifferentials, Straszewicz approximation, and exposed-face outer semicontinuity into LocalSubgradientClusterDensityOn.

theorem AleksandrovDifferentiability.localSubgradientClusterDensityOn_of_compact_straszewiczClosure_outer {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {domain sample : Set E} {u : E → ℝ} (hcompact : ∀ ⦃y : E⦄, y ∈ sample → IsCompact {q : E | SubgradientOn domain u y q}) (hstrasz : ∀ ⦃y : E⦄, y ∈ sample → Set.extremePoints ℝ {q : E | SubgradientOn domain u y q} ⊆ closure (exposedPoints {q : E | SubgradientOn domain u y q})) (hne : ∀ ⦃y : E⦄, y ∈ sample → (nhdsWithin y (differentiabilitySetOn sample u)).NeBot) (houter : ∀ ⦃y p normal : E⦄, y ∈ sample → ExposesPoint {q : E | SubgradientOn domain u y q} normal p → ∀ ε > 0, ∀ᶠ (w : E) in nhdsWithin y (differentiabilitySetOn sample u), gradient u w ∈ normThickening (exposedFace {q : E | SubgradientOn domain u y q} normal) ε) : LocalSubgradientClusterDensityOn domain sample u

Local cluster density from compact subdifferentials, literal Straszewicz, and the Rockafellar exposed-face outer-semicontinuity estimate.

This is the local assembly of the two hard inputs in Rockafellar 25.6. The Straszewicz hypothesis gives the closed-convex-hull representation of each compact subdifferential by its exposed points; the outer-semicontinuity hypothesis puts every exposed subgradient into the gradient cluster hull.

theorem AleksandrovDifferentiability.localSubgradientClusterDensityOn_of_compact_straszewiczClosure_directionalOuter {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {domain sample : Set E} {u : E → ℝ} (hcompact : ∀ ⦃y : E⦄, y ∈ sample → IsCompact {q : E | SubgradientOn domain u y q}) (hstrasz : ∀ ⦃y : E⦄, y ∈ sample → Set.extremePoints ℝ {q : E | SubgradientOn domain u y q} ⊆ closure (exposedPoints {q : E | SubgradientOn domain u y q})) (houter : ∀ ⦃y p normal : E⦄, y ∈ sample → ExposesPoint {q : E | SubgradientOn domain u y q} normal p → ∃ (ι : Type u_2) (l : Filter ι) (φ : ι → E), l.NeBot ∧ Filter.Tendsto φ l (nhdsWithin y (differentiabilitySetOn sample u)) ∧ ∀ ε > 0, ∀ᶠ (a : ι) in l, gradient u (φ a) ∈ normThickening (exposedFace {q : E | SubgradientOn domain u y q} normal) ε) : LocalSubgradientClusterDensityOn domain sample u

Local cluster density from compact subdifferentials, literal Straszewicz, and a directional outer-semicontinuity input supplied along an auxiliary approach filter.

This is closer to Rockafellar's exposed-point proof than localSubgradientClusterDensityOn_of_compact_straszewiczClosure_outer: for each exposed subgradient it is enough to construct one nontrivial family of differentiability points tending to the base point and satisfying the exposed-face estimate.

theorem AleksandrovDifferentiability.localSubgradientClusterDensityOn_of_compact_straszewiczClosure_rayOuter {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {domain sample : Set E} {u : E → ℝ} (hcompact : ∀ ⦃y : E⦄, y ∈ sample → IsCompact {q : E | SubgradientOn domain u y q}) (hstrasz : ∀ ⦃y : E⦄, y ∈ sample → Set.extremePoints ℝ {q : E | SubgradientOn domain u y q} ⊆ closure (exposedPoints {q : E | SubgradientOn domain u y q})) (houter : ∀ ⦃y p : E⦄, y ∈ sample → p ∈ exposedPoints {q : E | SubgradientOn domain u y q} → ∃ (normal : E), ‖normal‖ = 1 ∧ ExposesPoint {q : E | SubgradientOn domain u y q} normal p ∧ ∃ (ι : Type u_2) (l : Filter ι) (φ : ι → E) (ε : ι → ℝ), l.NeBot ∧ Filter.Tendsto ε l (nhds 0) ∧ (∀ᶠ (a : ι) in l, 0 < ε a) ∧ (∀ᶠ (a : ι) in l, φ a ∈ differentiabilitySetOn sample u) ∧ (∀ᶠ (a : ι) in l, ‖φ a - (y + ε a • normal)‖ ≤ ε a ^ 2) ∧ (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) δ)) : LocalSubgradientClusterDensityOn domain sample u

Local cluster density from compact subdifferentials and Rockafellar's concrete ray sequence.

This is the most literal assembly form for the exposed-point part of Theorem 25.6: for every exposed subgradient one chooses a unit exposing normal, differentiability samples within ε^2 of the exposing ray, and the exposed-face thickening estimate supplied by directional outer semicontinuity along that ray.

theorem AleksandrovDifferentiability.localSubgradientClusterDensityOn_of_compact_mathlibStraszewicz_outer {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {domain sample : Set E} {u : E → ℝ} (hcompact : ∀ ⦃y : E⦄, y ∈ sample → IsCompact {q : E | SubgradientOn domain u y q}) (hstrasz : ∀ ⦃y : E⦄, y ∈ sample → Set.extremePoints ℝ {q : E | SubgradientOn domain u y q} ⊆ closure (Set.exposedPoints ℝ {q : E | SubgradientOn domain u y q})) (hne : ∀ ⦃y : E⦄, y ∈ sample → (nhdsWithin y (differentiabilitySetOn sample u)).NeBot) (houter : ∀ ⦃y p normal : E⦄, y ∈ sample → ExposesPoint {q : E | SubgradientOn domain u y q} normal p → ∀ ε > 0, ∀ᶠ (w : E) in nhdsWithin y (differentiabilitySetOn sample u), gradient u w ∈ normThickening (exposedFace {q : E | SubgradientOn domain u y q} normal) ε) : LocalSubgradientClusterDensityOn domain sample u

Local cluster density from compact subdifferentials and a Mathlib-shaped Straszewicz hypothesis.

theorem AleksandrovDifferentiability.localSubgradientClusterDensityOn_of_bounded_straszewiczClosure_outer {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [ProperSpace E] {domain sample : Set E} {u : E → ℝ} (hbounded : ∀ ⦃y : E⦄, y ∈ sample → Bornology.IsBounded {q : E | SubgradientOn domain u y q}) (hstrasz : ∀ ⦃y : E⦄, y ∈ sample → Set.extremePoints ℝ {q : E | SubgradientOn domain u y q} ⊆ closure (exposedPoints {q : E | SubgradientOn domain u y q})) (hne : ∀ ⦃y : E⦄, y ∈ sample → (nhdsWithin y (differentiabilitySetOn sample u)).NeBot) (houter : ∀ ⦃y p normal : E⦄, y ∈ sample → ExposesPoint {q : E | SubgradientOn domain u y q} normal p → ∀ ε > 0, ∀ᶠ (w : E) in nhdsWithin y (differentiabilitySetOn sample u), gradient u w ∈ normThickening (exposedFace {q : E | SubgradientOn domain u y q} normal) ε) : LocalSubgradientClusterDensityOn domain sample u

Bounded-subdifferential version of localSubgradientClusterDensityOn_of_compact_straszewiczClosure_outer.

This is the most source-cube-friendly local Rockafellar assembly theorem: local boundedness of the subdifferential supplies compactness in a proper metric space, while the remaining two hypotheses are exactly the literal Straszewicz closure input and the directional outer-semicontinuity input for exposed faces.

theorem AleksandrovDifferentiability.localSubgradientClusterDensityOn_of_bounded_straszewiczClosure_directionalOuter {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [ProperSpace E] {domain sample : Set E} {u : E → ℝ} (hbounded : ∀ ⦃y : E⦄, y ∈ sample → Bornology.IsBounded {q : E | SubgradientOn domain u y q}) (hstrasz : ∀ ⦃y : E⦄, y ∈ sample → Set.extremePoints ℝ {q : E | SubgradientOn domain u y q} ⊆ closure (exposedPoints {q : E | SubgradientOn domain u y q})) (houter : ∀ ⦃y p normal : E⦄, y ∈ sample → ExposesPoint {q : E | SubgradientOn domain u y q} normal p → ∃ (ι : Type u_2) (l : Filter ι) (φ : ι → E), l.NeBot ∧ Filter.Tendsto φ l (nhdsWithin y (differentiabilitySetOn sample u)) ∧ ∀ ε > 0, ∀ᶠ (a : ι) in l, gradient u (φ a) ∈ normThickening (exposedFace {q : E | SubgradientOn domain u y q} normal) ε) : LocalSubgradientClusterDensityOn domain sample u

Bounded-subdifferential local cluster density from a directional outer-semicontinuity input.

theorem AleksandrovDifferentiability.localSubgradientClusterDensityOn_of_bounded_straszewiczClosure_rayOuter {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [ProperSpace E] {domain sample : Set E} {u : E → ℝ} (hbounded : ∀ ⦃y : E⦄, y ∈ sample → Bornology.IsBounded {q : E | SubgradientOn domain u y q}) (hstrasz : ∀ ⦃y : E⦄, y ∈ sample → Set.extremePoints ℝ {q : E | SubgradientOn domain u y q} ⊆ closure (exposedPoints {q : E | SubgradientOn domain u y q})) (houter : ∀ ⦃y p : E⦄, y ∈ sample → p ∈ exposedPoints {q : E | SubgradientOn domain u y q} → ∃ (normal : E), ‖normal‖ = 1 ∧ ExposesPoint {q : E | SubgradientOn domain u y q} normal p ∧ ∃ (ι : Type u_2) (l : Filter ι) (φ : ι → E) (ε : ι → ℝ), l.NeBot ∧ Filter.Tendsto ε l (nhds 0) ∧ (∀ᶠ (a : ι) in l, 0 < ε a) ∧ (∀ᶠ (a : ι) in l, φ a ∈ differentiabilitySetOn sample u) ∧ (∀ᶠ (a : ι) in l, ‖φ a - (y + ε a • normal)‖ ≤ ε a ^ 2) ∧ (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) δ)) : LocalSubgradientClusterDensityOn domain sample u

Bounded-subdifferential local cluster density from Rockafellar's concrete ray sequence.

theorem AleksandrovDifferentiability.localSubgradientClusterDensityOn_of_bounded_mathlibStraszewicz_outer {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [ProperSpace E] {domain sample : Set E} {u : E → ℝ} (hbounded : ∀ ⦃y : E⦄, y ∈ sample → Bornology.IsBounded {q : E | SubgradientOn domain u y q}) (hstrasz : ∀ ⦃y : E⦄, y ∈ sample → Set.extremePoints ℝ {q : E | SubgradientOn domain u y q} ⊆ closure (Set.exposedPoints ℝ {q : E | SubgradientOn domain u y q})) (hne : ∀ ⦃y : E⦄, y ∈ sample → (nhdsWithin y (differentiabilitySetOn sample u)).NeBot) (houter : ∀ ⦃y p normal : E⦄, y ∈ sample → ExposesPoint {q : E | SubgradientOn domain u y q} normal p → ∀ ε > 0, ∀ᶠ (w : E) in nhdsWithin y (differentiabilitySetOn sample u), gradient u w ∈ normThickening (exposedFace {q : E | SubgradientOn domain u y q} normal) ε) : LocalSubgradientClusterDensityOn domain sample u

Bounded-subdifferential local cluster density from a Mathlib-shaped Straszewicz hypothesis.