OAI/Geometry/UnitDistances/Circles.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.PopularCircles.neighbors line 10
  2. def OAI.PlanarUnitDistances.PopularCircles.candidates line 11
  3. def OAI.PlanarUnitDistances.PopularCircles.popular line 13
  4. def OAI.PlanarUnitDistances.PopularCircles.multiple line 15
  5. lemma OAI.PlanarUnitDistances.PopularCircles.mem_neighbors line 18
  6. lemma OAI.PlanarUnitDistances.PopularCircles.mem_candidates line 20
  7. theorem OAI.PlanarUnitDistances.PopularCircles.mem_popular line 30
  8. lemma OAI.PlanarUnitDistances.PopularCircles.intersection_card line 37
  9. lemma OAI.PlanarUnitDistances.PopularCircles.pair_neighbors line 45
  10. theorem OAI.PlanarUnitDistances.PopularCircles.count line 52
  11. lemma OAI.PlanarUnitDistances.PopularCircles.multi_pairs line 73
  12. theorem OAI.PlanarUnitDistances.PopularCircles.multiple_count line 80
  13. theorem OAI.PlanarUnitDistances.PopularCircles.exceptional_partner_count line 97
  14. lemma OAI.PlanarUnitDistances.PopularCircleCost.event_injective_bound line 129
  15. lemma OAI.PlanarUnitDistances.PopularCircleCost.support_event_bound line 147
  16. theorem OAI.PlanarUnitDistances.PopularCircleCost.cost line 164
  17. def OAI.PlanarUnitDistances.IncidencePopular.points line 249
  18. def OAI.PlanarUnitDistances.IncidencePopular.k line 250
  19. def OAI.PlanarUnitDistances.IncidencePopular.centers line 251
  20. def OAI.PlanarUnitDistances.IncidencePopular.bad line 252
  21. lemma OAI.PlanarUnitDistances.IncidencePopular.points_card line 255
  22. lemma OAI.PlanarUnitDistances.IncidencePopular.tpos line 257
  23. lemma OAI.PlanarUnitDistances.IncidencePopular.center_atom line 258
  24. lemma OAI.PlanarUnitDistances.IncidencePopular.column_atom line 276
  25. lemma OAI.PlanarUnitDistances.IncidencePopular.k_large line 288
  26. lemma OAI.PlanarUnitDistances.IncidencePopular.count_bound line 292
  27. lemma OAI.PlanarUnitDistances.IncidencePopular.cost line 323
  28. lemma OAI.PlanarUnitDistances.IncidencePopular.cost_limit line 338
  29. def OAI.PlanarUnitDistances.LawDeletion.keep line 363
  30. lemma OAI.PlanarUnitDistances.LawDeletion.cost line 364
  31. lemma OAI.PlanarUnitDistances.LawDeletion.wedge_support line 371
  32. def OAI.PlanarUnitDistances.PlaceLogGeometry.supported line 396
  33. lemma OAI.PlanarUnitDistances.PlaceLogGeometry.supported_of_mem line 399
  34. lemma OAI.PlanarUnitDistances.PlaceLogGeometry.log_mul line 403
  35. lemma OAI.PlanarUnitDistances.PlaceLogGeometry.log_div line 407
  36. lemma OAI.PlanarUnitDistances.PlaceLogGeometry.supported_mul line 410
  37. lemma OAI.PlanarUnitDistances.PlaceLogGeometry.supported_div line 414
  38. lemma OAI.PlanarUnitDistances.PlaceLogGeometry.height_identity line 419
  39. lemma OAI.PlanarUnitDistances.PlaceLogGeometry.unit_pair_identity line 437
  40. theorem OAI.PlanarUnitDistances.PlaceLogGeometry.rectangle line 446