# 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. 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
• b.log x = if h : b x 1 < b then let_fun this := ; b.log (x / b) + 1 else 0
Instances For
@[simp]
theorem Nat.log_eq_zero_iff {b : } {n : } :
b.log n = 0 n < b b 1
theorem Nat.log_of_lt {b : } {n : } (hb : n < b) :
b.log n = 0
theorem Nat.log_of_left_le_one {b : } (hb : b 1) (n : ) :
b.log n = 0
@[simp]
theorem Nat.log_pos_iff {b : } {n : } :
0 < b.log n b n 1 < b
theorem Nat.log_pos {b : } {n : } (hb : 1 < b) (hbn : b n) :
0 < b.log n
theorem Nat.log_of_one_lt_of_le {b : } {n : } (h : 1 < b) (hn : b n) :
b.log n = b.log (n / b) + 1
@[simp]
theorem Nat.log_zero_left (n : ) :
Nat.log 0 n = 0
@[simp]
theorem Nat.log_zero_right (b : ) :
b.log 0 = 0
@[simp]
theorem Nat.log_one_left (n : ) :
Nat.log 1 n = 0
@[simp]
theorem Nat.log_one_right (b : ) :
b.log 1 = 0
theorem Nat.pow_le_iff_le_log {b : } (hb : 1 < b) {x : } {y : } (hy : y 0) :
b ^ x y x b.log 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 b.log y < x
theorem Nat.pow_le_of_le_log {b : } {x : } {y : } (hy : y 0) (h : x b.log y) :
b ^ x y
theorem Nat.le_log_of_pow_le {b : } {x : } {y : } (hb : 1 < b) (h : b ^ x y) :
x b.log y
theorem Nat.pow_log_le_self (b : ) {x : } (hx : x 0) :
b ^ b.log x x
theorem Nat.log_lt_of_lt_pow {b : } {x : } {y : } (hy : y 0) :
y < b ^ xb.log y < x
theorem Nat.lt_pow_of_log_lt {b : } {x : } {y : } (hb : 1 < b) :
b.log y < xy < b ^ x
theorem Nat.lt_pow_succ_log_self {b : } (hb : 1 < b) (x : ) :
x < b ^ (b.log x).succ
theorem Nat.log_eq_iff {b : } {m : } {n : } (h : m 0 1 < b n 0) :
b.log 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)) :
b.log n = m
theorem Nat.log_pow {b : } (hb : 1 < b) (x : ) :
b.log (b ^ x) = x
theorem Nat.log_eq_one_iff' {b : } {n : } :
b.log n = 1 b n n < b * b
theorem Nat.log_eq_one_iff {b : } {n : } :
b.log n = 1 n < b * b 1 < b b n
theorem Nat.log_mul_base {b : } {n : } (hb : 1 < b) (hn : n 0) :
b.log (n * b) = b.log n + 1
theorem Nat.pow_log_le_add_one (b : ) (x : ) :
b ^ b.log x x + 1
theorem Nat.log_monotone {b : } :
Monotone b.log
theorem Nat.log_mono_right {b : } {n : } {m : } (h : n m) :
b.log n b.log m
theorem Nat.log_anti_left {b : } {c : } {n : } (hc : 1 < c) (hb : c b) :
b.log n c.log n
theorem Nat.log_antitone_left {n : } :
AntitoneOn (fun (b : ) => b.log n) ()
@[simp]
theorem Nat.log_div_base (b : ) (n : ) :
b.log (n / b) = b.log n - 1
@[simp]
theorem Nat.log_div_mul_self (b : ) (n : ) :
b.log (n / b * b) = b.log n
theorem Nat.add_pred_div_lt {b : } {n : } (hb : 1 < b) (hn : 2 n) :
(n + b - 1) / 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
• b.clog x = if h : 1 < b 1 < x then let_fun this := ; b.clog ((x + b - 1) / b) + 1 else 0
Instances For
theorem Nat.clog_of_left_le_one {b : } (hb : b 1) (n : ) :
b.clog n = 0
theorem Nat.clog_of_right_le_one {n : } (hn : n 1) (b : ) :
b.clog n = 0
@[simp]
theorem Nat.clog_zero_left (n : ) :
Nat.clog 0 n = 0
@[simp]
theorem Nat.clog_zero_right (b : ) :
b.clog 0 = 0
@[simp]
theorem Nat.clog_one_left (n : ) :
Nat.clog 1 n = 0
@[simp]
theorem Nat.clog_one_right (b : ) :
b.clog 1 = 0
theorem Nat.clog_of_two_le {b : } {n : } (hb : 1 < b) (hn : 2 n) :
b.clog n = b.clog ((n + b - 1) / b) + 1
theorem Nat.clog_pos {b : } {n : } (hb : 1 < b) (hn : 2 n) :
0 < b.clog n
theorem Nat.clog_eq_one {b : } {n : } (hn : 2 n) (h : n b) :
b.clog n = 1
theorem Nat.le_pow_iff_clog_le {b : } (hb : 1 < b) {x : } {y : } :
x b ^ y b.clog 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 < b.clog x
theorem Nat.clog_pow (b : ) (x : ) (hb : 1 < b) :
b.clog (b ^ x) = x
theorem Nat.pow_pred_clog_lt_self {b : } (hb : 1 < b) {x : } (hx : 1 < x) :
b ^ (b.clog x).pred < x
theorem Nat.le_pow_clog {b : } (hb : 1 < b) (x : ) :
x b ^ b.clog x
theorem Nat.clog_mono_right (b : ) {n : } {m : } (h : n m) :
b.clog n b.clog m
theorem Nat.clog_anti_left {b : } {c : } {n : } (hc : 1 < c) (hb : c b) :
b.clog n c.clog n
theorem Nat.clog_monotone (b : ) :
Monotone b.clog
theorem Nat.clog_antitone_left {n : } :
AntitoneOn (fun (b : ) => b.clog n) ()
theorem Nat.log_le_clog (b : ) (n : ) :
b.log n b.clog n