OAI/MeasureTheory/Falconer/Geometry/TripleGridRounding.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Rounding bounded physical point sets in transverse coordinates

  1. def OAI.Falconer.tripleRound line 12
  2. theorem OAI.Falconer.round_mesh_error line 15
  3. theorem OAI.Falconer.tripleRound_distance line 22
  4. def OAI.Falconer.tripleIntegerBox line 32
  5. theorem OAI.Falconer.round_bound line 36
  6. theorem OAI.Falconer.tripleRound_mem_box line 49
  7. def OAI.Falconer.roundedTripleGrid line 57
  8. theorem OAI.Falconer.roundedTripleGrid_mem line 62
  9. theorem OAI.Falconer.roundedTripleGrid_original line 68