OAI/Combinatorics/MatchingCount/Complexity/OnlineSampleCost.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.OnlineSample.work_repeatInput line 12
  2. def OAI.MatchingFPRAS.OnlineSample.mass line 25
  3. lemma OAI.MatchingFPRAS.OnlineSample.weight_le_mass line 26
  4. lemma OAI.MatchingFPRAS.OnlineSample.mass_mem line 27
  5. lemma OAI.MatchingFPRAS.OnlineSample.weight_replicate line 39
  6. lemma OAI.MatchingFPRAS.OnlineSample.mass_replicate line 43
  7. lemma OAI.MatchingFPRAS.OnlineSample.work_traverse_mass line 47
  8. def OAI.MatchingFPRAS.OnlineSample.repeatMeasure line 52
  9. lemma OAI.MatchingFPRAS.OnlineSample.work_repeat line 53
  10. def OAI.MatchingFPRAS.OnlineSample.pairMeasure line 69
  11. lemma OAI.MatchingFPRAS.OnlineSample.work_firstWord line 70
  12. lemma OAI.MatchingFPRAS.OnlineSample.work_words line 81
  13. lemma OAI.MatchingFPRAS.OnlineSample.work_local line 101
  14. lemma OAI.MatchingFPRAS.OnlineSample.work_scan line 104
  15. def OAI.MatchingFPRAS.OnlineSample.scansMeasure line 108
  16. lemma OAI.MatchingFPRAS.OnlineSample.work_scans line 109
  17. def OAI.MatchingFPRAS.OnlineSample.markMeasure line 131
  18. lemma OAI.MatchingFPRAS.OnlineSample.work_markWord line 132
  19. lemma OAI.MatchingFPRAS.OnlineSample.sum_map_le line 137
  20. lemma OAI.MatchingFPRAS.OnlineSample.mass_le line 146
  21. def OAI.MatchingFPRAS.OnlineSample.marksMeasure line 153
  22. lemma OAI.MatchingFPRAS.OnlineSample.work_marks line 154
  23. def OAI.MatchingFPRAS.OnlineSample.requestMeasure line 178
  24. lemma OAI.MatchingFPRAS.OnlineSample.work_sample line 179
  25. lemma OAI.MatchingFPRAS.OnlineSample.work_many line 194