OAI/Geometry/RCD/Sobolev/DistancePoissonMeanData.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous compact extensions and cutoffs of the actual Poisson family

  1. structure OAI.RegularPointCoordinates.DistancePoissonMeanData line 17
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.distance_poisson_mean_data line 33
  3. def OAI.RegularPointCoordinates.DistancePoissonMeanData.budget line 67
  4. theorem OAI.RegularPointCoordinates.DistancePoissonMeanData.budget_nonneg line 71
  5. theorem OAI.RegularPointCoordinates.DistancePoissonMeanData.normalized_budget_tendsto_zero line 76