OAI/Combinatorics/RamseyFive/Entropy/UnionMarking.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.FiniteEntropy.unionRecord line 16
2. abbrev OAI.SharpRamseyFive.FiniteEntropy.RankTypes line 19
3. def OAI.SharpRamseyFive.FiniteEntropy.unionMask line 21
4. lemma OAI.SharpRamseyFive.FiniteEntropy.unionRecord_present line 26
5. theorem OAI.SharpRamseyFive.FiniteEntropy.union_marking_entropy line 36
6. lemma OAI.SharpRamseyFive.FiniteEntropy.unionRecord_decode_left line 62
7. lemma OAI.SharpRamseyFive.FiniteEntropy.unionRecord_decode_right line 68
8. def OAI.SharpRamseyFive.FiniteEntropy.withMessage line 78
9. lemma OAI.SharpRamseyFive.FiniteEntropy.first_withMessage line 81
10. lemma OAI.SharpRamseyFive.FiniteEntropy.second_withMessage line 86
11. lemma OAI.SharpRamseyFive.FiniteEntropy.entropy_withMessage line 91
12. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_withMessage_label line 99
13. lemma OAI.SharpRamseyFive.FiniteEntropy.withMessage_support line 104
14. lemma OAI.SharpRamseyFive.FiniteEntropy.fiber_withMessage_support line 115
15. theorem OAI.SharpRamseyFive.FiniteEntropy.message_deficit_bound line 125