OAI/Computability/Logspace/HierarchicalEstimator.lean

GitHub source file

224 declarations, 0 contain sorry, 0 declared as axioms

The hierarchical estimator and its well-founded error induction.

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

  1. structure OAI.ExactDerandomization.Net.Scene line 23
  2. def OAI.ExactDerandomization.Net.Scene.P line 33
  3. def OAI.ExactDerandomization.Net.Scene.frame line 34
  4. def OAI.ExactDerandomization.Net.Scene.stage line 35
  5. lemma OAI.ExactDerandomization.Net.Scene.aligned line 36
  6. def OAI.ExactDerandomization.Net.Scene.mode line 37
  7. structure OAI.ExactDerandomization.Net.Scene.SetUp line 40

    Source documentation

    Uniform hypotheses supplied for the whole finite stage range.

    structure SetUp : Prop where
…
  8. lemma OAI.ExactDerandomization.Net.Scene.phase line 48
  9. lemma OAI.ExactDerandomization.Net.Scene.rights line 49
  10. lemma OAI.ExactDerandomization.Net.Scene.rankok line 50
  11. lemma OAI.ExactDerandomization.Net.Scene.fits line 54
  12. def OAI.ExactDerandomization.Net.pad line 59
  13. lemma OAI.ExactDerandomization.Net.stayed line 60
  14. lemma OAI.ExactDerandomization.Net.beyond line 66
  15. inductive OAI.ExactDerandomization.Net.Kind line 83

    Source documentation

    Echo labels have k as the predecessor iteration number.

    inductive Kind where
…
  16. structure OAI.ExactDerandomization.Net.Quest line 90
  17. structure OAI.ExactDerandomization.Net.Peek line 98
  18. def OAI.ExactDerandomization.Net.Kind.theta line 105
  19. def OAI.ExactDerandomization.Net.Kind.depth line 110
  20. def OAI.ExactDerandomization.Net.Kind.matrix line 117
  21. def OAI.ExactDerandomization.Net.Kind.piece line 124
  22. def OAI.ExactDerandomization.Net.Kind.narrow line 130
  23. def OAI.ExactDerandomization.Net.Kind.paired line 133
  24. def OAI.ExactDerandomization.Net.Kind.sane line 137
  25. lemma OAI.ExactDerandomization.Net.Kind.lowp line 143
  26. lemma OAI.ExactDerandomization.Net.Kind.highp line 144
  27. lemma OAI.ExactDerandomization.Net.Kind.wall line 145
  28. def OAI.ExactDerandomization.Net.lag line 155
  29. def OAI.ExactDerandomization.Net.coreR line 156
  30. def OAI.ExactDerandomization.Net.Quest.plan line 161
  31. def OAI.ExactDerandomization.Net.Quest.key line 162
  32. def OAI.ExactDerandomization.Net.Quest.stair line 164
  33. def OAI.ExactDerandomization.Net.Quest.ready line 166
  34. def OAI.ExactDerandomization.Net.Quest.question line 169
  35. def OAI.ExactDerandomization.Net.Quest.builder line 172
  36. def OAI.ExactDerandomization.Net.Quest.two line 175
  37. def OAI.ExactDerandomization.Net.Quest.phi line 176
  38. def OAI.ExactDerandomization.Net.Quest.trio line 178
  39. def OAI.ExactDerandomization.Net.Quest.steps line 181
  40. def OAI.ExactDerandomization.Net.Quest.damp line 186
  41. def OAI.ExactDerandomization.Net.Quest.guardP line 188
  42. def OAI.ExactDerandomization.Net.Quest.truth_second line 191

    Source documentation

    true stochastic row represented by the same building blocks.

    def truth_second (s : Scene n) : Mat :=
…

    Mentions: OAI.ExactDerandomization.Net.Scene

  43. def OAI.ExactDerandomization.Net.Quest.origin line 195
  44. def OAI.ExactDerandomization.Net.Quest.need line 199
  45. lemma OAI.ExactDerandomization.Net.Quest.normal line 201
  46. lemma OAI.ExactDerandomization.Net.Quest.prepared line 210
  47. lemma OAI.ExactDerandomization.Net.Quest.wall0 line 220
  48. lemma OAI.ExactDerandomization.Net.Quest.dammed line 225
  49. lemma OAI.ExactDerandomization.Net.Quest.ampl line 228
  50. def OAI.ExactDerandomization.Net.Peek.plan line 237
  51. def OAI.ExactDerandomization.Net.Peek.key line 238
  52. def OAI.ExactDerandomization.Net.Peek.stair line 239
  53. def OAI.ExactDerandomization.Net.Peek.ready line 240
  54. def OAI.ExactDerandomization.Net.Peek.pursue line 245
  55. def OAI.ExactDerandomization.Net.Peek.wear line 249
  56. structure OAI.ExactDerandomization.Net.Surround line 264
  57. lemma OAI.ExactDerandomization.Net.surround_exists line 268
  58. structure OAI.ExactDerandomization.Net.Tonic line 277
  59. def OAI.ExactDerandomization.Net.width line 287
  60. abbrev OAI.ExactDerandomization.Net.Tonic.size line 290
  61. lemma OAI.ExactDerandomization.Net.Tonic.size1 line 291
  62. lemma OAI.ExactDerandomization.Net.Tonic.fee line 292
  63. lemma OAI.ExactDerandomization.Net.tonic_up line 297
  64. lemma OAI.ExactDerandomization.Net.Quest.kept line 332
  65. lemma OAI.ExactDerandomization.Net.Quest.canon line 337
  66. lemma OAI.ExactDerandomization.Net.Quest.covered line 340
  67. abbrev OAI.ExactDerandomization.Net.Quest.axle line 346
  68. lemma OAI.ExactDerandomization.Net.Quest.form0 line 348
  69. lemma OAI.ExactDerandomization.Net.Quest.free_mean line 390
  70. structure OAI.ExactDerandomization.Net.Tick line 447
  71. abbrev OAI.ExactDerandomization.Net.Roll line 450
  72. def OAI.ExactDerandomization.Net.Tick.empty line 452
  73. abbrev OAI.ExactDerandomization.Net.detector line 453
  74. abbrev OAI.ExactDerandomization.Net.prizep line 454
  75. def OAI.ExactDerandomization.Net.oracle line 456
  76. def OAI.ExactDerandomization.Net.leaderP line 458
  77. def OAI.ExactDerandomization.Net.carrier line 459
  78. def OAI.ExactDerandomization.Net.Quest.tower line 464
  79. def OAI.ExactDerandomization.Net.Quest.tray line 467
  80. structure OAI.ExactDerandomization.Net.Quest.Batch line 469
  81. def OAI.ExactDerandomization.Net.Quest.previous line 473
  82. def OAI.ExactDerandomization.Net.Quest.binReq line 476
  83. def OAI.ExactDerandomization.Net.Quest.bend line 477
  84. def OAI.ExactDerandomization.Net.Quest.binsV line 480
  85. def OAI.ExactDerandomization.Net.Quest.localR line 482
  86. def OAI.ExactDerandomization.Net.Quest.shareR line 485
  87. def OAI.ExactDerandomization.Net.Quest.cutR line 491
  88. def OAI.ExactDerandomization.Net.Quest.company line 496
  89. def OAI.ExactDerandomization.Net.Quest.sign line 500
  90. def OAI.ExactDerandomization.Net.Quest.pipe line 504
  91. def OAI.ExactDerandomization.Net.Quest.briq line 507
  92. def OAI.ExactDerandomization.Net.Quest.divided line 509
  93. def OAI.ExactDerandomization.Net.Quest.fleet line 514
  94. def OAI.ExactDerandomization.Net.Quest.inbound line 515
  95. def OAI.ExactDerandomization.Net.Quest.agency line 522
  96. def OAI.ExactDerandomization.Net.Quest.blankLine line 525
  97. def OAI.ExactDerandomization.Net.Quest.start line 526
  98. def OAI.ExactDerandomization.Net.Quest.fore line 536
  99. def OAI.ExactDerandomization.Net.Quest.companion line 537
  100. def OAI.ExactDerandomization.Net.Quest.flame line 542
  101. def OAI.ExactDerandomization.Net.Quest.rowBlock line 544
  102. def OAI.ExactDerandomization.Net.Quest.activeR line 547
  103. def OAI.ExactDerandomization.Net.Peek.score line 554
  104. def OAI.ExactDerandomization.Net.Peek.di line 555
  105. def OAI.ExactDerandomization.Net.Peek.bay line 561
  106. def OAI.ExactDerandomization.Net.Peek.primeQ line 562
  107. def OAI.ExactDerandomization.Net.Peek.syncQ line 566
  108. def OAI.ExactDerandomization.Net.Peek.roy line 575
  109. def OAI.ExactDerandomization.Net.Peek.weave line 579
  110. def OAI.ExactDerandomization.Net.Peek.activeV line 586
  111. def OAI.ExactDerandomization.Net.onQ line 590
  112. def OAI.ExactDerandomization.Net.current line 591
  113. def OAI.ExactDerandomization.Net.rolls line 595
  114. def OAI.ExactDerandomization.Net.forecast line 598
  115. lemma OAI.ExactDerandomization.Net.vault line 600
  116. def OAI.ExactDerandomization.Net.Tonic.bank line 621
  117. def OAI.ExactDerandomization.Net.Tonic.ticket line 622
  118. def OAI.ExactDerandomization.Net.Tonic.clergy line 623
  119. def OAI.ExactDerandomization.Net.Tonic.natural line 624
  120. lemma OAI.ExactDerandomization.Net.Tonic.four line 626
  121. lemma OAI.ExactDerandomization.Net.Tonic.positiveT line 628
  122. lemma OAI.ExactDerandomization.Net.Tonic.positiveC line 629
  123. structure OAI.ExactDerandomization.Net.Purse line 633
  124. lemma OAI.ExactDerandomization.Net.finance line 655
  125. def OAI.ExactDerandomization.Net.Purse.prize line 668
  126. def OAI.ExactDerandomization.Net.Purse.venture line 669
  127. def OAI.ExactDerandomization.Net.Purse.askFor line 671
  128. lemma OAI.ExactDerandomization.Net.Purse.one_peak line 673
  129. lemma OAI.ExactDerandomization.Net.Purse.toll_ok line 674
  130. lemma OAI.ExactDerandomization.Net.Purse.prize_pos line 675
  131. lemma OAI.ExactDerandomization.Net.Purse.credit line 680
  132. structure OAI.ExactDerandomization.Net.Trust line 694
  133. structure OAI.ExactDerandomization.Net.Tuned line 704
  134. structure OAI.ExactDerandomization.Net.Tuned.Connection line 712
  135. lemma OAI.ExactDerandomization.Net.Tuned.estimate line 716
  136. lemma OAI.ExactDerandomization.Net.Tuned.path line 726
  137. lemma OAI.ExactDerandomization.Net.Tuned.route line 731
  138. lemma OAI.ExactDerandomization.Net.Tuned.election line 738
  139. abbrev OAI.ExactDerandomization.Net.Quest.goal line 783
  140. lemma OAI.ExactDerandomization.Net.Quest.leavable line 784
  141. lemma OAI.ExactDerandomization.Net.Quest.cutaway line 785
  142. lemma OAI.ExactDerandomization.Net.Quest.fuelCap line 787
  143. lemma OAI.ExactDerandomization.Net.Quest.trayBudget line 793
  144. lemma OAI.ExactDerandomization.Net.Quest.security line 801
  145. lemma OAI.ExactDerandomization.Net.Quest.ownedValid line 804
  146. lemma OAI.ExactDerandomization.Net.Quest.amount line 814
  147. lemma OAI.ExactDerandomization.Net.Quest.slug line 822
  148. lemma OAI.ExactDerandomization.Net.Quest.vapor line 825
  149. lemma OAI.ExactDerandomization.Net.Quest.unscale line 828
  150. lemma OAI.ExactDerandomization.Net.Quest.transit line 842
  151. lemma OAI.ExactDerandomization.Net.Quest.valid_E line 856
  152. lemma OAI.ExactDerandomization.Net.Quest.complete line 893
  153. lemma OAI.ExactDerandomization.Net.peek_U line 905
  154. def OAI.ExactDerandomization.Net.Quest.Befit line 950
  155. lemma OAI.ExactDerandomization.Net.Quest.Befit.outer line 954
  156. lemma OAI.ExactDerandomization.Net.Quest.Befit.count line 960
  157. lemma OAI.ExactDerandomization.Net.Quest.Befit.pos line 966
  158. lemma OAI.ExactDerandomization.Net.Quest.Befit.equal line 971
  159. lemma OAI.ExactDerandomization.Net.Quest.Befit.ports line 985
  160. lemma OAI.ExactDerandomization.Net.Quest.prev0 line 995
  161. lemma OAI.ExactDerandomization.Net.Quest.Befit.covering line 998
  162. lemma OAI.ExactDerandomization.Net.Quest.eddy line 1031
  163. lemma OAI.ExactDerandomization.Net.Quest.eddy_rank line 1038
  164. lemma OAI.ExactDerandomization.Net.Quest.BendOK line 1045
  165. lemma OAI.ExactDerandomization.Net.Quest.BendRank line 1051
  166. lemma OAI.ExactDerandomization.Net.ratioN_self line 1075
  167. abbrev OAI.ExactDerandomization.Net.Quest.ideal line 1082
  168. abbrev OAI.ExactDerandomization.Net.Quest.grant line 1083
  169. lemma OAI.ExactDerandomization.Net.Quest.hpure line 1085
  170. lemma OAI.ExactDerandomization.Net.Quest.transact line 1091

    Source comment

    standard authorization for first-channel line, in deterministic unscaled units.
    lemma transact (v:Purse T) (he:s.SetUp) (h:q.ready s M) {L:Line n} {k}
    (P : Mat) (a : ℕ→ Pics n) (g : Pics n) (_:Pics n)
    (hs:L.seq=fun m=> (q.plan s).carry k (a m)) (hA:L.account=fun x y=>P x y/rate q.a)
    (ha:a 0=fun _ _ _=>0)
    (hI:∀ i ∈ (q.plan s).S,∀ j∈(q.plan s).S,
         rate k*((q.plan s).narrowed (nar q.a k)).fm g i j=P i j)
    (hH:∀ i∈(q.plan s).S,∀ j∈(q.plan s).S,P i j ≤ v.ceil * (q.question s).G i j)
    (hK:2^nar q.a k≤n) (hp:RCap v.ceil g) (hr:(q.plan s).pinned (nar q.a k) g)
    (hR:∀ m≤ M-(q.stair s M).cut k,RCap v.ceil (a m) ∧ (q.plan s).pinned (nar q.a k) (a m) ∧
             ((q.plan s).narrowed (nar q.a k)).terr g (a m) ≤ v.slip*(q.stair s M).theta m k) :
    q.grant v M k L := by
…

    Mentions: OAI.ExactDerandomization.Net.Purse, OAI.ExactDerandomization.L

  171. lemma OAI.ExactDerandomization.Net.Quest.direct line 1118
  172. lemma OAI.ExactDerandomization.Net.Quest.Befit.staying line 1158
  173. lemma OAI.ExactDerandomization.Net.Quest.Befit.negative line 1178
  174. lemma OAI.ExactDerandomization.Net.Quest.Befit.pooled line 1221
  175. def OAI.ExactDerandomization.Net.Quest.scrap line 1324
  176. lemma OAI.ExactDerandomization.Net.Quest.trayDust line 1326
  177. lemma OAI.ExactDerandomization.Net.Quest.massCover line 1336
  178. lemma OAI.ExactDerandomization.Net.Quest.pipeDust line 1354
  179. lemma OAI.ExactDerandomization.Net.Quest.cap_heat line 1427
  180. lemma OAI.ExactDerandomization.Net.Quest.wellPiped line 1452
  181. def OAI.ExactDerandomization.Net.candidate line 1490
  182. lemma OAI.ExactDerandomization.Net.castVote line 1492
  183. lemma OAI.ExactDerandomization.Net.candid line 1510
  184. lemma OAI.ExactDerandomization.Net.bounder line 1511
  185. lemma OAI.ExactDerandomization.Net.Scene.mature line 1518
  186. lemma OAI.ExactDerandomization.Net.Scene.reset line 1519
  187. lemma OAI.ExactDerandomization.Net.Scene.org line 1522
  188. lemma OAI.ExactDerandomization.Net.Scene.resid_mem line 1529
  189. lemma OAI.ExactDerandomization.Net.Quest.precinct line 1546
  190. abbrev OAI.ExactDerandomization.Net.Peek.envtarget line 1681
  191. lemma OAI.ExactDerandomization.Net.Peek.gaze line 1683
  192. lemma OAI.ExactDerandomization.Net.Peek.clear line 1687
  193. lemma OAI.ExactDerandomization.Net.Peek.shape line 1689
  194. abbrev OAI.ExactDerandomization.Net.Peek.owed line 1691
  195. lemma OAI.ExactDerandomization.Net.Peek.lensDue line 1694
  196. lemma OAI.ExactDerandomization.Net.Peek.stance line 1716
  197. lemma OAI.ExactDerandomization.Net.Peek.dueProbe line 1731
  198. lemma OAI.ExactDerandomization.Net.Peek.climb line 1803
  199. lemma OAI.ExactDerandomization.Net.Peek.dueStage line 1807
  200. lemma OAI.ExactDerandomization.Net.Peek.partners line 1822

    Source comment

    generic minting case of direct W and passV
    lemma partners (v:Purse T) (h:s.SetUp) (hr:Tuned T M r) (hp:q.ready s M)
    {l i : ℕ} (he:q.i=l+1) (hi:i< s.P.M) (u:Paint n) (p : Vec) (g:ℕ→Paint n)
    (h0:g 0=fun _ _=>0)
    (hd:∀ x∈(s.stage l).S,(s.mode l q.u l).vm u x=p x)
    {c a : ℝ} (ha:0≤a)
    (hb:∀ m≤M-(q.stair s M).cut q.i,∀ s i,|g m s i|≤a)
    (hh:∀ m≤M-(q.stair s M).cut q.i,(s.mode l q.u l).von (fun s i=>u s i-g m s i) ≤
                       c*(q.stair s M).theta m q.i)
    (hz:c+a*4*T.clergy≤ v.toll) :
   let F:=fun m=> vim s.P.M i (fame (carrier s r m l i) (g m))
…

    Mentions: OAI.ExactDerandomization.Net.Purse, OAI.ExactDerandomization.Net.Tuned, OAI.ExactDerandomization.Net.carrier

  201. lemma OAI.ExactDerandomization.Net.Peek.prior line 1880
  202. lemma OAI.ExactDerandomization.Net.Peek.ownsPrime line 1887
  203. lemma OAI.ExactDerandomization.Net.Peek.ownsMix line 1925
  204. lemma OAI.ExactDerandomization.Net.Peek.home line 1996
  205. lemma OAI.ExactDerandomization.Net.Quest.residual_copies line 2052
  206. lemma OAI.ExactDerandomization.Net.Quest.dues_in line 2122
  207. lemma OAI.ExactDerandomization.Net.Quest.owesFirst line 2134
  208. lemma OAI.ExactDerandomization.Net.Quest.lit line 2157
  209. lemma OAI.ExactDerandomization.Net.Quest.toothway line 2177
  210. lemma OAI.ExactDerandomization.Net.Quest.forerunner line 2186
  211. lemma OAI.ExactDerandomization.Net.Quest.foreground line 2189
  212. lemma OAI.ExactDerandomization.Net.Quest.owesBath line 2196
  213. lemma OAI.ExactDerandomization.Net.Quest.tepid line 2254
  214. lemma OAI.ExactDerandomization.Net.Quest.exhaust line 2263
  215. lemma OAI.ExactDerandomization.Net.Quest.rootBills line 2281
  216. lemma OAI.ExactDerandomization.Net.Quest.wallClock line 2314
  217. lemma OAI.ExactDerandomization.Net.Quest.threshold line 2319
  218. lemma OAI.ExactDerandomization.Net.Quest.lively line 2365
  219. lemma OAI.ExactDerandomization.Net.Quest.contents line 2416
  220. lemma OAI.ExactDerandomization.Net.Peek.owedPeek line 2461
  221. lemma OAI.ExactDerandomization.Net.Peek.objective line 2486
  222. lemma OAI.ExactDerandomization.Net.Peek.contentsPeek line 2490
  223. lemma OAI.ExactDerandomization.Net.origin0 line 2527
  224. lemma OAI.ExactDerandomization.Net.error_estimate line 2533

    Source documentation

    Error and finite-index bounds of the actual (no fingerprint) estimates by statistical budget recursion.

    lemma error_estimate (v:Purse T) (h:s.SetUp) (hw:v.askFor s.gap) (M) :
    Trust T M (forecast s M) := by
…

    Mentions: OAI.ExactDerandomization.Net.Purse, OAI.ExactDerandomization.Net.Trust, OAI.ExactDerandomization.Net.forecast