OAI/MeasureTheory/Falconer/Slicing/PlanarSliceGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Oriented planar coordinates and the strip equations of sliced tubes

  1. theorem OAI.Falconer.exists_unit_axis_isometry line 11
  2. def OAI.Falconer.planarSlope line 21
  3. def OAI.Falconer.planarIntercept line 23
  4. theorem OAI.Falconer.planarSlope_small_of_axis_close line 25
  5. theorem OAI.Falconer.planarIntercept_sub line 39
  6. theorem OAI.Falconer.planarIntercept_perpendicular line 44
  7. theorem OAI.Falconer.planarIntercept_norm_bound line 51
  8. theorem OAI.Falconer.planar_tube_strip line 61