OAI/MeasureTheory/Falconer/Geometry/HalfSlopeGrid.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Dyadic nearest-grid rounding preserves the slope interval used by the recursive cell construction. The endpoints are actual points of the grid.

  1. theorem OAI.Falconer.lineGridRound_monotone line 9
  2. theorem OAI.Falconer.lineGridRound_grid line 18
  3. theorem OAI.Falconer.lineGridRound_half_interval line 22
  4. theorem OAI.Falconer.lineGridRound_dyadic_half line 37
  5. theorem OAI.Falconer.dyadic_local_mesh line 45
  6. theorem OAI.Falconer.dyadic_relative_mesh line 53
  7. theorem OAI.Falconer.lineGridRound_local_dyadic_half line 60