OAI/Combinatorics/MatchingCount/Algorithm/OnlineInitial.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.OnlineInitial.Seed line 11
  2. abbrev OAI.MatchingFPRAS.OnlineInitial.Config line 12
  3. def OAI.MatchingFPRAS.OnlineInitial.seedK line 14
  4. def OAI.MatchingFPRAS.OnlineInitial.seedKRealizer line 15
  5. def OAI.MatchingFPRAS.OnlineInitial.seedN line 17
  6. def OAI.MatchingFPRAS.OnlineInitial.seedNRealizer line 18
  7. def OAI.MatchingFPRAS.OnlineInitial.seedD line 20
  8. def OAI.MatchingFPRAS.OnlineInitial.seedDRealizer line 22
  9. def OAI.MatchingFPRAS.OnlineInitial.config line 24
  10. def OAI.MatchingFPRAS.OnlineInitial.configRealizer line 25
  11. def OAI.MatchingFPRAS.OnlineInitial.root line 27
  12. def OAI.MatchingFPRAS.OnlineInitial.rootRealizer line 28
  13. lemma OAI.MatchingFPRAS.OnlineInitial.root_eq line 30
  14. def OAI.MatchingFPRAS.OnlineInitial.initialScale line 33
  15. def OAI.MatchingFPRAS.OnlineInitial.initialScaleRealizer line 34
  16. lemma OAI.MatchingFPRAS.OnlineInitial.initialScale_repr line 36
  17. def OAI.MatchingFPRAS.OnlineInitial.scaleVector line 41
  18. def OAI.MatchingFPRAS.OnlineInitial.scaleVectorRealizer line 42
  19. lemma OAI.MatchingFPRAS.OnlineInitial.scaleVector_source line 45
  20. def OAI.MatchingFPRAS.OnlineInitial.nRealizer line 54
  21. def OAI.MatchingFPRAS.OnlineInitial.count line 56
  22. def OAI.MatchingFPRAS.OnlineInitial.countRealizer line 57
  23. def OAI.MatchingFPRAS.OnlineInitial.data line 60
  24. def OAI.MatchingFPRAS.OnlineInitial.dataRealizer line 64
  25. def OAI.MatchingFPRAS.OnlineInitial.trialInput line 72
  26. def OAI.MatchingFPRAS.OnlineInitial.trialInputRealizer line 74
  27. def OAI.MatchingFPRAS.OnlineInitial.runInput line 77
  28. def OAI.MatchingFPRAS.OnlineInitial.runInputRealizer line 79
  29. def OAI.MatchingFPRAS.OnlineInitial.initializeInput line 82
  30. def OAI.MatchingFPRAS.OnlineInitial.initializeInputRealizer line 83