OAI/Combinatorics/RamseyFive/Geometry/PeelingGeometry.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.ScoreScalars.plane_threshold_exp line 10
  2. lemma OAI.SharpRamseyFive.ScoreScalars.plane_list_cutoff line 17
  3. lemma OAI.SharpRamseyFive.TrainingCells.sdiff_clip line 56
  4. lemma OAI.SharpRamseyFive.TrainingCells.sdiff_union_clip line 61
  5. lemma OAI.SharpRamseyFive.ScoreGeometry.outsideAt_clip line 75
  6. lemma OAI.SharpRamseyFive.ScoreGeometry.richCenters_clip line 79
  7. lemma OAI.SharpRamseyFive.ScoreGeometry.localLines_clip line 84
  8. lemma OAI.SharpRamseyFive.ScoreGeometry.badCenters_clip line 89
  9. lemma OAI.SharpRamseyFive.ScoreGeometry.radialExceptions_clip line 94
  10. lemma OAI.SharpRamseyFive.ScoreGeometry.badCenters_threshold_mono line 99
  11. lemma OAI.SharpRamseyFive.ScoreGeometry.radialExceptions_normalization line 106
  12. lemma OAI.SharpRamseyFive.ScoreScalars.nonsmall_strength line 123
  13. lemma OAI.SharpRamseyFive.ScoreScalars.high_exception_scalar line 140
  14. def OAI.SharpRamseyFive.ScoreGeometry.highPlaneExceptions line 186
  15. lemma OAI.SharpRamseyFive.ScoreGeometry.off_highPlaneExceptions line 193
  16. theorem OAI.SharpRamseyFive.ScoreGeometry.highPlaneExceptions_card line 204