OAI/Computability/RandomMean/Chunks.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.TreeDevice.Certified.Chunks.decode line 10
  2. theorem OAI.MeanPayoff.TreeDevice.Certified.Chunks.sample_exact line 13
  3. theorem OAI.MeanPayoff.TreeDevice.Certified.Chunks.fold_decode line 22
  4. theorem OAI.MeanPayoff.TreeDevice.Certified.Chunks.run_exact line 37
  5. theorem OAI.MeanPayoff.TreeDevice.Certified.Chunks.decode_append line 43
  6. theorem OAI.MeanPayoff.RandomTree.bind_congr_all line 53
  7. theorem OAI.MeanPayoff.TreeDevice.Certified.Chunks.decode_law line 61
  8. abbrev OAI.MeanPayoff.TreeDevice.Certified.PostCode.Input line 84
  9. def OAI.MeanPayoff.TreeDevice.Certified.PostCode.samples line 85
  10. def OAI.MeanPayoff.TreeDevice.Certified.PostCode.start line 87
  11. def OAI.MeanPayoff.TreeDevice.Certified.PostCode.execute line 88
  12. def OAI.MeanPayoff.TreeDevice.Certified.PostCode.returned line 90
  13. def OAI.MeanPayoff.TreeDevice.Certified.PostCode.classify line 92
  14. def OAI.MeanPayoff.TreeDevice.Certified.PostCode.boolean line 94
  15. theorem OAI.MeanPayoff.TreeDevice.Certified.PostCode.boolean_poly line 98
  16. def OAI.MeanPayoff.TreeDevice.Certified.PostCode.digits line 101
  17. def OAI.MeanPayoff.TreeDevice.Certified.PostCode.run line 107
  18. theorem OAI.MeanPayoff.TreeDevice.Certified.PostCode.classify_eval line 108
  19. theorem OAI.MeanPayoff.TreeDevice.Certified.PostCode.returned_eval line 115
  20. theorem OAI.MeanPayoff.TreeDevice.Certified.PostCode.digits_eval line 116
  21. theorem OAI.MeanPayoff.TreeDevice.Certified.PostCode.samples_eval line 117
  22. theorem OAI.MeanPayoff.TreeDevice.Certified.PostCode.execute_eval line 118