OAI/Combinatorics/RamseyFive/Entropy/BaseFiniteCost.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.ScoreGeometry.baseFiniteCost line 15
2. lemma OAI.SharpRamseyFive.ScoreGeometry.baseFinite_sound line 19
3. theorem OAI.SharpRamseyFive.ScoreGeometry.baseFinite_cost line 29
4. def OAI.SharpRamseyFive.ScoreGeometry.reversedBaseCost line 48
5. lemma OAI.SharpRamseyFive.ScoreGeometry.reversedBase_prefixes line 54
6. theorem OAI.SharpRamseyFive.ScoreGeometry.reversedBase_cost line 72
7. def OAI.SharpRamseyFive.ScoreGeometry.twoPublicCost line 120
8. theorem OAI.SharpRamseyFive.ScoreGeometry.twoPublic_cost line 126