OAI/Computability/Logspace/RowEvaluation.lean

GitHub source file

207 declarations, 0 contain sorry, 0 declared as axioms

Evaluation of row scores, ranks, and compressed numerical values.

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

  1. abbrev OAI.ExactDerandomization.Cambria.Hull line 26
  2. abbrev OAI.ExactDerandomization.Cambria.Helm line 27
  3. abbrev OAI.ExactDerandomization.Cambria.Surf line 29
  4. abbrev OAI.ExactDerandomization.Cambria.Surf.mx line 31
  5. abbrev OAI.ExactDerandomization.Cambria.Surf.days line 32
  6. abbrev OAI.ExactDerandomization.Cambria.Surf.chartQ line 33
  7. abbrev OAI.ExactDerandomization.Cambria.Surf.dye line 34
  8. abbrev OAI.ExactDerandomization.Cambria.Surf.A line 35
  9. abbrev OAI.ExactDerandomization.Cambria.Surf.U line 36
  10. abbrev OAI.ExactDerandomization.Cambria.Surf.sunset line 37
  11. abbrev OAI.ExactDerandomization.Cambria.Surf.windC line 38
  12. abbrev OAI.ExactDerandomization.Cambria.Surf.priceC line 39
  13. def OAI.ExactDerandomization.Cambria.Surf.green line 40
  14. def OAI.ExactDerandomization.Cambria.Surf.heatC line 42
  15. def OAI.ExactDerandomization.Cambria.Surf.flareQ line 44
  16. def OAI.ExactDerandomization.Cambria.Surf.frontC line 45
  17. def OAI.ExactDerandomization.Cambria.Surf.finalC line 46
  18. lemma OAI.ExactDerandomization.Cambria.Surf.Prep.windK line 50
  19. lemma OAI.ExactDerandomization.Cambria.Surf.Prep.headF line 53
  20. lemma OAI.ExactDerandomization.Cambria.Surf.Prep.chapter line 58
  21. lemma OAI.ExactDerandomization.Cambria.Surf.Prep.facet line 62
  22. lemma OAI.ExactDerandomization.Cambria.Surf.Prep.aideK line 64
  23. abbrev OAI.ExactDerandomization.Cambria.PondQ line 70
  24. abbrev OAI.ExactDerandomization.Cambria.Hood.codeE line 76
  25. def OAI.ExactDerandomization.Cambria.Hood.spill line 77
  26. lemma OAI.ExactDerandomization.Cambria.Hood.ankle line 80
  27. lemma OAI.ExactDerandomization.Cambria.Hood.bloomK line 85
  28. lemma OAI.ExactDerandomization.Cambria.Hood.fledK line 88
  29. def OAI.ExactDerandomization.Cambria.Hood.saute line 93
  30. lemma OAI.ExactDerandomization.Cambria.Hood.codePos line 96
  31. lemma OAI.ExactDerandomization.Cambria.Hood.lastE line 104
  32. lemma OAI.ExactDerandomization.Cambria.Hood.dawn line 123
  33. def OAI.ExactDerandomization.Cambria.Keel.early line 138
  34. def OAI.ExactDerandomization.Cambria.Keel.foilT line 140
  35. def OAI.ExactDerandomization.Cambria.Keel.quarry line 141
  36. def OAI.ExactDerandomization.Cambria.Keel.cream line 142
  37. lemma OAI.ExactDerandomization.Cambria.Keel.creamK line 143
  38. def OAI.ExactDerandomization.Cambria.Keel.renew line 145
  39. abbrev OAI.ExactDerandomization.Cambria.Keel.Tor line 147
  40. def OAI.ExactDerandomization.Cambria.Keel.broom line 148
  41. def OAI.ExactDerandomization.Cambria.Keel.frontQ line 150
  42. lemma OAI.ExactDerandomization.Cambria.Keel.answer line 158
  43. lemma OAI.ExactDerandomization.Cambria.Keel.tome line 163
  44. lemma OAI.ExactDerandomization.Cambria.Keel.summons line 172
  45. def OAI.ExactDerandomization.Cambria.Mica.cube line 206
  46. lemma OAI.ExactDerandomization.Cambria.Mica.cubeK line 209
  47. def OAI.ExactDerandomization.Cambria.Mica.giz line 217
  48. abbrev OAI.ExactDerandomization.Cambria.Mica.clue line 220
  49. abbrev OAI.ExactDerandomization.Cambria.Mica.invite line 221
  50. def OAI.ExactDerandomization.Cambria.Mica.leafC line 222
  51. abbrev OAI.ExactDerandomization.Cambria.Mica.ole line 225
  52. def OAI.ExactDerandomization.Cambria.Mica.moth line 226
  53. abbrev OAI.ExactDerandomization.Cambria.Mica.host line 227
  54. structure OAI.ExactDerandomization.Cambria.Mica.LiftQ line 233
  55. abbrev OAI.ExactDerandomization.Cambria.Mica.Stars line 240
  56. inductive OAI.ExactDerandomization.Cambria.Mica.Partner line 241
  57. def OAI.ExactDerandomization.Cambria.Mica.census line 250
  58. def OAI.ExactDerandomization.Cambria.Mica.exitE line 254
  59. lemma OAI.ExactDerandomization.Cambria.Mica.exitJ line 255
  60. lemma OAI.ExactDerandomization.Cambria.Mica.glow0 line 258
  61. lemma OAI.ExactDerandomization.Cambria.Mica.theEnd line 267
  62. def OAI.ExactDerandomization.Cambria.BadgeX.iris line 317
  63. def OAI.ExactDerandomization.Cambria.BadgeX.portM line 320
  64. def OAI.ExactDerandomization.Cambria.BadgeX.pointE line 323
  65. def OAI.ExactDerandomization.Cambria.BadgeX.collect line 326
  66. lemma OAI.ExactDerandomization.Cambria.BadgeX.iris_le line 333
  67. lemma OAI.ExactDerandomization.Cambria.BadgeX.spark line 337
  68. structure OAI.ExactDerandomization.Cambria.BadgeX.Crew line 356
  69. abbrev OAI.ExactDerandomization.Cambria.BadgeX.Crew.outR line 368
  70. abbrev OAI.ExactDerandomization.Cambria.BadgeX.Crew.src line 369
  71. abbrev OAI.ExactDerandomization.Cambria.BadgeX.Crew.skill line 370
  72. abbrev OAI.ExactDerandomization.Cambria.BadgeX.Crew.stationP line 371
  73. abbrev OAI.ExactDerandomization.Cambria.BadgeX.Crew.host0 line 372
  74. abbrev OAI.ExactDerandomization.Cambria.BadgeX.Crew.lampQ line 373
  75. structure OAI.ExactDerandomization.Cambria.BadgeX.Crew.Good line 374
  76. abbrev OAI.ExactDerandomization.Cambria.BadgeX.Crew.hitP line 383
  77. structure OAI.ExactDerandomization.Cambria.BadgeX.Crew.Arrived line 384
  78. lemma OAI.ExactDerandomization.Cambria.BadgeX.Crew.Arrived.throng line 394
  79. lemma OAI.ExactDerandomization.Cambria.BadgeX.Crew.Arrived.wreath line 411
  80. lemma OAI.ExactDerandomization.Cambria.BadgeX.Crew.Arrived.paths line 446
  81. def OAI.ExactDerandomization.Cambria.Era.budget line 525
  82. def OAI.ExactDerandomization.Cambria.Era.tariff line 526
  83. lemma OAI.ExactDerandomization.Cambria.Era.billed line 527
  84. lemma OAI.ExactDerandomization.Cambria.Era.educated line 529
  85. lemma OAI.ExactDerandomization.Cambria.Era.orn line 542
  86. lemma OAI.ExactDerandomization.Cambria.Era.oust line 552
  87. structure OAI.ExactDerandomization.Cambria.Era.Spell line 574
  88. lemma OAI.ExactDerandomization.Cambria.Era.overly line 581
  89. lemma OAI.ExactDerandomization.Cambria.Era.basePort line 590
  90. lemma OAI.ExactDerandomization.Cambria.Era.echoPort line 617
  91. abbrev OAI.ExactDerandomization.Cambria.Wear.Rus line 676
  92. abbrev OAI.ExactDerandomization.Cambria.Wear.GridY line 677
  93. abbrev OAI.ExactDerandomization.Cambria.Wear.allQ line 678
  94. abbrev OAI.ExactDerandomization.Cambria.Wear.skyG line 679
  95. abbrev OAI.ExactDerandomization.Cambria.Wear.rx line 680
  96. def OAI.ExactDerandomization.Cambria.Wear.shelf line 681
  97. def OAI.ExactDerandomization.Cambria.Wear.tin line 684
  98. abbrev OAI.ExactDerandomization.Cambria.Wear.pin1 line 685
  99. abbrev OAI.ExactDerandomization.Cambria.Wear.pin2 line 686
  100. abbrev OAI.ExactDerandomization.Cambria.Wear.packC line 687
  101. def OAI.ExactDerandomization.Cambria.Wear.tone line 688
  102. def OAI.ExactDerandomization.Cambria.Wear.pitch line 692
  103. abbrev OAI.ExactDerandomization.Cambria.Wear.rate0 line 696
  104. def OAI.ExactDerandomization.Cambria.Wear.prefixD line 697
  105. lemma OAI.ExactDerandomization.Cambria.Wear.prefD line 704
  106. abbrev OAI.ExactDerandomization.Cambria.Wear.Health line 706
  107. abbrev OAI.ExactDerandomization.Cambria.Wear.range0 line 707
  108. def OAI.ExactDerandomization.Cambria.Wear.powerF line 708
  109. def OAI.ExactDerandomization.Cambria.Wear.falls line 709
  110. abbrev OAI.ExactDerandomization.Cambria.Wear.visitAt line 711
  111. def OAI.ExactDerandomization.Cambria.Wear.spreadC line 712
  112. def OAI.ExactDerandomization.Cambria.Wear.dose line 714
  113. def OAI.ExactDerandomization.Cambria.Wear.puff line 715
  114. def OAI.ExactDerandomization.Cambria.Wear.nook line 719
  115. def OAI.ExactDerandomization.Cambria.Wear.gemini line 722
  116. abbrev OAI.ExactDerandomization.Cambria.Wear.markR line 727
  117. abbrev OAI.ExactDerandomization.Cambria.Wear.moss line 731
  118. abbrev OAI.ExactDerandomization.Cambria.Wear.past line 733
  119. def OAI.ExactDerandomization.Cambria.Wear.bia line 735
  120. abbrev OAI.ExactDerandomization.Cambria.Wear.shapeC line 739
  121. abbrev OAI.ExactDerandomization.Cambria.Wear.sourceB line 740
  122. def OAI.ExactDerandomization.Cambria.Wear.coast line 747

    Source documentation

    mask kind2 and kind1 use lit-only pricing.

    def coast (p:MintV)(c:Knob)(r:Rock q w h)(s:Scheme)(b:Bool)(i:ℕ):Cog:=
…
  123. def OAI.ExactDerandomization.Cambria.Wear.hub line 753
  124. abbrev OAI.ExactDerandomization.Cambria.Wear.grainq line 754
  125. def OAI.ExactDerandomization.Cambria.Wear.Paper.same line 758
  126. lemma OAI.ExactDerandomization.Cambria.Wear.Paper.oneself line 759
  127. lemma OAI.ExactDerandomization.Cambria.Wear.Paper.use line 760
  128. lemma OAI.ExactDerandomization.Cambria.Wear.Paper.everF line 761
  129. lemma OAI.ExactDerandomization.Cambria.Wear.Paper.same.stronger line 763
  130. lemma OAI.ExactDerandomization.Cambria.Wear.Paper.same.plies line 766
  131. lemma OAI.ExactDerandomization.Cambria.Wear.Paper.same.score0 line 768
  132. lemma OAI.ExactDerandomization.Cambria.Wear.Paper.same.txt line 770
  133. lemma OAI.ExactDerandomization.Cambria.Wear.Paper.same.rosebud line 773
  134. lemma OAI.ExactDerandomization.Cambria.Wear.Paper.same.red line 775
  135. lemma OAI.ExactDerandomization.Cambria.Wear.Paper.same.stow line 777
  136. lemma OAI.ExactDerandomization.Cambria.Wear.Paper.reed line 779
  137. lemma OAI.ExactDerandomization.Cambria.Wear.Paper.reedX line 783
  138. lemma OAI.ExactDerandomization.Cambria.Wear.Paper.biaS line 786
  139. lemma OAI.ExactDerandomization.Cambria.Wear.Paper.backS line 791
  140. abbrev OAI.ExactDerandomization.Cambria.Wear.Paper.noneT line 794
  141. def OAI.ExactDerandomization.Cambria.Wear.Paper.money0 line 795
  142. def OAI.ExactDerandomization.Cambria.Wear.Paper.budgetD line 798
  143. lemma OAI.ExactDerandomization.Cambria.Wear.Paper.eras line 804
  144. structure OAI.ExactDerandomization.Cambria.Rime.Nest line 843
  145. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.ray line 851
  146. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.krod line 852
  147. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.a line 853
  148. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.v line 854
  149. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.t line 855
  150. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.H line 856
  151. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.T line 857
  152. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.home line 858
  153. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.whereF line 859
  154. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.beaming line 860
  155. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.optic line 861
  156. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.addr1 line 862
  157. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.addr2 line 863
  158. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.capV line 864
  159. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.cut line 865
  160. def OAI.ExactDerandomization.Cambria.Rime.Nest.addr3 line 866
  161. def OAI.ExactDerandomization.Cambria.Rime.Nest.catshot line 867
  162. structure OAI.ExactDerandomization.Cambria.Rime.Nest.Good line 868
  163. def OAI.ExactDerandomization.Cambria.Rime.Nest.VoiceS line 877

    Source documentation

    score service at another location.W-clock sufficient. power j normalizer.

    def VoiceS(x y j:ℕ)(A:ℝ): Prop := ∃ b m,
…
  164. def OAI.ExactDerandomization.Cambria.Rime.Nest.Loom0 line 880
  165. structure OAI.ExactDerandomization.Cambria.Rime.Nest.Etude line 882
  166. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.primary line 889
  167. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.nested line 893
  168. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.born0 line 912
  169. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.press line 913
  170. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.ru line 914
  171. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.shade0 line 917
  172. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.visE0 line 918
  173. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.sell0 line 922
  174. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.keep0 line 928
  175. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.scales line 929
  176. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.trueL line 934
  177. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.scrys line 935
  178. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.barre line 941
  179. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.salve line 959
  180. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.waltz line 964
  181. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.upso line 970
  182. def OAI.ExactDerandomization.Cambria.Rime.Nest.Good.maxs line 991
  183. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.carmen line 994
  184. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.tensorB line 1003
  185. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.warm line 1004
  186. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.salutation line 1007
  187. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.lecture line 1017
  188. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.valueOld line 1061
  189. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.biast line 1067
  190. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.knows0 line 1079
  191. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.Good.C0 line 1082
  192. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.Good.title line 1083
  193. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.Good.capsum line 1084
  194. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.Good.sailed line 1085
  195. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.Good.holding line 1087
  196. abbrev OAI.ExactDerandomization.Cambria.Rime.Nest.Good.gross line 1089
  197. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.home0 line 1092
  198. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.inoculates line 1097
  199. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.lame line 1100
  200. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.zen0 line 1105
  201. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.help0 line 1107
  202. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.stellar line 1114
  203. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.torn line 1122
  204. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.partOld line 1125
  205. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.youngNo line 1132
  206. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.youngYes line 1139
  207. lemma OAI.ExactDerandomization.Cambria.Rime.Nest.Good.shekel line 1152