OAI/MeasureTheory/Falconer/Angular/GnomonicChart.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The north-hemisphere gnomonic chart

This is the explicit inverse gnomonic map, in Euclidean coordinates. The measure identity used with this map is kept separate as a published input; all the coordinate identities below are proved.

  1. def OAI.Falconer.northLift line 18
  2. theorem OAI.Falconer.northLift_zero line 21
  3. theorem OAI.Falconer.northLift_succ line 23
  4. theorem OAI.Falconer.northLift_ne_zero line 26
  5. theorem OAI.Falconer.northLift_norm_sq line 31
  6. theorem OAI.Falconer.northLift_continuous line 35
  7. def OAI.Falconer.gnomonicChart line 43
  8. theorem OAI.Falconer.gnomonicChart_continuous line 49
  9. theorem OAI.Falconer.gnomonicChart_zero line 54
  10. theorem OAI.Falconer.gnomonicChart_succ line 58
  11. def OAI.Falconer.northHemisphere line 62
  12. theorem OAI.Falconer.gnomonicChart_mem_hemisphere line 65
  13. theorem OAI.Falconer.gnomonicChart_coordinate_ratio line 71
  14. theorem OAI.Falconer.gnomonicChart_injective line 77
  15. def OAI.Falconer.gnomonicDensity line 83
  16. theorem OAI.Falconer.gnomonicDensity_pos line 86
  17. theorem OAI.Falconer.gnomonicDensity_continuous line 89