zpow_pred_clog_lt_self — Mathlib

English

For base b > 1 and positive r, the inequality (b)^{clog_b(r) - 1} < r holds.

Русский

Для основания b>1 и положительного r выполняется (b)^{clog_b(r) - 1} < r.

LaTeX

$$$ (b)^{\operatorname{clog}_b(r) - 1} < r, \quad b>1, r>0 $$$

Lean4

theorem zpow_pred_clog_lt_self {b : ℕ} {r : R} (hb : 1 < b) (hr : 0 < r) : (b : R) ^ (clog b r - 1) < r :=
  by
  rw [← neg_log_inv_eq_clog, ← neg_add', zpow_neg, inv_lt_comm₀ _ hr]
  · exact lt_zpow_succ_log_self hb _
  · exact zpow_pos (Nat.cast_pos.mpr <| zero_le_one.trans_lt hb) _

Похожие утверждения