OAI/Combinatorics/HalvingLines/Tokens.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarHalving.Boundary.sum_cube_le line 11
2. lemma OAI.PlanarHalving.Boundary.sum_angular_power_le line 18
3. lemma OAI.PlanarHalving.Boundary.high_mass_bound line 48
4. lemma OAI.PlanarHalving.Boundary.activity_sum_bound line 68
5. lemma OAI.PlanarHalving.Boundary.low_cube_bound line 85
6. lemma OAI.PlanarHalving.Boundary.low_bound_tendsto_zero line 140
7. theorem OAI.PlanarHalving.Boundary.mass_eq_zero line 169
8. lemma OAI.PlanarHalving.RankCoordinates.exists_slope_avoiding line 225
9. lemma OAI.PlanarHalving.RankCoordinates.exists_affine_avoiding line 242
10. lemma OAI.PlanarHalving.Batches.ConvexPath.interior_slopes line 258
11. lemma OAI.PlanarHalving.Batches.ConvexPath.exists_clean_extension line 287
12. def OAI.PlanarHalving.RankCoordinates.slot line 320
13. lemma OAI.PlanarHalving.RankCoordinates.slot_lt_of_le_imp_lt line 323
14. lemma OAI.PlanarHalving.RankCoordinates.slot_chord_bounds line 339
15. theorem OAI.PlanarHalving.RankCoordinates.pair_slots_injOn line 357
16. lemma OAI.PlanarHalving.RankCoordinates.slot_lt_card line 377