OAI/Geometry/UnitDistances/RareBudget.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.IncidenceNoise.dp line 10
  2. def OAI.PlanarUnitDistances.IncidenceNoise.collision line 11
  3. def OAI.PlanarUnitDistances.IncidenceNoise.rootInfo line 12
  4. def OAI.PlanarUnitDistances.IncidenceNoise.noise line 13
  5. lemma OAI.PlanarUnitDistances.IncidenceNoise.tpos line 14
  6. lemma OAI.PlanarUnitDistances.IncidenceNoise.dp_nonneg line 15
  7. lemma OAI.PlanarUnitDistances.IncidenceNoise.collision_nonneg line 16
  8. lemma OAI.PlanarUnitDistances.IncidenceNoise.root_nonneg line 17
  9. lemma OAI.PlanarUnitDistances.IncidenceNoise.nonneg line 19
  10. lemma OAI.PlanarUnitDistances.IncidenceNoise.limit line 25
  11. lemma OAI.PlanarUnitDistances.IncidenceNoise.components line 38
  12. lemma OAI.PlanarUnitDistances.IncidenceNoise.dp_le_collision line 49
  13. lemma OAI.PlanarUnitDistances.IncidenceNoise.row_atom line 53
  14. lemma OAI.PlanarUnitDistances.IncidenceNoise.row line 58
  15. lemma OAI.PlanarUnitDistances.IncidenceNoise.column line 65
  16. lemma OAI.PlanarUnitDistances.IncidenceEstimates.template_collision line 95
  17. lemma OAI.PlanarUnitDistances.IncidenceEstimates.history_collision line 108
  18. theorem OAI.PlanarUnitDistances.IncidenceEstimates.basic line 117
  19. lemma OAI.PlanarUnitDistances.IncidenceEstimates.raw_point line 175
  20. lemma OAI.PlanarUnitDistances.IncidenceEstimates.raw_center line 182
  21. lemma OAI.PlanarUnitDistances.IncidenceEstimates.raw_template line 189
  22. lemma OAI.PlanarUnitDistances.IncidenceEstimates.raw_prediction line 197
  23. lemma OAI.PlanarUnitDistances.IncidenceEstimates.star_upper line 204
  24. lemma OAI.PlanarUnitDistances.IncidenceEstimates.prediction_upper line 212
  25. theorem OAI.PlanarUnitDistances.IncidenceEstimates.upper line 222
  26. def OAI.PlanarUnitDistances.EnvelopeCoercivity.pointConstant line 271
  27. def OAI.PlanarUnitDistances.EnvelopeCoercivity.lossConstant line 272
  28. theorem OAI.PlanarUnitDistances.EnvelopeCoercivity.bounds line 274
  29. lemma OAI.PlanarUnitDistances.EnvelopeCoercivity.positive_fraction line 306
  30. def OAI.PlanarUnitDistances.ProfileBudget.weighted line 325
  31. def OAI.PlanarUnitDistances.ProfileBudget.l1 line 326
  32. def OAI.PlanarUnitDistances.ProfileBudget.height line 327
  33. def OAI.PlanarUnitDistances.ProfileBudget.error line 328
  34. lemma OAI.PlanarUnitDistances.ProfileBudget.weighted_nonneg line 330
  35. lemma OAI.PlanarUnitDistances.ProfileBudget.weighted_mono line 332
  36. lemma OAI.PlanarUnitDistances.ProfileBudget.weighted_add line 334
  37. lemma OAI.PlanarUnitDistances.ProfileBudget.weighted_sub line 336
  38. lemma OAI.PlanarUnitDistances.ProfileBudget.integrate line 339
  39. lemma OAI.PlanarUnitDistances.ProfileBudget.height_eq line 353
  40. lemma OAI.PlanarUnitDistances.ProfileBudget.error_eq line 355
  41. lemma OAI.PlanarUnitDistances.ProfileBudget.height_nonneg line 358
  42. lemma OAI.PlanarUnitDistances.ProfileBudget.error_nonneg line 359
  43. lemma OAI.PlanarUnitDistances.ProfileBudget.height_average line 361
  44. lemma OAI.PlanarUnitDistances.ProfileBudget.wedge_height_average line 367
  45. theorem OAI.PlanarUnitDistances.ProfileBudget.residual_budget line 372
  46. theorem OAI.PlanarUnitDistances.ProfileBudget.size_budget line 379
  47. theorem OAI.PlanarUnitDistances.ProfileBudget.residual line 386
  48. theorem OAI.PlanarUnitDistances.ProfileBudget.size line 393
  49. lemma OAI.PlanarUnitDistances.RarePairBudget.slot_pointwise line 410
  50. def OAI.PlanarUnitDistances.RarePairBudget.cap line 421
  51. lemma OAI.PlanarUnitDistances.RarePairBudget.cap_left line 425
  52. lemma OAI.PlanarUnitDistances.RarePairBudget.cap_right line 443
  53. theorem OAI.PlanarUnitDistances.RarePairBudget.positive_budget line 455
  54. theorem OAI.PlanarUnitDistances.RareGlobalBudget.weighted_pair line 476
  55. def OAI.PlanarUnitDistances.ActualRarePair.positive line 503
  56. def OAI.PlanarUnitDistances.ActualRarePair.score line 507
  57. lemma OAI.PlanarUnitDistances.ActualRarePair.positive_bounds line 512
  58. lemma OAI.PlanarUnitDistances.ActualRarePair.cap_nonneg line 520
  59. lemma OAI.PlanarUnitDistances.ActualRarePair.cap_eq line 526
  60. theorem OAI.PlanarUnitDistances.ActualRarePair.positive_cap line 533
  61. theorem OAI.PlanarUnitDistances.ActualRarePair.upper line 563
  62. lemma OAI.PlanarUnitDistances.ActualRarePair.lower_slot line 626
  63. theorem OAI.PlanarUnitDistances.ActualRarePair.pointwise line 652
  64. def OAI.PlanarUnitDistances.ActualHeights.center line 710
  65. def OAI.PlanarUnitDistances.ActualHeights.mistake line 712
  66. lemma OAI.PlanarUnitDistances.ActualHeights.center_nonneg line 714
  67. lemma OAI.PlanarUnitDistances.ActualHeights.mistake_nonneg line 720
  68. lemma OAI.PlanarUnitDistances.ActualHeights.center_average line 726
  69. lemma OAI.PlanarUnitDistances.ActualHeights.mistake_average line 737
  70. lemma OAI.PlanarUnitDistances.ActualHeights.point_integral line 741
  71. lemma OAI.PlanarUnitDistances.ActualHeights.center_integral line 757
  72. lemma OAI.PlanarUnitDistances.ActualHeights.inconsistent_integral line 773
  73. lemma OAI.PlanarUnitDistances.ActualHeights.common_integral line 779
  74. lemma OAI.PlanarUnitDistances.ActualHeights.bad_integral line 785
  75. theorem OAI.PlanarUnitDistances.ActualHeights.pointwise line 791