JointSupportAnchors.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Joint plane-fit control and uniform affine escape produce support anchors with quantitative spanning bounds. The separation parameter is chosen uniformly before the measure.

theorem OAI.RieszRectifiability.exists_uniform_joint_support_anchors line 20