OAI/Computability/PerfectCompleteness/Decoding/HierarchicalUsefulCollision.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.HierarchicalUsefulCollision.probability_product line 20
  2. theorem OAI.PerfectCompleteness.HierarchicalUsefulCollision.probability_product_first line 27
  3. abbrev OAI.PerfectCompleteness.HierarchicalUsefulCollision.Background line 41
  4. abbrev OAI.PerfectCompleteness.HierarchicalUsefulCollision.Matrix line 42
  5. abbrev OAI.PerfectCompleteness.HierarchicalUsefulCollision.Direction line 43
  6. abbrev OAI.PerfectCompleteness.HierarchicalUsefulCollision.Tape line 44
  7. def OAI.PerfectCompleteness.HierarchicalUsefulCollision.directionLaw line 56
  8. def OAI.PerfectCompleteness.HierarchicalUsefulCollision.bucketLaw line 62
  9. abbrev OAI.PerfectCompleteness.HierarchicalUsefulCollision.Sample line 70
  10. def OAI.PerfectCompleteness.HierarchicalUsefulCollision.law line 72
  11. def OAI.PerfectCompleteness.HierarchicalUsefulCollision.pairRecord line 78
  12. def OAI.PerfectCompleteness.HierarchicalUsefulCollision.pairLaw line 83
  13. def OAI.PerfectCompleteness.HierarchicalUsefulCollision.usefulAccepted line 95
  14. def OAI.PerfectCompleteness.HierarchicalUsefulCollision.usefulEvent line 107
  15. theorem OAI.PerfectCompleteness.HierarchicalUsefulCollision.direction_collision_lower_bound line 112
  16. theorem OAI.PerfectCompleteness.HierarchicalUsefulCollision.useful_probability_eq line 132
  17. theorem OAI.PerfectCompleteness.HierarchicalUsefulCollision.collision_probability_eq line 152
  18. theorem OAI.PerfectCompleteness.HierarchicalUsefulCollision.collision_probability_lower_bound line 173
  19. theorem OAI.PerfectCompleteness.HierarchicalUsefulCollision.collision_probability_ge_eighth line 190