Exponentials of polynomial-time exponents

For an exponent L x computable in unary in polynomial time, 2 ^ L x is computable in unary within time O(2 ^ |x| + 4 ^ L x) and space O(2 ^ |x| + 2 ^ L x) (Turing.MultiTapeTM.ComputableInPolyTime.exists_computableInO_unary_two_pow): compute L x, then double L x times (Turing.MultiTapeTM.ComputableInO.unary_two_pow). The polynomial cost of computing the exponent is absorbed by 2 ^ |x| (Turing.MultiTapeTM.PolyBounded.exists_le_mul_two_pow).

Padding. If f is polynomial-time on pairs (a, N) with N in unary, then a ↦ f (a, 2 ^ ν a) is computable within time and space C 2 ^ (D ν a) (|a| + 1) ^ D, for an exponent ν computable in unary in polynomial time (Turing.MultiTapeTM.ComputableInPolyTime.exists_computableInO_pad). This turns a polynomial-time algorithm on padded inputs into a 2 ^ O(ν a)-time algorithm on the original input.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.exists_computableInO_unary_two_pow: 2 ^ L x in unary within exponential time and space.
• Turing.MultiTapeTM.ComputableInPolyTime.exists_computableInO_pad: polynomial time on inputs padded by 2 ^ ν a gives time and space 2 ^ O(ν a) times a polynomial in |a|.

theorem Turing.MultiTapeTM.ComputableInPolyTime.exists_computableInO_unary_two_pow {α : Type} {enc : α ↪ List Bool} {L : α → ℕ} (hL : ComputableInPolyTime L enc encUnary) : ∃ (C : ℕ), ComputableInO (fun (x : α) => 2 ^ L x) enc encUnary (fun (x : α) => C * 2 ^ (enc x).length + 4 ^ L x) fun (x : α) => C * 2 ^ (enc x).length + 2 ^ L x

2 ^ L x in unary, for an exponent L x computable in unary in polynomial time, within time O(2 ^ |x| + 4 ^ L x) and space O(2 ^ |x| + 2 ^ L x).

theorem Turing.MultiTapeTM.ComputableInPolyTime.exists_computableInO_pad {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α × ℕ → β} {ν : α → ℕ} (hf : ComputableInPolyTime f (encPair encIn encUnary) encOut) (hν : ComputableInPolyTime ν encIn encUnary) : ∃ (C : ℕ) (D : ℕ), ComputableInO (fun (a : α) => f (a, 2 ^ ν a)) encIn encOut (fun (a : α) => C * 2 ^ (D * ν a) * ((encIn a).length + 1) ^ D) fun (a : α) => C * 2 ^ (D * ν a) * ((encIn a).length + 1) ^ D

Polynomial time on padded inputs. If f is polynomial-time on pairs (a, N) with N in unary, then a ↦ f (a, 2 ^ ν a) is computable within time and space C 2 ^ (D ν a) (|a| + 1) ^ D, for an exponent ν computable in unary in polynomial time: write the padding 2 ^ ν a in unary, then run f.