Comparisons of powers and logarithms

For a base b ∈ (0, 1), a positive real x and natural numbers m and n with 0 < n, the comparison of x ^ n with b ^ m is a comparison of Real.logb b x with the ratio m / n. The inequalities reverse because Real.logb b is antitone for such a base. In the same way, the integer floor ⌊logb b x⌋ is the largest integer n with x ≤ b ^ n.

For a base greater than one, the natural floor of the logarithm locates a real number at least one between two consecutive powers. These intervals support dyadic decompositions and convergence estimates.

Main results

• Real.pow_le_pow_iff_div_le_logb_of_base_lt_one: x ^ n ≤ b ^ m ↔ m / n ≤ logb b x.
• Real.pow_le_pow_iff_logb_le_div_of_base_lt_one: b ^ m ≤ x ^ n ↔ logb b x ≤ m / n.
• Real.le_floor_logb_iff_zpow_le_of_base_lt_one: n ≤ ⌊logb b x⌋ ↔ x ≤ b ^ n for n : ℤ.
• Real.pow_natFloor_logb_le_self: b ^ ⌊logb b x⌋₊ ≤ x for 1 < b and 1 ≤ x.
• Real.lt_pow_natFloor_logb_add_one: x < b ^ (⌊logb b x⌋₊ + 1) for 1 < b and 0 < x.

theorem Real.pow_le_pow_iff_div_le_logb_of_base_lt_one {b x : ℝ} {m n : ℕ} (b_pos : 0 < b) (b_lt_one : b < 1) (hx : 0 < x) (hn : 0 < n) : x ^ n ≤ b ^ m ↔ ↑m / ↑n ≤ logb b x

For a base b ∈ (0, 1) and 0 < x, the power comparison x ^ n ≤ b ^ m is the lower bound m / n ≤ logb b x.

theorem Real.pow_le_pow_iff_logb_le_div_of_base_lt_one {b x : ℝ} {m n : ℕ} (b_pos : 0 < b) (b_lt_one : b < 1) (hx : 0 < x) (hn : 0 < n) : b ^ m ≤ x ^ n ↔ logb b x ≤ ↑m / ↑n

For a base b ∈ (0, 1) and 0 < x, the power comparison b ^ m ≤ x ^ n is the upper bound logb b x ≤ m / n.

theorem Real.le_floor_logb_iff_zpow_le_of_base_lt_one {b x : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) (hx : 0 < x) (n : ℤ) : n ≤ ⌊logb b x⌋ ↔ x ≤ b ^ n

For a base b ∈ (0, 1) and 0 < x, the floor ⌊logb b x⌋ is the largest integer n with x ≤ b ^ n.

theorem Real.pow_natFloor_logb_le_self {b x : ℝ} (hb : 1 < b) (hx : 1 ≤ x) : b ^ ⌊logb b x⌋₊ ≤ x

For b > 1 and x ≥ 1, the power of b at the natural floor of logb b x is at most x.

theorem Real.lt_pow_natFloor_logb_add_one {b x : ℝ} (hb : 1 < b) (hx : 0 < x) : x < b ^ (⌊logb b x⌋₊ + 1)

For b > 1 and 0 < x, x is less than the power of b one past the natural floor of logb b x.