BoundedRegularNormalization.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Choosing the normalization radius and raw error under prescribed caps

theorem OAI.RegularPointCoordinates.bounded_regular_controlled_normalization line 17
Source documentation
The published normalization inputs allow the working radius and the raw initial error to be capped independently of the later target error.
```
theorem bounded_regular_controlled_normalization {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 1) X) (hn : 2 ≤ m + 1) {p : X} {a : ℝ} (ha : 0 ≤ a)
    (hcompact : PointedRescalingPrecompactness p) (hregular : IsRegular (m + 1) p)
    (_hvolume : EuclideanRescalingVolumeConvergence (hausdorff (m + 1) X) (m + 1) p
      (euclideanUnitVolume (m + 1)))
    (hmeasured : EuclideanMeasuredRescalingConvergence (hausdorff (m + 1) X) (m + 1) p)
    (hBG : BallVolumeComparison (hausdorff (m + 1) X) (comparisonModelVolume m a))
    (_hdensity : ∀ y, SmallScaleVolumeUpper (hausdorff (m + 1) X)
      (comparisonModelVolume m a) y (euclideanUnitVolume (m + 1)))
    (hinitial : LocalInitialSplittingInput hX) (htrans : LocalTransformationInput hX)
    (hsplit : LocalFlatSplittingInput hX) (hrigidity : UniformRegularFlatnessInput hX)
    {ρ β : ℝ} (hρ : 0 < ρ) (hβ : 0 < β)
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.PointedRescalingPrecompactness, OAI.RegularPointCoordinates.IsRegular, OAI.RegularPointCoordinates.EuclideanRescalingVolumeConvergence, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.euclideanUnitVolume, OAI.RegularPointCoordinates.EuclideanMeasuredRescalingConvergence, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.SmallScaleVolumeUpper, OAI.RegularPointCoordinates.LocalInitialSplittingInput, OAI.RegularPointCoordinates.LocalTransformationInput, OAI.RegularPointCoordinates.LocalFlatSplittingInput, OAI.RegularPointCoordinates.UniformRegularFlatnessInput