OAI/Geometry/UnitDistances/RareEvents.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PlanarUnitDistances.CommonRareScore.balanced line 12
  2. theorem OAI.PlanarUnitDistances.CommonRareScore.balanced_average line 44
  3. def OAI.PlanarUnitDistances.RareMass.nonsharedCoord line 74
  4. lemma OAI.PlanarUnitDistances.RareMass.coordinate_mismatch line 76
  5. lemma OAI.PlanarUnitDistances.RareMass.minority_mass line 80
  6. theorem OAI.PlanarUnitDistances.RareMass.minority_le_exceptions line 95
  7. lemma OAI.PlanarUnitDistances.RareMass.mismatch_le_minority_error line 111
  8. def OAI.PlanarUnitDistances.RareLabels.minorityMass line 127
  9. def OAI.PlanarUnitDistances.RareLabels.error line 129
  10. lemma OAI.PlanarUnitDistances.RareLabels.exception_diag line 132
  11. theorem OAI.PlanarUnitDistances.RareLabels.dominant line 135
  12. lemma OAI.PlanarUnitDistances.RareLabels.minority_le line 163
  13. def OAI.PlanarUnitDistances.RareLabels.label line 173
  14. lemma OAI.PlanarUnitDistances.RareLabels.label_spec line 178
  15. lemma OAI.PlanarUnitDistances.LawRare.event_domination line 196
  16. theorem OAI.PlanarUnitDistances.LawRare.small_rect line 204
  17. lemma OAI.PlanarUnitDistances.LawRare.sqrt_le_half_sum line 240
  18. theorem OAI.PlanarUnitDistances.LawRare.edge_rare line 245
  19. lemma OAI.PlanarUnitDistances.LawWedges.conditional_eq line 264
  20. lemma OAI.PlanarUnitDistances.LawWedges.wedgeMass_eq line 270
  21. theorem OAI.PlanarUnitDistances.LawWedges.rare line 282
  22. lemma OAI.PlanarUnitDistances.LawWedges.pair_event_sq line 293
  23. def OAI.PlanarUnitDistances.RareMoments.hp line 312
  24. def OAI.PlanarUnitDistances.RareMoments.hq line 314
  25. def OAI.PlanarUnitDistances.RareMoments.joint line 316
  26. def OAI.PlanarUnitDistances.RareMoments.wedge line 319
  27. theorem OAI.PlanarUnitDistances.RareMoments.joint_wedge line 325
  28. theorem OAI.PlanarUnitDistances.RareMoments.uniform line 354
  29. lemma OAI.PlanarUnitDistances.FiniteLaw.event_markov line 392
  30. theorem OAI.PlanarUnitDistances.CommonTemplate.marginal_score line 411
  31. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.joint_le_left line 447
  32. lemma OAI.PlanarUnitDistances.FiniteStarCoupling.conditional_collision line 450
  33. def OAI.PlanarUnitDistances.LevelBookkeeping.goodRare line 473
  34. def OAI.PlanarUnitDistances.LevelBookkeeping.damaged line 476
  35. lemma OAI.PlanarUnitDistances.LevelBookkeeping.minority_nonneg line 480
  36. lemma OAI.PlanarUnitDistances.LevelBookkeeping.minority_le_half line 483
  37. lemma OAI.PlanarUnitDistances.LevelBookkeeping.not_common line 489
  38. theorem OAI.PlanarUnitDistances.LevelBookkeeping.select line 497
  39. theorem OAI.PlanarUnitDistances.LevelBookkeeping.widths line 532
  40. theorem OAI.PlanarUnitDistances.LevelBookkeeping.moments line 556
  41. lemma OAI.PlanarUnitDistances.FiniteLaw.avg_neg line 598
  42. def OAI.PlanarUnitDistances.FiniteLaw.cut line 600
  43. lemma OAI.PlanarUnitDistances.FiniteLaw.cut_add line 601
  44. lemma OAI.PlanarUnitDistances.FiniteLaw.cut_smul line 604
  45. lemma OAI.PlanarUnitDistances.FiniteLaw.cut_const line 607
  46. lemma OAI.PlanarUnitDistances.FiniteLaw.cut_nonneg line 610
  47. lemma OAI.PlanarUnitDistances.FiniteLaw.cut_le_avg line 612
  48. lemma OAI.PlanarUnitDistances.FiniteLaw.cut_mono line 614