OAI/Combinatorics/MatchingCount/Algorithm/OnlineCoolingSchedule.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.OnlineSchedule.fuelRealizer line 12
  2. lemma OAI.MatchingFPRAS.OnlineSchedule.fuel_numeric_work line 14
  3. lemma OAI.MatchingFPRAS.OnlineSchedule.work_fuelAfter line 16
  4. abbrev OAI.MatchingFPRAS.OnlineSchedule.CoolingInput line 20
  5. def OAI.MatchingFPRAS.OnlineSchedule.scheduleBound line 21
  6. def OAI.MatchingFPRAS.OnlineSchedule.scheduleBoundRealizer line 22
  7. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_scheduleBound line 25
  8. lemma OAI.MatchingFPRAS.OnlineSchedule.scheduleBound_repr line 31
  9. abbrev OAI.MatchingFPRAS.OnlineSchedule.CoolingPowerInput line 36
  10. def OAI.MatchingFPRAS.OnlineSchedule.coolingPowerPlan line 37
  11. def OAI.MatchingFPRAS.OnlineSchedule.coolingPowerPlanRealizer line 40
  12. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_coolingPowerPlan line 46
  13. lemma OAI.MatchingFPRAS.OnlineSchedule.coolingPowerPlan_repr line 54
  14. def OAI.MatchingFPRAS.OnlineSchedule.coolingSearchInput line 64
  15. def OAI.MatchingFPRAS.OnlineSchedule.coolingSearchInputRealizer line 66
  16. def OAI.MatchingFPRAS.OnlineSchedule.coolingSchedule line 69
  17. def OAI.MatchingFPRAS.OnlineSchedule.coolingScheduleRealizer line 70
  18. def OAI.MatchingFPRAS.OnlineSchedule.coolingMeasure line 72
  19. lemma OAI.MatchingFPRAS.OnlineSchedule.weight_le_coolingMeasure line 73
  20. lemma OAI.MatchingFPRAS.OnlineSchedule.work_coolingSearchInput line 74
  21. lemma OAI.MatchingFPRAS.OnlineSchedule.work_coolingSchedule line 97
  22. lemma OAI.MatchingFPRAS.OnlineSchedule.schedule_power_iff line 100
  23. lemma OAI.MatchingFPRAS.OnlineSchedule.coolingSchedule_eq line 121