OAI/MeasureTheory/Falconer/Geometry/ProjectionRows.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The row geometry in Orponen--Shmerkin, Appendix A.7, expressed in the original line chart. A line is incident to only a bounded number of points on a separated row. Its parameter projection stays close to that row point.

  1. def OAI.Falconer.lineParameterProjection line 14
  2. def OAI.Falconer.rowPoint line 15
  3. theorem OAI.Falconer.rowPoint_zero line 17
  4. theorem OAI.Falconer.rowPoint_one line 18
  5. theorem OAI.Falconer.rowPoint_dist line 20
  6. theorem OAI.Falconer.lineParameterProjection_dist line 25
  7. theorem OAI.Falconer.tube_projection_near line 36
  8. theorem OAI.Falconer.row_dist_projection line 41
  9. theorem OAI.Falconer.separated_row_tube_count line 51
  10. theorem OAI.Falconer.row_tube_union_count line 68