OAI/Combinatorics/RamseyFive/Entropy/TreeWeights.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.MessageWeights.prod_weight_le line 11
2. lemma OAI.SharpRamseyFive.MessageWeights.option_bit_weight line 21
3. def OAI.SharpRamseyFive.TreeCodec.slotCost line 39
4. lemma OAI.SharpRamseyFive.TreeCodec.slotCost_weight line 48
5. lemma OAI.SharpRamseyFive.TreeCodec.slotCost_le line 78
6. lemma OAI.SharpRamseyFive.ProjectiveIncidence.finiteNode_weight line 103
7. lemma OAI.SharpRamseyFive.ProjectiveIncidence.orientedNode_weight line 110
8. def OAI.SharpRamseyFive.ProjectiveIncidence.orientedPivotSlotCost line 124
9. lemma OAI.SharpRamseyFive.ProjectiveIncidence.orientedPivotTree_weight line 131
10. lemma OAI.SharpRamseyFive.ProjectiveIncidence.fourPivotTree_weight line 138