OAI/Combinatorics/RamseyFive/Geometry/PencilCount.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.ScoreGeometry.pencilCount line 19
  2. lemma OAI.SharpRamseyFive.ScoreGeometry.pencilCount_nonneg line 23
  3. lemma OAI.SharpRamseyFive.ScoreGeometry.pencilCount_weight line 27
  4. lemma OAI.SharpRamseyFive.ScoreGeometry.mean_ratio_lower line 32
  5. theorem OAI.SharpRamseyFive.ScoreGeometry.empty_ambient_card line 41
  6. lemma OAI.SharpRamseyFive.ScoreGeometry.pencilCount_training_sum line 81
  7. lemma OAI.SharpRamseyFive.ScoreGeometry.empty_training_mass line 87
  8. theorem OAI.SharpRamseyFive.ScoreGeometry.empty_training_card line 100
  9. def OAI.SharpRamseyFive.ScoreGeometry.hyperplaneSupport line 128
  10. def OAI.SharpRamseyFive.ScoreGeometry.ownSupport line 131
  11. lemma OAI.SharpRamseyFive.ScoreGeometry.pointScore_eq_sum line 135
  12. lemma OAI.SharpRamseyFive.ScoreGeometry.pointScore_split line 158
  13. def OAI.SharpRamseyFive.ScoreGeometry.pencil line 165
  14. lemma OAI.SharpRamseyFive.ScoreGeometry.emptyTests_pencil line 169
  15. theorem OAI.SharpRamseyFive.ScoreGeometry.pointScore_exceptional line 178