OAI/Computability/PerfectCompleteness/Decoding/BucketUsefulCollision.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.BucketUsefulCollision.fill line 22
  2. theorem OAI.PerfectCompleteness.BucketUsefulCollision.fill_self line 27
  3. theorem OAI.PerfectCompleteness.BucketUsefulCollision.fill_update line 32
  4. theorem OAI.PerfectCompleteness.BucketUsefulCollision.fill_others line 41
  5. theorem OAI.PerfectCompleteness.BucketUsefulCollision.fill_others_update line 49
  6. theorem OAI.PerfectCompleteness.BucketUsefulCollision.probability_eq_expectation line 53
  7. theorem OAI.PerfectCompleteness.BucketUsefulCollision.probability_background_first line 61
  8. theorem OAI.PerfectCompleteness.BucketUsefulCollision.probability_resampling line 71
  9. theorem OAI.PerfectCompleteness.BucketUsefulCollision.assembledMatrix_fill line 92
  10. theorem OAI.PerfectCompleteness.BucketUsefulCollision.collision_probability_lower_bound line 103