Polynomial bounds are eventually below exponentials

A polynomially bounded function is eventually smaller than 2 ^ n (PolynomiallyBounded.eventually_lt_two_pow): exponential lower bounds rule out polynomial upper bounds. Summing the finitely many exceptions, it is bounded everywhere by a constant multiple of 2 ^ n (PolynomiallyBounded.exists_le_mul_two_pow).

Main results

• Cslib.PolynomiallyBounded.eventually_lt_two_pow.
• Cslib.PolynomiallyBounded.exists_le_mul_two_pow.

theorem Cslib.PolynomiallyBounded.eventually_lt_two_pow {f : ℕ → ℕ} (hf : PolynomiallyBounded f) : ∀ᶠ (n : ℕ) in Filter.atTop, f n < 2 ^ n

A polynomially bounded function is eventually below 2 ^ n.

theorem Cslib.PolynomiallyBounded.exists_le_mul_two_pow {p : ℕ → ℕ} (hp : PolynomiallyBounded p) : ∃ (C : ℕ), ∀ (n : ℕ), p n ≤ C * 2 ^ n

A polynomially bounded function is bounded by a constant multiple of 2 ^ n.