OAI/Combinatorics/RamseyFive/Entropy/SubsetEncoding.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.SubsetEncoding.log_factorial_lower line 9
  2. lemma OAI.SharpRamseyFive.SubsetEncoding.log_choose_le line 20
  3. abbrev OAI.SharpRamseyFive.SubsetEncoding.Alphabet line 36
  4. lemma OAI.SharpRamseyFive.SubsetEncoding.alphabet_card line 38
  5. def OAI.SharpRamseyFive.SubsetEncoding.encode line 47
  6. def OAI.SharpRamseyFive.SubsetEncoding.decode line 50
  7. lemma OAI.SharpRamseyFive.SubsetEncoding.decode_encode line 53
  8. theorem OAI.SharpRamseyFive.SubsetEncoding.small_set_description line 56
  9. def OAI.SharpRamseyFive.ScoreGeometry.sizeScoreCutoff line 82
  10. def OAI.SharpRamseyFive.ScoreGeometry.baseAlphabet line 86
  11. instance OAI.SharpRamseyFive.ScoreGeometry.(instance at line 91) line 91
  12. def OAI.SharpRamseyFive.ScoreGeometry.baseDecoded line 96
  13. lemma OAI.SharpRamseyFive.ScoreGeometry.baseDecoded_small line 108
  14. lemma OAI.SharpRamseyFive.ScoreGeometry.baseDecoded_large line 115
  15. lemma OAI.SharpRamseyFive.ScoreGeometry.base_cost_scalar line 123