RegularDistanceReplacements.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform dyadic Poisson data throughout a regular neighborhood

theorem OAI.RegularPointCoordinates.regular_distance_replacements line 19
Source documentation
A regular neighborhood has actual squared-distance replacements with one set of constants, while the total full source mass is arbitrarily small. The constants precede the center and every smaller dyadic root.
```
theorem regular_distance_replacements {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) {p : X} {a κ rho eta : ℝ}
    (ha : 0 ≤ a) (hκ : 0 ≤ κ) (hK : -κ ≤ K) (hrho : 0 < rho) (heta : 0 < eta)
    (hcompact : PointedRescalingPrecompactness p) (hregular : IsRegular (m + 2) p)
    (hvolume : EuclideanRescalingVolumeConvergence (hausdorff (m + 2) X) (m + 2) p
      (euclideanUnitVolume (m + 2)))
    (hBG : BallVolumeComparison (hausdorff (m + 2) X) (comparisonModelVolume (m + 1) a))
    (hdensity : ∀ y, SmallScaleVolumeUpper (hausdorff (m + 2) X)
      (comparisonModelVolume (m + 1) a) y (euclideanUnitVolume (m + 2)))
    (hdistance : LocalSquaredDistanceInput hX)
    (hsobolev : LocalDirichletSobolevInput hX) (hcutoff : LocalGoodCutoffInput hX) :
    letI : IsLocallyFiniteMeasure (hausdorff (m + 2) X) :=
…
```
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.LocalSquaredDistanceInput, OAI.RegularPointCoordinates.LocalDirichletSobolevInput, OAI.RegularPointCoordinates.LocalGoodCutoffInput