Powers with logarithmic exponents

The power b ^ ⌈log_b n⌉ overshoots n by less than a factor b (Nat.pow_clog_le_mul), so m ^ ⌈log_b n⌉, which is at most (b ^ ⌈log_b m⌉) ^ ⌈log_b n⌉ = (b ^ ⌈log_b n⌉) ^ ⌈log_b m⌉, is at most b ^ ⌈log_b m⌉ * n ^ ⌈log_b m⌉ (Nat.pow_clog_le_pow_clog_mul_pow_clog): a factor m applied ⌈log_b n⌉ times is polynomial in n. This is how the size of an iterated construction stays polynomial after logarithmically many rounds. Similarly 2 ^ (⌊log₂ n⌋ + 1) and 2 ^ ⌈log₂ n⌉ are at most 2 (n + 1) (Nat.two_pow_log2_succ_le, Nat.two_pow_clog_two_le).

Main results

• Nat.pow_clog_le_mul: b ^ ⌈log_b n⌉ ≤ b * n for n ≠ 0.
• Nat.pow_clog_le_pow_clog_mul_pow_clog: m ^ ⌈log_b n⌉ ≤ b ^ ⌈log_b m⌉ * n ^ ⌈log_b m⌉ for n ≠ 0.
• Nat.two_pow_log2_succ_le: 2 ^ (⌊log₂ n⌋ + 1) ≤ 2 (n + 1).
• Nat.two_pow_clog_two_le: 2 ^ ⌈log₂ n⌉ ≤ 2 (n + 1), also for n = 0.

theorem Nat.pow_clog_le_mul {b n : ℕ} (hb : 1 < b) (hn : n ≠ 0) : b ^ clog b n ≤ b * n

The power b ^ ⌈log_b n⌉ overshoots n ≠ 0 by less than a factor b.

theorem Nat.pow_clog_le_pow_clog_mul_pow_clog {b n : ℕ} (hb : 1 < b) (m : ℕ) (hn : n ≠ 0) : m ^ clog b n ≤ b ^ clog b m * n ^ clog b m

A factor m applied ⌈log_b n⌉ times is polynomial in n ≠ 0: m ^ ⌈log_b n⌉ ≤ b ^ ⌈log_b m⌉ * n ^ ⌈log_b m⌉.

theorem Nat.two_pow_log2_succ_le (n : ℕ) : 2 ^ (n.log2 + 1) ≤ 2 * (n + 1)

2 ^ (log₂ n + 1) is at most 2 (n + 1).

theorem Nat.two_pow_clog_two_le (n : ℕ) : 2 ^ clog 2 n ≤ 2 * (n + 1)

2 ^ ⌈log₂ n⌉ is at most 2 (n + 1), also for n = 0.