OAI/Combinatorics/RamseyFive/Entropy/PreRoundDeletion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.FiniteEntropy.preRoundBad line 18
2. theorem OAI.SharpRamseyFive.FiniteEntropy.preRound_bad_budget line 24
3. theorem OAI.SharpRamseyFive.FiniteEntropy.preRound_selected_bad line 63
4. lemma OAI.SharpRamseyFive.FiniteEntropy.badIndexIndicator_zero_or_one line 85
5. theorem OAI.SharpRamseyFive.FiniteEntropy.exists_good_window_pair line 90
6. theorem OAI.SharpRamseyFive.FiniteEntropy.preRound_good_early_middle line 118