OAI/Combinatorics/HalvingLines/Zoom.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarHalving.Zoom.LineControl.between_chord line 12
2. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.axis_bounded line 37
3. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.good_reciprocal line 58
4. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.good_rational_grid line 91
5. def OAI.PlanarHalving.Zoom.FoliatedSequence.axisConstant line 98
6. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.axisConstant_nonneg line 101
7. def OAI.PlanarHalving.Zoom.FoliatedSequence.rectConstant line 104
8. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.rectConstant_nonneg line 107
9. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.horizontal_between line 113
10. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.vertical_between line 120
11. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.rectangle_chord line 127
12. lemma OAI.PlanarHalving.Zoom.norm_rectangle_corner line 160
13. lemma OAI.PlanarHalving.Zoom.norm_image_edge line 172
14. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.rectangle_error line 182
15. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.small_good_rectangle line 208
16. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.good_eventual_error line 253
17. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.locally_uniform line 259
18. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.uniform_on_compact line 289
19. lemma OAI.PlanarHalving.Zoom.inverse_bound_sign line 296
20. lemma OAI.PlanarHalving.Zoom.norm_sign_inverse_error line 331
21. lemma OAI.PlanarHalving.Zoom.inverse_near_sign line 338
22. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.inverse_uniform_on_compact line 354
23. theorem OAI.PlanarHalving.Zoom.FoliatedSequence.normalized_compactness line 379