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

Source-cube cluster-density ray reductions

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) → ∀ δ > 0, ∀ᶠ (k : ℕ) in Filter.atTop, frechetGradient u (φ k) ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) δ) : SourceCubeSubgradientClusterDensity n u

theorem AleksandrovDifferentiability.eventually_frechetGradient_mem_normThickening_exposedFace_of_sourceCube_ray {n : ℕ} {u : SourceCubeSpace n → ℝ} {y normal : SourceCubeSpace n} {φ : ℕ → SourceCubeSpace n} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hconvex : ConvexOn ℝ (sourceOpenCube n 3) u) (hy : y ∈ sourceOpenCube n 1) (hnormal : ‖normal‖ = 1) (hmem : ∀ᶠ (k : ℕ) in Filter.atTop, φ k ∈ sourceCubeDifferentiabilitySet n 1 u) (hclose : ∀ᶠ (k : ℕ) in Filter.atTop, ‖φ k - (y + sourceForwardSecantStep k • normal)‖ ≤ sourceForwardSecantStep k ^ 2) (δ : ℝ) : δ > 0 → ∀ᶠ (k : ℕ) in Filter.atTop, frechetGradient u (φ k) ∈ normThickening (exposedFace {q : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u y q} normal) δ

Source-cube directional outer semicontinuity along Rockafellar's canonical ray samples.

This is the cube-local version of the analytic input used in the exposed-point part of Rockafellar 25.6. Boundedness of u on Q_3 supplies a compact ball containing all gradients at differentiability samples in Q_1; the generic compact directional wrapper then puts every cluster value in the exposed face of the base subdifferential.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_mathlibStraszewicz_ray {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})) : SourceCubeSubgradientClusterDensity n u

Inner-cube source-cube cluster density from Straszewicz closure and the proved source-cube directional outer semicontinuity.

Compared with SourceCubeSubgradientClusterDensity.of_bounded_mathlibStraszewicz_ray_one_unitOuter_seq', this wrapper discharges the houter hypothesis using eventually_frechetGradient_mem_normThickening_exposedFace_of_sourceCube_ray. Thus the remaining mathematical input is the Straszewicz-style approximation of extreme subgradients by exposed subgradients.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_straszewiczCompactConvex {n : ℕ} (hn : 0 < n) {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hconvex : ConvexOn ℝ (sourceOpenCube n 3) u) (hstrasz : StraszewiczCompactConvexStatement (SourceCubeSpace n)) : SourceCubeSubgradientClusterDensity n u

Inner-cube source-cube cluster density from the standard compact-convex Straszewicz theorem.

This is the source-cube bridge from the reusable convex-geometry theorem boundary StraszewiczCompactConvexStatement to the Rockafellar subgradient cluster-density input.

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_compactStraszewicz {n : ℕ} (hn : 0 < n) {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hconvex : ConvexOn ℝ (sourceOpenCube n 3) u) : SourceCubeSubgradientClusterDensity n u

Inner-cube source-cube cluster density from the proved compact-convex Straszewicz theorem.