OAI/MeasureTheory/Falconer/Geometry/GeneralGridRounding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Bounded original point sets admit finite transverse lattice approximations

  1. def OAI.Falconer.euclideanRound line 12
  2. theorem OAI.Falconer.euclideanRound_distance line 15
  3. def OAI.Falconer.integerGridBox line 22
  4. theorem OAI.Falconer.euclideanRound_mem_box line 25
  5. def OAI.Falconer.roundedEuclideanGrid line 32
  6. theorem OAI.Falconer.roundedEuclideanGrid_mem line 37
  7. theorem OAI.Falconer.roundedEuclideanGrid_original line 43