Natural number logarithms #

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

log b n: Lower logarithm, or floor log. Greatest k such that b^k ≤ n.
clog b n: Upper logarithm, or ceil log. Least k such that n ≤ b^k.

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 #

source

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

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

source

theorem nat.log_of_lt {b n : ℕ} (hb : n < b) :

nat.log b n = 0

source

theorem nat.log_of_left_le_one {b : ℕ} (hb : b ≤ 1) (n : ℕ) :

nat.log b n = 0

source

theorem nat.log_of_one_lt_of_le {b n : ℕ} (h : 1 < b) (hn : b ≤ n) :

nat.log b n = nat.log b (n / b) + 1

source

theorem nat.log_eq_zero_iff {b n : ℕ} :

nat.log b n = 0 ↔ n < b ∨ b ≤ 1

source

theorem nat.log_eq_one_iff {b n : ℕ} :

nat.log b n = 1 ↔ n < b * b ∧ 1 < b ∧ b ≤ n

source

@[simp]

theorem nat.log_zero_left (n : ℕ) :

nat.log 0 n = 0

source

@[simp]

theorem nat.log_zero_right (b : ℕ) :

nat.log b 0 = 0

source

@[simp]

theorem nat.log_one_left (n : ℕ) :

nat.log 1 n = 0

source

@[simp]

theorem nat.log_one_right (b : ℕ) :

nat.log b 1 = 0

source

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.

source

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

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

source

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

nat.log b (b ^ x) = x

source

theorem nat.log_pos {b n : ℕ} (hb : 1 < b) (hn : b ≤ n) :

0 < nat.log b n

source

theorem nat.log_mul_base (b n : ℕ) (hb : 1 < b) (hn : 0 < n) :

nat.log b (n * b) = nat.log b n + 1

source

theorem nat.lt_pow_succ_log_self {b : ℕ} (hb : 1 < b) (x : ℕ) :

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

source

theorem nat.pow_log_le_self {b : ℕ} (hb : 1 < b) {x : ℕ} (hx : 0 < x) :

b ^ nat.log b x ≤ x

source

theorem nat.log_mono_right {b n m : ℕ} (h : n ≤ m) :

nat.log b n ≤ nat.log b m

source

theorem nat.log_anti_left {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) :

nat.log b n ≤ nat.log c n

source

theorem nat.log_monotone {b : ℕ} :

monotone (nat.log b)

source

theorem nat.log_antitone_left {n : ℕ} :

antitone_on (λ (b : ℕ), nat.log b n) (set.Ioi 1)

source

@[simp]

theorem nat.log_div_mul_self (b n : ℕ) :

nat.log b (n / b * b) = nat.log b n

source

@[simp]

theorem nat.log_div_base (b n : ℕ) :

nat.log b (n / b) = nat.log b n - 1

Ceil logarithm #

source

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