RegularDistanceSources.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniformly small full distance sources near a regular point

theorem OAI.RegularPointCoordinates.regular_small_distance_sources line 18

Source documentation

The same neighborhood works for every center and every smaller root radius. Both the full source and its small total mass are constructed.

theorem regular_small_distance_sources {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) :
    letI : IsLocallyFiniteMeasure (hausdorff (m + 2) X) :=
…