OAI/Combinatorics/HalvingLines/Activity.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarHalving.Sweep.projection line 9
2. def OAI.PlanarHalving.Sweep.Separates line 11
3. lemma OAI.PlanarHalving.Sweep.comparison_persists line 14
4. lemma OAI.PlanarHalving.Sweep.exchange_rightward line 29
5. theorem OAI.PlanarHalving.Sweep.distance_of_outside_visitors line 37
6. structure OAI.PlanarHalving.Sweep.ProjectionIndex line 72
7. def OAI.PlanarHalving.Sweep.projectionIndexEquiv line 75
8. theorem OAI.PlanarHalving.Sweep.exists_state line 81
9. lemma OAI.PlanarHalving.Sweep.states_nested line 124
10. theorem OAI.PlanarHalving.Sweep.outside_class_distance line 136
11. lemma OAI.PlanarHalving.Sweep.separates_neg_compl line 166
12. def OAI.PlanarHalving.Sweep.activity line 177
13. lemma OAI.PlanarHalving.Sweep.mem_activity line 182
14. theorem OAI.PlanarHalving.Sweep.activity_distance line 189
15. lemma OAI.PlanarHalving.Sweep.projection_lt_between line 261
16. lemma OAI.PlanarHalving.Sweep.separates_between line 272
17. lemma OAI.PlanarHalving.Sweep.states_unique line 278
18. theorem OAI.PlanarHalving.Sweep.activity_pos_distance line 282
19. lemma OAI.PlanarHalving.Sweep.exchange_slope_between line 303