OAI/Combinatorics/MatchingCount/Algorithm/OnlineScheduleNat.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeTyped.Realizer.addNat line 9
  2. def OAI.MatchingFPRAS.TreeTyped.Realizer.mulNat line 11
  3. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_addNat line 13
  4. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_mulNat line 16
  5. def OAI.MatchingFPRAS.TreeTyped.fixedPower line 20
  6. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_fixedPower line 23
  7. lemma OAI.MatchingFPRAS.TreeTyped.clog_two_size_pred line 27
  8. def OAI.MatchingFPRAS.TreeTyped.clogTwo line 36
  9. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_clogTwo line 38
  10. def OAI.MatchingFPRAS.OnlineSchedule.lRealizer line 45
  11. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_l line 47
  12. def OAI.MatchingFPRAS.OnlineSchedule.qRealizer line 52
  13. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_q line 54
  14. abbrev OAI.MatchingFPRAS.OnlineSchedule.ScanInput line 57
  15. def OAI.MatchingFPRAS.OnlineSchedule.mRealizer line 59
  16. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_m line 62
  17. def OAI.MatchingFPRAS.OnlineSchedule.lambdaRealizer line 68
  18. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_lambda line 73
  19. def OAI.MatchingFPRAS.OnlineSchedule.scansRealizer line 88
  20. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_scans line 93