OAI/Combinatorics/MatchingCount/Algorithm/OnlineRequest.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.OnlineSchedule.lengthAfter line 16
  2. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_lengthAfter line 18
  3. def OAI.MatchingFPRAS.OnlineSchedule.rangeAfter line 22
  4. def OAI.MatchingFPRAS.OnlineSchedule.listIndices line 25
  5. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_listIndices line 27
  6. def OAI.MatchingFPRAS.OnlineSchedule.indicesAfter line 30
  7. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_indicesAfter line 32
  8. abbrev OAI.MatchingFPRAS.OnlineSchedule.PrecisionData line 36
  9. def OAI.MatchingFPRAS.OnlineSchedule.scanError line 38
  10. def OAI.MatchingFPRAS.OnlineSchedule.scanErrorRealizer line 42
  11. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_scanError line 49
  12. def OAI.MatchingFPRAS.OnlineSchedule.precisionPlan line 58
  13. def OAI.MatchingFPRAS.OnlineSchedule.precisionPlanRealizer line 62
  14. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_precisionPlan line 67
  15. abbrev OAI.MatchingFPRAS.OnlineSchedule.RequestInput line 77
  16. def OAI.MatchingFPRAS.OnlineSchedule.sourcePrecision line 79
  17. def OAI.MatchingFPRAS.OnlineSchedule.requestBagRealizer line 84
  18. def OAI.MatchingFPRAS.OnlineSchedule.requestKRealizer line 86
  19. def OAI.MatchingFPRAS.OnlineSchedule.requestNDRealizer line 88
  20. def OAI.MatchingFPRAS.OnlineSchedule.requestKTRealizer line 90
  21. def OAI.MatchingFPRAS.OnlineSchedule.requestMRealizer line 92
  22. def OAI.MatchingFPRAS.OnlineSchedule.requestScanRealizer line 94
  23. def OAI.MatchingFPRAS.OnlineSchedule.requestTablesRealizer line 98
  24. def OAI.MatchingFPRAS.OnlineSchedule.requestCatalogRealizer line 101
  25. def OAI.MatchingFPRAS.OnlineSchedule.requestEdgesRealizer line 103
  26. def OAI.MatchingFPRAS.OnlineSchedule.requestLabelsRealizer line 105
  27. def OAI.MatchingFPRAS.OnlineSchedule.sourcePrecisionRealizer line 107
  28. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_requestBag line 109
  29. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_requestK line 111
  30. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_requestND line 116
  31. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_requestKT line 122
  32. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_requestM line 127
  33. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_requestScan line 129
  34. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_requestTables line 131
  35. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_requestCatalog line 133
  36. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_requestEdges line 135
  37. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_requestLabels line 137
  38. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_sourcePrecision line 140
  39. def OAI.MatchingFPRAS.OnlineSchedule.sourceRequest line 143
  40. def OAI.MatchingFPRAS.OnlineSchedule.requestPlanRealizer line 146
  41. def OAI.MatchingFPRAS.OnlineSchedule.requestIndicesRealizer line 148
  42. def OAI.MatchingFPRAS.OnlineSchedule.sourceRequestRealizer line 150
  43. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_requestPlan line 152
  44. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_requestIndices line 154
  45. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_sourceRequest line 156
  46. lemma OAI.MatchingFPRAS.OnlineSchedule.sparseBagInput_source line 160
  47. lemma OAI.MatchingFPRAS.OnlineSchedule.sourcePrecision_source line 167