English
Let b > 1 and r > 0. Then (b)^{log_b r} ≤ r. The z-power with the logarithm base b does not exceed r.
Русский
Пусть b > 1 и r > 0. Тогда b^{log_b r} ≤ r. Степенная функция по основанию b и логарифму не превосходит r.
LaTeX
$$$(b : \mathbb{R})^{\log_b r} \le r \quad\text{для } b>1,\; r>0$$$
Lean4
theorem zpow_log_le_self {b : ℕ} {r : R} (hb : 1 < b) (hr : 0 < r) : (b : R) ^ log b r ≤ r :=
by
rcases le_total 1 r with hr1 | hr1
· rw [log_of_one_le_right _ hr1]
rw [zpow_natCast, ← Nat.cast_pow, ← Nat.le_floor_iff hr.le]
exact Nat.pow_log_le_self b (Nat.floor_pos.mpr hr1).ne'
· rw [log_of_right_le_one _ hr1, zpow_neg, zpow_natCast, ← Nat.cast_pow]
exact inv_le_of_inv_le₀ hr (Nat.ceil_le.1 <| Nat.le_pow_clog hb _)
