OAI/Geometry/RCD/Sobolev/DistancePoissonConstruction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform actual Poisson replacements for arbitrary distance sources

Only one radius at each center is needed by the near-regular limit argument. The same constants work simultaneously for every such center and source.

  1. theorem OAI.RegularPointCoordinates.distance_curvature_lower line 19
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.uniform_distance_poisson_replacement line 26