OAI/Combinatorics/RamseyFive/Geometry/ScoreDegreeLowNormalized.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpRamseyFive.ScoreGeometry.score_degree_low_normalized line 19
  2. lemma OAI.SharpRamseyFive.ScoreGeometry.offRow_bounded_cover line 36
  3. theorem OAI.SharpRamseyFive.ScoreGeometry.score_row_low_moment line 48
  4. theorem OAI.SharpRamseyFive.ScoreGeometry.shift_row_from_power line 78
  5. theorem OAI.SharpRamseyFive.ScoreGeometry.shift_pair_from_power line 103
  6. theorem OAI.SharpRamseyFive.ScoreGeometry.certificate_pair_eq_power line 122
  7. def OAI.SharpRamseyFive.ScoreGeometry.certificateMajorant line 143
  8. lemma OAI.SharpRamseyFive.ScoreGeometry.certificateMajorant_nonneg line 149
  9. theorem OAI.SharpRamseyFive.ScoreGeometry.score_certificate_majorant line 160