OAI/Combinatorics/MatchingCount/Graphs/AdaptiveStream.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.PhysicalStream.Bits line 9
  2. abbrev OAI.MatchingFPRAS.PhysicalStream.Stream line 10
  3. def OAI.MatchingFPRAS.PhysicalStream.shift line 12
  4. lemma OAI.MatchingFPRAS.PhysicalStream.shift_zero line 13
  5. def OAI.MatchingFPRAS.PhysicalStream.extend line 14
  6. def OAI.MatchingFPRAS.PhysicalStream.concat line 16
  7. def OAI.MatchingFPRAS.PhysicalStream.split line 18
  8. lemma OAI.MatchingFPRAS.PhysicalStream.concat_left line 24
  9. lemma OAI.MatchingFPRAS.PhysicalStream.concat_right line 26
  10. def OAI.MatchingFPRAS.PhysicalStream.average line 29
  11. lemma OAI.MatchingFPRAS.PhysicalStream.average_const line 32
  12. lemma OAI.MatchingFPRAS.PhysicalStream.average_add line 35
  13. lemma OAI.MatchingFPRAS.PhysicalStream.average_mul line 39
  14. lemma OAI.MatchingFPRAS.PhysicalStream.average_split line 43
  15. lemma OAI.MatchingFPRAS.PhysicalStream.average_one line 57
  16. lemma OAI.MatchingFPRAS.PhysicalStream.shift_extend_concat line 66
  17. lemma OAI.MatchingFPRAS.PhysicalStream.extend_concat_zero line 72
  18. inductive OAI.MatchingFPRAS.PhysicalStream.Experiment line 77
  19. def OAI.MatchingFPRAS.PhysicalStream.Experiment.cost line 85
  20. def OAI.MatchingFPRAS.PhysicalStream.Experiment.run line 90
  21. def OAI.MatchingFPRAS.PhysicalStream.Experiment.mean line 95
  22. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.run_cost line 100
  23. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.run_congr line 109
  24. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.run_suffix line 130
  25. theorem OAI.MatchingFPRAS.PhysicalStream.Experiment.average_run line 137
  26. def OAI.MatchingFPRAS.PhysicalStream.Experiment.bind line 165
  27. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.mean_bind line 170
  28. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.run_bind line 177
  29. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.cost_bind_le line 195
  30. def OAI.MatchingFPRAS.PhysicalStream.Experiment.map line 206
  31. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.cost_map line 208
  32. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.run_map line 214
  33. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.mean_map line 217
  34. def OAI.MatchingFPRAS.PhysicalStream.Experiment.word line 220
  35. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.cost_word line 224
  36. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.run_word line 229
  37. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.mean_word line 242
  38. theorem OAI.MatchingFPRAS.PhysicalStream.Experiment.adaptive_word_law line 251