Natural number logarithms #
This file defines two ℕ
-valued analogs of the logarithm of n
with base b
:
log b n
: Lower logarithm, or floor log. Greatestk
such thatb^k ≤ n
.clog b n
: Upper logarithm, or ceil log. Leastk
such thatn ≤ b^k
.
These are interesting because, for 1 < b
, nat.log b
and nat.clog b
are respectively right and
left adjoints of nat.pow b
. See pow_le_iff_le_log
and le_pow_iff_clog_le
.