OAI/Computability/Logspace/TerminalEvaluation.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

Evaluation of terminal estimator requests and their approximation guarantees.

From OpenAI, Exact Derandomization of Logarithmic Space: L = RL = BPL.

  1. abbrev OAI.ExactDerandomization.Gyre.Term.selfC line 30
  2. abbrev OAI.ExactDerandomization.Gyre.Term.header line 31
  3. abbrev OAI.ExactDerandomization.Gyre.Term.spirit line 32
  4. def OAI.ExactDerandomization.Gyre.Term.ahead line 33
  5. def OAI.ExactDerandomization.Gyre.Term.stomp line 34
  6. def OAI.ExactDerandomization.Gyre.Term.ebit line 37
  7. def OAI.ExactDerandomization.Gyre.Term.avail line 40
  8. def OAI.ExactDerandomization.Gyre.Term.fire line 43
  9. abbrev OAI.ExactDerandomization.Gyre.Term.te line 44
  10. def OAI.ExactDerandomization.Gyre.Term.rally line 47
  11. def OAI.ExactDerandomization.Gyre.Term.ent line 53
  12. structure OAI.ExactDerandomization.Gyre.OrbitR.Prism line 62
  13. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.v line 67
  14. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.origin line 68
  15. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.src line 69
  16. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.target line 70
  17. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.screen line 71
  18. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.fare line 72
  19. structure OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ready line 73
  20. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ready.motto line 80
  21. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ready.crown line 82
  22. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ready.includes0 line 83
  23. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ready.price0 line 85
  24. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ready.price2 line 87
  25. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ready.playsC line 91
  26. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ready.toneC line 98
  27. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ready.gem line 126
  28. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ready.spinC line 135
  29. def OAI.ExactDerandomization.Gyre.OrbitR.Prism.lifted line 144
  30. structure OAI.ExactDerandomization.Gyre.OrbitR.Prism.Enabled line 147
  31. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.rankF line 174
  32. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.chooses line 175
  33. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.doesno line 178
  34. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.Enabled.core12 line 184
  35. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.Enabled.frame line 185
  36. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Enabled.capR line 186
  37. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Enabled.roves line 195
  38. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Enabled.mounted line 243
  39. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Enabled.ancestor line 290
  40. abbrev OAI.ExactDerandomization.Gyre.Term.need line 340
  41. def OAI.ExactDerandomization.Gyre.Term.noteQ line 343
  42. abbrev OAI.ExactDerandomization.Gyre.Term.sees line 348
  43. def OAI.ExactDerandomization.Gyre.Term.portals line 351
  44. lemma OAI.ExactDerandomization.Gyre.Term.portalsK line 354
  45. def OAI.ExactDerandomization.Gyre.Term.candle line 357
  46. def OAI.ExactDerandomization.Gyre.Term.changeP line 358
  47. lemma OAI.ExactDerandomization.Gyre.Term.changeK line 359
  48. def OAI.ExactDerandomization.Gyre.Term.atlas line 361
  49. lemma OAI.ExactDerandomization.Gyre.Term.atlasK line 366
  50. abbrev OAI.ExactDerandomization.Gyre.Term.b0 line 374
  51. abbrev OAI.ExactDerandomization.Gyre.Term.bright line 375
  52. def OAI.ExactDerandomization.Gyre.Term.tuneE line 378
  53. abbrev OAI.ExactDerandomization.Gyre.Term.originC line 382
  54. def OAI.ExactDerandomization.Gyre.Term.summit line 383
  55. def OAI.ExactDerandomization.Gyre.Term.double line 386
  56. def OAI.ExactDerandomization.Gyre.Term.melody line 390
  57. def OAI.ExactDerandomization.Gyre.Term.costamp line 396
  58. def OAI.ExactDerandomization.Gyre.Term.endC line 399
  59. abbrev OAI.ExactDerandomization.Gyre.Term.fullD line 400
  60. abbrev OAI.ExactDerandomization.Gyre.Term.Budget0.H line 403
  61. abbrev OAI.ExactDerandomization.Gyre.Term.Budget0.wallet line 404
  62. def OAI.ExactDerandomization.Gyre.Term.Budget0.cost line 405
  63. lemma OAI.ExactDerandomization.Gyre.Term.Budget0.mantis line 409
  64. lemma OAI.ExactDerandomization.Gyre.Term.Budget0.fareE line 424
  65. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.LampT line 454
  66. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.Hx line 455
  67. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.Tc line 456
  68. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.across line 458
  69. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.heightR line 459
  70. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.vale line 460
  71. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.euro line 461
  72. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.stationE line 462
  73. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.paintE line 463
  74. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.outV line 464
  75. structure OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court line 465
  76. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.skewed line 480
  77. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.readyK line 485
  78. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.stake0 line 489
  79. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.invoice line 497
  80. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.seeks line 514
  81. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.realm line 526
  82. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.lampC line 531
  83. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.seesR line 532
  84. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.okY line 597
  85. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.awakeY line 598
  86. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.tinted line 622
  87. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.bill line 641
  88. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.sharp line 643
  89. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.frail line 647
  90. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.summitR line 662
  91. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.prompter line 684
  92. def OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.sumR line 736
  93. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.pg line 740
  94. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.towerQ line 743
  95. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.warmV line 781
  96. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.showR line 789
  97. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.earnsR line 793
  98. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.plain line 829
  99. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.salmon line 838
  100. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.choirR line 844
  101. structure OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ace line 922
  102. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ace.price line 931
  103. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ace.emits line 934
  104. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ace.songT line 938
  105. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ace.kingdom line 943
  106. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ace.deadgate line 950
  107. abbrev OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.tribe line 961
  108. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.matter line 963
  109. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.roy line 991
  110. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Court.plants line 1002
  111. def OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ace.flat line 1075
  112. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ace.past line 1077
  113. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ace.mark0 line 1080
  114. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ace.seed0 line 1084
  115. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ace.deltaP line 1096
  116. lemma OAI.ExactDerandomization.Gyre.OrbitR.Prism.Ace.water line 1101