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

@[irreducible]

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 x✝ = if h : b ≤ x✝ ∧ 1 < b then Nat.log b (x✝ / b) + 1 else 0

@[simp]

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

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

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

@[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

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.

@[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

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

@[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

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

Ceil logarithm

@[irreducible]

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

• Nat.clog b x✝ = if h : 1 < b ∧ 1 < x✝ then Nat.clog b ((x✝ + b - 1) / b) + 1 else 0

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_of_two_le {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : clog b n = clog b ((n + b - 1) / b) + 1

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

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

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

clog b and pow b form a Galois connection.

@[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

@[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

Computating the logarithm efficiently

def Nat.logC (b m : ℕ) : ℕ

An alternate definition for Nat.log which computes more efficiently. For mathematical purposes, use Nat.log instead, and see Nat.log_eq_logC.

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.logC:

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

The definition Nat.logC is not tail-recursive, however, but the stack limit will only be reached if the output size is around 2^10000, meaning the input will be around 2^(2^10000), which will take far too long to compute in the first place.

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

Equations

• Nat.logC b m = if h : 1 < b then match Nat.logC.step m b h with | (fst, e) => e else 0

@[irreducible]

def Nat.logC.step (m pw : ℕ) (hpw : 1 < pw) : ℕ × ℕ

An auxiliary definition for Nat.logC, where the base of the logarithm is squared in each loop. This allows significantly faster computation of the logarithm: it takes logarithmic time in the size of the output, rather than linear time.

Equations

• Nat.logC.step m pw hpw = if h : m < pw then (m, 0) else match Nat.logC.step m (pw * pw) ⋯ with | (q, e) => if q < pw then (q, 2 * e) else (q / pw, 2 * e + 1)

@[csimp]

theorem Nat.log_eq_logC : log = logC

The result of Nat.log agrees with the result of Nat.logC. The latter will be computed more efficiently, but the former is easier to prove things about and has more lemmas. This lemma is tagged @[csimp] so that the code generated for Nat.log uses Nat.logC instead.