OAI/Computability/MeanPayoff/Preparation.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.Label.exponent_arithmetic line 6
  2. theorem OAI.MeanPayoff.Label.initialExponent_linear line 22
  3. theorem OAI.MeanPayoff.Label.root_steps_bound line 27
  4. theorem OAI.MeanPayoff.TreeDevice.Certified.Counter.inc_length line 82
  5. def OAI.MeanPayoff.TreeDevice.Certified.DetRoot.nWord line 85
  6. def OAI.MeanPayoff.TreeDevice.Certified.DetRoot.nPlus line 86
  7. def OAI.MeanPayoff.TreeDevice.Certified.DetRoot.wPlus line 87
  8. def OAI.MeanPayoff.TreeDevice.Certified.DetRoot.threshold line 88
  9. def OAI.MeanPayoff.TreeDevice.Certified.DetRoot.exponent line 89
  10. def OAI.MeanPayoff.TreeDevice.Certified.DetRoot.width line 90
  11. def OAI.MeanPayoff.TreeDevice.Certified.DetRoot.lower line 91
  12. def OAI.MeanPayoff.TreeDevice.Certified.DetRoot.mass line 92
  13. def OAI.MeanPayoff.TreeDevice.Certified.DetRoot.input line 93
  14. def OAI.MeanPayoff.TreeDevice.Certified.DetRoot.root line 94
  15. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRoot.threshold_val line 95
  16. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRoot.exponent_length line 100
  17. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRoot.input_rep line 104
  18. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRoot.root_game line 128
  19. def OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.inputLength line 134
  20. def OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.logarithm line 140
  21. def OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.exponent line 142
  22. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.logarithm_length line 144
  23. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.exponent_length line 149
  24. def OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.seed line 151
  25. def OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.inflate line 152
  26. def OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.assemble line 155
  27. def OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.value line 157
  28. def OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.device line 159
  29. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.value_game line 164
  30. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.seed_eval line 192
  31. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.inflate_limit line 193
  32. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.device_limit line 200
  33. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.exponent_poly line 207
  34. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.root_poly line 208
  35. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.seed_poly line 209
  36. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.assemble_poly line 210
  37. def OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.resource line 215
  38. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.input_bound line 216
  39. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.seed_cost line 218
  40. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.seed_size_le line 224
  41. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.seed_size line 226
  42. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.exponent_size line 228
  43. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.exponent_size_length line 234
  44. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.power_bound line 236
  45. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.allocation_init_cost line 238
  46. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.allocation_fold_cost line 240
  47. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.allocation_cost line 247
  48. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.allocation_size line 251
  49. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.root_size line 254
  50. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.inflate_cost line 260
  51. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.inflate_size line 266
  52. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.assemble_cost line 270
  53. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.cost_bound line 274
  54. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.output_size_le line 278
  55. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPreparation.output_bound line 280