self_le_zpow_clog — Mathlib

English

For base b > 1 and any r, the value r is bounded above by b raised to the clog_b(r): r ≤ b^clog_b(r).

Русский

Для основание b>1 и любого r имеем: r ≤ b^{clog_b(r)}.

LaTeX

$$$ r \le (b)^{\operatorname{clog}_b(r)} $$$

Lean4

theorem self_le_zpow_clog {b : ℕ} (hb : 1 < b) (r : R) : r ≤ (b : R) ^ clog b r :=
  by
  rcases le_or_gt r 0 with hr | hr
  · rw [clog_of_right_le_zero _ hr, zpow_zero]
    exact hr.trans zero_le_one
  rw [← neg_log_inv_eq_clog, zpow_neg, le_inv_comm₀ hr (zpow_pos ..)]
  · exact zpow_log_le_self hb (inv_pos.mpr hr)
  · exact Nat.cast_pos.mpr (zero_le_one.trans_lt hb)

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