OAI/Combinatorics/SharpRamsey/Execution/ExecutedSecondTrim.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.FreshExecution.rightPath line 13
2. lemma OAI.SharpLogRamsey.FreshExecution.rightPath_subset line 18
3. lemma OAI.SharpLogRamsey.FreshExecution.rightPath_card line 28
4. def OAI.SharpLogRamsey.FreshExecution.secondLoss line 39
5. lemma OAI.SharpLogRamsey.FreshExecution.secondLoss_nonneg line 47
6. theorem OAI.SharpLogRamsey.FreshExecution.reached_second_loss line 53
7. theorem OAI.SharpLogRamsey.FreshExecution.expected_second_path_loss line 128
8. def OAI.SharpLogRamsey.FreshExecution.secondTrim line 147
9. theorem OAI.SharpLogRamsey.FreshExecution.reached_second_trim_charge line 154
10. theorem OAI.SharpLogRamsey.FreshExecution.expected_second_trim line 178