OAI/Computability/Logspace/CompressionBounds.lean

GitHub source file

171 declarations, 0 contain sorry, 0 declared as axioms

Row compression, shutdown thresholds, and accumulated approximation error.

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

  1. lemma OAI.ExactDerandomization.Buf.maxnear line 21

    Source comment

    scalar helpers
    lemma maxnear {x a y b t : ℝ}
    (h:|x-y| ≤ t) (e:|a-b|≤t) : |max x a-max y b| ≤ t := by
…
  2. lemma OAI.ExactDerandomization.Buf.minnear line 25
  3. lemma OAI.ExactDerandomization.Buf.absnear line 29
  4. lemma OAI.ExactDerandomization.Buf.addnear line 31
  5. lemma OAI.ExactDerandomization.Buf.subnear line 35
  6. lemma OAI.ExactDerandomization.Buf.sat_near line 39
  7. lemma OAI.ExactDerandomization.Buf.sat_id line 48
  8. lemma OAI.ExactDerandomization.Buf.sat_eq_min line 50
  9. lemma OAI.ExactDerandomization.Buf.sat_abs line 51
  10. lemma OAI.ExactDerandomization.Buf.sat_between line 58
  11. lemma OAI.ExactDerandomization.Buf.sat_size line 60
  12. lemma OAI.ExactDerandomization.Buf.sat_add line 61
  13. abbrev OAI.ExactDerandomization.Buf.Row line 69

    Source documentation

    Compression coordinate binary vector helpers.

    abbrev Row := ℕ → Pt
  14. def OAI.ExactDerandomization.Buf.ht line 70
  15. lemma OAI.ExactDerandomization.Buf.ht_nn line 71
  16. def OAI.ExactDerandomization.Buf.near line 72
  17. def OAI.ExactDerandomization.Buf.clp line 73
  18. lemma OAI.ExactDerandomization.Buf.ht_clp line 74
  19. lemma OAI.ExactDerandomization.Buf.near_ht line 76
  20. lemma OAI.ExactDerandomization.Buf.ht_near line 77
  21. lemma OAI.ExactDerandomization.Buf.near_self line 78
  22. lemma OAI.ExactDerandomization.Buf.near_le line 79
  23. lemma OAI.ExactDerandomization.Buf.near_add line 80
  24. lemma OAI.ExactDerandomization.Buf.near_sub line 82
  25. lemma OAI.ExactDerandomization.Buf.ht_add line 84
  26. lemma OAI.ExactDerandomization.Buf.ht_sub line 87
  27. abbrev OAI.ExactDerandomization.Buf.line line 89
  28. lemma OAI.ExactDerandomization.Buf.ht_line line 90
  29. def OAI.ExactDerandomization.Buf.suit line 92
  30. lemma OAI.ExactDerandomization.Buf.suit_self line 94
  31. lemma OAI.ExactDerandomization.Buf.suit0 line 95
  32. lemma OAI.ExactDerandomization.Buf.suit_rk line 104
  33. lemma OAI.ExactDerandomization.Buf.suit_val line 107
  34. lemma OAI.ExactDerandomization.Buf.rank_min line 111
  35. lemma OAI.ExactDerandomization.Buf.rank_sat line 133
  36. structure OAI.ExactDerandomization.Buf.Params line 163
  37. def OAI.ExactDerandomization.Buf.Params.U line 171
  38. def OAI.ExactDerandomization.Buf.Params.Z line 172
  39. lemma OAI.ExactDerandomization.Buf.Params.U_nn line 174
  40. lemma OAI.ExactDerandomization.Buf.Params.U_four line 175
  41. lemma OAI.ExactDerandomization.Buf.Params.U_old line 176
  42. lemma OAI.ExactDerandomization.Buf.Params.U_rho line 177
  43. lemma OAI.ExactDerandomization.Buf.Params.Z_w line 178
  44. lemma OAI.ExactDerandomization.Buf.Params.Z_nn line 181
  45. def OAI.ExactDerandomization.Buf.Params.push line 183
  46. lemma OAI.ExactDerandomization.Buf.Params.base_push line 191
  47. lemma OAI.ExactDerandomization.Buf.Params.nearbase line 193
  48. lemma OAI.ExactDerandomization.Buf.Params.offbase line 199
  49. def OAI.ExactDerandomization.Buf.Params.Between line 217
  50. lemma OAI.ExactDerandomization.Buf.Params.middle line 218
  51. lemma OAI.ExactDerandomization.Buf.Params.perturb line 228
  52. lemma OAI.ExactDerandomization.Buf.Params.U_near line 238
  53. lemma OAI.ExactDerandomization.Buf.Params.Z_near line 245
  54. lemma OAI.ExactDerandomization.Buf.Params.smooth_push line 254
  55. def OAI.ExactDerandomization.Buf.struck line 278
  56. lemma OAI.ExactDerandomization.Buf.strike_U line 280
  57. lemma OAI.ExactDerandomization.Buf.strike_rk line 285
  58. lemma OAI.ExactDerandomization.Buf.strike_Z line 289
  59. lemma OAI.ExactDerandomization.Buf.strike_push line 295
  60. lemma OAI.ExactDerandomization.Buf.strike_val line 332
  61. lemma OAI.ExactDerandomization.Buf.closed line 344

    Source documentation

    At gate-close baseline, any arrays represent zero row outputs.

    lemma closed {theta C f} {v:Blob} (h:TS theta C f) (he : theta/40 ≤ v.base)
   (S : Domain) (K i) : v.val S K f i=0 := by
…
  62. abbrev OAI.ExactDerandomization.Buf.mist line 361
  63. lemma OAI.ExactDerandomization.Buf.smallp line 362
  64. lemma OAI.ExactDerandomization.Buf.mistp line 363
  65. lemma OAI.ExactDerandomization.Buf.mist1 line 364
  66. lemma OAI.ExactDerandomization.Buf.mist_eta line 365
  67. lemma OAI.ExactDerandomization.Buf.mist_shut line 367
  68. def OAI.ExactDerandomization.Buf.Calm line 370
  69. lemma OAI.ExactDerandomization.Buf.Params.still_calm line 375
  70. lemma OAI.ExactDerandomization.Buf.Params.toprank line 383
  71. lemma OAI.ExactDerandomization.Buf.Params.hold_U line 398
  72. lemma OAI.ExactDerandomization.Buf.Params.hold_Z line 412
  73. lemma OAI.ExactDerandomization.Buf.Params.raising_rank line 415
  74. lemma OAI.ExactDerandomization.Buf.Params.same line 434
  75. lemma OAI.ExactDerandomization.Buf.Params.motionless line 447
  76. def OAI.ExactDerandomization.Buf.trim line 474
  77. lemma OAI.ExactDerandomization.Buf.trim_safe line 479

    Source documentation

    Positions with their first entry below mist are below sensitivity. Drop them to compare only the other positions.

    lemma trim_safe {theta C f} (h : TS theta C f) (ht: delta ≤ theta)
    (S F : Domain) {v:Blob} (he:v.base≤ mist)
    (hh : ∀ i∈S,i∉F → (v.ts i).1≤ mist) (K) {i} (hi:i∈S) :
    v.val S K f i=(trim F v).val S K f i := by
…

    Mentions: OAI.ExactDerandomization.Buf.ht, OAI.ExactDerandomization.Buf.mist, OAI.ExactDerandomization.Buf.trim

  78. structure OAI.ExactDerandomization.Buf.Run line 532
  79. abbrev OAI.ExactDerandomization.Buf.Run.pm line 543
  80. def OAI.ExactDerandomization.Buf.Run.pile line 545
  81. def OAI.ExactDerandomization.Buf.Run.shifted line 548
  82. def OAI.ExactDerandomization.Buf.Run.mid line 549
  83. def OAI.ExactDerandomization.Buf.Run.enter line 552
  84. lemma OAI.ExactDerandomization.Buf.Run.mid_succ line 553
  85. def OAI.ExactDerandomization.Buf.Run.loss line 554
  86. lemma OAI.ExactDerandomization.Buf.Run.total_enter line 555
  87. lemma OAI.ExactDerandomization.Buf.Run.iter_loss line 559
  88. def OAI.ExactDerandomization.Buf.Run.epi line 563
  89. def OAI.ExactDerandomization.Buf.Run.bad line 567
  90. lemma OAI.ExactDerandomization.Buf.Run.epi_nn line 568
  91. lemma OAI.ExactDerandomization.Buf.Run.bad_epi line 569
  92. lemma OAI.ExactDerandomization.Buf.Run.bad_nn line 574
  93. def OAI.ExactDerandomization.Buf.Run.dust line 576
  94. def OAI.ExactDerandomization.Buf.Run.rain line 577
  95. def OAI.ExactDerandomization.Buf.Run.overflow line 578
  96. def OAI.ExactDerandomization.Buf.Run.pre line 579
  97. structure OAI.ExactDerandomization.Buf.Run.Good line 581
  98. lemma OAI.ExactDerandomization.Buf.Run.base_mid line 590
  99. lemma OAI.ExactDerandomization.Buf.Run.dust_nn line 594
  100. lemma OAI.ExactDerandomization.Buf.Run.rain_nn line 596
  101. lemma OAI.ExactDerandomization.Buf.Run.dust_le line 601
  102. lemma OAI.ExactDerandomization.Buf.Run.dust_next line 605
  103. lemma OAI.ExactDerandomization.Buf.Run.rain_next line 606
  104. lemma OAI.ExactDerandomization.Buf.Run.rho_dust line 609
  105. lemma OAI.ExactDerandomization.Buf.Run.rho_mist line 613
  106. lemma OAI.ExactDerandomization.Buf.Run.literal line 617
  107. lemma OAI.ExactDerandomization.Buf.Run.pre_head line 628

    Source documentation

    preloss biggest bound, until the first overflow

    lemma pre_head (h:r.Good) {i} (hh:i≤r.L) (hp:r.pre i) :
   (r.mid i).base≤r.dust i ∧ ∀ x∈r.S, ht (r.loss i x) ≤ r.dust i := by
…

    Mentions: OAI.ExactDerandomization.Buf.ht

  108. lemma OAI.ExactDerandomization.Buf.Run.flag line 654

    Source documentation

    At a significant position changed during preloss, the prefix made definite relative error.

    lemma flag (h:r.Good) {i x} (hi:i<r.L) (hp:r.pre i) (hx:x∈r.S)
    (hs:¬r.overflow i) (hh:4*small≤(r.aim x).1)
    (he : (r.mid (i+1)).ts x ≠ (r.enter i).ts x) :
    small/4 ≤ r.bad i := by
…
  109. lemma OAI.ExactDerandomization.Buf.Run.pre_marks line 687
  110. def OAI.ExactDerandomization.Buf.Run.origin line 712
  111. def OAI.ExactDerandomization.Buf.Run.corrected line 713
  112. lemma OAI.ExactDerandomization.Buf.Run.start_calm line 714
  113. lemma OAI.ExactDerandomization.Buf.Run.rain_effect line 728
  114. lemma OAI.ExactDerandomization.Buf.suit_map line 773
  115. lemma OAI.ExactDerandomization.Buf.suit_idem line 786
  116. lemma OAI.ExactDerandomization.Buf.suit0_trans line 793
  117. lemma OAI.ExactDerandomization.Buf.suit0_symm line 797
  118. def OAI.ExactDerandomization.Buf.Run.die line 804
  119. def OAI.ExactDerandomization.Buf.Run.actual line 805
  120. abbrev OAI.ExactDerandomization.Buf.Run.taken line 810
  121. lemma OAI.ExactDerandomization.Buf.Run.actual_push line 813
  122. lemma OAI.ExactDerandomization.Buf.Run.actual_base line 814
  123. lemma OAI.ExactDerandomization.Buf.Run.actual_closed line 817
  124. def OAI.ExactDerandomization.Buf.Run.bridged line 823
  125. lemma OAI.ExactDerandomization.Buf.Run.cross_zero line 826
  126. lemma OAI.ExactDerandomization.Buf.Run.next_bridge line 840
  127. theorem OAI.ExactDerandomization.Buf.Run.clamped line 870
  128. lemma OAI.ExactDerandomization.Buf.Params.enough line 901
  129. lemma OAI.ExactDerandomization.Buf.Params.listed line 910
  130. lemma OAI.ExactDerandomization.Buf.Blobext line 932
  131. def OAI.ExactDerandomization.Buf.ears line 938

    Source documentation

    A comparison replacing very positive first coordinates by a bounded comparison sentinel.

    def ears (F : Domain) (L : ℝ) (v : Blob) : Blob :=
…

    Mentions: OAI.ExactDerandomization.L

  132. def OAI.ExactDerandomization.Buf.tall line 940
  133. lemma OAI.ExactDerandomization.Buf.tower_struck line 942
  134. lemma OAI.ExactDerandomization.Buf.towering line 954
  135. lemma OAI.ExactDerandomization.Buf.tower_push line 960
  136. lemma OAI.ExactDerandomization.Buf.tower_val line 982
  137. def OAI.ExactDerandomization.Buf.Run.wide line 991
  138. def OAI.ExactDerandomization.Buf.Run.steady line 993
  139. lemma OAI.ExactDerandomization.Buf.Run.steady_zero line 996
  140. lemma OAI.ExactDerandomization.Buf.Run.steady_push line 997
  141. lemma OAI.ExactDerandomization.Buf.Run.still_here_c line 1000
  142. lemma OAI.ExactDerandomization.Buf.Run.still_here line 1006
  143. lemma OAI.ExactDerandomization.Buf.Run.still_hi line 1017
  144. def OAI.ExactDerandomization.Buf.Run.Mild line 1036

    Source documentation

    Known large first values don't cross the capped thresholds when relative prefix errors are small. Keep track of the discrepancy from the raw prefix at such locations.

    def Mild (j) := ∀ i, j≤ i → i<r.L → r.bad i≤1/4
  145. lemma OAI.ExactDerandomization.Buf.Run.enter_tall line 1038
  146. def OAI.ExactDerandomization.Buf.hood line 1074
  147. def OAI.ExactDerandomization.Buf.blast line 1076
  148. lemma OAI.ExactDerandomization.Buf.blast_apply line 1078
  149. lemma OAI.ExactDerandomization.Buf.blast_add line 1079
  150. lemma OAI.ExactDerandomization.Buf.blast_sub line 1081
  151. lemma OAI.ExactDerandomization.Buf.hooded line 1083
  152. abbrev OAI.ExactDerandomization.Buf.Run.wideK line 1093

    Source documentation

    Absolute bounds when ears are sentinels.

    abbrev wideK (B : ℝ) := 1+4*B
  153. lemma OAI.ExactDerandomization.Buf.Run.hood_at line 1094
  154. lemma OAI.ExactDerandomization.Buf.Run.hood_prev line 1109
  155. lemma OAI.ExactDerandomization.Buf.Run.hood_init line 1121
  156. lemma OAI.ExactDerandomization.Buf.Run.hood_link line 1134
  157. def OAI.ExactDerandomization.Buf.Run.cloud line 1148

    Source documentation

    Envelope for propagation coefficient.

    def cloud (j i) := ∑ k ∈ Ico j (i+1),(32:ℝ)^(i-k)*r.bad k
  158. def OAI.ExactDerandomization.Buf.Run.tail line 1149
  159. lemma OAI.ExactDerandomization.Buf.Run.cloud_adj line 1150
  160. lemma OAI.ExactDerandomization.Buf.Run.cloud0 line 1156
  161. lemma OAI.ExactDerandomization.Buf.Run.cloud_step line 1157
  162. lemma OAI.ExactDerandomization.Buf.Run.cloud_bad line 1160
  163. lemma OAI.ExactDerandomization.Buf.Run.tail_bad line 1164
  164. lemma OAI.ExactDerandomization.Buf.Run.hood_cmp line 1171
  165. abbrev OAI.ExactDerandomization.Buf.Run.charge line 1200

    Source documentation

    Final pointwise estimate after starting before group j.

    abbrev charge (C : ℝ) := 16*C^3 * wideK (C+12)
…

    Mentions: OAI.ExactDerandomization.Buf.Run.wideK

  166. lemma OAI.ExactDerandomization.Buf.Run.wave line 1202
  167. def OAI.ExactDerandomization.Buf.Run.fatties line 1271
  168. def OAI.ExactDerandomization.Buf.Run.binge line 1272
  169. def OAI.ExactDerandomization.Buf.Run.hap line 1273
  170. lemma OAI.ExactDerandomization.Buf.Run.fake line 1275
  171. lemma OAI.ExactDerandomization.Buf.Run.earliest line 1339