OAI/Combinatorics/RamseyFive/Entropy/ClippedWeight.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.ScoreRegularity.clippedWeight line 16
2. lemma OAI.SharpRamseyFive.ScoreRegularity.clippedWeight_bounds line 22
3. lemma OAI.SharpRamseyFive.ScoreRegularity.clippedWeight_sum_bound line 29
4. lemma OAI.SharpRamseyFive.ScoreRegularity.mean_ratio_le line 46
5. def OAI.SharpRamseyFive.ScoreRegularity.irregular line 55
6. theorem OAI.SharpRamseyFive.ScoreRegularity.irregular_card_bound line 60