OAI/Combinatorics/RamseyFive/Geometry/OverlapDyads.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.ScoreGeometry.overlapDyads line 18
  2. lemma OAI.SharpRamseyFive.ScoreGeometry.score_dyadic_cover line 23
  3. def OAI.SharpRamseyFive.ScoreGeometry.geometricPairBudget line 42
  4. def OAI.SharpRamseyFive.ScoreGeometry.pairPowerBudget line 47
  5. lemma OAI.SharpRamseyFive.ScoreGeometry.pairPowerBudget_nonneg line 51
  6. theorem OAI.SharpRamseyFive.ScoreGeometry.score_overlap_power line 58
  7. theorem OAI.SharpRamseyFive.ScoreGeometry.score_shift_pair_budget line 71
  8. theorem OAI.SharpRamseyFive.ScoreGeometry.score_certificate_pair_budget line 91
  9. def OAI.SharpRamseyFive.ScoreGeometry.offRow line 123
  10. lemma OAI.SharpRamseyFive.ScoreGeometry.offRow_nonneg line 128
  11. def OAI.SharpRamseyFive.ScoreGeometry.geometricRowBudget line 135
  12. def OAI.SharpRamseyFive.ScoreGeometry.rowPowerBudget line 140
  13. lemma OAI.SharpRamseyFive.ScoreGeometry.offRow_cover line 145
  14. theorem OAI.SharpRamseyFive.ScoreGeometry.score_row_power line 156
  15. theorem OAI.SharpRamseyFive.ScoreGeometry.score_shift_row_budget line 177