mathlib documentation

data.nat.log

Natural number logarithm #

This file defines log b n, the logarithm of n with base b, to be the largest k such that b ^ k ≤ n.

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_eq_zero_of_lt {b n : } (hn : n < b) :
nat.log b n = 0
theorem nat.log_eq_zero_of_le {b n : } (hb : b 1) :
nat.log b n = 0
theorem nat.log_zero_eq_zero {b : } :
nat.log b 0 = 0
theorem nat.log_one_eq_zero {b : } :
nat.log b 1 = 0
theorem nat.log_b_zero_eq_zero {n : } :
nat.log 0 n = 0
theorem nat.log_b_one_eq_zero {n : } :
nat.log 1 n = 0
theorem nat.pow_le_iff_le_log (x y : ) {b : } (hb : 1 < b) (hy : 1 y) :
b ^ x y x nat.log b y
theorem nat.log_pow (b x : ) (hb : 1 < b) :
nat.log b (b ^ x) = x
theorem nat.pow_succ_log_gt_self (b x : ) (hb : 1 < b) (hy : 1 x) :
x < b ^ (nat.log b x).succ
theorem nat.pow_log_le_self (b x : ) (hb : 1 < b) (hx : 1 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_succ {b n : } :
theorem nat.log_mono {b : } :
monotone (λ (n : ), nat.log b n)