OAI/Computability/Logspace/Amplification.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Two independent finite-coin trials and the inclusion of one-sided in two-sided randomized logspace.

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

  1. abbrev OAI.ExactDerandomization.Table.TM.PS line 26
  2. def OAI.ExactDerandomization.Table.TM.ans line 28
  3. def OAI.ExactDerandomization.Table.TM.combineAct line 33
  4. def OAI.ExactDerandomization.Table.TM.twice line 39
  5. def OAI.ExactDerandomization.Table.TM.join line 50
  6. def OAI.ExactDerandomization.Table.TM.pend line 54
  7. theorem OAI.ExactDerandomization.Table.TM.step_buf line 57
  8. theorem OAI.ExactDerandomization.Table.TM.step_exec line 63
  9. theorem OAI.ExactDerandomization.Table.TM.step_two line 74
  10. def OAI.ExactDerandomization.Table.TM.ev line 89
  11. def OAI.ExactDerandomization.Table.TM.od line 90
  12. theorem OAI.ExactDerandomization.Table.TM.run_twice line 92
  13. theorem OAI.ExactDerandomization.Table.TM.positions_twice line 106
  14. theorem OAI.ExactDerandomization.Table.TM.out_twice line 115
  15. theorem OAI.ExactDerandomization.Table.TM.halts_twice line 120
  16. theorem OAI.ExactDerandomization.Table.TM.half_le line 127
  17. theorem OAI.ExactDerandomization.Table.TM.space_twice line 136
  18. abbrev OAI.ExactDerandomization.Table.TM.Flips line 144
  19. def OAI.ExactDerandomization.Table.TM.flipSplit line 146
  20. theorem OAI.ExactDerandomization.Table.TM.split_ev line 164
  21. theorem OAI.ExactDerandomization.Table.TM.split_od line 174
  22. abbrev OAI.ExactDerandomization.Table.TM.wins line 184
  23. abbrev OAI.ExactDerandomization.Table.TM.Losers line 187
  24. theorem OAI.ExactDerandomization.Table.TM.prob_losers line 189
  25. theorem OAI.ExactDerandomization.Table.TM.prob_twice line 202
  26. theorem OAI.ExactDerandomization.RL_subset_BPL line 227

    Source documentation

    Amplification on the concrete classes (interleaved trials).

    theorem RL_subset_BPL : RL ⊆ BPL := by
…

    Mentions: OAI.ExactDerandomization.RL, OAI.ExactDerandomization.BPL