OAI/Computability/RandomMean/Control.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MeanPayoff.TreeDevice.Certified.RawControl.Orient line 16
  2. abbrev OAI.MeanPayoff.TreeDevice.Certified.RawControl.Tuple line 17
  3. structure OAI.MeanPayoff.TreeDevice.Certified.RawControl.Pack line 18
  4. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.Pack.tuple line 28
  5. instance OAI.MeanPayoff.TreeDevice.Certified.RawControl.(instance at line 29) line 29
  6. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.zeroBudget line 31
  7. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.zeroBox line 32
  8. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.Pack.zero line 33
  9. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.proj line 35
  10. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.p line 37
  11. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.b line 38
  12. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.t line 39
  13. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.q line 40
  14. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.r line 41
  15. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.vs line 42
  16. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.o line 43
  17. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.os line 44
  18. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.p_eval line 46
  19. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.b_eval line 47
  20. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.t_eval line 48
  21. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.q_eval line 49
  22. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.r_eval line 50
  23. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.vs_eval line 51
  24. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.o_eval line 52
  25. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.os_eval line 53
  26. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.pack line 55
  27. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.pack_eval line 65
  28. abbrev OAI.MeanPayoff.TreeDevice.Certified.RawControl.Cell line 70
  29. abbrev OAI.MeanPayoff.TreeDevice.Certified.RawControl.State line 71
  30. abbrev OAI.MeanPayoff.TreeDevice.Certified.RawControl.Env line 72
  31. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.arena line 74
  32. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.exponent line 75
  33. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.samples line 76
  34. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.trials line 77
  35. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.basicSteps line 78
  36. abbrev OAI.MeanPayoff.TreeDevice.Certified.RawControl.Input line 80
  37. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.env line 81
  38. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.random line 82
  39. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.state line 83
  40. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.current line 84
  41. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.stack line 85
  42. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.caller line 86
  43. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.rest line 87
  44. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.makeCell line 88
  45. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.call line 90
  46. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.ret line 92
  47. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.push line 93
  48. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.save line 95
  49. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.smallWidth line 96
  50. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.basic line 98
  51. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.narrow line 100
  52. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.wide line 102
  53. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.delta line 104
  54. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.capWidth line 106
  55. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.solveCase line 109
  56. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.askCase line 115
  57. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.trialsCase line 117
  58. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.updateCase line 121
  59. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.centersCase line 123
  60. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.orientCase line 127
  61. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.orientTrialsCase line 131
  62. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.orientPlusCase line 134
  63. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.tightenCase line 136
  64. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.reweightCase line 138
  65. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.fold_select_bound line 159
  66. def OAI.MeanPayoff.TreeDevice.Certified.Array.foldSelect line 171
  67. def OAI.MeanPayoff.TreeDevice.Certified.Array.foldMin line 190
  68. def OAI.MeanPayoff.TreeDevice.Certified.Array.foldMax line 191
  69. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.foldMin_rep line 193
  70. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.foldMax_rep line 204
  71. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.trialsHeadCase line 225
  72. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.vectorConsCase line 228
  73. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.medianCase line 230
  74. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.centerFirstCase line 232
  75. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.centerSecondCase line 235
  76. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.centersHeadCase line 237
  77. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.centerAt line 240
  78. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.lastPositive line 242
  79. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.lastNegative line 244
  80. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.orientLoopCase line 246
  81. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.orientTailCase line 253
  82. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.orientHeadCase line 256
  83. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.orientConsCase line 259
  84. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.combineCase line 261
  85. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.tightenFirstCase line 263
  86. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.tightenSecondCase line 268
  87. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.boxPassCase line 273
  88. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.solveTightCase line 274
  89. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.solveOrientedCase line 277
  90. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.reweightHeadCase line 280
  91. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.solveReweightedCase line 283
  92. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.capHighCase line 289
  93. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.capLowCase line 291
  94. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.includeInnerCase line 293
  95. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.resume line 295
  96. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.dispatch line 303
  97. def OAI.MeanPayoff.SourceControl.sampledResume line 314
  98. def OAI.MeanPayoff.SourceControl.sampledStep line 362