OAI/Computability/Logspace/Deterministic.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

Deterministic logarithmic-space machines and their probabilistic-class inclusions.

  1. abbrev OAI.ExactDerandomization.Word line 9

    Also declared: ComparatorChallenges/LogspaceEquality.lean:9 (same declaration text).

  2. abbrev OAI.ExactDerandomization.Language line 10

    Also declared: ComparatorChallenges/LogspaceEquality.lean:10 (same declaration text).

  3. abbrev OAI.ExactDerandomization.CoinTape line 11

    Also declared: ComparatorChallenges/LogspaceEquality.lean:11 (same declaration text).

  4. inductive OAI.ExactDerandomization.Direction line 13

    Also declared: ComparatorChallenges/LogspaceEquality.lean:13 (same declaration text).

  5. inductive OAI.ExactDerandomization.InputSymbol line 17

    Also declared: ComparatorChallenges/LogspaceEquality.lean:17 (same declaration text).

  6. def OAI.ExactDerandomization.Direction.move line 21

    Also declared: ComparatorChallenges/LogspaceEquality.lean:21 (same declaration text).

  7. def OAI.ExactDerandomization.Direction.moveInput line 27

    Also declared: ComparatorChallenges/LogspaceEquality.lean:27 (same declaration text).

  8. def OAI.ExactDerandomization.readInput line 33

    Also declared: ComparatorChallenges/LogspaceEquality.lean:33 (same declaration text).

  9. structure OAI.ExactDerandomization.Action line 39

    Also declared: ComparatorChallenges/LogspaceEquality.lean:39 (same declaration text).

  10. structure OAI.ExactDerandomization.Machine line 45

    Also declared: ComparatorChallenges/LogspaceEquality.lean:45 (same declaration text).

  11. structure OAI.ExactDerandomization.Configuration line 51

    Also declared: ComparatorChallenges/LogspaceEquality.lean:51 (same declaration text).

  12. def OAI.ExactDerandomization.Machine.initial line 61

    Also declared: ComparatorChallenges/LogspaceEquality.lean:61 (same declaration text).

  13. def OAI.ExactDerandomization.Machine.step line 67

    Also declared: ComparatorChallenges/LogspaceEquality.lean:67 (same declaration text).

  14. def OAI.ExactDerandomization.Machine.run line 79

    Also declared: ComparatorChallenges/LogspaceEquality.lean:79 (same declaration text).

  15. def OAI.ExactDerandomization.Machine.spaceThrough line 84

    Also declared: ComparatorChallenges/LogspaceEquality.lean:84 (same declaration text).

  16. def OAI.ExactDerandomization.Machine.LogSpace line 88

    Also declared: ComparatorChallenges/LogspaceEquality.lean:88 (same declaration text).

  17. def OAI.ExactDerandomization.Machine.Deterministic line 92

    Also declared: ComparatorChallenges/LogspaceEquality.lean:92 (same declaration text).

  18. def OAI.ExactDerandomization.Machine.HaltsBy line 95

    Also declared: ComparatorChallenges/LogspaceEquality.lean:95 (same declaration text).

  19. def OAI.ExactDerandomization.Machine.Decides line 98

    Also declared: ComparatorChallenges/LogspaceEquality.lean:98 (same declaration text).

  20. def OAI.ExactDerandomization.Machine.extendCoins line 103

    Also declared: ComparatorChallenges/LogspaceEquality.lean:103 (same declaration text).

  21. def OAI.ExactDerandomization.Machine.acceptanceProbability line 106

    Also declared: ComparatorChallenges/LogspaceEquality.lean:106 (same declaration text).

  22. def OAI.ExactDerandomization.polynomialClock line 113

    Also declared: ComparatorChallenges/LogspaceEquality.lean:113 (same declaration text).

  23. def OAI.ExactDerandomization.L line 115

    Also declared: ComparatorChallenges/LogspaceEquality.lean:115 (same declaration text).

  24. def OAI.ExactDerandomization.RL line 119

    Also declared: ComparatorChallenges/LogspaceEquality.lean:119 (same declaration text).

  25. def OAI.ExactDerandomization.BPL line 127

    Also declared: ComparatorChallenges/LogspaceEquality.lean:127 (same declaration text).

  26. theorem OAI.ExactDerandomization.Machine.run_zero line 139
  27. theorem OAI.ExactDerandomization.Machine.run_succ line 142
  28. theorem OAI.ExactDerandomization.Machine.run_eq_of_prefix line 145
  29. theorem OAI.ExactDerandomization.Machine.extendCoins_apply line 154
  30. theorem OAI.ExactDerandomization.Machine.step_eq_self_of_output line 158
  31. theorem OAI.ExactDerandomization.Machine.run_add_of_output line 163
  32. theorem OAI.ExactDerandomization.Machine.run_later_of_output line 172
  33. theorem OAI.ExactDerandomization.Machine.halted_outputs_eq line 178
  34. theorem OAI.ExactDerandomization.Machine.HaltsBy.mono line 187
  35. theorem OAI.ExactDerandomization.Machine.step_eq_of_deterministic line 193
  36. theorem OAI.ExactDerandomization.Machine.run_eq_of_deterministic line 199
  37. theorem OAI.ExactDerandomization.Machine.spaceThrough_zero line 208
  38. theorem OAI.ExactDerandomization.Machine.spaceThrough_mono line 212
  39. theorem OAI.ExactDerandomization.Machine.acceptanceProbability_nonneg line 220
  40. theorem OAI.ExactDerandomization.Machine.acceptanceProbability_le_one line 225
  41. theorem OAI.ExactDerandomization.Machine.acceptanceProbability_eq_of_output line 236
  42. theorem OAI.ExactDerandomization.Machine.Decides.output_at_halt line 241
  43. theorem OAI.ExactDerandomization.clocked_exact_decider_mem_RL_and_BPL line 254
  44. theorem OAI.ExactDerandomization.intervals_subset_visited line 288
  45. theorem OAI.ExactDerandomization.abs_le_visited_card line 315
  46. theorem OAI.ExactDerandomization.Machine.workPos_step_bounds line 329
  47. theorem OAI.ExactDerandomization.Machine.workPos_abs_le_space line 341
  48. theorem OAI.ExactDerandomization.Machine.work_eq_false_outside line 354
  49. abbrev OAI.ExactDerandomization.ConfigurationCode line 372
  50. def OAI.ExactDerandomization.cellPosition line 376
  51. def OAI.ExactDerandomization.cellIndex line 378
  52. theorem OAI.ExactDerandomization.cellPosition_cellIndex line 381
  53. def OAI.ExactDerandomization.Configuration.encode line 391
  54. theorem OAI.ExactDerandomization.Configuration.eq_of_encode_eq line 396
  55. theorem OAI.ExactDerandomization.Machine.run_add_eq_of_eq line 430
  56. theorem OAI.ExactDerandomization.Machine.haltsBy_card_codes line 439
  57. theorem OAI.ExactDerandomization.card_configurationCode line 486
  58. theorem OAI.ExactDerandomization.two_pow_clog_le line 493
  59. theorem OAI.ExactDerandomization.card_configurationCode_log_bound line 503
  60. theorem OAI.ExactDerandomization.Machine.Deterministic.polynomial_clock line 532
  61. theorem OAI.ExactDerandomization.L_subset_RL line 546
  62. theorem OAI.ExactDerandomization.L_subset_BPL line 552
  63. theorem OAI.ExactDerandomization.inverse_cubic_le_eighth line 558
  64. theorem OAI.ExactDerandomization.no_input_approximation_bound line 567
  65. theorem OAI.ExactDerandomization.yes_input_approximation_bound line 572
  66. theorem OAI.ExactDerandomization.two_trial_probability_gap line 577