Further asymptotic bounds on natural numbers

For any natural base b > 1, Nat.log b tends to infinity at infinity (Nat.tendsto_log_atTop), every affine function of a shifted logarithm a + c * log b (n + d) is eventually at most n (Nat.eventually_add_mul_log_add_le), and every fixed multiple of (n + 1) ^ k is eventually at most b ^ n (Nat.eventually_mul_add_one_pow_le_pow) and at most b ^ (n / m) for m > 0 (Nat.eventually_mul_add_one_pow_le_pow_div).

Main results

• Nat.tendsto_log_atTop: Tendsto (Nat.log b) atTop atTop for 1 < b.
• Nat.eventually_le_log: ∀ᶠ n in atTop, k ≤ Nat.log b n for 1 < b.
• Nat.eventually_add_mul_log_add_le: ∀ᶠ n in atTop, a + c * Nat.log b (n + d) ≤ n for 1 < b.
• Nat.eventually_add_mul_log_le: ∀ᶠ n in atTop, a + c * Nat.log b n ≤ n for 1 < b.
• Nat.eventually_mul_add_one_pow_le_pow_div: ∀ᶠ n in atTop, c * (n + 1) ^ k ≤ b ^ (n / m) for 1 < b and 0 < m.
• Nat.eventually_mul_add_one_pow_le_pow: ∀ᶠ n in atTop, c * (n + 1) ^ k ≤ b ^ n for 1 < b.
• Nat.eventually_mul_pow_le_pow_div: ∀ᶠ n in atTop, c * n ^ k ≤ b ^ (n / m) for 1 < b and 0 < m.
• Nat.eventually_add_one_pow_mul_lt_pow: ∀ᶠ n in atTop, (n + 1) ^ k * n < b ^ n for 1 < b.

theorem Nat.tendsto_log_atTop {b : ℕ} (hb : 1 < b) : Filter.Tendsto (log b) Filter.atTop Filter.atTop

The base-b logarithm tends to infinity for 1 < b.

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

Every constant is eventually at most log b n for 1 < b.

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

Every affine function of a shifted logarithm a + c * log b (n + d) is eventually at most n for 1 < b.

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

Every affine function a + c * log b n is eventually at most n for 1 < b.

theorem Nat.eventually_mul_add_one_pow_le_pow_div (c k m : ℕ) {b : ℕ} (hb : 1 < b) (hm : 0 < m) : ∀ᶠ (n : ℕ) in Filter.atTop, c * (n + 1) ^ k ≤ b ^ (n / m)

Every fixed multiple of (n + 1) ^ k is eventually at most b ^ (n / m) for 1 < b and 0 < m.

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

Every fixed multiple of (n + 1) ^ k is eventually at most b ^ n for 1 < b.

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

Every fixed multiple of n ^ k is eventually at most b ^ (n / m) for 1 < b and 0 < m.

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

Every (n + 1) ^ k * n is eventually strictly below b ^ n for 1 < b.