OAI/MeasureTheory/Falconer/Geometry/ChartCoordinates.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Normalized line sections of the gnomonic chart

The first tangent coordinate is isolated exactly. The other coordinates give a vector perpendicular to both the pole and the chosen tangent axis.

  1. theorem OAI.Falconer.coordinateJoin_inner line 14
  2. theorem OAI.Falconer.coordinateJoin_norm_sq line 20
  3. def OAI.Falconer.chartPole line 25
  4. def OAI.Falconer.chartAxis line 28
  5. def OAI.Falconer.transverseLift line 31
  6. theorem OAI.Falconer.chartPole_norm line 34
  7. theorem OAI.Falconer.chartAxis_norm line 42
  8. theorem OAI.Falconer.transverseLift_norm line 51
  9. theorem OAI.Falconer.chartPole_inner_transverse line 58
  10. theorem OAI.Falconer.chartPole_inner_axis line 62
  11. theorem OAI.Falconer.transverseLift_inner_axis line 66
  12. theorem OAI.Falconer.northLift_coordinateJoin line 70
  13. theorem OAI.Falconer.gnomonicChart_coordinateJoin line 81
  14. theorem OAI.Falconer.gnomonicDensity_coordinateJoin line 86