OAI/Combinatorics/MatchingCount/Complexity/OnlineRequestCost.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.NumericBounds.Bound line 11
2. lemma OAI.MatchingFPRAS.NumericBounds.self line 12
3. lemma OAI.MatchingFPRAS.NumericBounds.of_le line 13
4. lemma OAI.MatchingFPRAS.NumericBounds.const line 14
5. lemma OAI.MatchingFPRAS.NumericBounds.mono line 15
6. lemma OAI.MatchingFPRAS.NumericBounds.add line 17
7. lemma OAI.MatchingFPRAS.NumericBounds.mul line 20
8. lemma OAI.MatchingFPRAS.NumericBounds.pow line 23
9. lemma OAI.MatchingFPRAS.NumericBounds.clog_le line 26
10. lemma OAI.MatchingFPRAS.NumericBounds.clog line 29
11. lemma OAI.MatchingFPRAS.NumericBounds.comp line 31
12. lemma OAI.MatchingFPRAS.NumericBounds.weight line 35
13. lemma OAI.MatchingFPRAS.NumericBounds.length line 39
14. def OAI.MatchingFPRAS.OnlineSchedule.precisionNorm line 47
15. lemma OAI.MatchingFPRAS.OnlineSchedule.bound_plan line 49
16. def OAI.MatchingFPRAS.OnlineSchedule.requestSize line 74
17. lemma OAI.MatchingFPRAS.OnlineSchedule.weight_le_requestSize line 75
18. lemma OAI.MatchingFPRAS.OnlineSchedule.bound_precision line 76
19. lemma OAI.MatchingFPRAS.OnlineSchedule.bound_sourceRequest line 110