PointedCompactness.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Pointed precompactness of RCD rescalings

Uniform finite nets, a countable distance-matrix limit, and metric completion supply the precise pointed compactness input. The only tail restriction makes the rescaled curvature at least minus one.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.pointedRescalingPrecompactness line 23
Source documentation
The pointed rescaling compactness premise follows from the actual CD condition and completeness in the manuscript's dimension range.
```
theorem NoncollapsedRCD.pointedRescalingPrecompactness {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) (p : X) :
    PointedRescalingPrecompactness p := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.PointedRescalingPrecompactness