OAI/Combinatorics/MatchingCount/Algorithm/OnlinePowerSearch.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MatchingFPRAS.OnlineSchedule.PowerSearchInput line 11
2. def OAI.MatchingFPRAS.OnlineSchedule.powerCandidate line 13
3. def OAI.MatchingFPRAS.OnlineSchedule.powerCandidateRealizer line 15
4. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_powerCandidate line 19
5. def OAI.MatchingFPRAS.OnlineSchedule.findPower line 29
6. def OAI.MatchingFPRAS.OnlineSchedule.findPowerRealizer line 31
7. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_findPower line 36
8. lemma OAI.MatchingFPRAS.OnlineSchedule.powerCandidate_repr line 53
9. lemma OAI.MatchingFPRAS.OnlineSchedule.findPower_le_fuel line 62
10. lemma OAI.MatchingFPRAS.OnlineSchedule.findPower_le line 64
11. lemma OAI.MatchingFPRAS.OnlineSchedule.le_findPower line 70
12. lemma OAI.MatchingFPRAS.OnlineSchedule.findPower_eq line 79
13. lemma OAI.MatchingFPRAS.OnlineSchedule.endpoint_le_bound line 85
14. lemma OAI.MatchingFPRAS.OnlineSchedule.endpoint_power_spec line 89
15. lemma OAI.MatchingFPRAS.OnlineSchedule.endpoint_power_min line 94
16. lemma OAI.MatchingFPRAS.OnlineSchedule.findPower_endpoint line 101