OAI/MeasureTheory/Falconer/Angular/GnomonicInverse.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Falconer.gnomonicCoordinates line 15
2. theorem OAI.Falconer.gnomonicCoordinates_apply line 18
3. theorem OAI.Falconer.gnomonicCoordinates_measurable line 21
4. theorem OAI.Falconer.gnomonicCoordinates_gnomonicChart line 27
5. theorem OAI.Falconer.northLift_gnomonicCoordinates line 33
6. theorem OAI.Falconer.gnomonicChart_gnomonicCoordinates line 44
7. theorem OAI.Falconer.northLift_distance line 53
8. theorem OAI.Falconer.gnomonicChart_distance_le line 59
9. def OAI.Falconer.gnomonicRatio line 74
10. theorem OAI.Falconer.gnomonicRatio_apply line 77
11. theorem OAI.Falconer.gnomonicRatio_continuousOn line 80
12. theorem OAI.Falconer.northLift_gnomonicRatio line 88
13. theorem OAI.Falconer.gnomonicRatio_chart line 97
14. theorem OAI.Falconer.northLift_ratio_norm line 103
15. theorem OAI.Falconer.gnomonicChart_ratio line 110
16. theorem OAI.Falconer.gnomonicChart_range line 120
17. theorem OAI.Falconer.gnomonicChart_measurableEmbedding line 127
18. def OAI.Falconer.gnomonicConePoint line 130
19. theorem OAI.Falconer.gnomonicConePoint_zero line 133
20. theorem OAI.Falconer.gnomonicConePoint_succ line 136
21. theorem OAI.Falconer.gnomonicRatio_conePoint line 139
22. theorem OAI.Falconer.gnomonicConePoint_radius line 145