OAI/Geometry/RCD/Sobolev/DistancePoissonDistanceValues.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Replacing compact Poisson values by the actual squared distance

  1. theorem OAI.RegularPointCoordinates.DistancePoissonMeanData.scaled_distance_error_ae line 18
  2. theorem OAI.RegularPointCoordinates.DistancePoissonMeanData.normalized_distance_mean_error line 37