OAI/Combinatorics/RamseyFive/Entropy/PermissibleLevels.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.FiniteEntropy.levelLoss line 12
2. def OAI.SharpRamseyFive.FiniteEntropy.levelBadMass line 14
3. def OAI.SharpRamseyFive.FiniteEntropy.permissibleLevels line 16
4. lemma OAI.SharpRamseyFive.FiniteEntropy.levelBadMass_nonneg line 20
5. lemma OAI.SharpRamseyFive.FiniteEntropy.sum_levelBadMass line 23
6. lemma OAI.SharpRamseyFive.FiniteEntropy.levelLoss_nonneg line 44
7. lemma OAI.SharpRamseyFive.FiniteEntropy.thin_level_mass line 53
8. theorem OAI.SharpRamseyFive.FiniteEntropy.permissible_mass line 73
9. lemma OAI.SharpRamseyFive.FiniteEntropy.positive_map_exists line 119
10. lemma OAI.SharpRamseyFive.FiniteEntropy.permissible_support_size line 130
11. def OAI.SharpRamseyFive.FiniteEntropy.goodSupportLaw line 150
12. theorem OAI.SharpRamseyFive.FiniteEntropy.goodSupportLaw_bounds line 155
13. theorem OAI.SharpRamseyFive.FiniteEntropy.goodSupportLaw_domination line 168
14. lemma OAI.SharpRamseyFive.FiniteEntropy.permissible_half_mass line 177