OAI/Combinatorics/MatchingCount/Sampling/OnlineSample.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.OnlineSample.word line 11
  2. def OAI.MatchingFPRAS.OnlineSample.repeatInputRealizer line 14
  3. def OAI.MatchingFPRAS.OnlineSample.words line 18
  4. def OAI.MatchingFPRAS.OnlineSample.wordsRealizer line 20
  5. def OAI.MatchingFPRAS.OnlineSample.localWords line 25
  6. def OAI.MatchingFPRAS.OnlineSample.localRealizer line 27
  7. def OAI.MatchingFPRAS.OnlineSample.scan line 31
  8. def OAI.MatchingFPRAS.OnlineSample.scanRealizer line 33
  9. def OAI.MatchingFPRAS.OnlineSample.scans line 37
  10. def OAI.MatchingFPRAS.OnlineSample.scansRealizer line 39
  11. def OAI.MatchingFPRAS.OnlineSample.markWord line 44
  12. def OAI.MatchingFPRAS.OnlineSample.markWordRealizer line 45
  13. def OAI.MatchingFPRAS.OnlineSample.markRequests line 48
  14. def OAI.MatchingFPRAS.OnlineSample.markRequestsRealizer line 49
  15. def OAI.MatchingFPRAS.OnlineSample.marks line 51
  16. def OAI.MatchingFPRAS.OnlineSample.marksRealizer line 53
  17. abbrev OAI.MatchingFPRAS.OnlineSample.Request line 56
  18. def OAI.MatchingFPRAS.OnlineSample.sample line 57
  19. def OAI.MatchingFPRAS.OnlineSample.sampleRealizer line 59
  20. def OAI.MatchingFPRAS.OnlineSample.many line 62
  21. def OAI.MatchingFPRAS.OnlineSample.manyRealizer line 64