MeasuredRescalingFromCoordinates.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Measured rescaling convergence from fixed-ball estimates

The quantitative measured-coordinate input already controls every measurable pointed approximation. Measurable net replacement and the vanishing rescaled curvature therefore give its sequential formulation.

theorem OAI.RegularPointCoordinates.LocalMeasuredCoordinateInput.euclideanMeasuredRescalingConvergence line 22
Source documentation
The fixed-ball measured-coordinate theorem supplies the separately stated measured rescaling convergence, with no additional measure input.
```
theorem LocalMeasuredCoordinateInput.euclideanMeasuredRescalingConvergence
    {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    (hinput : LocalMeasuredCoordinateInput hX) (hn : 2 ≤ n) (p : X) :
    EuclideanMeasuredRescalingConvergence (hausdorff n X) n p := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalMeasuredCoordinateInput, OAI.RegularPointCoordinates.EuclideanMeasuredRescalingConvergence, OAI.RegularPointCoordinates.hausdorff