OAI/Combinatorics/HalvingLines/Boundary.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarHalving.Boundary.outside_strip line 9
2. lemma OAI.PlanarHalving.Boundary.initially_marked_loss line 18
3. lemma OAI.PlanarHalving.Boundary.initially_unmarked_gain line 30
4. theorem OAI.PlanarHalving.Boundary.three_strips_core line 42
5. lemma OAI.PlanarHalving.Boundary.token_population line 154
6. lemma OAI.PlanarHalving.Boundary.filter_population_change line 162
7. theorem OAI.PlanarHalving.Boundary.token_population_budget line 188
8. theorem OAI.PlanarHalving.Boundary.three_strips_tokens line 217
9. lemma OAI.PlanarHalving.Boundary.changes_initial line 246
10. def OAI.PlanarHalving.Boundary.dot line 263
11. def OAI.PlanarHalving.Boundary.sqNorm line 265
12. lemma OAI.PlanarHalving.Boundary.dot_sq_le line 267
13. lemma OAI.PlanarHalving.Boundary.abs_dot_le line 271
14. theorem OAI.PlanarHalving.Boundary.three_strips_geometric line 280
15. lemma OAI.PlanarHalving.Boundary.active_le_outside_add_strips line 317