OAI/Combinatorics/RamseyFive/Entropy/ScoreFiniteCost.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.ScoreGeometry.scoreFiniteCost line 13
2. lemma OAI.SharpRamseyFive.ScoreGeometry.scoreFinite_header line 18
3. lemma OAI.SharpRamseyFive.ScoreGeometry.scoreFinite_sound line 27
4. lemma OAI.SharpRamseyFive.ScoreGeometry.scoreFinite_cost_of_header line 38
5. abbrev OAI.SharpRamseyFive.FiniteEntropy.BranchMessage line 56
6. def OAI.SharpRamseyFive.FiniteEntropy.branchDecoded line 57
7. def OAI.SharpRamseyFive.FiniteEntropy.branchEncoded line 59
8. theorem OAI.SharpRamseyFive.FiniteEntropy.branch_output_law line 63
9. lemma OAI.SharpRamseyFive.FiniteEntropy.branch_header line 72
10. lemma OAI.SharpRamseyFive.FiniteEntropy.branch_sent line 79