OAI/Computability/RandomMean/Allocation.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.TreeDevice.Certified.Counter.fixedPower line 11
  2. theorem OAI.MeanPayoff.TreeDevice.Certified.Counter.fixedPower_length line 14
  3. def OAI.MeanPayoff.TreeDevice.Certified.RootCode.g line 22
  4. def OAI.MeanPayoff.TreeDevice.Certified.RootCode.argument line 23
  5. def OAI.MeanPayoff.TreeDevice.Certified.RootCode.exponent line 24
  6. def OAI.MeanPayoff.TreeDevice.Certified.RootCode.cap line 25
  7. def OAI.MeanPayoff.TreeDevice.Certified.RootCode.samples line 26
  8. def OAI.MeanPayoff.TreeDevice.Certified.RootCode.trialBase line 27
  9. def OAI.MeanPayoff.TreeDevice.Certified.RootCode.trials line 28
  10. def OAI.MeanPayoff.TreeDevice.Certified.RootCode.basic line 29
  11. def OAI.MeanPayoff.TreeDevice.Certified.RootCode.env line 30
  12. theorem OAI.MeanPayoff.TreeDevice.Certified.RootCode.g_length line 32
  13. theorem OAI.MeanPayoff.TreeDevice.Certified.RootCode.argument_length line 37
  14. theorem OAI.MeanPayoff.TreeDevice.Certified.RootCode.exponent_length line 39
  15. theorem OAI.MeanPayoff.TreeDevice.Certified.RootCode.samples_length line 43
  16. theorem OAI.MeanPayoff.TreeDevice.Certified.RootCode.trials_length line 53
  17. theorem OAI.MeanPayoff.TreeDevice.Certified.RootCode.basic_length line 57
  18. theorem OAI.MeanPayoff.TreeDevice.Certified.RootCode.env_rep line 59
  19. def OAI.MeanPayoff.TreeDevice.Certified.RootCode.ones line 74
  20. def OAI.MeanPayoff.TreeDevice.Certified.RootCode.budgets line 75
  21. def OAI.MeanPayoff.TreeDevice.Certified.RootCode.box line 78
  22. def OAI.MeanPayoff.TreeDevice.Certified.RootCode.state line 80
  23. def OAI.MeanPayoff.TreeDevice.Certified.RootCode.start line 82
  24. theorem OAI.MeanPayoff.TreeDevice.Certified.RootCode.budgets_rep line 85
  25. theorem OAI.MeanPayoff.TreeDevice.Certified.RootCode.box_rep line 105
  26. theorem OAI.MeanPayoff.TreeDevice.Certified.RootCode.state_rep line 117