OAI/MeasureTheory/Falconer/Incidence/RoundedRowPencils.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Turn the width-three incidences produced by a coarse packet into exact mesh-scale incidences. The output slope and intercept lie on the mesh, and every output line remains within nine mesh lengths of its original line.

  1. def OAI.Falconer.rowAdjustedRaw line 12
  2. def OAI.Falconer.rowAdjustedLine line 15
  3. theorem OAI.Falconer.rowAdjustedLine_zero line 18
  4. theorem OAI.Falconer.rowAdjustedLine_one line 21
  5. theorem OAI.Falconer.rowAdjustedLine_residual line 24
  6. theorem OAI.Falconer.rowAdjustedLine_incident line 29
  7. theorem OAI.Falconer.rowAdjustedLine_coordinate_error line 37
  8. theorem OAI.Falconer.rowAdjustedLine_near line 60
  9. theorem OAI.Falconer.rowAdjustedLine_family_separated line 66
  10. theorem OAI.Falconer.rowAdjustedLine_family_card line 77
  11. theorem OAI.Falconer.rowAdjustedLine_pencil_card line 91
  12. theorem OAI.Falconer.rowAdjustedLine_pencil_regular line 99