English
The function log(b, n) is the logarithm of n in base b: it returns the largest k such that b^k ≤ n, with the convention that if b ≤ 1 or n < b the value is 0.
Русский
Функция log(b, n) — это логарифм числа n по основанию b: наибольший k such that b^k ≤ n, при этом если b ≤ 1 или n < b, логарифм равен 0.
LaTeX
$$$\\log_b(n) = \\max\\{k \\in \\mathbb{N} : b^{k} \\le n\\}.$$$
Lean4
/-- `log b n`, is the logarithm of natural number `n` in base `b`. It returns the largest `k : ℕ`
such that `b^k ≤ n`, so if `b^k = n`, it returns exactly `k`. -/
@[pp_nodot]
def log (b : ℕ) : ℕ → ℕ
| n => if h : b ≤ n ∧ 1 < b then log b (n / 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 < n := div_lt_self ((Nat.zero_lt_one.trans h.2).trans_le h.1) h.2
decreasing_trivial
