OAI/Combinatorics/HalvingLines/Densities.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarHalving.RankLimits.Subwindows line 11
2. instance OAI.PlanarHalving.RankLimits.(instance at line 12) line 12
3. lemma OAI.PlanarHalving.RankLimits.Converges.crossing_real_projection_disjoint line 14
4. lemma OAI.PlanarHalving.RankLimits.Converges.rank_regular_ae line 29
5. lemma OAI.PlanarHalving.RankLimits.Converges.rank_independent_ae line 47
6. def OAI.PlanarHalving.RankLimits.reflectSecond line 110
7. lemma OAI.PlanarHalving.RankLimits.reflectSecond_apply line 113
8. lemma OAI.PlanarHalving.RankLimits.reflectSecond_signed line 115
9. def OAI.PlanarHalving.RankLimits.Configuration.rankChart line 117
10. lemma OAI.PlanarHalving.RankLimits.Configuration.rankChart_apply line 126
11. lemma OAI.PlanarHalving.RankLimits.Configuration.rankChart_source line 135
12. lemma OAI.PlanarHalving.RankLimits.Configuration.rankChart_target line 139
13. def OAI.PlanarHalving.RankLimits.Configuration.timeSlope line 160
14. lemma OAI.PlanarHalving.RankLimits.Configuration.timeSlope_before line 163
15. lemma OAI.PlanarHalving.RankLimits.Configuration.timeSlope_after line 169
16. lemma OAI.PlanarHalving.RankLimits.coordinate_forward_before line 176
17. lemma OAI.PlanarHalving.RankLimits.coordinate_forward_after line 187
18. lemma OAI.PlanarHalving.RankLimits.Configuration.rank_forward_before line 198
19. lemma OAI.PlanarHalving.RankLimits.Configuration.rank_forward_after line 205
20. lemma OAI.PlanarHalving.Directions.allowed_nonempty_of_approx line 217
21. lemma OAI.PlanarHalving.Directions.ray_exit_at_radius line 260
22. lemma OAI.PlanarHalving.Directions.chord_firstOrder line 276
23. def OAI.PlanarHalving.RankLimits.reflectFirst line 291
24. lemma OAI.PlanarHalving.RankLimits.reflectFirst_apply line 294
25. lemma OAI.PlanarHalving.RankLimits.rank_firstOrder_filter line 296
26. theorem OAI.PlanarHalving.RankLimits.actual_allowed_nonempty line 314