OAI/Computability/Logspace/AffineSampling.lean

GitHub source file

361 declarations, 0 contain sorry, 0 declared as axioms

Finite averages, affine spectral gaps, and fourth-moment sampling estimates.

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

  1. def OAI.ExactDerandomization.Analysis.fourth line 22
  2. def OAI.ExactDerandomization.Analysis.Ic line 23
  3. def OAI.ExactDerandomization.Analysis.Lip line 25
  4. def OAI.ExactDerandomization.Analysis.smooth line 26
  5. def OAI.ExactDerandomization.Analysis.in01 line 27
  6. lemma OAI.ExactDerandomization.Analysis.fourth_nn line 29
  7. lemma OAI.ExactDerandomization.Analysis.fourth_four line 30
  8. lemma OAI.ExactDerandomization.Analysis.four_fourth line 32
  9. lemma OAI.ExactDerandomization.Analysis.Ic.lip line 35
  10. lemma OAI.ExactDerandomization.Analysis.unit_mem line 43
  11. lemma OAI.ExactDerandomization.Analysis.unit_ic line 45
  12. lemma OAI.ExactDerandomization.Analysis.exp4inc line 47
  13. lemma OAI.ExactDerandomization.Analysis.icUnitFour line 56
  14. def OAI.ExactDerandomization.Analysis.fade line 62
  15. lemma OAI.ExactDerandomization.Analysis.fade_low line 63
  16. lemma OAI.ExactDerandomization.Analysis.fade_symm line 67
  17. lemma OAI.ExactDerandomization.Analysis.fade_ic line 71
  18. lemma OAI.ExactDerandomization.Analysis.fade_bot line 76
  19. lemma OAI.ExactDerandomization.Analysis.fade_top line 80
  20. lemma OAI.ExactDerandomization.Analysis.fade_mem line 83
  21. def OAI.ExactDerandomization.Analysis.rising line 92
  22. lemma OAI.ExactDerandomization.Analysis.rising_ic line 93
  23. lemma OAI.ExactDerandomization.Analysis.rising_bot line 100
  24. lemma OAI.ExactDerandomization.Analysis.rising_top line 102
  25. lemma OAI.ExactDerandomization.Analysis.rising_mem line 104
  26. def OAI.ExactDerandomization.Analysis.shoulder line 107

    Source documentation

    simpler shoulder for the hierarchy threshold; gap W.

    def shoulder (A W x : ℝ) :=
…
  27. lemma OAI.ExactDerandomization.Analysis.shoulder_ic line 109
  28. lemma OAI.ExactDerandomization.Analysis.shoulder_bot line 123
  29. lemma OAI.ExactDerandomization.Analysis.shoulder_spec line 127
  30. lemma OAI.ExactDerandomization.Analysis.fourth_mono line 146
  31. lemma OAI.ExactDerandomization.Analysis.fourth_pos line 147
  32. lemma OAI.ExactDerandomization.Analysis.fourth_mul line 149
  33. lemma OAI.ExactDerandomization.Analysis.join_inc line 154

    Source documentation

    For increasing cutoffs it suffices to explicitly bound the root in the part close to the zero threshold.

    lemma join_inc {t a b : ℝ} {f : ℝ → ℝ} (ha : 0≤a) (hb : 0≤b)
    (l : ∀ x y, x≤y → y≤t → f x ≤ f y ∧ f y-f x≤a*(y-x))
    (r : ∀ x y, x≤y → t≤x → f x ≤ f y ∧ f y-f x≤b*(y-x)) :
    Ic (a+b) f := by
…

    Mentions: OAI.ExactDerandomization.Analysis.Ic

  34. lemma OAI.ExactDerandomization.Analysis.rise_root line 169
  35. lemma OAI.ExactDerandomization.Analysis.fade_root line 197
  36. lemma OAI.ExactDerandomization.Analysis.rising_root line 209
  37. lemma OAI.ExactDerandomization.Analysis.shoulder_root line 225
  38. def OAI.ExactDerandomization.Analysis.avs line 262
  39. def OAI.ExactDerandomization.Analysis.av line 263
  40. lemma OAI.ExactDerandomization.Analysis.av_cmul line 266
  41. lemma OAI.ExactDerandomization.Analysis.av_mulc line 268
  42. lemma OAI.ExactDerandomization.Analysis.av_add line 270
  43. lemma OAI.ExactDerandomization.Analysis.av_sub line 272
  44. lemma OAI.ExactDerandomization.Analysis.av_div line 274
  45. lemma OAI.ExactDerandomization.Analysis.av_mono line 277
  46. lemma OAI.ExactDerandomization.Analysis.av_nonneg line 279
  47. lemma OAI.ExactDerandomization.Analysis.av_swap line 282
  48. lemma OAI.ExactDerandomization.Analysis.av_sum line 287
  49. lemma OAI.ExactDerandomization.Analysis.av_equiv line 292
  50. lemma OAI.ExactDerandomization.Analysis.av_perm line 295
  51. lemma OAI.ExactDerandomization.Analysis.av_prod line 297
  52. lemma OAI.ExactDerandomization.Analysis.av_const line 303
  53. lemma OAI.ExactDerandomization.Analysis.av_zero line 305
  54. lemma OAI.ExactDerandomization.Analysis.av_card line 307
  55. lemma OAI.ExactDerandomization.Analysis.av_sq_le line 312
  56. lemma OAI.ExactDerandomization.Analysis.av_four_le line 318
  57. def OAI.ExactDerandomization.Analysis.var2 line 325

    Source documentation

    Variance around the finite average.

    def var2 (f : α → ℝ) := av (fun i=>(f i-av f)^2)

    Mentions: OAI.ExactDerandomization.Analysis.av

  58. lemma OAI.ExactDerandomization.Analysis.var2_sum line 327
  59. lemma OAI.ExactDerandomization.Analysis.var2_best line 333
  60. lemma OAI.ExactDerandomization.Analysis.var2_pair line 339
  61. lemma OAI.ExactDerandomization.Analysis.pair_four line 345
  62. abbrev OAI.ExactDerandomization.Analysis.Square.T line 366
  63. abbrev OAI.ExactDerandomization.Analysis.Square.order line 367
  64. abbrev OAI.ExactDerandomization.Analysis.Square.c line 370
  65. lemma OAI.ExactDerandomization.Analysis.Square.cab line 372
  66. lemma OAI.ExactDerandomization.Analysis.Square.csq line 373
  67. lemma OAI.ExactDerandomization.Analysis.Square.cconj line 374
  68. def OAI.ExactDerandomization.Analysis.Square.dot line 380
  69. abbrev OAI.ExactDerandomization.Analysis.Square.e line 381
  70. lemma OAI.ExactDerandomization.Analysis.Square.ortho line 383
  71. lemma OAI.ExactDerandomization.Analysis.Square.cross line 393
  72. def OAI.ExactDerandomization.Analysis.Square.hat line 401
  73. lemma OAI.ExactDerandomization.Analysis.Square.parse line 403
  74. lemma OAI.ExactDerandomization.Analysis.Square.hat_sub line 416
  75. lemma OAI.ExactDerandomization.Analysis.Square.hat_shift line 419
  76. def OAI.ExactDerandomization.Analysis.Square.shear line 433
  77. lemma OAI.ExactDerandomization.Analysis.Square.shear_shear line 439
  78. def OAI.ExactDerandomization.Analysis.Square.shPerm line 442
  79. lemma OAI.ExactDerandomization.Analysis.Square.e_shear line 445
  80. lemma OAI.ExactDerandomization.Analysis.Square.hat_sh line 449
  81. def OAI.ExactDerandomization.Analysis.Square.mass line 453
  82. lemma OAI.ExactDerandomization.Analysis.Square.allmass line 455
  83. lemma OAI.ExactDerandomization.Analysis.Square.at0 line 461
  84. lemma OAI.ExactDerandomization.Analysis.Square.vnonzero line 468
  85. abbrev OAI.ExactDerandomization.Analysis.Square.lift line 476

    Source documentation

    Character displacement away from low frequencies.

    abbrev lift (i : ZMod n) := i.valMinAbs
  86. def OAI.ExactDerandomization.Analysis.Square.near line 477
  87. instance OAI.ExactDerandomization.Analysis.Square.(instance at line 479) line 479
  88. def OAI.ExactDerandomization.Analysis.Square.threshold line 481
  89. lemma OAI.ExactDerandomization.Analysis.Square.pos_threshold line 483
  90. lemma OAI.ExactDerandomization.Analysis.Square.far_threshold line 490
  91. def OAI.ExactDerandomization.Analysis.energy line 537
  92. def OAI.ExactDerandomization.Analysis.mass4 line 539
  93. abbrev OAI.ExactDerandomization.Analysis.Family line 540
  94. def OAI.ExactDerandomization.Analysis.energies line 541
  95. def OAI.ExactDerandomization.Analysis.expands line 544
  96. lemma OAI.ExactDerandomization.Analysis.samesq line 547
  97. lemma OAI.ExactDerandomization.Analysis.oppsq line 553
  98. lemma OAI.ExactDerandomization.Analysis.signedsq line 560
  99. lemma OAI.ExactDerandomization.Analysis.signedsq_eps line 575
  100. lemma OAI.ExactDerandomization.Analysis.even4 line 580
  101. lemma OAI.ExactDerandomization.Analysis.e4 line 586

    Source documentation

    L4 Poincare via L2 on signed-squares.

    lemma e4 {G : Family γ α} {C : ℝ} (hC : 1≤C) (h : expands G C)
    (f : α → ℝ) (ef : av f=0) :
    let A := C*Fintype.card γ
…

    Mentions: OAI.ExactDerandomization.Analysis.Family, OAI.ExactDerandomization.Analysis.expands, OAI.ExactDerandomization.Analysis.av

  102. def OAI.ExactDerandomization.Analysis.lazyK line 620
  103. lemma OAI.ExactDerandomization.Analysis.K_av line 624
  104. lemma OAI.ExactDerandomization.Analysis.K_dec line 633
  105. def OAI.ExactDerandomization.Analysis.loss line 653
  106. lemma OAI.ExactDerandomization.Analysis.loss_bounds line 655
  107. lemma OAI.ExactDerandomization.Analysis.K_shrink line 665
  108. def OAI.ExactDerandomization.Analysis.walk line 680
  109. lemma OAI.ExactDerandomization.Analysis.walk_mix line 684
  110. def OAI.ExactDerandomization.Analysis.Square.core line 735
  111. instance OAI.ExactDerandomization.Analysis.Square.(instance at line 736) line 736
  112. def OAI.ExactDerandomization.Analysis.Square.sector line 738
  113. def OAI.ExactDerandomization.Analysis.Square.signcode line 739
  114. lemma OAI.ExactDerandomization.Analysis.Square.lift_zero line 742
  115. abbrev OAI.ExactDerandomization.Analysis.Square.Shears line 744
  116. def OAI.ExactDerandomization.Analysis.Square.amount line 746
  117. def OAI.ExactDerandomization.Analysis.Square.move line 748

    Source documentation

    Frequency moves

    def move (b : Shears) : Equiv.Perm (T n) := shPerm (!b.1) (amount b.2 : ZMod n)

    Mentions: OAI.ExactDerandomization.Analysis.Square.Shears, OAI.ExactDerandomization.Analysis.Square.T, OAI.ExactDerandomization.Analysis.Square.shPerm, OAI.ExactDerandomization.Analysis.Square.amount

  118. lemma OAI.ExactDerandomization.Analysis.Square.swing_near line 750
  119. lemma OAI.ExactDerandomization.Analysis.Square.squash line 761
  120. lemma OAI.ExactDerandomization.Analysis.Square.ping line 770
  121. lemma OAI.ExactDerandomization.Analysis.Square.sqcompare line 801
  122. def OAI.ExactDerandomization.Analysis.Square.atoms line 808
  123. lemma OAI.ExactDerandomization.Analysis.Square.ann line 810
  124. def OAI.ExactDerandomization.Analysis.Square.changeF line 812
  125. def OAI.ExactDerandomization.Analysis.Square.changed line 814
  126. lemma OAI.ExactDerandomization.Analysis.Square.trial line 817
  127. lemma OAI.ExactDerandomization.Analysis.Square.deflect line 831
  128. def OAI.ExactDerandomization.Analysis.Square.axial line 867
  129. def OAI.ExactDerandomization.Analysis.Square.shifted line 868
  130. def OAI.ExactDerandomization.Analysis.Square.evalC line 869
  131. lemma OAI.ExactDerandomization.Analysis.Square.disp_shift line 872
  132. lemma OAI.ExactDerandomization.Analysis.Square.wings line 885
  133. lemma OAI.ExactDerandomization.Analysis.Square.gapFuel_pos line 906
  134. def OAI.ExactDerandomization.Analysis.Square.meanSq line 908
  135. lemma OAI.ExactDerandomization.Analysis.Square.meanSqNN line 910
  136. lemma OAI.ExactDerandomization.Analysis.Square.packA line 913
  137. lemma OAI.ExactDerandomization.Analysis.Square.square_gap line 922

    Source documentation

    shear on chart large-first operates on first physical coordinate; left action is simultaneous on any allowed external index.

    lemma square_gap (u : Shears → Equiv.Perm α) :
    av (fun i=>var2 (F i)) ≤
        (6+4/threshold) * ((∑ b : Shears, meanSq (changeF F b (u b))) +
             ∑ b : Bool, meanSq (shifted F b)) := by
…

    Mentions: OAI.ExactDerandomization.Analysis.Square.Shears, OAI.ExactDerandomization.Analysis.av, OAI.ExactDerandomization.Analysis.var2, OAI.ExactDerandomization.Analysis.Square.threshold, OAI.ExactDerandomization.Analysis.Square.meanSq, OAI.ExactDerandomization.Analysis.Square.changeF, OAI.ExactDerandomization.Analysis.Square.shifted

  138. lemma OAI.ExactDerandomization.Analysis.var2_decomp line 973
  139. lemma OAI.ExactDerandomization.Analysis.var2_prod line 979
  140. lemma OAI.ExactDerandomization.Analysis.var2_project line 985
  141. lemma OAI.ExactDerandomization.Analysis.energy_project line 997

    Source documentation

    Product permutations and projection onto first factor.

    lemma energy_project (f : α × β → ℝ) (p : Equiv.Perm α) (q : Equiv.Perm β) :
    energy 2 (fun i=> av (fun j=> f (i,j))) p ≤ energy 2 f (p.prodCongr q) := by
…

    Mentions: OAI.ExactDerandomization.Analysis.energy, OAI.ExactDerandomization.Analysis.av

  142. abbrev OAI.ExactDerandomization.Analysis.Punc line 1007
  143. lemma OAI.ExactDerandomization.Analysis.punc_sum line 1013
  144. lemma OAI.ExactDerandomization.Analysis.card_punc line 1019
  145. lemma OAI.ExactDerandomization.Analysis.av_insert line 1024
  146. lemma OAI.ExactDerandomization.Analysis.var_insert line 1038
  147. def OAI.ExactDerandomization.Analysis.rows line 1043
  148. def OAI.ExactDerandomization.Analysis.ctr line 1044
  149. abbrev OAI.ExactDerandomization.Analysis.switch line 1045
  150. lemma OAI.ExactDerandomization.Analysis.rows_ctrl line 1047
  151. lemma OAI.ExactDerandomization.Analysis.nonempty_punc line 1076
  152. lemma OAI.ExactDerandomization.Analysis.punctured line 1081

    Source documentation

    Return normalization factors explicitly.

    lemma punctured [Nonempty (Punc (α×α))] (f : α → α → ℝ) :
    (Fintype.card (Punc (α×α)):ℝ)*var2 (fun i : Punc (α×α)=> f i.val.1 i.val.2) ≤
      (Fintype.card (Punc α):ℝ)*Fintype.card α*(9 * (rows f + rows (switch f))) := by
…

    Mentions: OAI.ExactDerandomization.Analysis.Punc, OAI.ExactDerandomization.Analysis.var2, OAI.ExactDerandomization.Analysis.rows, OAI.ExactDerandomization.Analysis.switch

  153. abbrev OAI.ExactDerandomization.Analysis.Affine.V line 1139
  154. abbrev OAI.ExactDerandomization.Analysis.Affine.Cmd line 1140
  155. abbrev OAI.ExactDerandomization.Analysis.Affine.Gen line 1141
  156. abbrev OAI.ExactDerandomization.Analysis.Affine.sh line 1142
  157. abbrev OAI.ExactDerandomization.Analysis.Affine.tran line 1143
  158. abbrev OAI.ExactDerandomization.Analysis.Affine.ov line 1144
  159. def OAI.ExactDerandomization.Analysis.Affine.crossTerm line 1148
  160. def OAI.ExactDerandomization.Analysis.Affine.lead line 1153

    Source documentation

    act on lead coordinates with parameter other pair fixed. aff=true includes translations

    def lead (k : Cmd) (aff : Bool) (d : T n) : Equiv.Perm (T n) :=
…

    Mentions: OAI.ExactDerandomization.Analysis.Affine.Cmd

  161. def OAI.ExactDerandomization.Analysis.Affine.face line 1159
  162. lemma OAI.ExactDerandomization.Analysis.Affine.face_face line 1163
  163. def OAI.ExactDerandomization.Analysis.Affine.leadPerm line 1165
  164. def OAI.ExactDerandomization.Analysis.Affine.act line 1169
  165. lemma OAI.ExactDerandomization.Analysis.Affine.orient line 1173
  166. lemma OAI.ExactDerandomization.Analysis.Affine.nodrift line 1178
  167. def OAI.ExactDerandomization.Analysis.Affine.Fperm line 1190
  168. lemma OAI.ExactDerandomization.Analysis.Affine.locked line 1197
  169. abbrev OAI.ExactDerandomization.Analysis.Affine.gap0 line 1201
  170. def OAI.ExactDerandomization.Analysis.Affine.stepE line 1208
  171. def OAI.ExactDerandomization.Analysis.Affine.chart line 1209
  172. lemma OAI.ExactDerandomization.Analysis.Affine.chart_cost line 1212
  173. lemma OAI.ExactDerandomization.Analysis.Affine.torus line 1254
  174. abbrev OAI.ExactDerandomization.Analysis.Affine.Frame line 1288
  175. instance OAI.ExactDerandomization.Analysis.Affine.square_punc line 1291
  176. instance OAI.ExactDerandomization.Analysis.Affine.frame_NE line 1293
  177. def OAI.ExactDerandomization.Analysis.Affine.zoom line 1295
  178. lemma OAI.ExactDerandomization.Analysis.Affine.slice_frame line 1299
  179. abbrev OAI.ExactDerandomization.Analysis.Affine.nf line 1343
  180. abbrev OAI.ExactDerandomization.Analysis.Affine.nu line 1344
  181. def OAI.ExactDerandomization.Analysis.Affine.weighingF line 1346
  182. def OAI.ExactDerandomization.Analysis.Affine.weighingU line 1347
  183. def OAI.ExactDerandomization.Analysis.Affine.fSlice line 1349
  184. def OAI.ExactDerandomization.Analysis.Affine.fSliceE line 1350
  185. lemma OAI.ExactDerandomization.Analysis.Affine.fE_le line 1352
  186. lemma OAI.ExactDerandomization.Analysis.Affine.slice_E line 1379
  187. lemma OAI.ExactDerandomization.Analysis.Affine.frame_gap line 1391
  188. lemma OAI.ExactDerandomization.Analysis.Affine.expands_frame line 1413
  189. def OAI.ExactDerandomization.Analysis.Affine.gens line 1417
  190. theorem OAI.ExactDerandomization.Analysis.Affine.slice_gap line 1421

    Source documentation

    Uniform spectral input needed by the conditional averaging.

    theorem slice_gap : expands (gens (n:=n) l) (10*gap0) := by
…

    Mentions: OAI.ExactDerandomization.Analysis.expands, OAI.ExactDerandomization.Analysis.Affine.gens, OAI.ExactDerandomization.Analysis.Affine.gap0

  191. theorem OAI.ExactDerandomization.Analysis.Affine.bits_gap line 1435
  192. def OAI.ExactDerandomization.Analysis.side line 1455
  193. instance OAI.ExactDerandomization.Analysis.(instance at line 1456) line 1456
  194. def OAI.ExactDerandomization.Analysis.rate line 1458
  195. def OAI.ExactDerandomization.Analysis.pct line 1459
  196. lemma OAI.ExactDerandomization.Analysis.rate_pos line 1460
  197. lemma OAI.ExactDerandomization.Analysis.pct_pos line 1461
  198. lemma OAI.ExactDerandomization.Analysis.side_zero line 1463
  199. lemma OAI.ExactDerandomization.Analysis.side_antitone line 1464
  200. lemma OAI.ExactDerandomization.Analysis.side_le line 1468
  201. lemma OAI.ExactDerandomization.Analysis.rate_ratio line 1471
  202. lemma OAI.ExactDerandomization.Analysis.pct_bounds line 1490
  203. def OAI.ExactDerandomization.Analysis.vmap line 1499
  204. def OAI.ExactDerandomization.Analysis.each line 1501
  205. abbrev OAI.ExactDerandomization.Analysis.Channel line 1506
  206. def OAI.ExactDerandomization.Analysis.restr line 1508
  207. def OAI.ExactDerandomization.Analysis.vwide line 1509
  208. def OAI.ExactDerandomization.Analysis.vshort line 1510
  209. instance OAI.ExactDerandomization.Analysis.(instance at line 1512) line 1512
  210. lemma OAI.ExactDerandomization.Analysis.wrest line 1513
  211. lemma OAI.ExactDerandomization.Analysis.restw line 1518
  212. def OAI.ExactDerandomization.Analysis.vEval line 1523
  213. def OAI.ExactDerandomization.Analysis.hit line 1524
  214. instance OAI.ExactDerandomization.Analysis.(instance at line 1525) line 1525
  215. abbrev OAI.ExactDerandomization.Analysis.pc line 1527
  216. def OAI.ExactDerandomization.Analysis.openP line 1528
  217. def OAI.ExactDerandomization.Analysis.closeP line 1530
  218. lemma OAI.ExactDerandomization.Analysis.hit_open line 1533
  219. lemma OAI.ExactDerandomization.Analysis.close_open line 1536
  220. lemma OAI.ExactDerandomization.Analysis.open_close line 1538
  221. def OAI.ExactDerandomization.Analysis.atP line 1542
  222. lemma OAI.ExactDerandomization.Analysis.cardinalV line 1544
  223. lemma OAI.ExactDerandomization.Analysis.ratioP line 1547
  224. lemma OAI.ExactDerandomization.Analysis.conditionP line 1553
  225. lemma OAI.ExactDerandomization.Analysis.contained line 1570
  226. lemma OAI.ExactDerandomization.Analysis.allhit line 1574
  227. def OAI.ExactDerandomization.Analysis.ind line 1577
  228. lemma OAI.ExactDerandomization.Analysis.marginal line 1579
  229. lemma OAI.ExactDerandomization.Analysis.pct_le line 1583
  230. def OAI.ExactDerandomization.Analysis.ri line 1587
  231. lemma OAI.ExactDerandomization.Analysis.marginal_box line 1589
  232. def OAI.ExactDerandomization.Analysis.scale line 1595
  233. def OAI.ExactDerandomization.Analysis.affineChannel line 1602

    Source documentation

    padding by a fixed suffix leaves joint law unchanged

    def affineChannel (u t : ZMod n) (h : u≠0) : Equiv.Perm (Channel n) :=
…

    Mentions: OAI.ExactDerandomization.Analysis.Channel

  234. lemma OAI.ExactDerandomization.Analysis.affine_eval line 1606
  235. lemma OAI.ExactDerandomization.Analysis.average_excl line 1610
  236. lemma OAI.ExactDerandomization.Analysis.pairMean line 1621
  237. lemma OAI.ExactDerandomization.Analysis.pair_avg line 1656
  238. lemma OAI.ExactDerandomization.Analysis.ind_nonneg line 1663
  239. lemma OAI.ExactDerandomization.Analysis.ind_mul line 1664
  240. lemma OAI.ExactDerandomization.Analysis.count_var line 1667

    Source documentation

    Variance estimate for deterministic test set.

    lemma count_var {α : Type} (s : Finset α) (g : α → ZMod n)
    (h : Set.InjOn g s) (k : ℕ) :
    let f i := ∑ j ∈ s, ind k (g j) i
…

    Mentions: OAI.ExactDerandomization.Analysis.ind

  241. abbrev OAI.ExactDerandomization.Analysis.Vals line 1711
  242. def OAI.ExactDerandomization.Analysis.rkSet line 1713
  243. lemma OAI.ExactDerandomization.Analysis.rkSet_zero line 1717
  244. def OAI.ExactDerandomization.Analysis.rank line 1720

    Source documentation

    zero-based descending rank, padded by zeros

    def rank (s : Finset α) (f : Vals α) (K : ℕ) :=
…

    Mentions: OAI.ExactDerandomization.Analysis.Vals

  245. lemma OAI.ExactDerandomization.Analysis.rank_nn line 1723
  246. lemma OAI.ExactDerandomization.Analysis.rank_member line 1726
  247. lemma OAI.ExactDerandomization.Analysis.rank_gt line 1728
  248. lemma OAI.ExactDerandomization.Analysis.rank_ge line 1755
  249. lemma OAI.ExactDerandomization.Analysis.rank_le line 1780
  250. lemma OAI.ExactDerandomization.Analysis.rank_compare line 1789
  251. lemma OAI.ExactDerandomization.Analysis.rank_lip line 1801
  252. structure OAI.ExactDerandomization.Analysis.Meter line 1819

    Source documentation

    A convenience for the different integrated-error sums.

    structure Meter (α : Type) where
…
  253. def OAI.ExactDerandomization.Analysis.Meter.Avg line 1828
  254. def OAI.ExactDerandomization.Analysis.Meter.Sum line 1829
  255. def OAI.ExactDerandomization.Analysis.Meter.Scale line 1832
  256. def OAI.ExactDerandomization.Analysis.Meter.Along line 1835
  257. lemma OAI.ExactDerandomization.Analysis.Meter.I0 line 1841
  258. lemma OAI.ExactDerandomization.Analysis.Meter.positive line 1842
  259. lemma OAI.ExactDerandomization.Analysis.Meter.Ineg line 1844
  260. lemma OAI.ExactDerandomization.Analysis.Meter.Isub line 1845
  261. lemma OAI.ExactDerandomization.Analysis.Meter.Isum line 1847
  262. def OAI.ExactDerandomization.Analysis.Meter.m2 line 1852
  263. def OAI.ExactDerandomization.Analysis.Meter.m4 line 1853
  264. def OAI.ExactDerandomization.Analysis.Meter.L line 1854
  265. lemma OAI.ExactDerandomization.Analysis.Meter.m2nn line 1855
  266. lemma OAI.ExactDerandomization.Analysis.Meter.m4nn line 1856
  267. lemma OAI.ExactDerandomization.Analysis.Meter.Lnn line 1857
  268. lemma OAI.ExactDerandomization.Analysis.Meter.L4 line 1858
  269. lemma OAI.ExactDerandomization.Analysis.Meter.LP line 1860
  270. lemma OAI.ExactDerandomization.Analysis.Meter.abs4 line 1866
  271. lemma OAI.ExactDerandomization.Analysis.Meter.neg4 line 1867
  272. lemma OAI.ExactDerandomization.Analysis.Meter.m4mono line 1868
  273. lemma OAI.ExactDerandomization.Analysis.Meter.Lmono line 1870
  274. lemma OAI.ExactDerandomization.Analysis.Meter.Labs line 1872
  275. lemma OAI.ExactDerandomization.Analysis.Meter.Lzero line 1873
  276. lemma OAI.ExactDerandomization.Analysis.Meter.Lneg line 1874
  277. lemma OAI.ExactDerandomization.Analysis.Meter.Lmul line 1875
  278. lemma OAI.ExactDerandomization.Analysis.Meter.cs line 1882
  279. lemma OAI.ExactDerandomization.Analysis.Meter.m2m4 line 1905
  280. lemma OAI.ExactDerandomization.Analysis.Meter.Holder2 line 1909
  281. lemma OAI.ExactDerandomization.Analysis.Meter.Holder3 line 1917
  282. lemma OAI.ExactDerandomization.Analysis.Meter.mink line 1928
  283. lemma OAI.ExactDerandomization.Analysis.Meter.many line 1940
  284. abbrev OAI.ExactDerandomization.Analysis.Wrap.Four line 1963
  285. def OAI.ExactDerandomization.Analysis.Wrap.lower line 1966
  286. def OAI.ExactDerandomization.Analysis.Wrap.pol line 1976
  287. lemma OAI.ExactDerandomization.Analysis.Wrap.act_formula line 1982
  288. def OAI.ExactDerandomization.Analysis.Wrap.reduceV line 1993
  289. def OAI.ExactDerandomization.Analysis.Wrap.raiseV line 1994
  290. lemma OAI.ExactDerandomization.Analysis.Wrap.reduce_add line 1997
  291. lemma OAI.ExactDerandomization.Analysis.Wrap.reducePol line 2001
  292. lemma OAI.ExactDerandomization.Analysis.Wrap.reraise line 2013
  293. lemma OAI.ExactDerandomization.Analysis.Wrap.modulo line 2016
  294. lemma OAI.ExactDerandomization.Analysis.Wrap.affine_apply line 2021
  295. abbrev OAI.ExactDerandomization.Analysis.Wrap.W line 2035
  296. def OAI.ExactDerandomization.Analysis.Wrap.addin line 2036
  297. def OAI.ExactDerandomization.Analysis.Wrap.chooseOne line 2038
  298. def OAI.ExactDerandomization.Analysis.Wrap.guess line 2041
  299. lemma OAI.ExactDerandomization.Analysis.Wrap.rem_one line 2043
  300. lemma OAI.ExactDerandomization.Analysis.Wrap.pol_bounded line 2053
  301. def OAI.ExactDerandomization.Analysis.Wrap.guessP line 2076
  302. lemma OAI.ExactDerandomization.Analysis.Wrap.affine_box line 2078
  303. def OAI.ExactDerandomization.Analysis.Wrap.Variant line 2093

    Source documentation

    each fixed guessed variant permutes the full environment and does not involve its not-yet-known retained point y.

    def Variant (k : ℕ) (g : Gen) (w : W) : Equiv.Perm (Channel n) :=
…

    Mentions: OAI.ExactDerandomization.Analysis.Wrap.W, OAI.ExactDerandomization.Analysis.Channel

  304. lemma OAI.ExactDerandomization.Analysis.Wrap.variant_pin line 2096
  305. abbrev OAI.ExactDerandomization.Analysis.Salt line 2119
  306. abbrev OAI.ExactDerandomization.Analysis.Salt.Reg line 2123
  307. def OAI.ExactDerandomization.Analysis.Salt.lo line 2125
  308. def OAI.ExactDerandomization.Analysis.Salt.hi line 2126
  309. def OAI.ExactDerandomization.Analysis.Salt.join line 2127
  310. def OAI.ExactDerandomization.Analysis.Salt.strip line 2129
  311. def OAI.ExactDerandomization.Analysis.Salt.par line 2151
  312. def OAI.ExactDerandomization.Analysis.Salt.splitBits line 2155
  313. theorem OAI.ExactDerandomization.Analysis.Salt.fst_split line 2158
  314. theorem OAI.ExactDerandomization.Analysis.Salt.snd_split line 2160
  315. abbrev OAI.ExactDerandomization.Analysis.Env line 2166

    Source documentation

    Canonical roles: X,Y,Z, then raw (unreduced) salt bits.

    abbrev Env (n w : ℕ) := Channel n × Channel n × Channel n × Salt w
…

    Mentions: OAI.ExactDerandomization.Analysis.Channel, OAI.ExactDerandomization.Analysis.Salt

  316. abbrev OAI.ExactDerandomization.Analysis.Env.Slice line 2171
  317. def OAI.ExactDerandomization.Analysis.Env.inward line 2173
  318. def OAI.ExactDerandomization.Analysis.Env.outward line 2175
  319. abbrev OAI.ExactDerandomization.Analysis.Env.mask line 2178
  320. theorem OAI.ExactDerandomization.Analysis.Env.inverse1 line 2181
  321. theorem OAI.ExactDerandomization.Analysis.Env.inverse2 line 2183
  322. theorem OAI.ExactDerandomization.Analysis.Env.hits line 2185
  323. def OAI.ExactDerandomization.Analysis.Env.cond line 2188
  324. theorem OAI.ExactDerandomization.Analysis.Env.two_cond line 2191
  325. def OAI.ExactDerandomization.Analysis.Env.subSalt line 2219
  326. def OAI.ExactDerandomization.Analysis.Env.panel line 2226
  327. lemma OAI.ExactDerandomization.Analysis.Env.mean_panel line 2230
  328. def OAI.ExactDerandomization.Analysis.unionG line 2249
  329. lemma OAI.ExactDerandomization.Analysis.expands_product line 2254
  330. lemma OAI.ExactDerandomization.Analysis.nonneg_en line 2277
  331. abbrev OAI.ExactDerandomization.Analysis.Env.Choice line 2284
  332. abbrev OAI.ExactDerandomization.Analysis.Env.Atom line 2285
  333. abbrev OAI.ExactDerandomization.Analysis.Env.Roller line 2286
  334. def OAI.ExactDerandomization.Analysis.Env.mixP line 2288
  335. lemma OAI.ExactDerandomization.Analysis.Env.full_gap line 2292
  336. def OAI.ExactDerandomization.Analysis.Env.rolling line 2302
  337. def OAI.ExactDerandomization.Analysis.Env.rollG line 2306
  338. def OAI.ExactDerandomization.Analysis.Env.rol line 2310
  339. def OAI.ExactDerandomization.Analysis.Env.winner line 2314
  340. def OAI.ExactDerandomization.Analysis.Env.fullact line 2321
  341. def OAI.ExactDerandomization.Analysis.Env.exportP line 2324
  342. theorem OAI.ExactDerandomization.Analysis.Env.winner_roll line 2327
  343. def OAI.ExactDerandomization.Analysis.Env.weight line 2336
  344. lemma OAI.ExactDerandomization.Analysis.Env.atom_mix line 2339
  345. abbrev OAI.ExactDerandomization.Analysis.Env.Paths line 2348
  346. instance OAI.ExactDerandomization.Analysis.Env.pathFin line 2351
  347. def OAI.ExactDerandomization.Analysis.Env.go line 2356
  348. def OAI.ExactDerandomization.Analysis.Env.live line 2361
  349. theorem OAI.ExactDerandomization.Analysis.Env.ok_dest line 2368
  350. def OAI.ExactDerandomization.Analysis.Env.sampling line 2387
  351. lemma OAI.ExactDerandomization.Analysis.Env.pathZero line 2392
  352. lemma OAI.ExactDerandomization.Analysis.Env.pathFold line 2395
  353. lemma OAI.ExactDerandomization.Analysis.Env.sampler_identity line 2398
  354. lemma OAI.ExactDerandomization.Analysis.Env.sampler_est line 2432

    Source documentation

    Kernel contraction for this sampling definition. Handles high salt bits z held fixed; target here is the mean in that panel.

    lemma sampler_est (k j : ℕ) (x y : ZMod n) (e : d≤w) (z : Salt (w-d)) (l : ℕ)
    (f : Env n w → ℝ) :
    let o := exportP k j x y e z
…

    Mentions: OAI.ExactDerandomization.Analysis.Salt, OAI.ExactDerandomization.Analysis.Env, OAI.ExactDerandomization.Analysis.Env.exportP

  355. lemma OAI.ExactDerandomization.Analysis.difference_L line 2453
  356. lemma OAI.ExactDerandomization.Analysis.integralRoot line 2465
  357. lemma OAI.ExactDerandomization.Analysis.mixtures line 2469
  358. abbrev OAI.ExactDerandomization.Analysis.rel line 2480
  359. lemma OAI.ExactDerandomization.Analysis.four_distance line 2482
  360. lemma OAI.ExactDerandomization.Analysis.ordinary line 2490
  361. lemma OAI.ExactDerandomization.Analysis.fidelity line 2493