English
logC(b, m) is an efficient alternative to the standard Nat.log, defined via a tail-recursive step.
Русский
logC(b, m) — эффективная альтернатива стандартному Nat.log, задается хвостовой рекурсией.
LaTeX
$$$\\text{logC}(b,m) := \\text{упрощение логарифма через шаг}$$$
Lean4
/-- An alternate definition for `Nat.log` which computes more efficiently. For mathematical purposes,
use `Nat.log` instead, and see `Nat.log_eq_logC`.
Note a tail-recursive version of `Nat.log` is also possible:
```
def logTR (b n : ℕ) : ℕ :=
let rec go : ℕ → ℕ → ℕ | n, acc => if h : b ≤ n ∧ 1 < b then go (n / b) (acc + 1) else acc
decreasing_by
have : n / b < n := Nat.div_lt_self (by omega) h.2
decreasing_trivial
go n 0
```
but performs worse for large numbers than `Nat.logC`:
```
#eval Nat.logTR 2 (2 ^ 1000000)
#eval Nat.logC 2 (2 ^ 1000000)
```
The definition `Nat.logC` is not tail-recursive, however, but the stack limit will only be reached
if the output size is around 2^10000, meaning the input will be around 2^(2^10000), which will
take far too long to compute in the first place.
Adapted from https://downloads.haskell.org/~ghc/9.0.1/docs/html/libraries/ghc-bignum-1.0/GHC-Num-BigNat.html#v:bigNatLogBase-35-
-/
@[pp_nodot]
def logC (b m : ℕ) : ℕ :=
if h : 1 < b then
let (_, e) := step b h;
e
else 0
where/-- An auxiliary definition for `Nat.logC`, where the base of the logarithm is _squared_ in each
loop. This allows significantly faster computation of the logarithm: it takes logarithmic time
in the size of the output, rather than linear time.
-/
step (pw : ℕ) (hpw : 1 < pw) : ℕ × ℕ :=
if h : m < pw then (m, 0)
else
let (q, e) := step (pw * pw) (Nat.mul_lt_mul_of_lt_of_lt hpw hpw)
if q < pw then (q, 2 * e) else (q / pw, 2 * e + 1)
termination_by m / pw
decreasing_by
have : m / (pw * pw) < m / pw := logC_aux hpw (le_of_not_gt h)
decreasing_trivial
