OAI/Combinatorics/RamseyFive/Entropy/FreshPublicFamily.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.FiniteEntropy.exists_accepted_index line 10
  2. def OAI.SharpRamseyFive.FiniteEntropy.acceptedIndex line 18
  3. lemma OAI.SharpRamseyFive.FiniteEntropy.acceptedIndex_decode line 20
  4. def OAI.SharpRamseyFive.ReverseCap.cardCutoff line 30
  5. abbrev OAI.SharpRamseyFive.ReverseCap.FreshTape line 33
  6. def OAI.SharpRamseyFive.ReverseCap.freshTapeLaw line 36
  7. abbrev OAI.SharpRamseyFive.ReverseCap.FreshMessage line 40
  8. def OAI.SharpRamseyFive.ReverseCap.freshDecoded line 43
  9. def OAI.SharpRamseyFive.ReverseCap.freshEncoded line 47
  10. lemma OAI.SharpRamseyFive.ReverseCap.freshEncoded_decoded line 53
  11. theorem OAI.SharpRamseyFive.ReverseCap.fresh_public_law line 64
  12. theorem OAI.SharpRamseyFive.ReverseCap.fresh_payload_cost line 86