OAI/Combinatorics/RamseyFive/Marking/WindowDeletionCount.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.Windows.goodWindowSet line 15
2. def OAI.SharpRamseyFive.Windows.survivingWindowSet line 17
3. lemma OAI.SharpRamseyFive.Windows.mem_goodWindowSet line 20
4. lemma OAI.SharpRamseyFive.Windows.mem_survivingWindowSet line 23
5. theorem OAI.SharpRamseyFive.Windows.ineligible_middle_count line 29
6. theorem OAI.SharpRamseyFive.Windows.reciprocal_loss_aggregate line 61
7. def OAI.SharpRamseyFive.Marking.allWindowLevelLaw line 102
8. def OAI.SharpRamseyFive.Marking.allWindowEncoded line 105
9. def OAI.SharpRamseyFive.Marking.allWindowExperiment line 111
10. def OAI.SharpRamseyFive.Marking.allWindowFailure line 115
11. lemma OAI.SharpRamseyFive.Marking.allWindowFailure_nonempty line 122
12. def OAI.SharpRamseyFive.Marking.allWindowPositions line 128
13. theorem OAI.SharpRamseyFive.Marking.allWindow_loss line 136