OAI/MeasureTheory/Falconer/Geometry/PlanarProjectionCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Coordinates supplied by two distinct planar projection directions. These are the actual coordinates used by the dense scalar graph reduction.

  1. def OAI.Falconer.planarProjectionCoordinates line 9
  2. theorem OAI.Falconer.planar_projection_interpolation line 12
  3. theorem OAI.Falconer.planar_projection_slope line 21
  4. theorem OAI.Falconer.planar_projection_intercept line 28
  5. theorem OAI.Falconer.planarProjectionCoordinates_injective line 35
  6. theorem OAI.Falconer.planar_projection_normalized line 49
  7. theorem OAI.Falconer.planar_projection_ratio_bound line 58
  8. theorem OAI.Falconer.planarProjectionCoordinates_dist_upper line 74
  9. theorem OAI.Falconer.planarProjectionCoordinates_dist_lower line 84