Polynomial bounds below exponentials

A resource function polynomially bounded in an input size size is within a constant multiple of 2 ^ size (Turing.MultiTapeTM.PolyBounded.exists_le_mul_two_pow), the form of Cslib.PolynomiallyBounded.exists_le_mul_two_pow for arbitrary inputs. Exponential resource bounds absorb the polynomial costs of their subroutines this way.

Main results

• Turing.MultiTapeTM.PolyBounded.exists_le_mul_two_pow: a polynomially bounded resource function is O(2 ^ size).

theorem Turing.MultiTapeTM.PolyBounded.exists_le_mul_two_pow {α : Type u_1} {size u : α → ℕ} (h : PolyBounded size u) : ∃ (C : ℕ), ∀ (a : α), u a ≤ C * 2 ^ size a

A polynomially bounded resource function is within a constant multiple of 2 ^ size.