mathlib documentation

data.nat.log

Natural number logarithms #

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

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
theorem nat.log_eq_zero {b n : } (hnb : n < b b 1) :
nat.log b n = 0
theorem nat.log_of_lt {b n : } (hnb : n < b) :
nat.log b n = 0
theorem nat.log_of_left_le_one {b n : } (hb : b 1) :
nat.log b n = 0
@[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 : 0 < y) :
b ^ x y x nat.log b y

pow b and log b (almost) form a Galois connection.

theorem nat.log_pow {b : } (hb : 1 < b) (x : ) :
nat.log b (b ^ x) = x
theorem nat.log_pos {b n : } (hb : 1 < b) (hn : b n) :
0 < nat.log b n
theorem nat.lt_pow_succ_log_self {b : } (hb : 1 < b) {x : } (hx : 0 < x) :
x < b ^ (nat.log b x).succ
theorem nat.pow_log_le_self {b : } (hb : 1 < b) {x : } (hx : 0 < x) :
b ^ nat.log b x x
theorem nat.log_le_log_of_le {b n m : } (h : n m) :
theorem nat.log_le_log_of_left_ge {b c n : } (hc : 1 < c) (hb : c b) :
theorem nat.log_monotone {b : } :
monotone (λ (n : ), nat.log b n)
theorem nat.log_antitone_left {n : } :
antitone_on (λ (b : ), nat.log b n) (set.Ioi 1)

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 : ) :
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.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.clog b x).pred < x
theorem nat.le_pow_clog {b : } (hb : 1 < b) (x : ) :
x b ^ nat.clog b x
theorem nat.clog_le_clog_of_le (b : ) {n m : } (h : n m) :
theorem nat.clog_le_clog_of_left_ge {b c n : } (hc : 1 < c) (hb : c b) :
theorem nat.clog_antitone_left {n : } :
antitone_on (λ (b : ), nat.clog b n) (set.Ioi 1)
theorem nat.log_le_clog (b n : ) :