OAI/Combinatorics/SharpRamsey/Execution/ExecutedTrim.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.FreshExecution.leftPath line 13
2. lemma OAI.SharpLogRamsey.FreshExecution.leftPath_subset line 18
3. lemma OAI.SharpLogRamsey.FreshExecution.leftPath_card line 28
4. def OAI.SharpLogRamsey.FreshExecution.firstLoss line 39
5. lemma OAI.SharpLogRamsey.FreshExecution.firstLoss_nonneg line 47
6. lemma OAI.SharpLogRamsey.FreshExecution.sdiff_inter_card line 53
7. theorem OAI.SharpLogRamsey.FreshExecution.reached_first_loss line 59
8. theorem OAI.SharpLogRamsey.FreshExecution.expected_first_path_loss line 135
9. def OAI.SharpLogRamsey.FreshExecution.firstTrim line 154
10. lemma OAI.SharpLogRamsey.FreshExecution.produced_nonneg line 162
11. theorem OAI.SharpLogRamsey.FreshExecution.reached_first_trim_charge line 174
12. theorem OAI.SharpLogRamsey.FreshExecution.expected_first_trim line 198