OAI/Combinatorics/RamseyFive/Entropy/CountedExtraction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.FiniteEntropy.RunAssignment line 14
2. instance OAI.SharpRamseyFive.FiniteEntropy.(instance at line 15) line 15
3. def OAI.SharpRamseyFive.FiniteEntropy.runCutoff line 17
4. lemma OAI.SharpRamseyFive.FiniteEntropy.le_iff_lt_runCutoff line 23
5. lemma OAI.SharpRamseyFive.FiniteEntropy.runCutoff_injective line 44
6. lemma OAI.SharpRamseyFive.FiniteEntropy.runAssignment_card line 56
7. lemma OAI.SharpRamseyFive.FiniteEntropy.runAssignment_entropy line 62
8. theorem OAI.SharpRamseyFive.FiniteEntropy.slot_context_entropy line 75
9. def OAI.SharpRamseyFive.FiniteEntropy.retainedAssignment line 106
10. theorem OAI.SharpRamseyFive.FiniteEntropy.counted_extracted_entropy line 110
11. theorem OAI.SharpRamseyFive.FiniteEntropy.counted_extracted_entropy_on_support line 144
12. lemma OAI.SharpRamseyFive.FiniteEntropy.independent_event_average line 173
13. theorem OAI.SharpRamseyFive.FiniteEntropy.fixed_table_extraction line 186