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  :

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 : } :
1 < b1 y(b ^ x y x nat.log b y)

theorem nat.log_pow (b x : ) :
1 < bnat.log b (b ^ x) = x

theorem nat.pow_succ_log_gt_self (b x : ) :
1 < b1 xx < b ^ (nat.log b x).succ

theorem nat.pow_log_le_self (b x : ) :
1 < b1 xb ^ nat.log b x x