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

Rockafellar-style subgradient cluster density

This compatibility module re-exports the conceptual pieces of the Rockafellar cluster-density formalization. The implementation is split across RockafellarCluster.Basic, RockafellarCluster.Exposed, RockafellarCluster.SupportingBall, RockafellarCluster.ConvexHull, RockafellarCluster.Straszewicz, RockafellarCluster.ExposedCluster, and RockafellarCluster.Recession.