OAI/Combinatorics/HalvingLines/Sweep.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarHalving.Sweep.setDistance line 10
  2. lemma OAI.PlanarHalving.Sweep.setDistance_self line 12
  3. lemma OAI.PlanarHalving.Sweep.setDistance_comm line 15
  4. lemma OAI.PlanarHalving.Sweep.setDistance_triangle line 18
  5. structure OAI.PlanarHalving.Sweep.States line 28
  6. def OAI.PlanarHalving.Sweep.States.distance line 38
  7. lemma OAI.PlanarHalving.Sweep.States.distance_self line 41
  8. lemma OAI.PlanarHalving.Sweep.States.distance_comm line 44
  9. lemma OAI.PlanarHalving.Sweep.States.distance_triangle line 47
  10. def OAI.PlanarHalving.Sweep.States.eligible line 50
  11. def OAI.PlanarHalving.Sweep.States.next line 53
  12. lemma OAI.PlanarHalving.Sweep.States.next_spec line 56
  13. lemma OAI.PlanarHalving.Sweep.States.before_next line 60
  14. lemma OAI.PlanarHalving.Sweep.States.next_distance line 70
  15. structure OAI.PlanarHalving.Sweep.States.Greedy line 84
  16. lemma OAI.PlanarHalving.Sweep.States.no_eligible_distance line 93
  17. lemma OAI.PlanarHalving.Sweep.States.close_distance line 100
  18. def OAI.PlanarHalving.Sweep.States.greedy line 106
  19. def OAI.PlanarHalving.Sweep.States.greedySystem line 147
  20. lemma OAI.PlanarHalving.Sweep.slope_symm line 160
  21. def OAI.PlanarHalving.Sweep.criticalSlopes line 164
  22. lemma OAI.PlanarHalving.Sweep.mem_criticalSlopes line 168
  23. lemma OAI.PlanarHalving.Sweep.projection_injective line 173
  24. structure OAI.PlanarHalving.Sweep.Traversal line 186
  25. lemma OAI.PlanarHalving.Sweep.strictMono_snoc line 192
  26. def OAI.PlanarHalving.Sweep.traversal line 207
  27. def OAI.PlanarHalving.Sweep.Traversal.sample line 241
  28. lemma OAI.PlanarHalving.Sweep.Traversal.sample_bounds line 244
  29. lemma OAI.PlanarHalving.Sweep.Traversal.sample_increasing line 250
  30. lemma OAI.PlanarHalving.Sweep.Traversal.sample_not_mem line 255
  31. lemma OAI.PlanarHalving.Sweep.Traversal.unique_critical line 267
  32. lemma OAI.PlanarHalving.Sweep.separates_step_distance line 282
  33. def OAI.PlanarHalving.Sweep.states line 305
  34. def OAI.PlanarHalving.Sweep.StepDisjoint line 322
  35. lemma OAI.PlanarHalving.Sweep.States.Greedy.packing line 325
  36. lemma OAI.PlanarHalving.Sweep.States.greedy_packing line 340
  37. lemma OAI.PlanarHalving.Sweep.States.distance_packing_cubic line 348
  38. def OAI.PlanarHalving.Sweep.States.intervalActivity line 371
  39. lemma OAI.PlanarHalving.Sweep.States.mem_intervalActivity line 375
  40. lemma OAI.PlanarHalving.Sweep.States.intervalActivity_pos_distance line 386
  41. lemma OAI.PlanarHalving.Sweep.states_intervalActivity_distance line 395
  42. lemma OAI.PlanarHalving.Sweep.cube_add_le line 421
  43. lemma OAI.PlanarHalving.Sweep.activity_packing_cubic line 424