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

Source-cube subgradient cluster-density boundary

This file names the remaining finite-dimensional convex-analysis input in the source cube proof. It does not prove the density theorem. It packages its exact source-aligned quantifiers and records that, once this density input is available, the normalized cube Aleksandrov theorem follows from the already-formalized upper-contact/Stieltjes route and second-order assembly.

def AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity (n : ℕ) (u : SourceCubeSpace n → ℝ) : Prop

Fixed-function form of the source subgradient cluster-density theorem.

For each good base point x, and for nearby punctured points y, every subgradient of u at y relative to the large source cube Q_3 lies in the closed convex hull of ambient cluster values of the Fréchet gradient along differentiability points in Q_{3/2} approaching y.

This is the precise Lean form of the density input corresponding to the preparatory convex source note's subgradient-extension lemma. The approach to y is ambient; there is no linewise accumulation requirement.

Equations

• One or more equations did not get rendered due to their size.

def AleksandrovDifferentiability.SourceCubeSubgradientClusterDensityStatement (n : ℕ) : Prop

Source-cube theorem-level form of the finite-dimensional subgradient cluster-density input.

This is the remaining Rockafellar-style convex-analysis theorem to prove for the normalized cube route. It is intentionally separated from boundedness: boundedness is needed elsewhere for the upper-contact/finiteness part of the Aleksandrov proof, while this density statement is purely local convex subdifferential closure.

Equations

• One or more equations did not get rendered due to their size.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_rockafellarLocal {n : ℕ} {u : SourceCubeSpace n → ℝ} (hlocal : LocalSubgradientClusterDensityOn (sourceOpenCube n 3) (sourceOpenCube n (3 / 2)) u) : SourceCubeSubgradientClusterDensity n u

The named source-cube density boundary follows from the local Rockafellar interior theorem.

This is only the easy specialization step: the remaining mathematical work is proving RockafellarLocalSubgradientClusterDensityStatement, or reducing it carefully from Rockafellar's closed proper extended-real theorem.

theorem AleksandrovDifferentiability.sourceOpenCube_exists_pos_forall_pos_lt_add_smul_mem {n : ℕ} {r : ℝ} {y normal : SourceCubeSpace n} (hy : y ∈ sourceOpenCube n r) : ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃t : ℝ⦄, 0 < t → t < δ → y + t • normal ∈ sourceOpenCube n r

In a source cube, sufficiently small positive steps in any fixed direction remain in the same cube. This is the source-cube form of the open-domain ray lemma used in the interior Rockafellar route.

theorem AleksandrovDifferentiability.exists_sourceCubeDifferentiabilitySet_one_norm_sub_ray_lt_sq_of_mem {n : ℕ} {u : SourceCubeSpace n → ℝ} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) {y normal : SourceCubeSpace n} {ε : ℝ} (hε : 0 < ε) (hray : y + ε • normal ∈ sourceOpenCube n 1) : ∃ w ∈ sourceCubeDifferentiabilitySet n 1 u, ‖w - (y + ε • normal)‖ < ε ^ 2

One-step version of Rockafellar's ε^2 differentiability-point choice along a ray.

If the ray point y + ε • normal remains in Q_1, density of differentiability points in Q_1 gives a differentiability point within distance ε^2 of that ray point.

theorem AleksandrovDifferentiability.exists_sourceCubeDifferentiabilitySet_one_ray_samples {ι : Type u_1} {l : Filter ι} {n : ℕ} {u : SourceCubeSpace n → ℝ} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) {y normal : SourceCubeSpace n} {ε : ι → ℝ} (hεpos : ∀ᶠ (a : ι) in l, 0 < ε a) (hray : ∀ᶠ (a : ι) in l, y + ε a • normal ∈ sourceOpenCube n 1) : ∃ (φ : ι → SourceCubeSpace n), (∀ᶠ (a : ι) in l, φ a ∈ sourceCubeDifferentiabilitySet n 1 u) ∧ ∀ᶠ (a : ι) in l, ‖φ a - (y + ε a • normal)‖ ≤ ε a ^ 2

Filter-level choice of Rockafellar differentiability samples near an exposing ray.

For any scalar family ε a whose positive ray points eventually remain in Q_1, choose differentiability samples φ a ∈ D_1 eventually satisfying the ε a ^ 2 ray estimate.

theorem AleksandrovDifferentiability.exists_sourceCubeDifferentiabilitySet_one_ray_samples_tendsto_zero {ι : Type u_1} {l : Filter ι} {n : ℕ} {u : SourceCubeSpace n → ℝ} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) {y normal : SourceCubeSpace n} {ε : ι → ℝ} (hy : y ∈ sourceOpenCube n 1) (hε : Filter.Tendsto ε l (nhds 0)) (hεpos : ∀ᶠ (a : ι) in l, 0 < ε a) : ∃ (φ : ι → SourceCubeSpace n), (∀ᶠ (a : ι) in l, φ a ∈ sourceCubeDifferentiabilitySet n 1 u) ∧ ∀ᶠ (a : ι) in l, ‖φ a - (y + ε a • normal)‖ ≤ ε a ^ 2

Rockafellar differentiability samples along sufficiently small positive ray parameters.

This is the filter-level source-cube form of the sequence choice in Rockafellar 25.6: if ε a -> 0 through positive values and the base point is in Q_1, then openness of Q_1 puts the ray points y + ε a • normal eventually in Q_1, where differentiability points are dense.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_straszewiczClosure_outer {n : ℕ} {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hstrasz : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → Set.extremePoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} ⊆ closure (exposedPoints {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q})) (hne : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → (nhdsWithin y (differentiabilitySetOn (sourceOpenCube n (3 / 2)) u)).NeBot) (houter : ∀ ⦃y p normal : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → ExposesPoint {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal p → ∀ ε > 0, ∀ᶠ (w : SourceCubeSpace n) in nhdsWithin y (differentiabilitySetOn (sourceOpenCube n (3 / 2)) u), gradient u w ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) ε) : SourceCubeSubgradientClusterDensity n u

Source-cube cluster density from the bounded local Rockafellar assembly theorem.

Boundedness of u on Q_3 supplies bounded subdifferentials at all points of Q_{3/2}. The remaining hypotheses are the literal Straszewicz closure input, nontrivial differentiability sampling filters, and Rockafellar's exposed-face outer-semicontinuity estimate.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_mathlibStraszewicz_outer {n : ℕ} {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hstrasz : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → Set.extremePoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} ⊆ closure (Set.exposedPoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q})) (hne : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → (nhdsWithin y (differentiabilitySetOn (sourceOpenCube n (3 / 2)) u)).NeBot) (houter : ∀ ⦃y p normal : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → ExposesPoint {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal p → ∀ ε > 0, ∀ᶠ (w : SourceCubeSpace n) in nhdsWithin y (differentiabilitySetOn (sourceOpenCube n (3 / 2)) u), gradient u w ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) ε) : SourceCubeSubgradientClusterDensity n u

Source-cube cluster density from the bounded local Rockafellar assembly theorem, with the Straszewicz closure hypothesis stated using Mathlib's Set.exposedPoints.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_straszewiczClosure_outer_sourceCube {n : ℕ} {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hstrasz : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → Set.extremePoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} ⊆ closure (exposedPoints {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q})) (hne : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → (nhdsWithin y (sourceCubeDifferentiabilitySet n (3 / 2) u)).NeBot) (houter : ∀ ⦃y p normal : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → ExposesPoint {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal p → ∀ ε > 0, ∀ᶠ (w : SourceCubeSpace n) in nhdsWithin y (sourceCubeDifferentiabilitySet n (3 / 2) u), frechetGradient u w ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) ε) : SourceCubeSubgradientClusterDensity n u

Source-cube cluster density from the same bounded Rockafellar assembly theorem, with the sampling set written in the cube-local notation used by the rest of the source-cube proof.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_straszewiczClosure_directional_sourceCube {n : ℕ} {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hstrasz : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → Set.extremePoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} ⊆ closure (exposedPoints {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q})) (houter : ∀ ⦃y p normal : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → ExposesPoint {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal p → ∃ (ι : Type u_1) (l : Filter ι) (φ : ι → SourceCubeSpace n), l.NeBot ∧ Filter.Tendsto φ l (nhdsWithin y (sourceCubeDifferentiabilitySet n (3 / 2) u)) ∧ ∀ ε > 0, ∀ᶠ (a : ι) in l, frechetGradient u (φ a) ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) ε) : SourceCubeSubgradientClusterDensity n u

Source-cube cluster density from the bounded Rockafellar assembly theorem, using the source-faithful directional outer-semicontinuity input.

For each exposed subgradient, the hypothesis supplies one nontrivial auxiliary approach filter through differentiability points; it does not require all nearby differentiability gradients to lie near the exposed face.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_straszewiczClosure_ray_sourceCube {n : ℕ} {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hstrasz : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → Set.extremePoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} ⊆ closure (exposedPoints {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q})) (houter : ∀ ⦃y p : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → p ∈ exposedPoints {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} → ∃ (normal : SourceCubeSpace n), ‖normal‖ = 1 ∧ ExposesPoint {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal p ∧ ∃ (ι : Type u_1) (l : Filter ι) (φ : ι → SourceCubeSpace n) (ε : ι → ℝ), l.NeBot ∧ Filter.Tendsto ε l (nhds 0) ∧ (∀ᶠ (a : ι) in l, 0 < ε a) ∧ (∀ᶠ (a : ι) in l, φ a ∈ sourceCubeDifferentiabilitySet n (3 / 2) 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, frechetGradient u (φ a) ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) δ)) : SourceCubeSubgradientClusterDensity n u

Source-cube cluster density from the bounded Rockafellar assembly theorem, using the concrete ray sequence from Rockafellar's exposed-point proof.

For each exposed subgradient, the hypothesis chooses a unit exposing normal and differentiability samples φ a satisfying the source estimate ||φ a - (y + ε a • normal)|| <= (ε a)^2; directional outer semicontinuity then supplies the exposed-face thickening estimate along that ray.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_mathlibStraszewicz_outer_sourceCube {n : ℕ} {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hstrasz : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → Set.extremePoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} ⊆ closure (Set.exposedPoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q})) (hne : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → (nhdsWithin y (sourceCubeDifferentiabilitySet n (3 / 2) u)).NeBot) (houter : ∀ ⦃y p normal : SourceCubeSpace n⦄, y ∈ sourceOpenCube n (3 / 2) → ExposesPoint {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal p → ∀ ε > 0, ∀ᶠ (w : SourceCubeSpace n) in nhdsWithin y (sourceCubeDifferentiabilitySet n (3 / 2) u), frechetGradient u w ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) ε) : SourceCubeSubgradientClusterDensity n u

Source-cube cluster density from the bounded Rockafellar assembly theorem, with cube-local differentiability notation and Mathlib's Set.exposedPoints in the Straszewicz hypothesis.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_straszewiczClosure_outer_sourceCube_one {n : ℕ} {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hconvex : ConvexOn ℝ (sourceOpenCube n 3) u) (hstrasz : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → Set.extremePoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} ⊆ closure (exposedPoints {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q})) (houter : ∀ ⦃y p normal : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → ExposesPoint {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal p → ∀ ε > 0, ∀ᶠ (w : SourceCubeSpace n) in nhdsWithin y (sourceCubeDifferentiabilitySet n 1 u), frechetGradient u w ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) ε) : SourceCubeSubgradientClusterDensity n u

Source-cube cluster density from the bounded Rockafellar assembly theorem, using only the inner sample cube Q_1.

This is the quantifier shape supplied by the already-formalized differentiability-density result: points of Q_1 have nontrivial differentiability filters inside Q_1. The final conclusion is still stated with clusters along D_{3/2}, since cluster closed-convex-hull membership is monotone under enlarging the sampling set.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_straszewiczClosure_directional_sourceCube_one {n : ℕ} {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hstrasz : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → Set.extremePoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} ⊆ closure (exposedPoints {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q})) (houter : ∀ ⦃y p normal : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → ExposesPoint {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal p → ∃ (ι : Type u_1) (l : Filter ι) (φ : ι → SourceCubeSpace n), l.NeBot ∧ Filter.Tendsto φ l (nhdsWithin y (sourceCubeDifferentiabilitySet n 1 u)) ∧ ∀ ε > 0, ∀ᶠ (a : ι) in l, frechetGradient u (φ a) ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) ε) : SourceCubeSubgradientClusterDensity n u

Inner-cube source-cube cluster density from the source-faithful directional outer input.

This is the preferred cube boundary when the differentiability-density input is available only inside Q_1: the directional approach filters live in D_1, and the final cluster set is enlarged to D_{3/2} by monotonicity.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_straszewiczClosure_ray_sourceCube_one {n : ℕ} {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hstrasz : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → Set.extremePoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} ⊆ closure (exposedPoints {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q})) (houter : ∀ ⦃y p : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → p ∈ exposedPoints {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} → ∃ (normal : SourceCubeSpace n), ‖normal‖ = 1 ∧ ExposesPoint {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal p ∧ ∃ (ι : Type u_1) (l : Filter ι) (φ : ι → SourceCubeSpace n) (ε : ι → ℝ), l.NeBot ∧ Filter.Tendsto ε l (nhds 0) ∧ (∀ᶠ (a : ι) in l, 0 < ε a) ∧ (∀ᶠ (a : ι) in l, φ a ∈ sourceCubeDifferentiabilitySet n 1 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, frechetGradient u (φ a) ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) δ)) : SourceCubeSubgradientClusterDensity n u

Inner-cube source-cube cluster density from Rockafellar's concrete ray sequence.

This is the source-faithful Q_1 version of SourceCubeSubgradientClusterDensity.of_bounded_straszewiczClosure_ray_sourceCube: the differentiability samples live in D_1, and the resulting cluster hull is enlarged to D_{3/2} by monotonicity.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_straszewiczClosure_ray_one_unitOuter {n : ℕ} (hn : 0 < n) {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hstrasz : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → Set.extremePoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} ⊆ closure (exposedPoints {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q})) (houter : ∀ ⦃y p normal : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → p ∈ exposedPoints {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} → ‖normal‖ = 1 → ExposesPoint {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal p → ∃ (ι : Type u_1) (l : Filter ι) (φ : ι → SourceCubeSpace n) (ε : ι → ℝ), l.NeBot ∧ Filter.Tendsto ε l (nhds 0) ∧ (∀ᶠ (a : ι) in l, 0 < ε a) ∧ (∀ᶠ (a : ι) in l, φ a ∈ sourceCubeDifferentiabilitySet n 1 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, frechetGradient u (φ a) ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) δ)) : SourceCubeSubgradientClusterDensity n u

Inner-cube source-cube cluster density from Rockafellar's concrete ray sequence, with the unit exposing normal chosen from exposed-point membership.

The positive-dimensional hypothesis supplies an ambient unit vector for the degenerate singleton case of an exposed point. Thus callers only need to prove the ray construction and directional outer-semicontinuity estimate for whichever unit exposing normal is selected.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_straszewiczClosure_ray_one_unitOuter_scalars {n : ℕ} (hn : 0 < n) {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hconvex : ConvexOn ℝ (sourceOpenCube n 3) u) (hstrasz : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → Set.extremePoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} ⊆ closure (exposedPoints {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q})) (houter : ∀ ⦃y p normal : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → p ∈ exposedPoints {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} → ‖normal‖ = 1 → ExposesPoint {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal p → ∃ (ι : Type u_1) (l : Filter ι) (ε : ι → ℝ), l.NeBot ∧ Filter.Tendsto ε l (nhds 0) ∧ (∀ᶠ (a : ι) in l, 0 < ε a) ∧ ∀ ⦃φ : ι → SourceCubeSpace n⦄, (∀ᶠ (a : ι) in l, φ a ∈ sourceCubeDifferentiabilitySet n 1 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, frechetGradient u (φ a) ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) δ) : SourceCubeSubgradientClusterDensity n u

Inner-cube source-cube cluster density from scalar ray parameters and directional outer semicontinuity.

Compared with SourceCubeSubgradientClusterDensity.of_bounded_straszewiczClosure_ray_one_unitOuter, this wrapper does not ask the caller to construct the differentiability samples. For each exposed subgradient and selected unit exposing normal, the caller supplies only a positive scalar filter ε -> 0 and an outer-semicontinuity estimate applying to any differentiability samples satisfying Rockafellar's ε^2 ray estimate. The samples themselves are chosen from density of differentiability points in Q_1.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_straszewiczClosure_ray_one_unitOuter_seq {n : ℕ} (hn : 0 < n) {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hconvex : ConvexOn ℝ (sourceOpenCube n 3) u) (hstrasz : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → Set.extremePoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} ⊆ closure (exposedPoints {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q})) (houter : ∀ ⦃y p normal : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → p ∈ exposedPoints {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} → ‖normal‖ = 1 → ExposesPoint {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal p → ∀ ⦃φ : ℕ → SourceCubeSpace n⦄, (∀ᶠ (k : ℕ) in Filter.atTop, φ k ∈ sourceCubeDifferentiabilitySet n 1 u) → (∀ᶠ (k : ℕ) in Filter.atTop, ‖φ k - (y + sourceForwardSecantStep k • normal)‖ ≤ sourceForwardSecantStep k ^ 2) → Filter.Tendsto (fun (k : ℕ) => ‖φ k - y‖⁻¹ • (φ k - y)) Filter.atTop (nhds normal) → ∀ δ > 0, ∀ᶠ (k : ℕ) in Filter.atTop, frechetGradient u (φ k) ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) δ) : SourceCubeSubgradientClusterDensity n u

Inner-cube source-cube cluster density using the canonical positive scalar sequence.

This fixes Rockafellar's ε_i ↓ 0 choice to the already-used source sequence sourceForwardSecantStep k. Thus the remaining exposed-point input is only the directional outer-semicontinuity estimate along differentiability samples satisfying the ε_k^2 ray estimate.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_mathlibStraszewicz_ray_one_unitOuter {n : ℕ} (hn : 0 < n) {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hstrasz : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → Set.extremePoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} ⊆ closure (Set.exposedPoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q})) (houter : ∀ ⦃y p normal : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → p ∈ Set.exposedPoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} → ‖normal‖ = 1 → ExposesPoint {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal p → ∃ (ι : Type u_1) (l : Filter ι) (φ : ι → SourceCubeSpace n) (ε : ι → ℝ), l.NeBot ∧ Filter.Tendsto ε l (nhds 0) ∧ (∀ᶠ (a : ι) in l, 0 < ε a) ∧ (∀ᶠ (a : ι) in l, φ a ∈ sourceCubeDifferentiabilitySet n 1 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, frechetGradient u (φ a) ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) δ)) : SourceCubeSubgradientClusterDensity n u

Inner-cube source-cube cluster density from Rockafellar's concrete ray sequence, with Mathlib's Set.exposedPoints notation and the unit normal chosen from exposed-point membership.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_mathlibStraszewicz_ray_one_unitOuter_seq {n : ℕ} (hn : 0 < n) {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hconvex : ConvexOn ℝ (sourceOpenCube n 3) u) (hstrasz : ∀ ⦃y : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → Set.extremePoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} ⊆ closure (Set.exposedPoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q})) (houter : ∀ ⦃y p normal : SourceCubeSpace n⦄, y ∈ sourceOpenCube n 1 → p ∈ Set.exposedPoints ℝ {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} → ‖normal‖ = 1 → ExposesPoint {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal p → ∀ ⦃φ : ℕ → SourceCubeSpace n⦄, (∀ᶠ (k : ℕ) in Filter.atTop, φ k ∈ sourceCubeDifferentiabilitySet n 1 u) → (∀ᶠ (k : ℕ) in Filter.atTop, ‖φ k - (y + sourceForwardSecantStep k • normal)‖ ≤ sourceForwardSecantStep k ^ 2) → Filter.Tendsto (fun (k : ℕ) => ‖φ k - y‖⁻¹ • (φ k - y)) Filter.atTop (nhds normal) → ∀ δ > 0, ∀ᶠ (k : ℕ) in Filter.atTop, frechetGradient u (φ k) ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) δ) : SourceCubeSubgradientClusterDensity n u

Inner-cube source-cube cluster density from the canonical ray sequence, with Mathlib's Set.exposedPoints notation.

This is the Mathlib-shaped version of SourceCubeSubgradientClusterDensity.of_bounded_straszewiczClosure_ray_one_unitOuter_seq: the Straszewicz and exposed-point hypotheses are stated using Set.exposedPoints, while the scalar sequence is fixed to sourceForwardSecantStep.