Asymptotic bounds on natural numbers

For any natural base greater than one, exponentials eventually dominate fixed multiples of powers, and fixed multiples of logarithms are eventually at most the input. The inequalities are stated in ℕ; the polynomial bound specializes Mathlib's isLittleO_pow_const_const_pow_of_one_lt.

theorem Nat.eventually_mul_pow_le_pow (c k : ℕ) {b : ℕ} (hb : 1 < b) : ∀ᶠ (n : ℕ) in Filter.atTop, c * n ^ k ≤ b ^ n

Every fixed multiple of a power is eventually at most an exponential of base greater than one.

theorem Nat.eventually_add_one_le_pow_div {b : ℕ} (hb : 1 < b) : ∀ᶠ (n : ℕ) in Filter.atTop, n + 1 ≤ b ^ n / n

The quotient of an exponential of base greater than one by the input is eventually at least the input plus one.

theorem Nat.eventually_mul_log_le (c : ℕ) {b : ℕ} (hb : 1 < b) : ∀ᶠ (n : ℕ) in Filter.atTop, c * log b n ≤ n

Every fixed multiple of the logarithm in a base greater than one is eventually at most the input.

theorem Nat.eventually_mul_log2_le (c : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, c * n.log2 ≤ n

Every fixed multiple of the binary logarithm is eventually at most the input.