OAI/Computability/Logspace/EstimatorBounds.lean

GitHub source file

347 declarations, 0 contain sorry, 0 declared as axioms

Fourth-root norms and integrated error estimates for the compressed estimator.

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

  1. def OAI.ExactDerandomization.Est.box line 22
  2. def OAI.ExactDerandomization.Est.dry line 23
  3. lemma OAI.ExactDerandomization.Est.box0 line 24
  4. lemma OAI.ExactDerandomization.Est.dry0 line 25
  5. lemma OAI.ExactDerandomization.Est.box_one line 26
  6. lemma OAI.ExactDerandomization.Est.dry_one line 27
  7. lemma OAI.ExactDerandomization.Est.boxP line 28
  8. lemma OAI.ExactDerandomization.Est.dryP line 29
  9. lemma OAI.ExactDerandomization.Est.boxM line 30
  10. lemma OAI.ExactDerandomization.Est.dryM line 31
  11. lemma OAI.ExactDerandomization.Est.unify line 32
  12. lemma OAI.ExactDerandomization.Est.reunite line 33
  13. lemma OAI.ExactDerandomization.Est.box_mono line 34
  14. lemma OAI.ExactDerandomization.Est.dry_mono line 36
  15. lemma OAI.ExactDerandomization.Est.exp_big line 39
  16. lemma OAI.ExactDerandomization.Est.box_big line 43
  17. lemma OAI.ExactDerandomization.Est.invsum line 45
  18. lemma OAI.ExactDerandomization.Est.thinSum line 50
  19. def OAI.ExactDerandomization.Est.gapD line 59

    Source documentation

    d-index of slack group number i, descending.

    def gapD (L i : ℕ) := 2^(L-1-i)

    Mentions: OAI.ExactDerandomization.L

  20. lemma OAI.ExactDerandomization.Est.gap_end line 60
  21. lemma OAI.ExactDerandomization.Est.gapD_pos line 61
  22. lemma OAI.ExactDerandomization.Est.gapD_succ line 62
  23. lemma OAI.ExactDerandomization.Est.gapD_mono line 65
  24. lemma OAI.ExactDerandomization.Est.gapD_tail line 68
  25. lemma OAI.ExactDerandomization.Est.binsum line 71
  26. lemma OAI.ExactDerandomization.Est.cyclo line 83
  27. def OAI.ExactDerandomization.Est.fexpo line 90

    Source documentation

    Abstract compression exponent packet with abundant room for both masked mean and false positives charges.

    def fexpo (b : ℕ) := b+100
  28. def OAI.ExactDerandomization.Est.cexpo line 91
  29. def OAI.ExactDerandomization.Est.floorR line 93
  30. def OAI.ExactDerandomization.Est.capacity line 94
  31. def OAI.ExactDerandomization.Est.liftB line 95
  32. def OAI.ExactDerandomization.Est.decay line 96
  33. def OAI.ExactDerandomization.Est.firm line 97
  34. lemma OAI.ExactDerandomization.Est.floor_pos line 99
  35. lemma OAI.ExactDerandomization.Est.lift_one line 100
  36. lemma OAI.ExactDerandomization.Est.decay_le line 101
  37. lemma OAI.ExactDerandomization.Est.cap_pos line 102
  38. lemma OAI.ExactDerandomization.Est.cap_K line 103
  39. lemma OAI.ExactDerandomization.Est.cap_box line 107
  40. lemma OAI.ExactDerandomization.Est.forfeit line 110
  41. lemma OAI.ExactDerandomization.Est.feed_power line 121
  42. lemma OAI.ExactDerandomization.Est.floor_lift line 128
  43. lemma OAI.ExactDerandomization.Est.firm_plain line 132
  44. lemma OAI.ExactDerandomization.Est.firm_big line 135
  45. lemma OAI.ExactDerandomization.Est.cyclone line 138
  46. lemma OAI.ExactDerandomization.Est.firm_tail line 144
  47. lemma OAI.ExactDerandomization.Est.min_chill line 164
  48. lemma OAI.ExactDerandomization.Est.first_bound line 168
  49. lemma OAI.ExactDerandomization.Est.totaldust line 171
  50. lemma OAI.ExactDerandomization.Est.freezeD line 177
  51. lemma OAI.ExactDerandomization.Est.lead_dust line 182
  52. abbrev OAI.ExactDerandomization.Est.X line 208
  53. abbrev OAI.ExactDerandomization.Est.src line 209
  54. abbrev OAI.ExactDerandomization.Est.dst line 210
  55. abbrev OAI.ExactDerandomization.Est.Vertex line 212
  56. abbrev OAI.ExactDerandomization.Est.TableF line 213
  57. def OAI.ExactDerandomization.Est.scaleM line 215
  58. lemma OAI.ExactDerandomization.Est.scaleM_nn line 216
  59. structure OAI.ExactDerandomization.Est.Axis line 218
  60. def OAI.ExactDerandomization.Est.Axis.VM line 227
  61. def OAI.ExactDerandomization.Est.Axis.TM line 230
  62. def OAI.ExactDerandomization.Est.Axis.vi line 233
  63. def OAI.ExactDerandomization.Est.Axis.ti line 234
  64. def OAI.ExactDerandomization.Est.Axis.von line 235
  65. def OAI.ExactDerandomization.Est.Axis.ton line 236
  66. def OAI.ExactDerandomization.Est.Axis.terr line 237
  67. lemma OAI.ExactDerandomization.Est.Axis.vi_apply line 240
  68. lemma OAI.ExactDerandomization.Est.Axis.ti_apply line 242
  69. lemma OAI.ExactDerandomization.Est.Axis.collapse line 245
  70. lemma OAI.ExactDerandomization.Est.Axis.vi_mono line 248
  71. lemma OAI.ExactDerandomization.Est.Axis.ti_mono line 252
  72. lemma OAI.ExactDerandomization.Est.Axis.conditional line 256
  73. lemma OAI.ExactDerandomization.Est.Axis.vi_const line 275
  74. lemma OAI.ExactDerandomization.Est.Axis.vi_one line 280
  75. lemma OAI.ExactDerandomization.Est.Axis.von_four line 294
  76. lemma OAI.ExactDerandomization.Est.Axis.ton_four line 295
  77. lemma OAI.ExactDerandomization.Est.panel_const line 299
  78. lemma OAI.ExactDerandomization.Est.Axis.tn0 line 320
  79. lemma OAI.ExactDerandomization.Est.Axis.vn0 line 321
  80. lemma OAI.ExactDerandomization.Est.Axis.tscale line 322
  81. lemma OAI.ExactDerandomization.Est.Axis.vscale line 324
  82. lemma OAI.ExactDerandomization.Est.Axis.tplus line 326
  83. lemma OAI.ExactDerandomization.Est.Axis.vplus line 328
  84. lemma OAI.ExactDerandomization.Est.Axis.tseries line 330
  85. lemma OAI.ExactDerandomization.Est.Axis.vseries line 338
  86. lemma OAI.ExactDerandomization.Est.Axis.tm_le line 347
  87. lemma OAI.ExactDerandomization.Est.Axis.vm_le line 349
  88. lemma OAI.ExactDerandomization.Est.Axis.torder line 352
  89. lemma OAI.ExactDerandomization.Est.Axis.vorder line 359
  90. lemma OAI.ExactDerandomization.Est.Axis.vi_nn line 364
  91. lemma OAI.ExactDerandomization.Est.Axis.ti_nn line 367
  92. lemma OAI.ExactDerandomization.Est.Axis.tmul line 371
  93. lemma OAI.ExactDerandomization.Est.Axis.vmul line 372
  94. def OAI.ExactDerandomization.Est.Axis.head line 376

    Source documentation

    Evaluate head of a row (L4 sum over columns), a convenient alternative to suprema that still bounds them.

    def head (f : TableF n w) : Vertex n w :=
…

    Mentions: OAI.ExactDerandomization.Est.TableF, OAI.ExactDerandomization.Est.Vertex

  95. lemma OAI.ExactDerandomization.Est.Axis.head_nn line 378
  96. lemma OAI.ExactDerandomization.Est.Axis.head_ge line 379
  97. lemma OAI.ExactDerandomization.Est.Axis.head_e line 387
  98. lemma OAI.ExactDerandomization.Est.Axis.head_mask line 392
  99. abbrev OAI.ExactDerandomization.Est.Axis.narrowed line 398

    Source documentation

    mask a deterministic array to possibly narrower terminal slices.

    abbrev narrowed (a : ℕ) : Axis := {d with a:=a}

    Mentions: OAI.ExactDerandomization.Est.Axis

  100. def OAI.ExactDerandomization.Est.Axis.wmask line 399
  101. lemma OAI.ExactDerandomization.Est.Axis.ti_mask line 401
  102. lemma OAI.ExactDerandomization.Est.Axis.tmask_power line 415
  103. lemma OAI.ExactDerandomization.Est.Axis.tmask line 422
  104. abbrev OAI.ExactDerandomization.Est.Pool line 444
  105. abbrev OAI.ExactDerandomization.Est.Pics line 445
  106. abbrev OAI.ExactDerandomization.Est.Paint line 446
  107. lemma OAI.ExactDerandomization.Est.pct_c0 line 449

    Source documentation

    index-based probability scale factoring

    lemma pct_c0 (n : ℕ) [Fact n.Prime] : pct n 0=1 := by
…
  108. lemma OAI.ExactDerandomization.Est.rr line 452
  109. def OAI.ExactDerandomization.Est.Axis.fm line 457
  110. def OAI.ExactDerandomization.Est.Axis.vm line 459
  111. def OAI.ExactDerandomization.Est.Axis.fw line 462
  112. def OAI.ExactDerandomization.Est.Axis.vw line 465
  113. lemma OAI.ExactDerandomization.Est.Axis.fdet line 468
  114. lemma OAI.ExactDerandomization.Est.Axis.vdet line 469
  115. lemma OAI.ExactDerandomization.Est.Axis.fscalar line 470
  116. lemma OAI.ExactDerandomization.Est.Axis.fmean_sub line 472
  117. lemma OAI.ExactDerandomization.Est.Axis.vmean_sub line 475
  118. lemma OAI.ExactDerandomization.Est.Axis.goodfm line 478
  119. lemma OAI.ExactDerandomization.Est.Axis.eqfm line 488
  120. lemma OAI.ExactDerandomization.Est.Axis.eqvm line 495
  121. lemma OAI.ExactDerandomization.Est.Axis.ite_wmask line 501
  122. lemma OAI.ExactDerandomization.Est.Axis.fpivot line 514
  123. lemma OAI.ExactDerandomization.Est.Axis.vpivot line 517
  124. lemma OAI.ExactDerandomization.Est.Axis.ftest line 527
  125. lemma OAI.ExactDerandomization.Est.Axis.vtest line 533
  126. lemma OAI.ExactDerandomization.Est.Axis.fnorm line 537
  127. lemma OAI.ExactDerandomization.Est.Axis.vnorm line 543
  128. lemma OAI.ExactDerandomization.Est.Axis.froot line 549
  129. lemma OAI.ExactDerandomization.Est.Axis.fswap_det line 558
  130. lemma OAI.ExactDerandomization.Est.shrink line 585
  131. lemma OAI.ExactDerandomization.Est.swell line 590
  132. lemma OAI.ExactDerandomization.Est.odds line 593
  133. abbrev OAI.ExactDerandomization.Est.nar line 604
  134. def OAI.ExactDerandomization.Est.salary line 605
  135. def OAI.ExactDerandomization.Est.loaded line 606
  136. def OAI.ExactDerandomization.Est.distn line 607
  137. lemma OAI.ExactDerandomization.Est.paypos line 608
  138. lemma OAI.ExactDerandomization.Est.coarse_pay line 612
  139. lemma OAI.ExactDerandomization.Est.cost_pos line 615
  140. lemma OAI.ExactDerandomization.Est.burden line 619
  141. def OAI.ExactDerandomization.Est.RCap line 636

    Source documentation

    uniformly bounded, in roots

    def RCap (K : ℝ) (f : Pics n) := ∀ s i j,0≤ f s i j ∧ fourth (f s i j) ≤ K
…

    Mentions: OAI.ExactDerandomization.Est.Pics

  142. lemma OAI.ExactDerandomization.Est.from_cap line 639
  143. def OAI.ExactDerandomization.Est.Axis.carry line 646
  144. def OAI.ExactDerandomization.Est.Axis.pinned line 649
  145. lemma OAI.ExactDerandomization.Est.Axis.ton_subnorm line 651
  146. lemma OAI.ExactDerandomization.Est.Axis.ton_ext line 652
  147. lemma OAI.ExactDerandomization.Est.Axis.root_fee line 661
  148. lemma OAI.ExactDerandomization.Est.Axis.unit_change line 671
  149. lemma OAI.ExactDerandomization.Est.Axis.mean_move line 688
  150. lemma OAI.ExactDerandomization.Est.Axis.carry_change line 694
  151. abbrev OAI.ExactDerandomization.Est.Axis.paycheck line 700
  152. lemma OAI.ExactDerandomization.Est.Axis.stream_fee line 704

    Source documentation

    Comparison of one conditioned first-channel contribution.

    lemma stream_fee {k : ℕ} (hp: 2^(nar d.a k)≤n) {K : ℝ} (hK:1≤K) {f g : Pics n}
    (hf:RCap K f) (hg:RCap K g)
    (hf':d.pinned (nar d.a k) f) (hg':d.pinned (nar d.a k) g)
    {D : Mat} (hD:∀ i∈d.S,∀ j∈d.S, 0≤D i j)
    (hb:∀ i∈d.S,∀ j∈d.S,d.fm (d.carry k f) i j≤K*D i j) :
    d.ton (n:=n) (w:=0) (fun _ i j=> rel (d.fm (d.carry k f) i j-
…

    Mentions: OAI.ExactDerandomization.Est.nar, OAI.ExactDerandomization.Est.Pics, OAI.ExactDerandomization.Est.RCap

  153. lemma OAI.ExactDerandomization.Est.Axis.realize_pin line 794
  154. lemma OAI.ExactDerandomization.Est.Axis.raw_fee line 800
  155. lemma OAI.ExactDerandomization.Est.Axis.fine_tail line 832

    Source documentation

    One collective loss of a wholly fine tail. X/rate d.a are the raw units.

    lemma fine_tail {X0 : Mat} {K : ℝ} {m : ℕ}
    (hK:1≤K) (hp : 2^d.a ≤ n) (hv : 2^d.u ≤ n)
    (hC:d.S.card≤d.N)
    (he:∀ i∈d.S,∀ j∈d.S,0≤X0 i j ∧ X0 i j ≤ K*rate (d.a+m))
    (hr:∀ i∈d.S,∑ j∈d.S,X0 i j ≤ K) :
    d.ton (n:=n) (w:=0) (fun _ i j=> X0 i j / rate d.a) ≤ 4*K*dry m^3 := by
…

    Mentions: OAI.ExactDerandomization.Est.dry

  156. instance OAI.ExactDerandomization.Est.s_one line 900
  157. lemma OAI.ExactDerandomization.Est.empty_seam line 901
  158. def OAI.ExactDerandomization.Est.ebb line 918
  159. lemma OAI.ExactDerandomization.Est.ebb_nn line 919
  160. def OAI.ExactDerandomization.Est.Wind line 924

    Source documentation

    lam = walk length per unit statistical slack.

    def Wind (e lam : ℕ) : Prop := ebb^lam*16≤dry e^4

    Mentions: OAI.ExactDerandomization.Est.ebb, OAI.ExactDerandomization.Est.dry

  161. lemma OAI.ExactDerandomization.Est.find_lam line 925
  162. lemma OAI.ExactDerandomization.Est.blow line 929
  163. lemma OAI.ExactDerandomization.Est.blows line 942
  164. def OAI.ExactDerandomization.Est.Axis.fluke line 965
  165. def OAI.ExactDerandomization.Est.Axis.vluke line 967
  166. lemma OAI.ExactDerandomization.Est.Axis.windF line 970
  167. lemma OAI.ExactDerandomization.Est.Axis.windV line 978
  168. lemma OAI.ExactDerandomization.Est.into_range line 988
  169. lemma OAI.ExactDerandomization.Est.magnitude line 1003
  170. structure OAI.ExactDerandomization.Est.StepKey line 1028
  171. def OAI.ExactDerandomization.Est.allowance line 1033
  172. def OAI.ExactDerandomization.Est.active line 1035
  173. def OAI.ExactDerandomization.Est.StepKey.allowanceStep line 1040
  174. def OAI.ExactDerandomization.Est.StepKey.token line 1041
  175. lemma OAI.ExactDerandomization.Est.StepKey.allow_p line 1042
  176. lemma OAI.ExactDerandomization.Est.StepKey.token_p line 1043
  177. lemma OAI.ExactDerandomization.Est.StepKey.inactive line 1045
  178. lemma OAI.ExactDerandomization.Est.StepKey.lower line 1050
  179. lemma OAI.ExactDerandomization.Est.StepKey.budget_gap line 1060
  180. lemma OAI.ExactDerandomization.Est.StepKey.transfer line 1067
  181. lemma OAI.ExactDerandomization.Est.StepKey.adjust line 1076
  182. lemma OAI.ExactDerandomization.Est.StepKey.divide line 1092
  183. lemma OAI.ExactDerandomization.Est.StepKey.raw_pay line 1118
  184. lemma OAI.ExactDerandomization.Est.StepKey.unbias line 1140
  185. lemma OAI.ExactDerandomization.Est.breeze_charge line 1157

    Source documentation

    coefficient remainders when summing all scale offsets/slack levels

    lemma breeze_charge (s d : ℕ) (h : d≤ s) :
    box (8*s)* dry (18*s) ≤ dry (8*d)*dry s := by
…

    Mentions: OAI.ExactDerandomization.Est.box, OAI.ExactDerandomization.Est.dry

  186. abbrev OAI.ExactDerandomization.Est.lull line 1162
  187. lemma OAI.ExactDerandomization.Est.low_total line 1164
  188. lemma OAI.ExactDerandomization.Est.scale_total line 1179
  189. structure OAI.ExactDerandomization.Est.Stair line 1229

    Source documentation

    Recipe-independent additive schedule.

    structure Stair where
…
  190. def OAI.ExactDerandomization.Est.Stair.L line 1238
  191. lemma OAI.ExactDerandomization.Est.Stair.length_pos line 1239
  192. def OAI.ExactDerandomization.Est.Stair.gap line 1240
  193. def OAI.ExactDerandomization.Est.Stair.cut line 1241
  194. def OAI.ExactDerandomization.Est.Stair.reach line 1244

    Source documentation

    budget reached by group i. Difference indices m denote the paired evaluation at m+1 and m.

    def reach (k i : ℕ) := s.M-max (s.gap i) (s.cut k)
  195. def OAI.ExactDerandomization.Est.Stair.yoke line 1245
  196. def OAI.ExactDerandomization.Est.Stair.layers line 1249
  197. def OAI.ExactDerandomization.Est.Stair.slack line 1250
  198. def OAI.ExactDerandomization.Est.Stair.theta line 1251
  199. def OAI.ExactDerandomization.Est.Stair.wide line 1252
  200. lemma OAI.ExactDerandomization.Est.Stair.wide_nn line 1254
  201. lemma OAI.ExactDerandomization.Est.Stair.theta_nn line 1255
  202. lemma OAI.ExactDerandomization.Est.Stair.last line 1256
  203. lemma OAI.ExactDerandomization.Est.Stair.reach_le line 1257
  204. lemma OAI.ExactDerandomization.Est.Stair.reach_M line 1259
  205. lemma OAI.ExactDerandomization.Est.Stair.reach_loss line 1260
  206. lemma OAI.ExactDerandomization.Est.Stair.under line 1261
  207. lemma OAI.ExactDerandomization.Est.Stair.precision line 1269
  208. lemma OAI.ExactDerandomization.Est.Stair.cheap line 1275
  209. lemma OAI.ExactDerandomization.Est.Stair.full line 1281
  210. lemma OAI.ExactDerandomization.Est.Stair.pegged line 1298
  211. lemma OAI.ExactDerandomization.Est.Stair.slack_plan line 1307
  212. lemma OAI.ExactDerandomization.Est.Stair.union_sum line 1317
  213. def OAI.ExactDerandomization.Est.toll line 1337
  214. lemma OAI.ExactDerandomization.Est.rel_nn line 1338
  215. lemma OAI.ExactDerandomization.Est.toll_nn line 1339
  216. lemma OAI.ExactDerandomization.Est.rel_tip line 1340
  217. lemma OAI.ExactDerandomization.Est.toll_tip line 1344
  218. lemma OAI.ExactDerandomization.Est.rel_subadd line 1345
  219. lemma OAI.ExactDerandomization.Est.toll_add line 1352
  220. lemma OAI.ExactDerandomization.Est.toll_minus line 1356
  221. lemma OAI.ExactDerandomization.Est.toll_sum line 1357
  222. structure OAI.ExactDerandomization.Est.Line line 1365
  223. def OAI.ExactDerandomization.Est.Line.shake line 1372
  224. def OAI.ExactDerandomization.Est.Line.pick line 1373
  225. def OAI.ExactDerandomization.Est.Line.wear line 1374
  226. def OAI.ExactDerandomization.Est.Line.waveR line 1375
  227. def OAI.ExactDerandomization.Est.Line.weatherR line 1377
  228. lemma OAI.ExactDerandomization.Est.Line.zeroWeather line 1380
  229. lemma OAI.ExactDerandomization.Est.Line.runoff line 1381
  230. lemma OAI.ExactDerandomization.Est.Line.storm line 1396
  231. structure OAI.ExactDerandomization.Est.Line.Due line 1402

    Source documentation

    Guarantees for one additive ray.

    structure Due (s : Stair) (k : ℕ) (d : Axis) (D : Mat)
     (b : Bool) (c : ℝ) (f : Line n) : Prop where
…

    Mentions: OAI.ExactDerandomization.Est.Stair, OAI.ExactDerandomization.Est.Axis, OAI.ExactDerandomization.Est.Line

  232. lemma OAI.ExactDerandomization.Est.Line.Due.enlarge line 1412
  233. lemma OAI.ExactDerandomization.Est.Line.winning line 1422
  234. lemma OAI.ExactDerandomization.Est.Line.foggy line 1430
  235. lemma OAI.ExactDerandomization.Est.opposing line 1486
  236. lemma OAI.ExactDerandomization.Est.joint line 1491
  237. lemma OAI.ExactDerandomization.Est.Line.Due.negR line 1500
  238. lemma OAI.ExactDerandomization.Est.Line.plain line 1514

    Source documentation

    Build unscaled strand, including a column rank or vector mean, from ordinary discrepancy of its full estimates to true pre-mean inputs.

    lemma plain {s : Stair} {f:Line n} {d : Axis} {D b c}
    (h:0≤c) {g:Pics n} (hd:∀ i∈d.S,∀ j∈d.S,0≤D i j)
    (hs:f.seq 0 = fun _ _ _=>0) (ht:∀ i∈d.S,∀ j∈d.S,d.fm g i j=f.account i j)
    (he:∀ m ≤ s.M-s.cut s.key.a,d.ton (fun u i j=>g u i j-f.seq m u i j) ≤
                  c*s.theta m s.key.a) : Due s s.key.a d D b c f := by
…

    Mentions: OAI.ExactDerandomization.Est.Stair, OAI.ExactDerandomization.Est.Line, OAI.ExactDerandomization.Est.Axis, OAI.ExactDerandomization.Est.Pics, OAI.ExactDerandomization.Est.Line.Due

  239. lemma OAI.ExactDerandomization.Est.Line.principal line 1541
  240. abbrev OAI.ExactDerandomization.Est.Ray line 1597
  241. structure OAI.ExactDerandomization.Est.Flame line 1599
  242. def OAI.ExactDerandomization.Est.Flame.first line 1609
  243. def OAI.ExactDerandomization.Est.Flame.portion line 1610
  244. def OAI.ExactDerandomization.Est.Flame.bundle line 1613
  245. def OAI.ExactDerandomization.Est.Flame.prefixR line 1616
  246. def OAI.ExactDerandomization.Est.Flame.central line 1619
  247. def OAI.ExactDerandomization.Est.Flame.smoke line 1621
  248. lemma OAI.ExactDerandomization.Est.Flame.prefix0 line 1624
  249. lemma OAI.ExactDerandomization.Est.Flame.next line 1625
  250. def OAI.ExactDerandomization.Est.Flame.tail line 1639
  251. structure OAI.ExactDerandomization.Est.Flame.Owes line 1642
  252. lemma OAI.ExactDerandomization.Est.Flame.Owes.more line 1651
  253. lemma OAI.ExactDerandomization.Est.Flame.coupling line 1657
  254. abbrev OAI.ExactDerandomization.Est.Flame.contract line 1664
  255. lemma OAI.ExactDerandomization.Est.Flame.protocol line 1665
  256. lemma OAI.ExactDerandomization.Est.Flame.fumes line 1668
  257. def OAI.ExactDerandomization.Est.Flame.picture line 1678
  258. lemma OAI.ExactDerandomization.Est.Flame.pink line 1681
  259. lemma OAI.ExactDerandomization.Est.Flame.tip_noise line 1721
  260. structure OAI.ExactDerandomization.Est.Spray line 1745

    Source documentation

    Inputs to the compression estimate.

    structure Spray (n w : ℕ) [Fact n.Prime] where
…
  261. abbrev OAI.ExactDerandomization.Est.Spray.dst0 line 1760
  262. abbrev OAI.ExactDerandomization.Est.Spray.dst1 line 1761
  263. abbrev OAI.ExactDerandomization.Est.Spray.src0 line 1762
  264. def OAI.ExactDerandomization.Est.Spray.go line 1763
  265. def OAI.ExactDerandomization.Est.Spray.s1 line 1766
  266. def OAI.ExactDerandomization.Est.Spray.s2 line 1767
  267. def OAI.ExactDerandomization.Est.Spray.pay line 1768
  268. structure OAI.ExactDerandomization.Est.Spray.Works line 1770
  269. lemma OAI.ExactDerandomization.Est.Spray.ok line 1785
  270. lemma OAI.ExactDerandomization.Est.Spray.pay_pub line 1797
  271. def OAI.ExactDerandomization.Est.Spray.heavy line 1804
  272. lemma OAI.ExactDerandomization.Est.Spray.binge_bits line 1806
  273. def OAI.ExactDerandomization.Est.Spray.busy line 1809
  274. instance OAI.ExactDerandomization.Est.Spray.(instance at line 1811) line 1811
  275. lemma OAI.ExactDerandomization.Est.Spray.wrapped line 1812
  276. lemma OAI.ExactDerandomization.Est.Spray.cut_belly line 1815
  277. abbrev OAI.ExactDerandomization.Est.Spray.hefty line 1828
  278. lemma OAI.ExactDerandomization.Est.Spray.raid line 1829
  279. def OAI.ExactDerandomization.Est.Spray.mh line 1884
  280. def OAI.ExactDerandomization.Est.Spray.nh line 1885
  281. def OAI.ExactDerandomization.Est.Spray.both line 1886
  282. lemma OAI.ExactDerandomization.Est.Spray.mnn line 1888
  283. lemma OAI.ExactDerandomization.Est.Spray.nnn line 1889
  284. lemma OAI.ExactDerandomization.Est.Spray.bnn line 1890
  285. lemma OAI.ExactDerandomization.Est.Spray.pointed line 1891
  286. lemma OAI.ExactDerandomization.Est.Spray.nh_ub line 1900
  287. lemma OAI.ExactDerandomization.Est.Spray.mh_ub line 1902
  288. lemma OAI.ExactDerandomization.Est.Spray.both_ub line 1906
  289. def OAI.ExactDerandomization.Est.Spray.phantom line 1912
  290. lemma OAI.ExactDerandomization.Est.Spray.false_nn line 1914
  291. abbrev OAI.ExactDerandomization.Est.Spray.fc line 1915
  292. lemma OAI.ExactDerandomization.Est.Spray.false_ub line 1917
  293. def OAI.ExactDerandomization.Est.Spray.chip line 1957
  294. def OAI.ExactDerandomization.Est.Spray.chipV line 1959
  295. lemma OAI.ExactDerandomization.Est.Spray.chipH line 1962
  296. lemma OAI.ExactDerandomization.Est.Spray.busy_avg line 1966
  297. lemma OAI.ExactDerandomization.Est.Spray.slice_costa line 1987
  298. lemma OAI.ExactDerandomization.Est.Spray.masked_leaf line 2006
  299. lemma OAI.ExactDerandomization.Est.Spray.masked_ub line 2025
  300. def OAI.ExactDerandomization.Est.Spray.sky line 2050
  301. def OAI.ExactDerandomization.Est.Spray.clouds line 2052
  302. def OAI.ExactDerandomization.Est.Spray.trail line 2054
  303. def OAI.ExactDerandomization.Est.Spray.march line 2056
  304. def OAI.ExactDerandomization.Est.Spray.rim line 2058
  305. def OAI.ExactDerandomization.Est.Spray.thunder line 2060
  306. def OAI.ExactDerandomization.Est.Spray.beasts line 2062
  307. def OAI.ExactDerandomization.Est.Spray.sumB line 2064
  308. lemma OAI.ExactDerandomization.Est.Spray.sky_nn line 2067
  309. lemma OAI.ExactDerandomization.Est.Spray.clouds_nn line 2069
  310. lemma OAI.ExactDerandomization.Est.Spray.trail_nn line 2070
  311. lemma OAI.ExactDerandomization.Est.Spray.march_nn line 2072
  312. lemma OAI.ExactDerandomization.Est.Spray.rim_nn line 2073
  313. lemma OAI.ExactDerandomization.Est.Spray.thunder_nn line 2074
  314. lemma OAI.ExactDerandomization.Est.Spray.beasts_nn line 2076
  315. lemma OAI.ExactDerandomization.Est.Spray.sumB_nn line 2077
  316. lemma OAI.ExactDerandomization.Est.Spray.cloud_plan line 2081
  317. lemma OAI.ExactDerandomization.Est.Spray.tail_route line 2089
  318. def OAI.ExactDerandomization.Est.Spray.diff line 2114
  319. lemma OAI.ExactDerandomization.Est.Spray.receipt line 2118
  320. abbrev OAI.ExactDerandomization.Est.Spray.droplets line 2166
  321. lemma OAI.ExactDerandomization.Est.Spray.vgeo line 2167
  322. lemma OAI.ExactDerandomization.Est.Spray.droplets_ub line 2175
  323. lemma OAI.ExactDerandomization.Est.Spray.beasts_ub line 2193
  324. lemma OAI.ExactDerandomization.Est.Spray.thunder_ub line 2202
  325. lemma OAI.ExactDerandomization.Est.Spray.rim_ub line 2210
  326. lemma OAI.ExactDerandomization.Est.Spray.march_ub line 2218
  327. def OAI.ExactDerandomization.Est.Spray.Bprice line 2237
  328. lemma OAI.ExactDerandomization.Est.Spray.bprice_pos line 2239
  329. lemma OAI.ExactDerandomization.Est.Spray.subtotal line 2244
  330. lemma OAI.ExactDerandomization.Est.Spray.charge_pos line 2257
  331. def OAI.ExactDerandomization.Est.Spray.localP line 2261
  332. theorem OAI.ExactDerandomization.Est.Spray.compress line 2266

    Source documentation

    Integrated buffered row estimate.

    theorem compress {p M theta C f} (h:s.Works p M) (hf:TS theta C f)
    (hz:delta≤theta) (hc:theta≤1) :
    s.d.ton (s.diff f) ≤localP s.K s.b C M*p := by
…

    Mentions: OAI.ExactDerandomization.Est.Spray.localP

  333. def OAI.ExactDerandomization.Est.Flame.spill line 2333
  334. lemma OAI.ExactDerandomization.Est.Flame.exact1 line 2342
  335. lemma OAI.ExactDerandomization.Est.Flame.exact2 line 2353
  336. lemma OAI.ExactDerandomization.Est.Flame.outputcard line 2367
  337. lemma OAI.ExactDerandomization.Est.Flame.earliestCost line 2370
  338. lemma OAI.ExactDerandomization.Est.Flame.ready line 2390
  339. def OAI.ExactDerandomization.Est.ridge line 2433

    Source documentation

    Use only diagonal of a picture as one vertex. Y conditioned nominally at rate 1, also pin at the diagonal for the mix.

    def ridge (f : Vec) : Mat := fun x y=> if x=y then f x else 0
  340. def OAI.ExactDerandomization.Est.core line 2434
  341. def OAI.ExactDerandomization.Est.diagP line 2435
  342. lemma OAI.ExactDerandomization.Est.Axis.diagh line 2439
  343. lemma OAI.ExactDerandomization.Est.Axis.diagonal line 2454
  344. lemma OAI.ExactDerandomization.Est.Axis.vproject line 2469
  345. def OAI.ExactDerandomization.Est.Axis.color line 2477
  346. lemma OAI.ExactDerandomization.Est.Axis.boundsC line 2479
  347. lemma OAI.ExactDerandomization.Est.Axis.drawn line 2484

    Source comment

    the group 1 slack answer of a vector flame.
    lemma drawn {s : Stair} {v:Flame n} {c : ℝ} (h : v.Owes s (d.narrowed 0) false c)
    {f : Vec} (hf:∀ x∈d.S,in01 (f x)) (he:∀ x∈d.S,v.lamp x x=f x) :
    d.von (fun u i=>d.color s v u i-f i) ≤ 6*Flame.contract s c := by
…

    Mentions: OAI.ExactDerandomization.Est.Stair, OAI.ExactDerandomization.Est.Flame, OAI.ExactDerandomization.Est.Flame.contract