clog_of_right_le_one — Mathlib

English

If r ≥ 1, then clog(b, r) = Nat.clog(b, ceil(r)_+).

Русский

Если r ≥ 1, то clog(b, r) = Nat.clog(b, ceil(r)_+).

LaTeX

$$$\operatorname{clog}(b, r) = \mathrm{Nat.clog}(b, \lceil r \rceil_+)$$$

Lean4

theorem clog_of_right_le_one (b : ℕ) {r : R} (hr : r ≤ 1) : clog b r = -Nat.log b ⌊r⁻¹⌋₊ :=
  by
  obtain rfl | hr := hr.eq_or_lt
  ·
    rw [clog, if_pos hr, inv_one, Nat.ceil_one, Nat.floor_one, Nat.log_one_right, Nat.clog_one_right, Int.ofNat_zero,
      neg_zero]
  · exact if_neg hr.not_ge

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