OAI/Combinatorics/RamseyFive/Decoding/ReverseCap.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.ReverseCap.neighbors line 11
2. def OAI.SharpRamseyFive.ReverseCap.cap line 14
3. lemma OAI.SharpRamseyFive.ReverseCap.expected_filter_card line 17
4. lemma OAI.SharpRamseyFive.ReverseCap.uniform_neighbor_mass line 29
5. theorem OAI.SharpRamseyFive.ReverseCap.expected_cap_card line 37
6. lemma OAI.SharpRamseyFive.ReverseCap.sum_hits line 66
7. theorem OAI.SharpRamseyFive.ReverseCap.deterministic_capture line 74
8. lemma OAI.SharpRamseyFive.FiniteEntropy.eventMass_filter_partition line 120
9. lemma OAI.SharpRamseyFive.FiniteEntropy.uniform_row_source line 129
10. lemma OAI.SharpRamseyFive.FiniteEntropy.markov_success line 142
11. lemma OAI.SharpRamseyFive.FiniteEntropy.firstAccepted_mem line 154
12. lemma OAI.SharpRamseyFive.FiniteEntropy.finite_table_failure line 165
13. theorem OAI.SharpRamseyFive.FiniteEntropy.uniform_table_failure line 176
14. def OAI.SharpRamseyFive.ReverseCap.successfulRows line 204
15. lemma OAI.SharpRamseyFive.ReverseCap.successfulRows_mass line 208