English
If b > 1 and r > 0, then r < b^{log_b r + 1}. The value r lies strictly below the next power of b after b^{log_b r}.
Русский
Пусть b > 1 и r > 0. Тогда r < b^{log_b r + 1}. Значение находится ниже следующей степени b после b^{log_b r}.
LaTeX
$$$r < b^{\log_b r + 1} \quad\text{для } b>1,\; r>0$$$
Lean4
theorem lt_zpow_succ_log_self {b : ℕ} (hb : 1 < b) (r : R) : r < (b : R) ^ (log b r + 1) :=
by
rcases le_or_gt r 0 with hr | hr
· rw [log_of_right_le_zero _ hr, zero_add, zpow_one]
exact hr.trans_lt (zero_lt_one.trans_le <| mod_cast hb.le)
rcases le_or_gt 1 r with hr1 | hr1
· rw [log_of_one_le_right _ hr1]
rw [Int.ofNat_add_one_out, zpow_natCast, ← Nat.cast_pow]
apply Nat.lt_of_floor_lt
exact Nat.lt_pow_succ_log_self hb _
· rw [log_of_right_le_one _ hr1.le]
have hcri : 1 < r⁻¹ := (one_lt_inv₀ hr).2 hr1
have : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊ :=
Nat.succ_le_of_lt (Nat.clog_pos hb <| Nat.one_lt_cast.1 <| hcri.trans_le (Nat.le_ceil _))
rw [neg_add_eq_sub, ← neg_sub, ← Int.ofNat_one, ← Int.ofNat_sub this, zpow_neg, zpow_natCast,
lt_inv_comm₀ hr (pow_pos (Nat.cast_pos.mpr <| zero_lt_one.trans hb) _), ← Nat.cast_pow]
refine Nat.lt_ceil.1 ?_
exact Nat.pow_pred_clog_lt_self hb <| Nat.one_lt_cast.1 <| hcri.trans_le <| Nat.le_ceil _
