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 (b ^ ·). See le_log_iff_pow_le and clog_le_iff_le_pow.

Implementation notes

We define both functions using recursion on b. In order to compute, e.g., Nat.log b n, we compute e = Nat.log (b * b) n first, then figure out whether the answer is 2 * e or 2 * e + 1. The actual implementations use fuel recursion so that (by decide : Nat.log 2 20 = 4) works.

Adapted from https://downloads.haskell.org/~ghc/9.0.1/docs/html/libraries/ghc-bignum-1.0/GHC-Num-BigNat.html#v:bigNatLogBase-35-

Note a tail-recursive version of Nat.log is also possible:

def logTR (b n : ℕ) : ℕ :=
  let rec go : ℕ → ℕ → ℕ | n, acc => if h : b ≤ n ∧ 1 < b then go (n / b) (acc + 1) else acc
  decreasing_by
    have : n / b < n := Nat.div_lt_self (by omega) h.2
    decreasing_trivial
  go n 0

but performs worse for large numbers than Nat.log:

#eval Nat.logTR 2 (2 ^ 1000000)
#eval Nat.log 2 (2 ^ 1000000)

Floor logarithm

def Nat.log (b n : ℕ) : ℕ

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 = if b ≤ 1 then 0 else (Nat.log.go n b n).snd

def Nat.log.go (n : ℕ) : ℕ → ℕ → ℕ × ℕ

An auxiliary definition for Nat.log.

For b > 1, n ≠ 0, n < b ^ fuel, Nat.log.go n b fuel = (n / b ^ b.log n, b.log n).

Equations

• Nat.log.go n x✝ 0 = (n, 0)
• Nat.log.go n x✝ fuel.succ = if n < x✝ then (n, 0) else match Nat.log.go n (x✝ * x✝) fuel with | (q, e) => if q < x✝ then (q, 2 * e) else (q / x✝, 2 * e + 1)

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

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

theorem Nat.log.go_spec {b n fuel : ℕ} (hb : 1 < b) (hn : n ≠ 0) (hfuel : n < b ^ fuel) : (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

(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.

@[deprecated Nat.le_log_iff_pow_le (since := "2025-10-05")]

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

@[deprecated Nat.log_lt_iff_lt_pow (since := "2025-10-05")]

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

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

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

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

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

See also log_lt_of_lt_pow' for a version that assumes x ≠ 0 instead of y ≠ 0.

theorem Nat.log_lt_of_lt_pow' {b x y : ℕ} (hx : x ≠ 0) (hlt : y < b ^ x) : log b y < x

A version of log_lt_of_lt_pow that assumes x ≠ 0 instead of y ≠ 0.

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

theorem Nat.log_lt_self (b : ℕ) {x : ℕ} (hx : x ≠ 0) : log b x < x

theorem Nat.log_le_self (b x : ℕ) : log b x ≤ x

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

theorem Nat.log_eq_iff {b m n : ℕ} (h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0) : log b 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)) : log b n = m

@[simp]

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

theorem Nat.log_div_base_pow (b n k : ℕ) : log b (n / b ^ k) = log b n - k

@[simp]

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

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

theorem Nat.log_two_bit {b : Bool} {n : ℕ} (hn : n ≠ 0) : log 2 (bit b n) = log 2 n + 1

theorem Nat.log2_eq_log_two {n : ℕ} : n.log2 = log 2 n

@[simp]

theorem Nat.log_pow_left (b k n : ℕ) : log (b ^ k) n = log b n / k

Ceil logarithm

def Nat.clog (b n : ℕ) : ℕ

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

• Nat.clog b n = if 1 < b ∧ 1 < n then (Nat.clog.go n b n).snd + 1 else 0

def Nat.clog.go (n : ℕ) : ℕ → ℕ → ℕ × ℕ

An auxiliary definition for Nat.clog.

For n > 1, b > 1, n ≤ b ^ fuel, returns (b ^ clog b n / n, clog b n - 1).

Equations

• Nat.clog.go n x✝ 0 = (x✝ / n, 0)
• Nat.clog.go n x✝ fuel.succ = if n ≤ x✝ then (x✝ / n, 0) else match Nat.clog.go n (x✝ * x✝) fuel with | (q, e) => if q < x✝ then (q, 2 * e + 1) else (q / x✝, 2 * e)

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Nat.clog.go_spec {n b fuel : ℕ} (hn : 1 < n) (hb : 1 < b) (hfuel : n < b ^ fuel) : (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧ b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)

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

For b > 1, clog b and (b ^ ·) form a Galois connection.

See also clog_le_of_le_pow for the implication that does not require 1 < b.

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

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

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

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

theorem Nat.clog_le_of_le_pow {b x y : ℕ} (h : x ≤ b ^ y) : clog b x ≤ y

@[deprecated Nat.clog_le_iff_le_pow (since := "2025-10-05")]

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

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

@[deprecated Nat.lt_clog_iff_pow_lt (since := "2025-10-05")]

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

theorem Nat.pow_lt_of_lt_clog {b x y : ℕ} (h : y < clog b x) : b ^ y < x

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

theorem Nat.clog_lt_clog_succ_iff {b n : ℕ} (hb : 1 < b) : clog b n < clog b (n + 1) ↔ b ^ clog b n = n

theorem Nat.clog_eq_clog_succ_iff {b n : ℕ} (hb : 1 < b) : clog b n = clog b (n + 1) ↔ b ^ clog b n ≠ n

theorem Nat.clog_pow_left (b k n : ℕ) : clog (b ^ k) n = (clog b n + (k - 1)) / k

This lemma says that `⌈log (b ^ k) n⌉ = ⌈(⌈log b n⌉ / k)⌉, using operations on natural numbers to express this equality.

Since Lean has no dedicated function for the ceiling division, we use (a + (b - 1)) / b for ⌈a / b⌉.