OAI/Computability/PerfectCompleteness/Sampling/BucketSampler.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.BucketSampler.F2 line 15
  2. abbrev OAI.PerfectCompleteness.BucketSampler.Direction line 17
  3. abbrev OAI.PerfectCompleteness.BucketSampler.Tape line 19
  4. def OAI.PerfectCompleteness.BucketSampler.rankOne line 23
  5. def OAI.PerfectCompleteness.BucketSampler.evaluate line 26
  6. theorem OAI.PerfectCompleteness.BucketSampler.evaluate_eq_sum line 29
  7. theorem OAI.PerfectCompleteness.BucketSampler.evaluate_update line 34
  8. theorem OAI.PerfectCompleteness.BucketSampler.linearMap_evaluate line 53
  9. theorem OAI.PerfectCompleteness.BucketSampler.evaluate_apply line 58
  10. instance OAI.PerfectCompleteness.BucketSampler.directionZero_isEmpty line 64
  11. theorem OAI.PerfectCompleteness.BucketSampler.evaluate_zero_width line 67
  12. def OAI.PerfectCompleteness.BucketSampler.tapeLaw line 76
  13. theorem OAI.PerfectCompleteness.BucketSampler.tapeLaw_weight line 79
  14. theorem OAI.PerfectCompleteness.BucketSampler.tapeLaw_marginal line 82
  15. theorem OAI.PerfectCompleteness.BucketSampler.expectation_product line 86
  16. theorem OAI.PerfectCompleteness.BucketSampler.expectation_bucket_mul line 93
  17. theorem OAI.PerfectCompleteness.BucketSampler.tapeLaw_zero_width_weight line 100
  18. theorem OAI.PerfectCompleteness.BucketSampler.bucket_marginal line 107
  19. def OAI.PerfectCompleteness.BucketSampler.law line 121
  20. theorem OAI.PerfectCompleteness.BucketSampler.probability_law line 125
  21. abbrev OAI.PerfectCompleteness.BucketSampler.FreshTape line 137
  22. def OAI.PerfectCompleteness.BucketSampler.freshTapeLaw line 139
  23. theorem OAI.PerfectCompleteness.BucketSampler.freshTapeLaw_marginal line 143
  24. theorem OAI.PerfectCompleteness.BucketSampler.freshArrays_expectation_product line 147
  25. abbrev OAI.PerfectCompleteness.BucketSampler.RecursiveTape line 163
  26. def OAI.PerfectCompleteness.BucketSampler.recursiveEvaluate line 167
  27. def OAI.PerfectCompleteness.BucketSampler.recursiveTapeLaw line 172
  28. theorem OAI.PerfectCompleteness.BucketSampler.recursiveTapeLaw_marginal line 177
  29. theorem OAI.PerfectCompleteness.BucketSampler.recursiveBucket_marginal line 184
  30. theorem OAI.PerfectCompleteness.BucketSampler.recursiveEvaluate_apply line 193