log_le_clog — Mathlib

English

For all b, n, log_b n ≤ clog_b n.

Русский

Для всех b, n выполняется log_b n ≤ clog_b n.

LaTeX

$$$ \\log_b n \\le \\operatorname{clog}_b n $$$

Lean4

@[simp]
theorem log_le_clog (b n : ℕ) : log b n ≤ clog b n :=
  by
  obtain hb | hb := le_or_gt b 1
  · rw [log_of_left_le_one hb]
    exact zero_le _
  cases n with
  | zero =>
    rw [log_zero_right]
    exact zero_le _
  | succ n => exact (Nat.pow_le_pow_iff_right hb).1 ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)

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