OAI/Computability/Logspace/EstimatorOperations.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

Error bounds for products, rank queries, and transported estimator values.

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

  1. def OAI.ExactDerandomization.Est.crossP line 22
  2. def OAI.ExactDerandomization.Est.leftP line 25
  3. def OAI.ExactDerandomization.Est.rightP line 28
  4. def OAI.ExactDerandomization.Est.ratioN line 32
  5. lemma OAI.ExactDerandomization.Est.upper_flip line 33
  6. structure OAI.ExactDerandomization.Est.Tile line 43
  7. def OAI.ExactDerandomization.Est.Shelf line 48
  8. lemma OAI.ExactDerandomization.Est.tile_zero line 50
  9. lemma OAI.ExactDerandomization.Est.shelf_zero line 53
  10. lemma OAI.ExactDerandomization.Est.Tile.extend line 54
  11. abbrev OAI.ExactDerandomization.Est.flaw line 59
  12. abbrev OAI.ExactDerandomization.Est.flawV line 61
  13. abbrev OAI.ExactDerandomization.Est.Axis.startd line 66
  14. lemma OAI.ExactDerandomization.Est.Axis.vsmall line 67
  15. lemma OAI.ExactDerandomization.Est.Axis.tsmall line 78
  16. lemma OAI.ExactDerandomization.Est.Axis.tperm line 87
  17. lemma OAI.ExactDerandomization.Est.Axis.vperm line 93
  18. lemma OAI.ExactDerandomization.Est.Axis.ti_add line 97
  19. lemma OAI.ExactDerandomization.Est.Axis.vi_add line 99
  20. lemma OAI.ExactDerandomization.Est.Axis.tvh line 101
  21. lemma OAI.ExactDerandomization.Est.Axis.zero_root line 110

    Source documentation

    trivial root error against zero

    lemma zero_root {K : ℝ} {D : ℕ} (h:2^d.u≤n) (he:d.S.card≤d.N)
    {f : Pics n} (hv:Tile d K D f) (hp:1≤K) :
     d.terr f (fun _ _ _=>0) ≤ 2*K*(D+1:ℝ) := by
…

    Mentions: OAI.ExactDerandomization.Est.Pics, OAI.ExactDerandomization.Est.Tile

  22. structure OAI.ExactDerandomization.Est.Builder line 143
  23. abbrev OAI.ExactDerandomization.Est.Builder.Block line 151
  24. def OAI.ExactDerandomization.Est.Builder.sess line 152
  25. def OAI.ExactDerandomization.Est.Builder.coins line 153
  26. def OAI.ExactDerandomization.Est.Builder.wrapped line 154
  27. lemma OAI.ExactDerandomization.Est.Builder.tiling line 157
  28. lemma OAI.ExactDerandomization.Est.Builder.tiling_out line 165
  29. lemma OAI.ExactDerandomization.Est.Builder.fromshelf line 188
  30. lemma OAI.ExactDerandomization.Est.Builder.bolts line 203
  31. def OAI.ExactDerandomization.Est.peeler line 230
  32. lemma OAI.ExactDerandomization.Est.spins line 231
  33. lemma OAI.ExactDerandomization.Est.spliff line 235
  34. lemma OAI.ExactDerandomization.Est.split_product line 241

    Source documentation

    Product split using final support of F and initial support of G. For a product-stochastic pair use mixture contraction individually per path.

    lemma split_product {K x y p q : ℝ} (hx:0≤x) (_:0≤y)
    (hp:0≤ p) (_:0≤ q) (hb:fourth p ≤ K) (he:fourth y≤K) :
    (fourth (x*y)- fourth (p*q))^4 ≤
      8*K^4*((if y≠0 then (fourth x-fourth p)^4 else 0)
                     +(if p≠0 then (fourth y-fourth q)^4 else 0)) := by
…
  35. lemma OAI.ExactDerandomization.Est.combine4 line 261
  36. lemma OAI.ExactDerandomization.Est.slots line 264
  37. abbrev OAI.ExactDerandomization.Est.Axis.deckX line 273
  38. abbrev OAI.ExactDerandomization.Est.Axis.deckY line 274
  39. abbrev OAI.ExactDerandomization.Est.Axis.midpoint line 275
  40. def OAI.ExactDerandomization.Est.Axis.pass line 276
  41. def OAI.ExactDerandomization.Est.Axis.spotL line 278
  42. def OAI.ExactDerandomization.Est.Axis.spotR line 280
  43. lemma OAI.ExactDerandomization.Est.Axis.spotL_on line 284

    Source documentation

    terminal sum eliminated by right row support

    lemma spotL_on (k : ℕ) (f g : Pics n) (D : ℕ) (h:∀ s x (S:Domain),
    (S.filter fun i=> g s x i≠0).card ≤ D) :
    d.ti (d.spotL k f g) ≤ D * (d.deckX k).ton f ^4 := by
…

    Mentions: OAI.ExactDerandomization.Est.Pics, OAI.ExactDerandomization.Est.Axis.ton

  44. lemma OAI.ExactDerandomization.Est.Axis.spotR_on line 300

    Source documentation

    release old source to charge right discrepancies

    lemma spotR_on (k l : ℕ) (f g : Pics n) (D : ℕ) (h:Shelf D f) (hl:l ≤ d.a) (hk:k≤d.u) :
    d.ti (d.spotR k f g) ≤ ratioN d.u k ^4 * (D * (d.deckY k l).ton g^4) := by
…

    Mentions: OAI.ExactDerandomization.Est.Pics, OAI.ExactDerandomization.Est.Shelf, OAI.ExactDerandomization.Est.ratioN, OAI.ExactDerandomization.Est.Axis.ton

  45. lemma OAI.ExactDerandomization.Est.Axis.swaying line 325
  46. abbrev OAI.ExactDerandomization.Est.Axis.fare line 347
  47. lemma OAI.ExactDerandomization.Est.Axis.cost_pass line 349
  48. lemma OAI.ExactDerandomization.Est.Axis.pass_range line 381
  49. lemma OAI.ExactDerandomization.Est.Axis.pass_pin line 411
  50. def OAI.ExactDerandomization.Est.Axis.Surf line 440
  51. def OAI.ExactDerandomization.Est.Axis.BothPin line 441
  52. def OAI.ExactDerandomization.Est.Axis.SinglePin line 443
  53. lemma OAI.ExactDerandomization.Est.Axis.marginalization line 446
  54. def OAI.ExactDerandomization.Est.Axis.through line 477
  55. lemma OAI.ExactDerandomization.Est.Axis.through_mean line 481
  56. lemma OAI.ExactDerandomization.Est.Axis.pass_id line 510
  57. def OAI.ExactDerandomization.Est.bed.pat line 532
  58. def OAI.ExactDerandomization.Est.bed.bath line 534
  59. def OAI.ExactDerandomization.Est.bed.dfix line 535
  60. lemma OAI.ExactDerandomization.Est.bed.truth line 537
  61. lemma OAI.ExactDerandomization.Est.bed.tooth line 542
  62. lemma OAI.ExactDerandomization.Est.bed.twopin line 544
  63. lemma OAI.ExactDerandomization.Est.bed.onepin line 548
  64. def OAI.ExactDerandomization.Est.replica line 574

    Source documentation

    A part is shared over one copy-symbol pair.

    def replica (M i : ℕ) : Equiv.Perm (Channel n) :=
…
  65. def OAI.ExactDerandomization.Est.pane line 577
  66. lemma OAI.ExactDerandomization.Est.raid_id line 580
  67. def OAI.ExactDerandomization.Est.mint line 592
  68. def OAI.ExactDerandomization.Est.markM line 593
  69. def OAI.ExactDerandomization.Est.pep line 596
  70. def OAI.ExactDerandomization.Est.vim line 598
  71. abbrev OAI.ExactDerandomization.Est.Axis.nextd line 604
  72. lemma OAI.ExactDerandomization.Est.Axis.transport line 606
  73. lemma OAI.ExactDerandomization.Est.Axis.transportV line 623
  74. lemma OAI.ExactDerandomization.Est.Axis.pep_mean line 630
  75. lemma OAI.ExactDerandomization.Est.Axis.vim_mean line 638
  76. lemma OAI.ExactDerandomization.Est.Axis.pane_ti line 644
  77. lemma OAI.ExactDerandomization.Est.Axis.pane_vi line 677
  78. lemma OAI.ExactDerandomization.Est.Axis.pep_terr line 692
  79. lemma OAI.ExactDerandomization.Est.Axis.vim_cost line 702
  80. lemma OAI.ExactDerandomization.Est.Axis.pep_pin line 712
  81. lemma OAI.ExactDerandomization.Est.Axis.pep_cap line 732
  82. abbrev OAI.ExactDerandomization.Est.Fwd line 752
  83. def OAI.ExactDerandomization.Est.Axis.spout line 757
  84. lemma OAI.ExactDerandomization.Est.Axis.spout_at line 760
  85. lemma OAI.ExactDerandomization.Est.Axis.rank_fee line 774
  86. lemma OAI.ExactDerandomization.Est.Axis.vm_two line 796
  87. lemma OAI.ExactDerandomization.Est.Axis.expect_spout line 807
  88. abbrev OAI.ExactDerandomization.Est.Axis.focus line 826
  89. lemma OAI.ExactDerandomization.Est.Axis.focal line 829
  90. lemma OAI.ExactDerandomization.Est.fourth0 line 880
  91. lemma OAI.ExactDerandomization.Est.fourth1 line 881
  92. lemma OAI.ExactDerandomization.Est.fourth_interval line 882
  93. lemma OAI.ExactDerandomization.Est.multrip line 885
  94. def OAI.ExactDerandomization.Est.Builder.confl line 903
  95. lemma OAI.ExactDerandomization.Est.Builder.sealed line 908

    Source documentation

    sparse final wrapper estimate from compressed pre-score and pre-main.

    lemma sealed (u v : Block n) {C r J : ℝ} (_:0≤r) (w w' : Paint n) (o : Trio) (b:Bool)
    (ho : TS f.tau C o) (hs:TS f.tau C (suppT f.tau false))
    (ht:0<f.tau) (hh:f.c=true) (hm:d.a≤d.u)
    (hw:∀ s x,in01 (w s x)) (hw':∀ s x,in01 (w' s x))
    (hz:Lip J (fun x=>fourth (shutoff x))) (he:0≤J)
    (hoP:Shelf (clim f.p) (f.wrapped u o b w)) (hvP:Shelf (clim f.p) (f.wrapped v o b w'))
    (hy:d.terr (f.coins u o b) (f.coins v o b)≤r)
    (hp:d.terr (f.coins u (suppT f.tau false) false) (f.coins v (suppT f.tau false) false)≤r) :
    d.terr (f.wrapped u o b w) (f.wrapped v o b w') ≤
       r + C^3*(1+2*clim f.p:ℝ)*(J*(4*(C^3)^3)*r+
                         ratioN d.u d.a * (d.startd d.a).von (flawV w w')) := by
…

    Mentions: OAI.ExactDerandomization.Est.Builder.Block, OAI.ExactDerandomization.Est.Paint, OAI.ExactDerandomization.Est.Shelf, OAI.ExactDerandomization.Est.ratioN, OAI.ExactDerandomization.Est.flawV

  96. lemma OAI.ExactDerandomization.Est.Builder.rated line 998

    Source documentation

    Full-array comparison with exact-ID compression, with membership mask.

    lemma rated (v : Spray n 0) {s M : ℝ} (he : v.d=d) (hz : v.K=f.p.K)
    {C : ℝ} {o : Trio} (ho : TS f.tau C o) (ht : v.Works s M)
    (h:delta≤f.tau) (hh:f.tau≤1)
    (b : Bool) :
   d.terr (f.coins (fun u x=> (v.go u x).mid v.L) o b)
            (f.coins (fun u x=> (v.go u x).origin) o b) ≤
                 Spray.localP v.K v.b C M*s := by
…

    Mentions: OAI.ExactDerandomization.Est.Spray, OAI.ExactDerandomization.Est.Spray.localP

  97. def OAI.ExactDerandomization.Est.Maxer line 1036
  98. def OAI.ExactDerandomization.Est.Leader line 1040
  99. lemma OAI.ExactDerandomization.Est.maxima line 1044
  100. lemma OAI.ExactDerandomization.Est.leaders_mean line 1054
  101. lemma OAI.ExactDerandomization.Est.Axis.v_abs line 1064
  102. lemma OAI.ExactDerandomization.Est.Axis.leader_cost line 1065
  103. lemma OAI.ExactDerandomization.Est.Axis.multiplier_fee line 1082
  104. def OAI.ExactDerandomization.Est.honor line 1105
  105. def OAI.ExactDerandomization.Est.fame line 1106
  106. lemma OAI.ExactDerandomization.Est.Axis.honors_fee line 1111
  107. lemma OAI.ExactDerandomization.Est.Axis.root_cap_hon line 1151
  108. lemma OAI.ExactDerandomization.Est.Axis.pinned_hon line 1158
  109. lemma OAI.ExactDerandomization.Est.Axis.fame_fee line 1166
  110. lemma OAI.ExactDerandomization.Est.crowd line 1202
  111. def OAI.ExactDerandomization.Est.Axis.passV line 1224
  112. lemma OAI.ExactDerandomization.Est.Axis.passV_id line 1227
  113. lemma OAI.ExactDerandomization.Est.Axis.left_cost line 1246
  114. lemma OAI.ExactDerandomization.Est.Axis.right_cost line 1276
  115. lemma OAI.ExactDerandomization.Est.Axis.pastime line 1346
  116. lemma OAI.ExactDerandomization.Est.Axis.pastbound line 1375