RegularPointedFlatness.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform metric flatness near a regular point from local volume rigidity

def OAI.RegularPointCoordinates.curvatureRadius line 15
theorem OAI.RegularPointCoordinates.curvatureRadius_pos line 17
theorem OAI.RegularPointCoordinates.curvature_bound_of_radius line 21
theorem OAI.RegularPointCoordinates.regular_uniform_pointed_flatness line 35
Source documentation
The regular-point volume neighborhood supplies a single neighborhood whose every sufficiently small ball is pointed close to Euclidean space.
```
theorem regular_uniform_pointed_flatness {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)))
    (hBG : BallVolumeComparison (hausdorff (m + 1) X) (comparisonModelVolume m a))
    (hdensity : ∀ y, SmallScaleVolumeUpper (hausdorff (m + 1) X)
      (comparisonModelVolume m a) y (euclideanUnitVolume (m + 1)))
    (hrigidity : LocalVolumeRigidityInput hX) {θ : ℝ} (hθ : 0 < θ) :
    ∃ D : ℝ, 0 < D ∧ ∀ q, dist p q ≤ D → ∀ r : ℝ, 0 < r → r ≤ D / 4 →
      ∃ f : X → Euclidean (m + 1), IsPointedApproximation q 0 r 2 θ f := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.PointedRescalingPrecompactness, OAI.RegularPointCoordinates.IsRegular, OAI.RegularPointCoordinates.EuclideanRescalingVolumeConvergence, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.euclideanUnitVolume, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.SmallScaleVolumeUpper, OAI.RegularPointCoordinates.LocalVolumeRigidityInput, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation