OAI/Computability/RandomMean/Traces.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.TreeDevice.Certified.Counter.bounded_length line 11
  2. def OAI.MeanPayoff.TreeDevice.Certified.Chunks.split line 31
  3. def OAI.MeanPayoff.TreeDevice.Certified.Chunks.positive line 38
  4. def OAI.MeanPayoff.TreeDevice.Certified.Chunks.reverseDigits line 43
  5. abbrev OAI.MeanPayoff.TreeDevice.Certified.Chunks.State line 48
  6. def OAI.MeanPayoff.TreeDevice.Certified.Chunks.params line 49
  7. def OAI.MeanPayoff.TreeDevice.Certified.Chunks.acc line 50
  8. def OAI.MeanPayoff.TreeDevice.Certified.Chunks.bits line 51
  9. def OAI.MeanPayoff.TreeDevice.Certified.Chunks.pieces line 52
  10. def OAI.MeanPayoff.TreeDevice.Certified.Chunks.sample line 53
  11. def OAI.MeanPayoff.TreeDevice.Certified.Chunks.next line 54
  12. def OAI.MeanPayoff.TreeDevice.Certified.Chunks.step line 55
  13. theorem OAI.MeanPayoff.TreeDevice.Certified.Chunks.next_params line 56
  14. theorem OAI.MeanPayoff.TreeDevice.Certified.Chunks.next_acc line 57
  15. theorem OAI.MeanPayoff.TreeDevice.Certified.Chunks.next_bits line 58
  16. theorem OAI.MeanPayoff.TreeDevice.Certified.Chunks.sample_length line 61
  17. theorem OAI.MeanPayoff.TreeDevice.Certified.Chunks.next_size line 62
  18. theorem OAI.MeanPayoff.TreeDevice.Certified.Chunks.fold_params line 77
  19. theorem OAI.MeanPayoff.TreeDevice.Certified.Chunks.fold_size line 81
  20. theorem OAI.MeanPayoff.TreeDevice.Certified.Chunks.prefix_size line 92
  21. def OAI.MeanPayoff.TreeDevice.Certified.Chunks.fold line 104
  22. def OAI.MeanPayoff.TreeDevice.Certified.Chunks.run line 105
  23. theorem OAI.MeanPayoff.RandomTree.all_of_read line 114
  24. def OAI.MeanPayoff.RegisterBits.Traces line 132
  25. theorem OAI.MeanPayoff.RegisterBits.Traces.leaf line 137
  26. theorem OAI.MeanPayoff.RegisterBits.Traces.wait line 138
  27. theorem OAI.MeanPayoff.RegisterBits.Traces.coin line 146
  28. theorem OAI.MeanPayoff.RegisterBits.Traces.bind line 173
  29. theorem OAI.MeanPayoff.RegisterBits.Traces.padded line 187
  30. theorem OAI.MeanPayoff.RegisterBits.read_tree line 197
  31. theorem OAI.MeanPayoff.RegisterBits.depth_tree line 205
  32. theorem OAI.MeanPayoff.RegisterBits.Traces.tree_all line 209
  33. theorem OAI.MeanPayoff.RegisterBits.Traces.expect line 217
  34. theorem OAI.MeanPayoff.RegisterBits.Flow.quiet_runs line 229
  35. theorem OAI.MeanPayoff.RandomTree.map_leaf' line 250
  36. theorem OAI.MeanPayoff.RandomTree.map_coin' line 251
  37. theorem OAI.MeanPayoff.RandomTree.map_congr_all line 253
  38. theorem OAI.MeanPayoff.RandomTree.expect_congr_all line 258
  39. def OAI.MeanPayoff.FairBits.draw line 267
  40. def OAI.MeanPayoff.FairBits.acc line 270
  41. theorem OAI.MeanPayoff.FairBits.length line 273
  42. theorem OAI.MeanPayoff.FairBits.acc_eq line 278
  43. theorem OAI.MeanPayoff.FairBits.append line 282
  44. theorem OAI.MeanPayoff.FairBits.prepend_value line 288
  45. theorem OAI.MeanPayoff.FairBits.number line 292