data.nat.log

# Natural number logarithms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines two ℕ-valued analogs of the logarithm of n with base b:

• log b n: Lower logarithm, or floor log. Greatest k such that b^k ≤ n.
• clog b n: Upper logarithm, or ceil log. Least k such that n ≤ 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.

### Floor logarithm #

def nat.log (b : ) :

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.

Equations
@[simp]
theorem nat.log_eq_zero_iff {b n : } :
n = 0 n < b b 1
theorem nat.log_of_lt {b n : } (hb : n < b) :
n = 0
theorem nat.log_of_left_le_one {b : } (hb : b 1) (n : ) :
n = 0
@[simp]
theorem nat.log_pos_iff {b n : } :
0 < n b n 1 < b
theorem nat.log_pos {b n : } (hb : 1 < b) (hbn : b n) :
0 < n
theorem nat.log_of_one_lt_of_le {b n : } (h : 1 < b) (hn : b n) :
n = (n / b) + 1
@[simp]
theorem nat.log_zero_left (n : ) :
n = 0
@[simp]
theorem nat.log_zero_right (b : ) :
0 = 0
@[simp]
theorem nat.log_one_left (n : ) :
n = 0
@[simp]
theorem nat.log_one_right (b : ) :
1 = 0
theorem nat.pow_le_iff_le_log {b : } (hb : 1 < b) {x y : } (hy : y 0) :
b ^ x y x y

pow b and log b (almost) form a Galois connection. See also nat.pow_le_of_le_log and nat.le_log_of_pow_le for individual implications under weaker assumptions.

theorem nat.lt_pow_iff_log_lt {b : } (hb : 1 < b) {x y : } (hy : y 0) :
y < b ^ x y < x
theorem nat.pow_le_of_le_log {b x y : } (hy : y 0) (h : x y) :
b ^ x y
theorem nat.le_log_of_pow_le {b x y : } (hb : 1 < b) (h : b ^ x y) :
x y
theorem nat.pow_log_le_self (b : ) {x : } (hx : x 0) :
b ^ x x
theorem nat.log_lt_of_lt_pow {b x y : } (hy : y 0) :
y < b ^ x y < x
theorem nat.lt_pow_of_log_lt {b x y : } (hb : 1 < b) :
y < x y < b ^ x
theorem nat.lt_pow_succ_log_self {b : } (hb : 1 < b) (x : ) :
x < b ^ (nat.log b x).succ
theorem nat.log_eq_iff {b m n : } (h : m 0 1 < b n 0) :
n = m b ^ m n n < b ^ (m + 1)
theorem nat.log_eq_of_pow_le_of_lt_pow {b m n : } (h₁ : b ^ m n) (h₂ : n < b ^ (m + 1)) :
n = m
theorem nat.log_pow {b : } (hb : 1 < b) (x : ) :
(b ^ x) = x
theorem nat.log_eq_one_iff' {b n : } :
n = 1 b n n < b * b
theorem nat.log_eq_one_iff {b n : } :
n = 1 n < b * b 1 < b b n
theorem nat.log_mul_base {b n : } (hb : 1 < b) (hn : n 0) :
(n * b) = n + 1
theorem nat.pow_log_le_add_one (b x : ) :
b ^ x x + 1
theorem nat.log_monotone {b : } :
theorem nat.log_mono_right {b n m : } (h : n m) :
n m
theorem nat.log_anti_left {b c n : } (hc : 1 < c) (hb : c b) :
n n
theorem nat.log_antitone_left {n : } :
antitone_on (λ (b : ), n) (set.Ioi 1)
@[simp]
theorem nat.log_div_base (b n : ) :
(n / b) = n - 1
@[simp]
theorem nat.log_div_mul_self (b n : ) :
(n / b * b) = n

### Ceil logarithm #

def nat.clog (b : ) :

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.

Equations
theorem nat.clog_of_left_le_one {b : } (hb : b 1) (n : ) :
n = 0
theorem nat.clog_of_right_le_one {n : } (hn : n 1) (b : ) :
n = 0
@[simp]
theorem nat.clog_zero_left (n : ) :
n = 0
@[simp]
theorem nat.clog_zero_right (b : ) :
0 = 0
@[simp]
theorem nat.clog_one_left (n : ) :
n = 0
@[simp]
theorem nat.clog_one_right (b : ) :
1 = 0
theorem nat.clog_of_two_le {b n : } (hb : 1 < b) (hn : 2 n) :
n = ((n + b - 1) / b) + 1
theorem nat.clog_pos {b n : } (hb : 1 < b) (hn : 2 n) :
0 < n
theorem nat.clog_eq_one {b n : } (hn : 2 n) (h : n b) :
n = 1
theorem nat.le_pow_iff_clog_le {b : } (hb : 1 < b) {x y : } :
x b ^ y x y

clog b and pow b form a Galois connection.

theorem nat.pow_lt_iff_lt_clog {b : } (hb : 1 < b) {x y : } :
b ^ y < x y < x
theorem nat.clog_pow (b x : ) (hb : 1 < b) :
(b ^ x) = x
theorem nat.pow_pred_clog_lt_self {b : } (hb : 1 < b) {x : } (hx : 1 < x) :
b ^ (nat.clog b x).pred < x
theorem nat.le_pow_clog {b : } (hb : 1 < b) (x : ) :
x b ^ x
theorem nat.clog_mono_right (b : ) {n m : } (h : n m) :
n m
theorem nat.clog_anti_left {b c n : } (hc : 1 < c) (hb : c b) :
n n
theorem nat.clog_antitone_left {n : } :
antitone_on (λ (b : ), n) (set.Ioi 1)
theorem nat.log_le_clog (b n : ) :
n n