English
clog b n is the least k with n ≤ b^k; equivalently clog_b(n) = min{k ∈ ℕ : n ≤ b^k}.
Русский
clog_b(n) — наименьшее k такое, что n ≤ b^k; эквивалентно clog_b(n) = min{ k ∈ ℕ : n ≤ b^k }.
LaTeX
$$$\operatorname{clog}(b,n) = \min\{ k \in \mathbb{N} : n \le b^k \}$$$
Lean4
/-- `clog b n`, is the upper logarithm of natural number `n` in base `b`. It returns the smallest
`k : ℕ` such that `n ≤ b^k`, so if `b^k = n`, it returns exactly `k`. -/
@[pp_nodot]
def clog (b : ℕ) : ℕ → ℕ
| n => if h : 1 < b ∧ 1 < n then clog b ((n + b - 1) / b) + 1 else 0
decreasing_by
-- putting this in the def triggers the `unusedHavesSuffices` linter:
-- https://github.com/leanprover-community/batteries/issues/428
have : (n + b - 1) / b < n := add_pred_div_lt h.1 h.2
decreasing_trivial
