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 a : ℕ) :

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

nat.log b n = ite (b ≤ n ∧ 1 < b) (nat.log b (n / b) + 1) 0

source

theorem nat.pow_le_iff_le_log (x y : ℕ) {b : ℕ} (hb : 1 < b) (hy : 1 ≤ y) :

b ^ x ≤ y ↔ x ≤ nat.log b y

source

theorem nat.log_pow (b x : ℕ) (hb : 1 < b) :

nat.log b (b ^ x) = x

source

theorem nat.pow_succ_log_gt_self (b x : ℕ) (hb : 1 < b) (hy : 1 ≤ x) :

x < b ^ (nat.log b x).succ

source

theorem nat.pow_log_le_self (b x : ℕ) (hb : 1 < b) (hx : 1 ≤ x) :

b ^ nat.log b x ≤ x