OAI/Combinatorics/SharpRamsey/Marking/MarkingMessage.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLogRamsey.Selection.entropy_cond_tuple_domains line 13
  2. lemma OAI.SharpLogRamsey.Selection.entropy_context_bound line 28
  3. lemma OAI.SharpLogRamsey.Selection.entropy_adjoin_mask line 44
  4. def OAI.SharpLogRamsey.Selection.maskedValues line 57
  5. def OAI.SharpLogRamsey.Selection.maskedDomains line 60
  6. lemma OAI.SharpLogRamsey.Selection.maskedValues_mem line 64
  7. lemma OAI.SharpLogRamsey.Selection.maskedDomains_log_card line 72
  8. def OAI.SharpLogRamsey.Selection.markingMessage line 87
  9. theorem OAI.SharpLogRamsey.Selection.marking_message_entropy line 91
  10. def OAI.SharpLogRamsey.Selection.markingDecodedDomains line 131
  11. lemma OAI.SharpLogRamsey.Selection.markingDecodedDomains_mem line 137
  12. lemma OAI.SharpLogRamsey.Selection.markingDecodedDomains_entropy line 150
  13. theorem OAI.SharpLogRamsey.Selection.marking_entropy_upper line 170