# Documentation

Mathlib.Data.Nat.Log

# 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≤ n.
• clog b n: Upper logarithm, or ceil log. Least k such that n ≤ b^k≤ 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≤ n, so if b^k = n, it returns exactly k.

Equations
@[simp]
theorem Nat.log_eq_zero_iff {b : } {n : } :
Nat.log b n = 0 n < b b 1
theorem Nat.log_of_lt {b : } {n : } (hb : n < b) :
Nat.log b n = 0
theorem Nat.log_of_left_le_one {b : } (hb : b 1) (n : ) :
Nat.log b n = 0
@[simp]
theorem Nat.log_pos_iff {b : } {n : } :
0 < Nat.log b n b n 1 < b
theorem Nat.log_pos {b : } {n : } (hb : 1 < b) (hbn : b n) :
0 < Nat.log b n
theorem Nat.log_of_one_lt_of_le {b : } {n : } (h : 1 < b) (hn : b n) :
Nat.log b n = Nat.log b (n / b) + 1
@[simp]
theorem Nat.log_zero_left (n : ) :
Nat.log 0 n = 0
@[simp]
theorem Nat.log_zero_right (b : ) :
Nat.log b 0 = 0
@[simp]
theorem Nat.log_one_left (n : ) :
Nat.log 1 n = 0
@[simp]
theorem Nat.log_one_right (b : ) :
Nat.log b 1 = 0
theorem Nat.pow_le_iff_le_log {b : } (hb : 1 < b) {x : } {y : } (hy : y 0) :
b ^ x y x Nat.log b 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 Nat.log b y < x
theorem Nat.pow_le_of_le_log {b : } {x : } {y : } (hy : y 0) (h : x Nat.log b y) :
b ^ x y
theorem Nat.le_log_of_pow_le {b : } {x : } {y : } (hb : 1 < b) (h : b ^ x y) :
x Nat.log b y
theorem Nat.pow_log_le_self (b : ) {x : } (hx : x 0) :
b ^ Nat.log b x x
theorem Nat.log_lt_of_lt_pow {b : } {x : } {y : } (hy : y 0) :
y < b ^ xNat.log b y < x
theorem Nat.lt_pow_of_log_lt {b : } {x : } {y : } (hb : 1 < b) :
Nat.log b y < xy < b ^ x
theorem Nat.lt_pow_succ_log_self {b : } (hb : 1 < b) (x : ) :
x < b ^ Nat.succ (Nat.log b x)
theorem Nat.log_eq_iff {b : } {m : } {n : } (h : m 0 1 < b n 0) :
Nat.log b 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)) :
Nat.log b n = m
theorem Nat.log_pow {b : } (hb : 1 < b) (x : ) :
Nat.log b (b ^ x) = x
theorem Nat.log_eq_one_iff' {b : } {n : } :
Nat.log b n = 1 b n n < b * b
theorem Nat.log_eq_one_iff {b : } {n : } :
Nat.log b n = 1 n < b * b 1 < b b n
theorem Nat.log_mul_base {b : } {n : } (hb : 1 < b) (hn : n 0) :
Nat.log b (n * b) = Nat.log b n + 1
theorem Nat.pow_log_le_add_one (b : ) (x : ) :
b ^ Nat.log b x x + 1
theorem Nat.log_mono_right {b : } {n : } {m : } (h : n m) :
theorem Nat.log_anti_left {b : } {c : } {n : } (hc : 1 < c) (hb : c b) :
theorem Nat.log_antitone_left {n : } :
AntitoneOn (fun b => Nat.log b n) ()
@[simp]
theorem Nat.log_div_base (b : ) (n : ) :
Nat.log b (n / b) = Nat.log b n - 1
@[simp]
theorem Nat.log_div_mul_self (b : ) (n : ) :
Nat.log b (n / b * b) = Nat.log b 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≤ b^k, so if b^k = n, it returns exactly k.

Equations
theorem Nat.clog_of_left_le_one {b : } (hb : b 1) (n : ) :
Nat.clog b n = 0
theorem Nat.clog_of_right_le_one {n : } (hn : n 1) (b : ) :
Nat.clog b n = 0
@[simp]
theorem Nat.clog_zero_left (n : ) :
Nat.clog 0 n = 0
@[simp]
theorem Nat.clog_zero_right (b : ) :
Nat.clog b 0 = 0
@[simp]
theorem Nat.clog_one_left (n : ) :
Nat.clog 1 n = 0
@[simp]
theorem Nat.clog_one_right (b : ) :
Nat.clog b 1 = 0
theorem Nat.clog_of_two_le {b : } {n : } (hb : 1 < b) (hn : 2 n) :
Nat.clog b n = Nat.clog b ((n + b - 1) / b) + 1
theorem Nat.clog_pos {b : } {n : } (hb : 1 < b) (hn : 2 n) :
0 < Nat.clog b n
theorem Nat.clog_eq_one {b : } {n : } (hn : 2 n) (h : n b) :
Nat.clog b n = 1
theorem Nat.le_pow_iff_clog_le {b : } (hb : 1 < b) {x : } {y : } :
x b ^ y Nat.clog b 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 < Nat.clog b x
theorem Nat.clog_pow (b : ) (x : ) (hb : 1 < b) :
Nat.clog b (b ^ x) = x
theorem Nat.pow_pred_clog_lt_self {b : } (hb : 1 < b) {x : } (hx : 1 < x) :
b ^ Nat.pred (Nat.clog b x) < x
theorem Nat.le_pow_clog {b : } (hb : 1 < b) (x : ) :
x b ^ Nat.clog b x
theorem Nat.clog_mono_right (b : ) {n : } {m : } (h : n m) :
theorem Nat.clog_anti_left {b : } {c : } {n : } (hc : 1 < c) (hb : c b) :
theorem Nat.clog_antitone_left {n : } :
AntitoneOn (fun b => Nat.clog b n) ()
theorem Nat.log_le_clog (b : ) (n : ) :