OAI/Combinatorics/SharpRamsey/Marking/MarkingActual.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.Marking.toScan line 16
2. def OAI.SharpLogRamsey.Marking.pairStep line 19
3. def OAI.SharpLogRamsey.Marking.pairReplay line 22
4. def OAI.SharpLogRamsey.Marking.pairCode line 27
5. lemma OAI.SharpLogRamsey.Marking.pairCode_length line 35
6. lemma OAI.SharpLogRamsey.Marking.pairCode_mask_sent line 42
7. lemma OAI.SharpLogRamsey.Marking.pairReplay_eq line 56
8. lemma OAI.SharpLogRamsey.Marking.pairCode_eq line 64
9. lemma OAI.SharpLogRamsey.Marking.pairCode_count line 77
10. lemma OAI.SharpLogRamsey.Marking.pairCode_spec line 88
11. def OAI.SharpLogRamsey.Marking.codeTuple line 127
12. def OAI.SharpLogRamsey.Marking.tupleMask line 131
13. def OAI.SharpLogRamsey.Marking.expensiveMask line 134
14. lemma OAI.SharpLogRamsey.Marking.mem_expensiveMask line 139
15. lemma OAI.SharpLogRamsey.Marking.ofFn_codeTuple line 144
16. lemma OAI.SharpLogRamsey.Marking.expensiveMask_card line 152
17. def OAI.SharpLogRamsey.Marking.cheapTuple line 165
18. lemma OAI.SharpLogRamsey.Marking.tuple_sent_eq line 171
19. lemma OAI.SharpLogRamsey.Marking.cheapTuple_mem line 181
20. lemma OAI.SharpLogRamsey.Marking.cheapTuple_card line 201
21. lemma OAI.SharpLogRamsey.Marking.cheapTuple_log_card line 207
22. theorem OAI.SharpLogRamsey.Marking.actual_entropy_upper line 219
23. lemma OAI.SharpLogRamsey.Marking.expected_expensive_bound line 242