OAI/Combinatorics/RamseyFive/Entropy/RetainedCounters.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.MessageWeights.CountedMessage line 12
2. instance OAI.SharpRamseyFive.MessageWeights.(instance at line 13) line 13
3. def OAI.SharpRamseyFive.MessageWeights.countedCost line 15
4. lemma OAI.SharpRamseyFive.MessageWeights.count_slots_weight line 17
5. lemma OAI.SharpRamseyFive.MessageWeights.counted_weight line 22
6. lemma OAI.SharpRamseyFive.MessageWeights.counted_entropy_bound line 28
7. theorem OAI.SharpRamseyFive.ProjectiveIncidence.eventually_actual_counted_context_entropy line 44