OAI/Computability/Logspace/CompressionEvaluation.lean

GitHub source file

176 declarations, 0 contain sorry, 0 declared as axioms

Correctness of the numerical row-compression evaluation.

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

  1. inductive OAI.ExactDerandomization.Aurora.Folk line 23

    Source documentation

    Arithmetic library with distinguished variable leaves

    inductive Folk where
…
  2. def OAI.ExactDerandomization.Aurora.Folk.bind line 29
  3. def OAI.ExactDerandomization.Aurora.Folk.meanF line 33
  4. lemma OAI.ExactDerandomization.Aurora.Folk.time line 37
  5. lemma OAI.ExactDerandomization.Aurora.Folk.stamina line 44
  6. abbrev OAI.ExactDerandomization.Aurora.Folk.sum line 50
  7. abbrev OAI.ExactDerandomization.Aurora.Folk.diff line 51
  8. abbrev OAI.ExactDerandomization.Aurora.Folk.times line 52
  9. abbrev OAI.ExactDerandomization.Aurora.Folk.join line 53
  10. abbrev OAI.ExactDerandomization.Aurora.Folk.meet line 54
  11. abbrev OAI.ExactDerandomization.Aurora.Folk.flop line 55
  12. abbrev OAI.ExactDerandomization.Aurora.Folk.price line 56
  13. lemma OAI.ExactDerandomization.Aurora.Folk.val0 line 57
  14. lemma OAI.ExactDerandomization.Aurora.Folk.val1 line 58
  15. lemma OAI.ExactDerandomization.Aurora.Folk.val2 line 59
  16. lemma OAI.ExactDerandomization.Aurora.Folk.val3 line 60
  17. lemma OAI.ExactDerandomization.Aurora.Folk.val4 line 61
  18. lemma OAI.ExactDerandomization.Aurora.Folk.val5 line 62
  19. lemma OAI.ExactDerandomization.Aurora.Folk.outV line 63
  20. lemma OAI.ExactDerandomization.Aurora.Folk.val6 line 64
  21. lemma OAI.ExactDerandomization.Aurora.Folk.borne line 65
  22. abbrev OAI.ExactDerandomization.Aurora.Folk.lo line 69

    Source comment

    Surface p(x,y).
    abbrev lo(a b x :Folk):=meet b (join a x)

    Mentions: OAI.ExactDerandomization.Aurora.Folk, OAI.ExactDerandomization.Aurora.Folk.meet, OAI.ExactDerandomization.Aurora.Folk.join

  23. abbrev OAI.ExactDerandomization.Aurora.Folk.tick line 70
  24. abbrev OAI.ExactDerandomization.Aurora.Folk.power4 line 71
  25. def OAI.ExactDerandomization.Aurora.Folk.heaven line 72
  26. def OAI.ExactDerandomization.Aurora.Folk.sweetF line 73
  27. lemma OAI.ExactDerandomization.Aurora.Folk.lowF line 75
  28. lemma OAI.ExactDerandomization.Aurora.Folk.ticking line 76
  29. lemma OAI.ExactDerandomization.Aurora.Folk.powering line 77
  30. lemma OAI.ExactDerandomization.Aurora.Folk.art line 80
  31. lemma OAI.ExactDerandomization.Aurora.Folk.sweetness line 82
  32. abbrev OAI.ExactDerandomization.Aurora.Folk.powerZ line 85
  33. abbrev OAI.ExactDerandomization.Aurora.Folk.az line 86
  34. abbrev OAI.ExactDerandomization.Aurora.Folk.az2 line 87
  35. def OAI.ExactDerandomization.Aurora.Folk.climate line 88
  36. lemma OAI.ExactDerandomization.Aurora.Folk.town line 90
  37. def OAI.ExactDerandomization.Aurora.Folk.vacation line 95
  38. lemma OAI.ExactDerandomization.Aurora.Folk.zoo line 100
  39. lemma OAI.ExactDerandomization.Aurora.Folk.azone line 101
  40. lemma OAI.ExactDerandomization.Aurora.Folk.azto line 102
  41. lemma OAI.ExactDerandomization.Aurora.Folk.homes line 103
  42. def OAI.ExactDerandomization.Aurora.Folk.gourd line 120
  43. lemma OAI.ExactDerandomization.Aurora.Folk.tract line 121
  44. abbrev OAI.ExactDerandomization.Aurora.Folk.fever line 126
  45. def OAI.ExactDerandomization.Aurora.Folk.localq line 127
  46. lemma OAI.ExactDerandomization.Aurora.Folk.feved line 132
  47. lemma OAI.ExactDerandomization.Aurora.Folk.correctq line 133
  48. def OAI.ExactDerandomization.Aurora.Folk.sliceF line 140
  49. lemma OAI.ExactDerandomization.Aurora.Folk.pairS line 143
  50. def OAI.ExactDerandomization.Aurora.Folk.binC line 148
  51. lemma OAI.ExactDerandomization.Aurora.Folk.excel line 154
  52. structure OAI.ExactDerandomization.Aurora.Nick line 188
  53. abbrev OAI.ExactDerandomization.Aurora.Nick.green line 195
  54. def OAI.ExactDerandomization.Aurora.Nick.mainC line 197
  55. def OAI.ExactDerandomization.Aurora.Nick.toastC line 198
  56. lemma OAI.ExactDerandomization.Aurora.Nick.realC line 202
  57. lemma OAI.ExactDerandomization.Aurora.Nick.realD line 208
  58. def OAI.ExactDerandomization.Aurora.Nick.league line 210
  59. def OAI.ExactDerandomization.Aurora.Nick.humor line 218
  60. def OAI.ExactDerandomization.Aurora.Nick.factorR line 221
  61. def OAI.ExactDerandomization.Aurora.Nick.witness line 224
  62. def OAI.ExactDerandomization.Aurora.Nick.temple line 227
  63. lemma OAI.ExactDerandomization.Aurora.Nick.fareC line 230
  64. lemma OAI.ExactDerandomization.Aurora.Nick.ten line 256
  65. lemma OAI.ExactDerandomization.Aurora.Nick.many line 265
  66. abbrev OAI.ExactDerandomization.Aurora.Scroll.Profile line 293
  67. def OAI.ExactDerandomization.Aurora.Scroll.copyN line 294
  68. def OAI.ExactDerandomization.Aurora.Scroll.decodeP line 295
  69. lemma OAI.ExactDerandomization.Aurora.Scroll.copyB line 296
  70. abbrev OAI.ExactDerandomization.Aurora.Scroll.ruler line 299
  71. def OAI.ExactDerandomization.Aurora.Scroll.bankS line 300
  72. lemma OAI.ExactDerandomization.Aurora.Scroll.within line 302
  73. def OAI.ExactDerandomization.Aurora.Scroll.checkN line 311
  74. lemma OAI.ExactDerandomization.Aurora.Scroll.checks line 314
  75. lemma OAI.ExactDerandomization.Aurora.Scroll.checkedK line 315
  76. def OAI.ExactDerandomization.Aurora.Scroll.book0 line 319
  77. lemma OAI.ExactDerandomization.Aurora.Scroll.earnK line 320
  78. abbrev OAI.ExactDerandomization.Aurora.Scroll.later line 326
  79. def OAI.ExactDerandomization.Aurora.Fort.sages line 334
  80. lemma OAI.ExactDerandomization.Aurora.Fort.sageK line 335
  81. def OAI.ExactDerandomization.Aurora.Fort.adj line 336
  82. lemma OAI.ExactDerandomization.Aurora.Fort.adjK line 339
  83. abbrev OAI.ExactDerandomization.Aurora.Fort.ratioE line 342
  84. def OAI.ExactDerandomization.Aurora.Fort.localF line 343
  85. abbrev OAI.ExactDerandomization.Aurora.Fort.root0 line 344
  86. def OAI.ExactDerandomization.Aurora.Fort.verse line 345
  87. abbrev OAI.ExactDerandomization.Aurora.Fort.theta line 352
  88. lemma OAI.ExactDerandomization.Aurora.Fort.real0 line 353
  89. abbrev OAI.ExactDerandomization.Aurora.Fort.stageP line 356
  90. def OAI.ExactDerandomization.Aurora.Fort.starsK line 358
  91. abbrev OAI.ExactDerandomization.Aurora.Fort.voiceK line 365
  92. abbrev OAI.ExactDerandomization.Aurora.Fort.lengthF line 367
  93. abbrev OAI.ExactDerandomization.Aurora.Fort.creditR line 368
  94. def OAI.ExactDerandomization.Aurora.Fort.legion line 369
  95. def OAI.ExactDerandomization.Aurora.Fort.divisionB line 373
  96. def OAI.ExactDerandomization.Aurora.Fort.inner line 376
  97. def OAI.ExactDerandomization.Aurora.Fort.entire line 377
  98. abbrev OAI.ExactDerandomization.Aurora.Fort.baseTc line 380
  99. lemma OAI.ExactDerandomization.Aurora.Fort.decant line 381
  100. abbrev OAI.ExactDerandomization.Aurora.Fort.priceR line 413
  101. def OAI.ExactDerandomization.Aurora.Fort.weightD line 415
  102. abbrev OAI.ExactDerandomization.Aurora.Fort.none0 line 417
  103. def OAI.ExactDerandomization.Aurora.Fort.topO line 419
  104. def OAI.ExactDerandomization.Aurora.Fort.budget4 line 420
  105. lemma OAI.ExactDerandomization.Aurora.Fort.countLink line 423
  106. lemma OAI.ExactDerandomization.Aurora.Fort.flow line 437
  107. lemma OAI.ExactDerandomization.Aurora.Fort.fungal line 440
  108. lemma OAI.ExactDerandomization.Aurora.Fort.story0 line 449
  109. structure OAI.ExactDerandomization.Aurora.Grape.Dew line 459
  110. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.g line 465
  111. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.f line 466
  112. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.bench line 467
  113. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.t line 468
  114. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.stage0 line 469
  115. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.court line 470
  116. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.cost line 471
  117. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.high line 472
  118. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.T line 473
  119. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.own line 474
  120. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.fig line 475
  121. structure OAI.ExactDerandomization.Aurora.Grape.Dew.Ready line 477
  122. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.account line 485
  123. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.now line 489
  124. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.last line 491
  125. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.fee line 492
  126. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.toward line 494
  127. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.elder line 501
  128. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.epi line 508
  129. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.flex line 509
  130. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.used line 512
  131. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.above line 513
  132. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.hoped line 517
  133. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.fitF line 521
  134. structure OAI.ExactDerandomization.Aurora.Grape.Dew.LensF line 546
  135. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.θ line 551
  136. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.roofG line 552
  137. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.ankle0 line 556
  138. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.billQ line 564
  139. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.bookG line 566
  140. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.receipt line 570
  141. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Ready.debt line 584
  142. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.LensF.porch line 605
  143. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.LensF.gotK line 608
  144. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.LensF.photo line 611
  145. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.LensF.price line 616
  146. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.LensF.surfD line 620
  147. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.LensF.felt line 628
  148. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.LensF.sum_house line 637
  149. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.LensF.express line 653
  150. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.LensF.scored line 689
  151. structure OAI.ExactDerandomization.Aurora.Grape.Dew.Dose line 726
  152. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.p line 733
  153. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.codeS line 734
  154. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.plex line 735
  155. structure OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens line 736
  156. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.chargeE line 740
  157. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.opted line 745
  158. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.readout line 754
  159. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.position line 764
  160. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.seats line 773
  161. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.journey line 792
  162. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.synced line 829
  163. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.upcoming line 846
  164. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.secure0 line 854
  165. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.panelF line 894
  166. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.roofp line 895
  167. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.k0T line 896
  168. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.area line 898
  169. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.supported line 902
  170. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.defend line 915
  171. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.blessed line 929
  172. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Dose.Lens.sunny line 933
  173. abbrev OAI.ExactDerandomization.Aurora.Grape.Dew.Supply.stageX line 939
  174. def OAI.ExactDerandomization.Aurora.Grape.Dew.Supply.catalogue line 941
  175. lemma OAI.ExactDerandomization.Aurora.Grape.Dew.Supply.sealed0 line 944
  176. theorem OAI.ExactDerandomization.Aurora.Grape.Dew.Supply.givenE line 1003