OAI/MeasureTheory/Falconer/Estimates/CoarsePlanarRounding.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A common coarse grid inside the original chart and the resulting point-line incidence error.

  1. def OAI.Falconer.coarsePlanarRound line 12
  2. theorem OAI.Falconer.coarsePlanarRound_zero line 15
  3. theorem OAI.Falconer.coarsePlanarRound_one line 18
  4. theorem OAI.Falconer.coarsePlanarRound_near line 21
  5. theorem OAI.Falconer.coarsePlanarRound_separated line 27
  6. theorem OAI.Falconer.lineGridRound_bounded line 38
  7. theorem OAI.Falconer.dyadic_coarse_round_chart line 63
  8. theorem OAI.Falconer.coarse_round_incident line 73