Natural number logarithms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[simp]

theorem nat.log_eq_zero_iff {b n : ℕ} :

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

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

@[simp]

theorem nat.log_pos_iff {b n : ℕ} :

0 < nat.log b n ↔ b ≤ n ∧ 1 < b

source

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

0 < nat.log b n

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

@[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 : y ≠ 0) :

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

pow b and log b (almost) form a Galois connection. See also nat.pow_le_of_le_log and nat.le_log_of_pow_le for individual implications under weaker assumptions.

source

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

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

source

theorem nat.pow_le_of_le_log {b x y : ℕ} (hy : y ≠ 0) (h : x ≤ nat.log b y) :

b ^ x ≤ y

source

theorem nat.le_log_of_pow_le {b x y : ℕ} (hb : 1 < b) (h : b ^ x ≤ y) :

x ≤ nat.log b y

source

theorem nat.pow_log_le_self (b : ℕ) {x : ℕ} (hx : x ≠ 0) :

b ^ nat.log b x ≤ x

source

theorem nat.log_lt_of_lt_pow {b x y : ℕ} (hy : y ≠ 0) :

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

source

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

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

source

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

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

source

theorem nat.log_eq_iff {b m n : ℕ} (h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0) :

nat.log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

source

theorem nat.log_eq_of_pow_le_of_lt_pow {b m n : ℕ} (h₁ : b ^ m ≤ n) (h₂ : n < b ^ (m + 1)) :

nat.log b n = m

source

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

nat.log b (b ^ x) = x

source

theorem nat.log_eq_one_iff' {b n : ℕ} :

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

source

theorem nat.log_eq_one_iff {b n : ℕ} :

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

source

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

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

source

theorem nat.pow_log_le_add_one (b x : ℕ) :

b ^ nat.log b x ≤ x + 1

source

theorem nat.log_monotone {b : ℕ} :

monotone (nat.log b)

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_antitone_left {n : ℕ} :

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

source

@[simp]

theorem nat.log_div_base (b n : ℕ) :

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

source

@[simp]

theorem nat.log_div_mul_self (b n : ℕ) :

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

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