OAI/MeasureTheory/Falconer/Geometry/BoundedProjectionCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Bounded actual projection coordinates, with exact finite cell-count comparison to the original planar projections.

  1. def OAI.Falconer.boundedProjectionCoordinates line 10
  2. theorem OAI.Falconer.boundedProjectionCoordinates_zero line 13
  3. theorem OAI.Falconer.boundedProjectionCoordinates_one line 18
  4. theorem OAI.Falconer.boundedProjectionCoordinates_injective line 23
  5. theorem OAI.Falconer.boundedProjectionCoordinates_image line 27
  6. theorem OAI.Falconer.boundedProjectionCoordinates_separated line 33
  7. theorem OAI.Falconer.boundedProjectionCoordinates_regular line 40
  8. theorem OAI.Falconer.boundedProjectionCoordinates_bound line 54
  9. theorem OAI.Falconer.boundedProjectionCoordinates_coordinate_cells line 73
  10. theorem OAI.Falconer.boundedProjectionCoordinates_projection_image line 101