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

Source-cube cluster-density final assembly

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensity.of_bounded_mathlibStraszewicz_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 (Set.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

theorem AleksandrovDifferentiability.SourceCubeSubgradientClusterDensityStatement.of_rockafellarLocal {n : ℕ} (hrock : RockafellarLocalSubgradientClusterDensityStatement (SourceCubeSpace n)) : SourceCubeSubgradientClusterDensityStatement n

If the local Rockafellar theorem is available in the source cube space, then the cube-level cluster-density statement has exactly the quantifiers used by the Aleksandrov assembly.

theorem AleksandrovDifferentiability.ae_restrict_sourceOpenCube_secondOrderDifferentiableAt_of_subgradientClusterDensity {n : ℕ} (hn : 1 ≤ n) {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hconvex : ConvexOn ℝ (sourceOpenCube n 3) u) (hdensity : SourceCubeSubgradientClusterDensityStatement n) : ∀ᵐ (x : SourceCubeSpace n) ∂MeasureTheory.volume.restrict (sourceOpenCube n 1), SecondOrderDifferentiableAt u x

The normalized source-cube Aleksandrov theorem from the named cluster-density statement.

All other cube-local analytic inputs are now supplied by the concrete convex Stieltjes route and the second-order assembly in Statements.Cube.SecondOrder.

theorem AleksandrovDifferentiability.ae_restrict_sourceOpenCube_secondOrderDifferentiableAt_of_mathlibStraszewicz {n : ℕ} (hn : 1 ≤ 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})) : ∀ᵐ (x : SourceCubeSpace n) ∂MeasureTheory.volume.restrict (sourceOpenCube n 1), SecondOrderDifferentiableAt u x

Normalized source-cube Aleksandrov theorem from the remaining Straszewicz-style convex-geometry input.

The directional exposed-face outer semicontinuity part of Rockafellar 25.6 is discharged by SourceCubeSubgradientClusterDensity.of_bounded_mathlibStraszewicz_ray; the only hypothesis left here is that the extreme points of each source-cube subdifferential are limits of Mathlib exposed points.

theorem AleksandrovDifferentiability.ae_restrict_sourceOpenCube_secondOrderDifferentiableAt_of_straszewiczCompactConvex {n : ℕ} (hn : 1 ≤ n) {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hconvex : ConvexOn ℝ (sourceOpenCube n 3) u) (hstrasz : StraszewiczCompactConvexStatement (SourceCubeSpace n)) : ∀ᵐ (x : SourceCubeSpace n) ∂MeasureTheory.volume.restrict (sourceOpenCube n 1), SecondOrderDifferentiableAt u x

Normalized source-cube Aleksandrov theorem from the standard compact-convex Straszewicz theorem.

This is now the cleanest source-cube boundary: after the upper-contact/Stieltjes analysis and Rockafellar directional outer-semicontinuity work, the only remaining external convex-geometry input is StraszewiczCompactConvexStatement for the finite-dimensional source cube space.

theorem AleksandrovDifferentiability.ae_restrict_sourceOpenCube_secondOrderDifferentiableAt {n : ℕ} (hn : 1 ≤ n) {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hconvex : ConvexOn ℝ (sourceOpenCube n 3) u) : ∀ᵐ (x : SourceCubeSpace n) ∂MeasureTheory.volume.restrict (sourceOpenCube n 1), SecondOrderDifferentiableAt u x

Normalized source-cube Aleksandrov theorem for bounded convex functions.

This version discharges the compact-convex Straszewicz input using straszewiczCompactConvexStatement.

theorem AleksandrovDifferentiability.ae_restrict_sourceOpenCube_secondOrderDifferentiableAt_of_rockafellarLocal {n : ℕ} (hn : 1 ≤ n) {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hconvex : ConvexOn ℝ (sourceOpenCube n 3) u) (hrock : RockafellarLocalSubgradientClusterDensityStatement (SourceCubeSpace n)) : ∀ᵐ (x : SourceCubeSpace n) ∂MeasureTheory.volume.restrict (sourceOpenCube n 1), SecondOrderDifferentiableAt u x

Normalized source-cube Aleksandrov theorem from the local Rockafellar cluster-density theorem.

This is the current source-faithful cube boundary: all analytic and integration work has already been discharged, and the remaining density input is exactly the local interior consequence of Rockafellar 25.6.