OAI/Combinatorics/RamseyFive/Entropy/SequentialLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.FiniteEntropy.adaptiveLaw line 12
2. lemma OAI.SharpRamseyFive.FiniteEntropy.adaptiveLaw_first line 19
3. lemma OAI.SharpRamseyFive.FiniteEntropy.map_positive line 26
4. def OAI.SharpRamseyFive.FiniteEntropy.pureLaw line 38
5. theorem OAI.SharpRamseyFive.FiniteEntropy.adaptive_option_failure line 43
6. def OAI.SharpRamseyFive.FiniteEntropy.finiteImageLaw line 82
7. lemma OAI.SharpRamseyFive.FiniteEntropy.finiteImageLaw_positive line 97
8. lemma OAI.SharpRamseyFive.FiniteEntropy.finiteImageLaw_event line 102
9. def OAI.SharpRamseyFive.FiniteEntropy.chooseMessage line 115
10. lemma OAI.SharpRamseyFive.FiniteEntropy.chooseMessage_none line 119
11. lemma OAI.SharpRamseyFive.FiniteEntropy.chooseMessage_sound line 125
12. theorem OAI.SharpRamseyFive.FiniteEntropy.selectedMessage_failure line 132