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

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

• b.log x = if h : b ≤ x ∧ 1 < b then let_fun this := ⋯; b.log (x / b) + 1 else 0

@[simp]

theorem Nat.log_eq_zero_iff {b : ℕ} {n : ℕ} : b.log n = 0 ↔ n < b ∨ b ≤ 1

theorem Nat.log_of_lt {b : ℕ} {n : ℕ} (hb : n < b) : b.log n = 0

theorem Nat.log_of_left_le_one {b : ℕ} (hb : b ≤ 1) (n : ℕ) : b.log n = 0

@[simp]

theorem Nat.log_pos_iff {b : ℕ} {n : ℕ} : 0 < b.log n ↔ b ≤ n ∧ 1 < b

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

theorem Nat.log_of_one_lt_of_le {b : ℕ} {n : ℕ} (h : 1 < b) (hn : b ≤ n) : b.log n = b.log (n / b) + 1

@[simp]

theorem Nat.log_zero_left (n : ℕ) : Nat.log 0 n = 0

@[simp]

theorem Nat.log_zero_right (b : ℕ) : b.log 0 = 0

@[simp]

theorem Nat.log_one_left (n : ℕ) : Nat.log 1 n = 0

@[simp]

theorem Nat.log_one_right (b : ℕ) : b.log 1 = 0

theorem Nat.pow_le_iff_le_log {b : ℕ} (hb : 1 < b) {x : ℕ} {y : ℕ} (hy : y ≠ 0) : b ^ x ≤ y ↔ x ≤ b.log 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.

theorem Nat.lt_pow_iff_log_lt {b : ℕ} (hb : 1 < b) {x : ℕ} {y : ℕ} (hy : y ≠ 0) : y < b ^ x ↔ b.log y < x

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

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

theorem Nat.pow_log_le_self (b : ℕ) {x : ℕ} (hx : x ≠ 0) : b ^ b.log x ≤ x

theorem Nat.log_lt_of_lt_pow {b : ℕ} {x : ℕ} {y : ℕ} (hy : y ≠ 0) : y < b ^ x → b.log y < x

theorem Nat.lt_pow_of_log_lt {b : ℕ} {x : ℕ} {y : ℕ} (hb : 1 < b) : b.log y < x → y < b ^ x

theorem Nat.lt_pow_succ_log_self {b : ℕ} (hb : 1 < b) (x : ℕ) : x < b ^ (b.log x).succ

theorem Nat.log_eq_iff {b : ℕ} {m : ℕ} {n : ℕ} (h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0) : b.log n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

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

theorem Nat.log_pow {b : ℕ} (hb : 1 < b) (x : ℕ) : b.log (b ^ x) = x

theorem Nat.log_eq_one_iff' {b : ℕ} {n : ℕ} : b.log n = 1 ↔ b ≤ n ∧ n < b * b

theorem Nat.log_eq_one_iff {b : ℕ} {n : ℕ} : b.log n = 1 ↔ n < b * b ∧ 1 < b ∧ b ≤ n

theorem Nat.log_mul_base {b : ℕ} {n : ℕ} (hb : 1 < b) (hn : n ≠ 0) : b.log (n * b) = b.log n + 1

theorem Nat.pow_log_le_add_one (b : ℕ) (x : ℕ) : b ^ b.log x ≤ x + 1

theorem Nat.log_monotone {b : ℕ} : Monotone b.log

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

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

theorem Nat.log_antitone_left {n : ℕ} : AntitoneOn (fun (b : ℕ) => b.log n) (Set.Ioi 1)

@[simp]

theorem Nat.log_div_base (b : ℕ) (n : ℕ) : b.log (n / b) = b.log n - 1

@[simp]

theorem Nat.log_div_mul_self (b : ℕ) (n : ℕ) : b.log (n / b * b) = b.log n

theorem Nat.add_pred_div_lt {b : ℕ} {n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : (n + b - 1) / b < n

Ceil logarithm

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

• b.clog x = if h : 1 < b ∧ 1 < x then let_fun this := ⋯; b.clog ((x + b - 1) / b) + 1 else 0

theorem Nat.clog_of_left_le_one {b : ℕ} (hb : b ≤ 1) (n : ℕ) : b.clog n = 0

theorem Nat.clog_of_right_le_one {n : ℕ} (hn : n ≤ 1) (b : ℕ) : b.clog n = 0

@[simp]

theorem Nat.clog_zero_left (n : ℕ) : Nat.clog 0 n = 0

@[simp]

theorem Nat.clog_zero_right (b : ℕ) : b.clog 0 = 0

@[simp]

theorem Nat.clog_one_left (n : ℕ) : Nat.clog 1 n = 0

@[simp]

theorem Nat.clog_one_right (b : ℕ) : b.clog 1 = 0

theorem Nat.clog_of_two_le {b : ℕ} {n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : b.clog n = b.clog ((n + b - 1) / b) + 1

theorem Nat.clog_pos {b : ℕ} {n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : 0 < b.clog n

theorem Nat.clog_eq_one {b : ℕ} {n : ℕ} (hn : 2 ≤ n) (h : n ≤ b) : b.clog n = 1

theorem Nat.le_pow_iff_clog_le {b : ℕ} (hb : 1 < b) {x : ℕ} {y : ℕ} : x ≤ b ^ y ↔ b.clog x ≤ y

clog b and pow b form a Galois connection.

theorem Nat.pow_lt_iff_lt_clog {b : ℕ} (hb : 1 < b) {x : ℕ} {y : ℕ} : b ^ y < x ↔ y < b.clog x

theorem Nat.clog_pow (b : ℕ) (x : ℕ) (hb : 1 < b) : b.clog (b ^ x) = x

theorem Nat.pow_pred_clog_lt_self {b : ℕ} (hb : 1 < b) {x : ℕ} (hx : 1 < x) : b ^ (b.clog x).pred < x

theorem Nat.le_pow_clog {b : ℕ} (hb : 1 < b) (x : ℕ) : x ≤ b ^ b.clog x

theorem Nat.clog_mono_right (b : ℕ) {n : ℕ} {m : ℕ} (h : n ≤ m) : b.clog n ≤ b.clog m

theorem Nat.clog_anti_left {b : ℕ} {c : ℕ} {n : ℕ} (hc : 1 < c) (hb : c ≤ b) : b.clog n ≤ c.clog n

theorem Nat.clog_monotone (b : ℕ) : Monotone b.clog

theorem Nat.clog_antitone_left {n : ℕ} : AntitoneOn (fun (b : ℕ) => b.clog n) (Set.Ioi 1)

theorem Nat.log_le_clog (b : ℕ) (n : ℕ) : b.log n ≤ b.clog n