OAI/Combinatorics/RamseyFive/Marking/TwoScanContext.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpRamseyFive.Marking.marking_posterior_domains line 22
2. lemma OAI.SharpRamseyFive.Marking.marking_posterior_cap line 35
3. lemma OAI.SharpRamseyFive.Marking.marking_deficit_nonneg line 53
4. theorem OAI.SharpRamseyFive.Marking.marking_expected_deficit line 72
5. def OAI.SharpRamseyFive.Marking.expensiveBound line 111
6. lemma OAI.SharpRamseyFive.Marking.positive_marked_context line 117
7. lemma OAI.SharpRamseyFive.Marking.marked_cheap_count line 125
8. def OAI.SharpRamseyFive.Marking.markedCode line 139
9. theorem OAI.SharpRamseyFive.Marking.marking_fixed_class line 142
10. def OAI.SharpRamseyFive.Marking.markedClassLaw line 159
11. lemma OAI.SharpRamseyFive.Marking.markedClassLaw_deficit line 168