OAI/Computability/Logspace/ProbabilityHierarchy.lean

GitHub source file

153 declarations, 0 contain sorry, 0 declared as axioms

Strictly forward substochastic matrices and the hierarchy of probability rewards.

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

  1. abbrev OAI.ExactDerandomization.Hie.Domain line 21
  2. abbrev OAI.ExactDerandomization.Hie.Vec line 22
  3. abbrev OAI.ExactDerandomization.Hie.Mat line 23
  4. def OAI.ExactDerandomization.Hie.mv line 24
  5. def OAI.ExactDerandomization.Hie.mm line 25
  6. def OAI.ExactDerandomization.Hie.wt line 26
  7. def OAI.ExactDerandomization.Hie.nodes line 28
  8. structure OAI.ExactDerandomization.Hie.SB line 32

    Source documentation

    support restricted to active set S'

    structure SB (S S' : Domain) (f : ℝ) (k : ℝ) (C : Mat) : Prop where
…

    Mentions: OAI.ExactDerandomization.Hie.Domain, OAI.ExactDerandomization.Hie.Mat

  9. abbrev OAI.ExactDerandomization.Hie.Step line 38
  10. lemma OAI.ExactDerandomization.Hie.wt_mm line 40
  11. lemma OAI.ExactDerandomization.Hie.mm_mv line 45
  12. lemma OAI.ExactDerandomization.Hie.restrict line 49
  13. lemma OAI.ExactDerandomization.Hie.relax line 56
  14. def OAI.ExactDerandomization.Hie.zero line 62
  15. lemma OAI.ExactDerandomization.Hie.sb0 line 63
  16. def OAI.ExactDerandomization.Hie.combine line 66
  17. lemma OAI.ExactDerandomization.Hie.data_bounds line 68
  18. abbrev OAI.ExactDerandomization.Hie.A line 104
  19. def OAI.ExactDerandomization.Hie.Q line 105
  20. def OAI.ExactDerandomization.Hie.correct line 107
  21. lemma OAI.ExactDerandomization.Hie.Qnn line 109
  22. lemma OAI.ExactDerandomization.Hie.Qhi line 111
  23. lemma OAI.ExactDerandomization.Hie.Qlo line 113
  24. lemma OAI.ExactDerandomization.Hie.Qic line 116
  25. lemma OAI.ExactDerandomization.Hie.Fbounds line 118
  26. lemma OAI.ExactDerandomization.Hie.Fle line 137
  27. lemma OAI.ExactDerandomization.Hie.Fsb line 143
  28. lemma OAI.ExactDerandomization.Hie.Fgrow line 150
  29. def OAI.ExactDerandomization.Hie.adjust line 161
  30. lemma OAI.ExactDerandomization.Hie.csr line 165
  31. lemma OAI.ExactDerandomization.Hie.mono_steps line 172
  32. def OAI.ExactDerandomization.Hie.residual line 179
  33. lemma OAI.ExactDerandomization.Hie.substochastic line 182
  34. abbrev OAI.ExactDerandomization.Hie.diff line 237
  35. lemma OAI.ExactDerandomization.Hie.transfer_diff line 240
  36. def OAI.ExactDerandomization.Hie.sub line 261
  37. lemma OAI.ExactDerandomization.Hie.sub_choose line 263
  38. lemma OAI.ExactDerandomization.Hie.factorial line 277
  39. def OAI.ExactDerandomization.Hie.kOK line 348
  40. lemma OAI.ExactDerandomization.Hie.can_cut line 350
  41. abbrev OAI.ExactDerandomization.Hie.good line 356
  42. lemma OAI.ExactDerandomization.Hie.good_col line 357
  43. lemma OAI.ExactDerandomization.Hie.cover line 374

    Source documentation

    Unsigned terms of residual dominated by residual.

    lemma cover {S f g C T} (hc : Step S f C) (hf : 0<f) (hg : ∀ i,in01 (g i)) (x y : ℕ) :
    let F:=adjust S f g C T
…

    Mentions: OAI.ExactDerandomization.Hie.Step, OAI.ExactDerandomization.Hie.adjust

  44. abbrev OAI.ExactDerandomization.Hie.delta line 406
  45. abbrev OAI.ExactDerandomization.Hie.eta line 407
  46. def OAI.ExactDerandomization.Hie.gate line 409
  47. def OAI.ExactDerandomization.Hie.light line 410
  48. lemma OAI.ExactDerandomization.Hie.gate_mem line 412
  49. lemma OAI.ExactDerandomization.Hie.gate_full line 415
  50. lemma OAI.ExactDerandomization.Hie.gate_shut line 418
  51. def OAI.ExactDerandomization.Hie.retain line 424
  52. def OAI.ExactDerandomization.Hie.tally line 425
  53. lemma OAI.ExactDerandomization.Hie.tally_eq line 426
  54. abbrev OAI.ExactDerandomization.Hie.legal line 430
  55. lemma OAI.ExactDerandomization.Hie.injNat line 432
  56. lemma OAI.ExactDerandomization.Hie.tally_av line 437
  57. lemma OAI.ExactDerandomization.Hie.tally_var line 440
  58. lemma OAI.ExactDerandomization.Hie.tally_cond line 444
  59. def OAI.ExactDerandomization.Hie.panel_rank line 467
  60. def OAI.ExactDerandomization.Hie.throttle line 469
  61. def OAI.ExactDerandomization.Hie.cost line 471
  62. lemma OAI.ExactDerandomization.Hie.gate_bound line 474
  63. def OAI.ExactDerandomization.Hie.mark line 525
  64. def OAI.ExactDerandomization.Hie.score line 528
  65. def OAI.ExactDerandomization.Hie.U line 531
  66. lemma OAI.ExactDerandomization.Hie.mark_mem line 534
  67. lemma OAI.ExactDerandomization.Hie.score_mem line 540
  68. lemma OAI.ExactDerandomization.Hie.expect_mem line 544
  69. lemma OAI.ExactDerandomization.Hie.U_mem line 548
  70. lemma OAI.ExactDerandomization.Hie.rfull line 551
  71. lemma OAI.ExactDerandomization.Hie.rzero line 552
  72. def OAI.ExactDerandomization.Hie.rowhi line 554
  73. def OAI.ExactDerandomization.Hie.rowlo line 556
  74. lemma OAI.ExactDerandomization.Hie.U_light line 559
  75. abbrev OAI.ExactDerandomization.Hie.limitJ line 593

    Source documentation

    A threshold usable for incoming normalization.

    abbrev limitJ (J : ℕ) := 128 + 4*(J+1:ℝ)
  76. lemma OAI.ExactDerandomization.Hie.U_heavy line 595
  77. structure OAI.ExactDerandomization.Hie.Const line 679
  78. lemma OAI.ExactDerandomization.Hie.exists_const line 689
  79. structure OAI.ExactDerandomization.Hie.Pilot line 697
  80. def OAI.ExactDerandomization.Hie.gamma line 703
  81. lemma OAI.ExactDerandomization.Hie.gamma_mem line 704
  82. lemma OAI.ExactDerandomization.Hie.gamma_anti line 707
  83. lemma OAI.ExactDerandomization.Hie.gamma_full line 710
  84. lemma OAI.ExactDerandomization.Hie.gamma_stop line 711
  85. structure OAI.ExactDerandomization.Hie.Stg line 713
  86. abbrev OAI.ExactDerandomization.Hie.Stg.f line 722
  87. def OAI.ExactDerandomization.Hie.Stg.update line 725
  88. def OAI.ExactDerandomization.Hie.Stg.pilots line 730
  89. def OAI.ExactDerandomization.Hie.Stg.testG line 734
  90. def OAI.ExactDerandomization.Hie.Stg.testU line 735
  91. def OAI.ExactDerandomization.Hie.Stg.probed line 736
  92. def OAI.ExactDerandomization.Hie.Stg.gm line 737
  93. def OAI.ExactDerandomization.Hie.Stg.corr line 738
  94. def OAI.ExactDerandomization.Hie.Stg.nextG line 739
  95. def OAI.ExactDerandomization.Hie.Stg.D line 740
  96. theorem OAI.ExactDerandomization.Hie.Stg.V_recur line 742
  97. lemma OAI.ExactDerandomization.Hie.Stg.V_mem line 744
  98. lemma OAI.ExactDerandomization.Hie.Stg.V_mono line 752
  99. lemma OAI.ExactDerandomization.Hie.Stg.prob_inc line 755
  100. lemma OAI.ExactDerandomization.Hie.Stg.pilot_bounds line 764
  101. lemma OAI.ExactDerandomization.Hie.Stg.tbounds line 773
  102. lemma OAI.ExactDerandomization.Hie.Stg.cbounds line 776
  103. lemma OAI.ExactDerandomization.Hie.Stg.cpilot line 780
  104. lemma OAI.ExactDerandomization.Hie.Stg.dbounds line 789
  105. lemma OAI.ExactDerandomization.Hie.Stg.columns line 793
  106. lemma OAI.ExactDerandomization.Hie.Stg.cols line 806
  107. lemma OAI.ExactDerandomization.Hie.Stg.mark_sum line 817
  108. def OAI.ExactDerandomization.Hie.Stg.active line 840
  109. lemma OAI.ExactDerandomization.Hie.Stg.rare line 841
  110. abbrev OAI.ExactDerandomization.Hie.radix line 907
  111. def OAI.ExactDerandomization.Hie.copyZone line 908
  112. lemma OAI.ExactDerandomization.Hie.fromrad line 909
  113. lemma OAI.ExactDerandomization.Hie.inside line 912
  114. lemma OAI.ExactDerandomization.Hie.repr_copy line 914
  115. lemma OAI.ExactDerandomization.Hie.member_copy line 918
  116. lemma OAI.ExactDerandomization.Hie.eval_copies line 924
  117. abbrev OAI.ExactDerandomization.Hie.bound0 line 932
  118. abbrev OAI.ExactDerandomization.Hie.bound1 line 933
  119. def OAI.ExactDerandomization.Hie.slice line 934
  120. def OAI.ExactDerandomization.Hie.share line 935
  121. lemma OAI.ExactDerandomization.Hie.share_nn line 938
  122. lemma OAI.ExactDerandomization.Hie.share_sum line 946
  123. lemma OAI.ExactDerandomization.Hie.share_le line 952
  124. abbrev OAI.ExactDerandomization.Hie.boost line 956
  125. def OAI.ExactDerandomization.Hie.Stg.fac line 961
  126. def OAI.ExactDerandomization.Hie.Stg.newMat line 962
  127. def OAI.ExactDerandomization.Hie.Stg.next line 966
  128. def OAI.ExactDerandomization.Hie.Stg.project line 967
  129. lemma OAI.ExactDerandomization.Hie.Stg.mpos line 971
  130. lemma OAI.ExactDerandomization.Hie.Stg.fac_mem line 972
  131. lemma OAI.ExactDerandomization.Hie.Stg.edge_w line 976
  132. lemma OAI.ExactDerandomization.Hie.Stg.edge_small line 982
  133. lemma OAI.ExactDerandomization.Hie.Stg.newGood line 1010
  134. lemma OAI.ExactDerandomization.Hie.Stg.nonprimary line 1042
  135. lemma OAI.ExactDerandomization.Hie.Stg.commute line 1057
  136. lemma OAI.ExactDerandomization.Hie.Stg.few_nodes line 1085
  137. lemma OAI.ExactDerandomization.Hie.apply_add line 1141
  138. lemma OAI.ExactDerandomization.Hie.add_apply line 1143
  139. lemma OAI.ExactDerandomization.Hie.sub_apply line 1145
  140. structure OAI.ExactDerandomization.Hie.Prize line 1148
  141. def OAI.ExactDerandomization.Hie.Prize.plus line 1158
  142. structure OAI.ExactDerandomization.Hie.Prize.Correct line 1163
  143. lemma OAI.ExactDerandomization.Hie.Prize.Correct.win line 1169
  144. lemma OAI.ExactDerandomization.Hie.Prize.Correct.raise line 1176
  145. def OAI.ExactDerandomization.Hie.Prize.iterate line 1210
  146. lemma OAI.ExactDerandomization.Hie.Prize.all line 1214
  147. lemma OAI.ExactDerandomization.Hie.Prize.par line 1219
  148. lemma OAI.ExactDerandomization.Hie.Prize.index line 1224
  149. def OAI.ExactDerandomization.Hie.Prize.child line 1232
  150. lemma OAI.ExactDerandomization.Hie.Prize.unchanged line 1236
  151. lemma OAI.ExactDerandomization.Hie.Prize.reach line 1245
  152. lemma OAI.ExactDerandomization.Hie.Prize.density line 1253
  153. lemma OAI.ExactDerandomization.Hie.Prize.finish line 1268