Exponential time bounds in a space bound

The simulations of space-bounded nondeterministic and alternating machines by deterministic ones run within time 2 ^ (c * (log₂ n + S n + 1)), where S n = c₁ * s n + c₂ is the space bound of the simulated machine. These lemmas put such a bound into the shape 2 ^ O(log₂ n + s n), and into 2 ^ O(s n) when log₂ n ≤ s n.

Main results

• Cslib.Complexity.DTIME_two_pow_log2_add_mul_add_subset: the constants of the space bound move into the exponent's factor.
• Cslib.Complexity.DTIME_two_pow_log2_add_subset: above logarithmic space, the logarithm is absorbed.
• Cslib.Complexity.DTIME_two_pow_mul_log2_succ_subset: in logarithmic space, the bound is polynomial.

theorem Cslib.Complexity.DTIME_two_pow_log2_add_mul_add_subset {α : Type} {enc : α ↪ List Bool} (c c₁ c₂ : ℕ) (s : ℕ → ℕ) : (DTIME enc fun (n : ℕ) => 2 ^ (c * (n.log2 + (c₁ * s n + c₂) + 1))) ⊆ DTIME enc fun (n : ℕ) => 2 ^ (c * (c₁ + c₂ + 1) * (n.log2 + s n + 1))

The constants of a space bound move into the exponent's factor: the class DTIME (2 ^ (c * (log₂ n + (c₁ * s n + c₂) + 1))) is within DTIME (2 ^ (c * (c₁ + c₂ + 1) * (log₂ n + s n + 1))).

theorem Cslib.Complexity.DTIME_two_pow_log2_add_subset {α : Type} {enc : α ↪ List Bool} {c : ℕ} {s : ℕ → ℕ} (hs : ∀ (n : ℕ), n.log2 ≤ s n) : (DTIME enc fun (n : ℕ) => 2 ^ (c * (n.log2 + s n + 1))) ⊆ DTIME enc fun (n : ℕ) => 2 ^ (2 * c * s n)

Above logarithmic space, the logarithm is absorbed: when log₂ n ≤ s n, DTIME (2 ^ (c * (log₂ n + s n + 1))) ⊆ DTIME (2 ^ (2 * c * s n)).

theorem Cslib.Complexity.DTIME_two_pow_mul_log2_succ_subset {α : Type} {enc : α ↪ List Bool} (d : ℕ) : (DTIME enc fun (n : ℕ) => 2 ^ (d * (n.log2 + 1))) ⊆ DTIME enc fun (n : ℕ) => n ^ d

In logarithmic space, the bound is polynomial: DTIME (2 ^ (d * (log₂ n + 1))) ⊆ DTIME (n ^ d), since 2 ^ log₂ n ≤ n.