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

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

@[simp]

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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.

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

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

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

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

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

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

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

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)

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

theorem Nat.log_div_mul_self (b : ℕ) (n : ℕ) : Nat.log b (n / b * b) = Nat.log b 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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

theorem Nat.le_pow_iff_clog_le {b : ℕ} (hb : 1 < b) {x : ℕ} {y : ℕ} : x ≤ b ^ y ↔ Nat.clog b 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 < Nat.clog b x

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

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

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

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

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

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

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

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