OAI/Computability/RandomMean/Preparation.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MeanPayoff.TreeDevice.Certified.Preparation.Seed line 11
  2. abbrev OAI.MeanPayoff.TreeDevice.Certified.Preparation.Aux line 12
  3. def OAI.MeanPayoff.TreeDevice.Certified.Preparation.inputLength line 13
  4. def OAI.MeanPayoff.TreeDevice.Certified.Preparation.logarithm line 19
  5. def OAI.MeanPayoff.TreeDevice.Certified.Preparation.exponent line 21
  6. def OAI.MeanPayoff.TreeDevice.Certified.Preparation.root line 23
  7. def OAI.MeanPayoff.TreeDevice.Certified.Preparation.seed line 25
  8. def OAI.MeanPayoff.TreeDevice.Certified.Preparation.inflate line 26
  9. def OAI.MeanPayoff.TreeDevice.Certified.Preparation.assemble line 29
  10. def OAI.MeanPayoff.TreeDevice.Certified.Preparation.value line 31
  11. def OAI.MeanPayoff.TreeDevice.Certified.Preparation.device line 33
  12. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.logarithm_length line 38
  13. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.exponent_length line 43
  14. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.iterations line 45
  15. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.bits_length line 46
  16. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.aux line 49
  17. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.seed_eval line 60
  18. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.inflate_limit line 61
  19. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.device_limit line 68
  20. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.exponent_poly line 81
  21. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.root_poly line 82
  22. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.seed_poly line 83
  23. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.assemble_poly line 84
  24. def OAI.MeanPayoff.TreeDevice.Certified.Preparation.resource line 92
  25. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.input_bound line 93
  26. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.seed_cost line 95
  27. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.seed_size_le line 101
  28. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.seed_size line 103
  29. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.exponent_size line 105
  30. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.exponent_size_length line 111
  31. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.power_bound line 113
  32. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.allocation_init_cost line 115
  33. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.allocation_fold_cost line 117
  34. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.allocation_cost line 124
  35. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.allocation_size line 128
  36. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.root_size line 131
  37. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.inflate_cost line 137
  38. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.inflate_size line 143
  39. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.assemble_cost line 147
  40. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.cost_bound line 151
  41. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.output_size_le line 155
  42. theorem OAI.MeanPayoff.TreeDevice.Certified.Preparation.output_bound line 157