OAI/Combinatorics/MatchingCount/Complexity/OnlineStageCost.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingFPRAS.OnlineTree.work_precompose line 11
2. lemma OAI.MatchingFPRAS.OnlineTree.work_from_weight line 16
3. def OAI.MatchingFPRAS.OnlineStage.inputSize line 25
4. lemma OAI.MatchingFPRAS.OnlineStage.work_execute line 26
5. def OAI.MatchingFPRAS.OnlineTrial.stateSize line 42
6. lemma OAI.MatchingFPRAS.OnlineTrial.weight_le_stateSize line 43
7. lemma OAI.MatchingFPRAS.OnlineTrial.bound_prepare line 44
8. lemma OAI.MatchingFPRAS.OnlineTrial.work_step line 50
9. lemma OAI.MatchingFPRAS.OnlineTrial.work_body line 63
10. lemma OAI.MatchingFPRAS.OnlineGuard.bound_testRequest line 74
11. lemma OAI.MatchingFPRAS.OnlineGuard.work_test line 79
12. lemma OAI.MatchingFPRAS.OnlineGuard.work_checked line 90