OAI/Geometry/UnitDistances/Sampling.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarUnitDistances.FiniteSampling.avoiding_count line 8
  2. lemma OAI.PlanarUnitDistances.FiniteSampling.exists_hit line 16
  3. lemma OAI.PlanarUnitDistances.FiniteSampling.exists_hit_of_exponential line 37
  4. def OAI.PlanarUnitDistances.FiniteSampling.sampleSize line 71
  5. lemma OAI.PlanarUnitDistances.FiniteSampling.sampleSize_error line 74
  6. lemma OAI.PlanarUnitDistances.FiniteSampling.sampleSize_pos line 93
  7. lemma OAI.PlanarUnitDistances.FiniteSampling.sampleSize_le line 98
  8. lemma OAI.PlanarUnitDistances.FiniteSampling.exists_hit_large_conflicts line 107
  9. lemma OAI.PlanarUnitDistances.FiniteSampling.sum_sample_coordinate line 129
  10. lemma OAI.PlanarUnitDistances.FiniteSampling.sum_sample_cost line 146
  11. lemma OAI.PlanarUnitDistances.FiniteSampling.exists_low_cost_in_large_set line 160
  12. lemma OAI.PlanarUnitDistances.FiniteSampling.avoiding_count_le line 180
  13. lemma OAI.PlanarUnitDistances.FiniteSampling.exists_hit_large_conflicts_with_cost line 196
  14. def OAI.PlanarUnitDistances.CircleCutting.conflicts line 253
  15. lemma OAI.PlanarUnitDistances.CircleCutting.conflicts_subtype_card line 256
  16. theorem OAI.PlanarUnitDistances.CircleCutting.cutting_good_position line 267
  17. lemma OAI.PlanarUnitDistances.CircleCutting.rotate_continuous line 315
  18. lemma OAI.PlanarUnitDistances.CircleCutting.conflicts_rotate line 319
  19. def OAI.PlanarUnitDistances.CircleCutting.cuttingLog line 331
  20. theorem OAI.PlanarUnitDistances.CircleCutting.cutting_with_cost line 333
  21. lemma OAI.PlanarUnitDistances.CircleIncidence.cutting_small_parameter line 396
  22. lemma OAI.PlanarUnitDistances.CircleIncidence.cutting_large_parameter line 406
  23. lemma OAI.PlanarUnitDistances.CircleIncidence.cutting_sqrt_identity line 427
  24. lemma OAI.PlanarUnitDistances.CircleIncidence.cutting_absorbed_numeric line 435
  25. lemma OAI.PlanarUnitDistances.CircleIncidence.cutting_parameter_exists line 461
  26. def OAI.PlanarUnitDistances.CircleIncidence.degree line 491
  27. def OAI.PlanarUnitDistances.CircleIncidence.incidences line 494
  28. lemma OAI.PlanarUnitDistances.CircleIncidence.degree_sum line 496
  29. lemma OAI.PlanarUnitDistances.CircleIncidence.degree_nonneg line 500
  30. lemma OAI.PlanarUnitDistances.CircleIncidence.incidences_nonneg line 502
  31. lemma OAI.PlanarUnitDistances.CircleIncidence.incidences_comm line 505
  32. lemma OAI.PlanarUnitDistances.CircleIncidence.degree_le line 511
  33. lemma OAI.PlanarUnitDistances.CircleIncidence.incidences_le line 514
  34. def OAI.PlanarUnitDistances.CircleIncidence.common line 518
  35. lemma OAI.PlanarUnitDistances.CircleIncidence.common_sum line 521
  36. lemma OAI.PlanarUnitDistances.CircleIncidence.common_le_two line 528
  37. lemma OAI.PlanarUnitDistances.CircleIncidence.common_self line 534
  38. lemma OAI.PlanarUnitDistances.CircleIncidence.degree_sq_sum line 537
  39. lemma OAI.PlanarUnitDistances.CircleIncidence.degree_sq_bound line 545
  40. lemma OAI.PlanarUnitDistances.CircleIncidence.incidences_pair_bound line 563
  41. lemma OAI.PlanarUnitDistances.CircleIncidence.degree_mono line 586
  42. lemma OAI.PlanarUnitDistances.CircleIncidence.incidences_mono_left line 590
  43. lemma OAI.PlanarUnitDistances.CircleIncidence.incidences_mono_right line 594
  44. lemma OAI.PlanarUnitDistances.CircleIncidence.incidences_filter_split line 598
  45. def OAI.PlanarUnitDistances.CircleIncidence.retained line 604
  46. def OAI.PlanarUnitDistances.CircleIncidence.deleted line 607
  47. lemma OAI.PlanarUnitDistances.CircleIncidence.incidence_deletion_split line 610
  48. lemma OAI.PlanarUnitDistances.CircleIncidence.deleted_degree_le line 621
  49. lemma OAI.PlanarUnitDistances.CircleIncidence.deleted_incidence_le line 639
  50. lemma OAI.PlanarUnitDistances.CircleIncidence.incidence_in_region line 657
  51. lemma OAI.PlanarUnitDistances.CircleIncidence.incidence_partition line 669
  52. lemma OAI.PlanarUnitDistances.CircleIncidence.incidence_cutting_regions line 678
  53. theorem OAI.PlanarUnitDistances.CircleIncidence.incidence_cutting_recurrence line 708
  54. lemma OAI.PlanarUnitDistances.CircleIncidence.incidence_cutting_absorbed line 736
  55. lemma OAI.PlanarUnitDistances.CircleIncidence.cuttingLog_one_le line 758
  56. lemma OAI.PlanarUnitDistances.CircleIncidence.cuttingLog_mono line 765
  57. lemma OAI.PlanarUnitDistances.CircleIncidence.incidence_bound_oriented line 772
  58. theorem OAI.PlanarUnitDistances.CircleIncidence.incidence_bound line 806
  59. theorem OAI.PlanarUnitDistances.FiniteTruncation.weighted_subset line 823
  60. lemma OAI.PlanarUnitDistances.CircleIncidence.dense_region_subset line 867
  61. lemma OAI.PlanarUnitDistances.CircleIncidence.deleted_incidence_trivial line 908
  62. theorem OAI.PlanarUnitDistances.CircleIncidence.exists_incidence_piece line 914