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.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