OAI/Combinatorics/MatchingCount/Algorithm/OnlineLadderSchedule.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.OnlineSchedule.LadderInput line 10
  2. def OAI.MatchingFPRAS.OnlineSchedule.vertexNumber line 12
  3. def OAI.MatchingFPRAS.OnlineSchedule.vertexNumberRealizer line 14
  4. lemma OAI.MatchingFPRAS.OnlineSchedule.vertexNumber_eq line 17
  5. lemma OAI.MatchingFPRAS.OnlineSchedule.vertexNumber_bound line 20
  6. def OAI.MatchingFPRAS.OnlineSchedule.distortion line 30
  7. def OAI.MatchingFPRAS.OnlineSchedule.distortionRealizer line 31
  8. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_distortion line 34
  9. lemma OAI.MatchingFPRAS.OnlineSchedule.distortion_source line 40
  10. def OAI.MatchingFPRAS.OnlineSchedule.tierBoundRealizer line 44
  11. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_tierBound line 47
  12. def OAI.MatchingFPRAS.OnlineSchedule.ladderPowerPlan line 54
  13. def OAI.MatchingFPRAS.OnlineSchedule.ladderPowerPlanRealizer line 57
  14. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_ladderPowerPlan line 62
  15. lemma OAI.MatchingFPRAS.OnlineSchedule.ladderPowerPlan_repr line 72
  16. def OAI.MatchingFPRAS.OnlineSchedule.ladderSearchInput line 85
  17. def OAI.MatchingFPRAS.OnlineSchedule.ladderSearchInputRealizer line 87
  18. def OAI.MatchingFPRAS.OnlineSchedule.ladderSchedule line 90
  19. def OAI.MatchingFPRAS.OnlineSchedule.ladderScheduleRealizer line 91
  20. lemma OAI.MatchingFPRAS.OnlineSchedule.ladderSchedule_eq line 92