OAI/Combinatorics/RamseyFive/Entropy/OriginalLevelLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.FiniteEntropy.positiveLaw line 10
2. lemma OAI.SharpRamseyFive.FiniteEntropy.positiveLaw_mean line 25
3. def OAI.SharpRamseyFive.FiniteEntropy.originalLevelLaw line 39
4. lemma OAI.SharpRamseyFive.FiniteEntropy.originalLevelLaw_cross_mean line 43
5. lemma OAI.SharpRamseyFive.FiniteEntropy.originalLevelLaw_cross_domination line 52
6. lemma OAI.SharpRamseyFive.TreeCodec.mean_pathBudget line 69
7. lemma OAI.SharpRamseyFive.TreeCodec.pathBudget_mono line 81
8. lemma OAI.SharpRamseyFive.TreeCodec.pathBudget_const_le_height line 93