OAI/Combinatorics/MatchingCount/Algorithm/OnlineSampleCount.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.OnlineSchedule.SigmaInput line 12
  2. def OAI.MatchingFPRAS.OnlineSchedule.sigma line 14
  3. def OAI.MatchingFPRAS.OnlineSchedule.sigmaRealizer line 17
  4. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_sigma line 21
  5. lemma OAI.MatchingFPRAS.OnlineSchedule.sigma_repr line 27
  6. abbrev OAI.MatchingFPRAS.OnlineSchedule.SampleCountInput line 37
  7. def OAI.MatchingFPRAS.OnlineSchedule.invSigma line 39
  8. def OAI.MatchingFPRAS.OnlineSchedule.reciprocalSigma line 40
  9. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_reciprocalSigma line 43
  10. def OAI.MatchingFPRAS.OnlineSchedule.fracProduct line 47
  11. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_fracProduct line 49
  12. def OAI.MatchingFPRAS.OnlineSchedule.sampleFactorFn line 53
  13. def OAI.MatchingFPRAS.OnlineSchedule.sampleFactor line 54
  14. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_sampleFactor line 55
  15. def OAI.MatchingFPRAS.OnlineSchedule.sampleSumFn line 58
  16. def OAI.MatchingFPRAS.OnlineSchedule.sampleSum line 59
  17. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_sampleSum line 61
  18. def OAI.MatchingFPRAS.OnlineSchedule.sampleProduct line 65
  19. def OAI.MatchingFPRAS.OnlineSchedule.sampleProductRealizer line 66
  20. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_sampleProduct line 67
  21. def OAI.MatchingFPRAS.OnlineSchedule.sampleCount line 70
  22. def OAI.MatchingFPRAS.OnlineSchedule.sampleCountRealizer line 71
  23. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_sampleCount line 73
  24. lemma OAI.MatchingFPRAS.OnlineSchedule.sampleCount_repr line 75
  25. lemma OAI.MatchingFPRAS.OnlineSchedule.sampleCount_source line 90
  26. def OAI.MatchingFPRAS.OnlineSchedule.repetitions line 95
  27. def OAI.MatchingFPRAS.OnlineSchedule.repetitionsRealizer line 96
  28. lemma OAI.MatchingFPRAS.OnlineSchedule.polynomial_repetitions line 98
  29. lemma OAI.MatchingFPRAS.OnlineSchedule.repetitions_repr line 105