OAI/Computability/Logspace/IterationSchedule.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Finite iteration schedules and the decomposition of estimator increments.

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

  1. abbrev OAI.ExactDerandomization.Rain.Crack line 23

    Source comment

    Enumerate the increments by a pool in which each piece of a telescope, variant of the walk, and multiplicand port have one reserved index.
    abbrev Crack:= Bool×ℕ
  2. abbrev OAI.ExactDerandomization.Rain.CellQ line 24
  3. abbrev OAI.ExactDerandomization.Rain.Fog line 25
  4. abbrev OAI.ExactDerandomization.Rain.Seed line 26
  5. abbrev OAI.ExactDerandomization.Rain.store0 line 27
  6. abbrev OAI.ExactDerandomization.Rain.Fog.first0 line 29
  7. abbrev OAI.ExactDerandomization.Rain.Fog.cell0 line 30
  8. abbrev OAI.ExactDerandomization.Rain.Fog.sig line 31
  9. abbrev OAI.ExactDerandomization.Rain.Fog.event line 32
  10. abbrev OAI.ExactDerandomization.Rain.Fog.k line 33
  11. abbrev OAI.ExactDerandomization.Rain.Fog.ray line 34
  12. abbrev OAI.ExactDerandomization.Rain.Fog.slackM line 35
  13. abbrev OAI.ExactDerandomization.Rain.Fog.budget line 36
  14. abbrev OAI.ExactDerandomization.Rain.Fog.tick line 37
  15. def OAI.ExactDerandomization.Rain.Fog.habitat line 39
  16. def OAI.ExactDerandomization.Rain.Fog.number0 line 45
  17. lemma OAI.ExactDerandomization.Rain.Fog.from0 line 48
  18. lemma OAI.ExactDerandomization.Rain.Fog.just line 53
  19. lemma OAI.ExactDerandomization.Rain.Fog.hews line 56
  20. lemma OAI.ExactDerandomization.Rain.Fog.totally line 76
  21. lemma OAI.ExactDerandomization.Rain.Fog.far0 line 86
  22. abbrev OAI.ExactDerandomization.Rain.Seed.fog line 100
  23. abbrev OAI.ExactDerandomization.Rain.Seed.x line 101
  24. abbrev OAI.ExactDerandomization.Rain.Seed.y line 102
  25. def OAI.ExactDerandomization.Rain.Seed.old line 103
  26. def OAI.ExactDerandomization.Rain.Seed.along line 104
  27. lemma OAI.ExactDerandomization.Rain.Seed.old_inj line 105
  28. lemma OAI.ExactDerandomization.Rain.Seed.along_inj line 107
  29. lemma OAI.ExactDerandomization.Rain.Seed.old_not line 108
  30. abbrev OAI.ExactDerandomization.Rain.CarryE line 111
  31. def OAI.ExactDerandomization.Rain.passport line 112
  32. lemma OAI.ExactDerandomization.Rain.Pass.small line 116
  33. abbrev OAI.ExactDerandomization.Rain.Pass.sized line 117
  34. lemma OAI.ExactDerandomization.Rain.Pass.pair line 118
  35. lemma OAI.ExactDerandomization.Rain.Pass.little line 122
  36. lemma OAI.ExactDerandomization.Rain.Pass.left line 124
  37. lemma OAI.ExactDerandomization.Rain.Pass.boo line 125
  38. abbrev OAI.ExactDerandomization.Rain.Pass.reserve line 129
  39. lemma OAI.ExactDerandomization.Rain.Pass.lengthC line 130
  40. abbrev OAI.ExactDerandomization.Rain.Census.h line 182
  41. def OAI.ExactDerandomization.Rain.Census.calendar line 183
  42. def OAI.ExactDerandomization.Rain.Census.tracks line 184
  43. abbrev OAI.ExactDerandomization.Rain.Census.Arc line 186
  44. lemma OAI.ExactDerandomization.Rain.Census.pat line 187
  45. def OAI.ExactDerandomization.Rain.Census.drops line 191
  46. lemma OAI.ExactDerandomization.Rain.Census.grange line 192
  47. lemma OAI.ExactDerandomization.Rain.Census.disjoint0 line 199
  48. lemma OAI.ExactDerandomization.Rain.Census.total line 206
  49. def OAI.ExactDerandomization.Rain.Census.wind line 221
  50. theorem OAI.ExactDerandomization.Rain.Census.humid line 229