OAI/Computability/Logspace/EstimatorParameters.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Choice of simultaneous resource and error parameters for the estimator.

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

  1. def OAI.ExactDerandomization.Terrain.Bank.bootC line 32
  2. abbrev OAI.ExactDerandomization.Terrain.Bank.hi line 34
  3. abbrev OAI.ExactDerandomization.Terrain.Bank.hu line 35
  4. abbrev OAI.ExactDerandomization.Terrain.Bank.hx line 36
  5. structure OAI.ExactDerandomization.Terrain.Bank.Green line 37
  6. lemma OAI.ExactDerandomization.Terrain.Bank.greenUp line 43
  7. structure OAI.ExactDerandomization.Terrain.Bank.Turf line 58
  8. lemma OAI.ExactDerandomization.Terrain.Bank.Green.tested line 66
  9. lemma OAI.ExactDerandomization.Terrain.Bank.Green.rooms line 68
  10. lemma OAI.ExactDerandomization.Terrain.Bank.Green.boxesK line 70
  11. lemma OAI.ExactDerandomization.Terrain.Bank.Green.capacityE line 74
  12. lemma OAI.ExactDerandomization.Terrain.Bank.Green.trunks line 77
  13. lemma OAI.ExactDerandomization.Terrain.Bank.Green.ray_size line 83
  14. lemma OAI.ExactDerandomization.Terrain.Bank.Green.bill0 line 85
  15. lemma OAI.ExactDerandomization.Terrain.Bank.Green.office line 92
  16. lemma OAI.ExactDerandomization.Terrain.Stone.W line 107
  17. lemma OAI.ExactDerandomization.Terrain.Stone.D line 108
  18. lemma OAI.ExactDerandomization.Terrain.Stone.roleR line 109
  19. lemma OAI.ExactDerandomization.Terrain.Stone.zeroR line 110
  20. lemma OAI.ExactDerandomization.Terrain.Stone.pointing line 114
  21. lemma OAI.ExactDerandomization.Terrain.Stone.alive line 116
  22. structure OAI.ExactDerandomization.Terrain.Stone.Rector line 125
  23. lemma OAI.ExactDerandomization.Terrain.Stone.Rector.tickets line 132
  24. lemma OAI.ExactDerandomization.Terrain.Stone.Rector.wide0 line 134
  25. lemma OAI.ExactDerandomization.Terrain.Stone.Rector.aft line 139
  26. lemma OAI.ExactDerandomization.Terrain.Stone.Rector.endUnits line 141
  27. lemma OAI.ExactDerandomization.Terrain.Stone.Rector.midUnits line 148
  28. lemma OAI.ExactDerandomization.Terrain.Stone.Rector.provision line 152
  29. lemma OAI.ExactDerandomization.Terrain.Stone.Rector.frontI line 170
  30. lemma OAI.ExactDerandomization.Terrain.Stone.Rector.frontP line 174
  31. lemma OAI.ExactDerandomization.Terrain.Stone.Rector.frontT line 178
  32. lemma OAI.ExactDerandomization.Terrain.Stone.Rector.frontE line 186