Inequalities on powers of natural numbers

Elementary inequalities on powers and products of natural numbers, in particular powers of two with scaled exponents: products and sums of quantities bounded by 2 ^ (a * k) and 2 ^ (b * k), and bounds by exponentials.

Main results

• Nat.mul_le_two_pow_add_mul: x ≤ 2 ^ (a * k) → y ≤ 2 ^ (b * k) → x * y ≤ 2 ^ ((a + b) * k).
• Nat.add_le_two_pow_add_add_one_mul: 1 ≤ k → x ≤ 2 ^ (a * k) → y ≤ 2 ^ (b * k) → x + y ≤ 2 ^ ((a + b + 1) * k).
• Nat.le_two_pow_mul: 1 ≤ k → c ≤ 2 ^ (c * k).
• Nat.mul_add_one_pow_le: (R + 1) * d ≤ M → R * (M + 1) ^ d ≤ (R + 1) * M ^ d.

theorem Nat.mul_le_two_pow_add_mul {k a b x y : ℕ} (hx : x ≤ 2 ^ (a * k)) (hy : y ≤ 2 ^ (b * k)) : x * y ≤ 2 ^ ((a + b) * k)

Products of numbers below 2 ^ (a * k) and 2 ^ (b * k) are below 2 ^ ((a + b) * k).

theorem Nat.add_le_two_pow_add_add_one_mul {k a b x y : ℕ} (hk : 1 ≤ k) (hx : x ≤ 2 ^ (a * k)) (hy : y ≤ 2 ^ (b * k)) : x + y ≤ 2 ^ ((a + b + 1) * k)

Sums of numbers below 2 ^ (a * k) and 2 ^ (b * k) are below 2 ^ ((a + b + 1) * k).

theorem Nat.le_two_pow_mul (c k : ℕ) (hk : 1 ≤ k) : c ≤ 2 ^ (c * k)

A constant c is below 2 ^ (c * k) for k ≥ 1.

theorem Nat.mul_add_one_pow_le {R M d : ℕ} (h : (R + 1) * d ≤ M) : R * (M + 1) ^ d ≤ (R + 1) * M ^ d

(1 + 1 / M) ^ d ≤ 1 + 1 / R when (R + 1) d ≤ M, without denominators.