OAI/Geometry/UnitDistances/Cutting.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PlanarUnitDistances.CircleCutting.Plane line 8
  2. lemma OAI.PlanarUnitDistances.CircleCutting.plane_dist_sq line 10
  3. lemma OAI.PlanarUnitDistances.CircleCutting.finite_circle_intersection line 15
  4. def OAI.PlanarUnitDistances.CircleCutting.circleIntersections line 28
  5. lemma OAI.PlanarUnitDistances.CircleCutting.mem_circleIntersections line 33
  6. def OAI.PlanarUnitDistances.CircleCutting.direction line 42
  7. lemma OAI.PlanarUnitDistances.CircleCutting.direction_unit line 45
  8. def OAI.PlanarUnitDistances.CircleCutting.projection line 52
  9. def OAI.PlanarUnitDistances.CircleCutting.directionPolynomial line 54
  10. lemma OAI.PlanarUnitDistances.CircleCutting.directionPolynomial_ne_zero line 57
  11. lemma OAI.PlanarUnitDistances.CircleCutting.directionPolynomial_eval line 66
  12. lemma OAI.PlanarUnitDistances.CircleCutting.avoids_finite_polynomials line 75
  13. theorem OAI.PlanarUnitDistances.CircleCutting.exists_good_direction line 91
  14. def OAI.PlanarUnitDistances.CircleCutting.rotate line 147
  15. lemma OAI.PlanarUnitDistances.CircleCutting.rotate_dist line 150
  16. lemma OAI.PlanarUnitDistances.CircleCutting.continuous_rotate line 158
  17. lemma OAI.PlanarUnitDistances.CircleCutting.rotate_injective line 162
  18. lemma OAI.PlanarUnitDistances.CircleCutting.circle_intersection_card line 168
  19. lemma OAI.PlanarUnitDistances.CircleCutting.circleIntersections_card line 182
  20. def OAI.PlanarUnitDistances.CircleCutting.branch line 196
  21. def OAI.PlanarUnitDistances.CircleCutting.active line 199
  22. lemma OAI.PlanarUnitDistances.CircleCutting.active_radicand line 201
  23. lemma OAI.PlanarUnitDistances.CircleCutting.closed_radicand line 206
  24. lemma OAI.PlanarUnitDistances.CircleCutting.continuous_branch line 210
  25. lemma OAI.PlanarUnitDistances.CircleCutting.branch_order line 213
  26. def OAI.PlanarUnitDistances.CircleCutting.graphPoint line 219
  27. lemma OAI.PlanarUnitDistances.CircleCutting.graphPoint_unit line 222
  28. lemma OAI.PlanarUnitDistances.CircleCutting.unit_iff_graph line 232
  29. lemma OAI.PlanarUnitDistances.CircleCutting.unit_projection_closed line 254
  30. lemma OAI.PlanarUnitDistances.CircleCutting.active_of_unit_nonextreme line 260
  31. def OAI.PlanarUnitDistances.CircleCutting.eventAbscissas line 265
  32. lemma OAI.PlanarUnitDistances.CircleCutting.extrema_mem_events line 268
  33. lemma OAI.PlanarUnitDistances.CircleCutting.branch_collision_event line 274
  34. lemma OAI.PlanarUnitDistances.CircleCutting.same_side_of_not_mem line 298
  35. lemma OAI.PlanarUnitDistances.CircleCutting.active_constant line 311
  36. lemma OAI.PlanarUnitDistances.CircleCutting.order_constant line 319
  37. lemma OAI.PlanarUnitDistances.Sweep.sdiff_triangle line 336
  38. lemma OAI.PlanarUnitDistances.Sweep.sdiff_insert_same line 346
  39. lemma OAI.PlanarUnitDistances.Sweep.sdiff_insert_left line 353
  40. lemma OAI.PlanarUnitDistances.Sweep.sdiff_insert_right line 361
  41. def OAI.PlanarUnitDistances.Sweep.links line 365
  42. def OAI.PlanarUnitDistances.Sweep.gaps line 369
  43. lemma OAI.PlanarUnitDistances.Sweep.links_card_le line 371
  44. lemma OAI.PlanarUnitDistances.Sweep.links_change_start line 379
  45. lemma OAI.PlanarUnitDistances.Sweep.links_delete_head line 389
  46. theorem OAI.PlanarUnitDistances.Sweep.links_filter_sdiff line 398
  47. def OAI.PlanarUnitDistances.Sweep.touches line 424
  48. lemma OAI.PlanarUnitDistances.Sweep.links_touch_card line 427
  49. theorem OAI.PlanarUnitDistances.Sweep.event_starts_card line 459
  50. lemma OAI.PlanarUnitDistances.SweepIntervals.between_finsets line 494
  51. def OAI.PlanarUnitDistances.SweepIntervals.span line 509
  52. abbrev OAI.PlanarUnitDistances.SweepIntervals.slab line 512
  53. lemma OAI.PlanarUnitDistances.SweepIntervals.span_ordConnected line 514
  54. lemma OAI.PlanarUnitDistances.SweepIntervals.span_open line 521
  55. lemma OAI.PlanarUnitDistances.SweepIntervals.slab_nonempty line 538
  56. lemma OAI.PlanarUnitDistances.SweepIntervals.slab_no_event line 553
  57. lemma OAI.PlanarUnitDistances.SweepIntervals.count_lt_iff line 559
  58. lemma OAI.PlanarUnitDistances.SweepIntervals.cover_slabs line 580
  59. lemma OAI.PlanarUnitDistances.SweepIntervals.slab_unique line 590
  60. lemma OAI.PlanarUnitDistances.SweepIntervals.slab_subset_span line 603
  61. lemma OAI.PlanarUnitDistances.SweepIntervals.event_mem_span line 608
  62. lemma OAI.PlanarUnitDistances.SweepIntervals.span_decomposition line 613
  63. lemma OAI.PlanarUnitDistances.Sweep.sorted_heights line 644
  64. abbrev OAI.PlanarUnitDistances.CircleCutting.Label line 665
  65. def OAI.PlanarUnitDistances.CircleCutting.labels line 666
  66. def OAI.PlanarUnitDistances.CircleCutting.height line 667
  67. def OAI.PlanarUnitDistances.CircleCutting.activeLabels line 668
  68. lemma OAI.PlanarUnitDistances.CircleCutting.mem_labels line 671
  69. lemma OAI.PlanarUnitDistances.CircleCutting.mem_activeLabels line 674
  70. lemma OAI.PlanarUnitDistances.CircleCutting.height_injOn line 678
  71. lemma OAI.PlanarUnitDistances.CircleCutting.exists_ordered_branches line 686
  72. def OAI.PlanarUnitDistances.CircleCutting.circleEvents line 691
  73. lemma OAI.PlanarUnitDistances.CircleCutting.circleEvents_subset line 695
  74. lemma OAI.PlanarUnitDistances.CircleCutting.circleEvents_card line 711
  75. lemma OAI.PlanarUnitDistances.CircleCutting.extrema_mem_circleEvents line 727
  76. lemma OAI.PlanarUnitDistances.CircleCutting.collision_mem_circleEvents line 731
  77. def OAI.PlanarUnitDistances.CircleCutting.critical line 740
  78. lemma OAI.PlanarUnitDistances.CircleCutting.critical_card_sum line 743
  79. lemma OAI.PlanarUnitDistances.CircleCutting.active_constant_without_events line 759
  80. lemma OAI.PlanarUnitDistances.CircleCutting.height_ne_without_events line 767
  81. lemma OAI.PlanarUnitDistances.CircleCutting.skeleton_constant line 794
  82. lemma OAI.PlanarUnitDistances.CircleCutting.event_span_no_other line 830
  83. lemma OAI.PlanarUnitDistances.CircleCutting.event_span_noncritical line 838
  84. theorem OAI.PlanarUnitDistances.CircleCutting.event_skeleton line 851