From 0f3e4683bc595501c4ec1f7ae6935166f63c8c13 Mon Sep 17 00:00:00 2001 From: Hyeokjun Kwon <86776403+Jun2M@users.noreply.github.com> Date: Thu, 5 Sep 2024 06:53:13 +0000 Subject: [PATCH] feat(Nat/log): Nat.log 2 = Nat.log2 and linear bound on Nat.log (#15096) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit There is a `Nat.log2` function in Lean (Init/Data/Nat/Log2.lean), which corresponds to the floor log base 2 over Nat. This PR proves this connection and uses it to show that `Nat.log b n ≤ n` as a simple upper bound on Nat.log. Co-authored-by: Hyeokjun Kwon Co-authored-by: Yury G. Kudryashov --- Mathlib/Data/Nat/Log.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Mathlib/Data/Nat/Log.lean b/Mathlib/Data/Nat/Log.lean index 65b509ab29c0e..eb2ae3bc58f52 100644 --- a/Mathlib/Data/Nat/Log.lean +++ b/Mathlib/Data/Nat/Log.lean @@ -109,6 +109,15 @@ theorem log_lt_of_lt_pow {b x y : ℕ} (hy : y ≠ 0) : y < b ^ x → log b y < theorem lt_pow_of_log_lt {b x y : ℕ} (hb : 1 < b) : log b y < x → y < b ^ x := lt_imp_lt_of_le_imp_le (le_log_of_pow_le hb) +lemma log_lt_self (b : ℕ) {x : ℕ} (hx : x ≠ 0) : log b x < x := + match le_or_lt b 1 with + | .inl h => log_of_left_le_one h x ▸ Nat.pos_iff_ne_zero.2 hx + | .inr h => log_lt_of_lt_pow hx <| lt_pow_self h _ + +lemma log_le_self (b x : ℕ) : log b x ≤ x := + if hx : x = 0 then by simp [hx] + else (log_lt_self b hx).le + theorem lt_pow_succ_log_self {b : ℕ} (hb : 1 < b) (x : ℕ) : x < b ^ (log b x).succ := lt_pow_of_log_lt hb (lt_succ_self _) @@ -197,6 +206,13 @@ theorem add_pred_div_lt {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : (n + b - 1) / succ_pred_eq_of_pos (by omega)] exact Nat.add_le_mul hn hb +lemma log2_eq_log_two {n : ℕ} : Nat.log2 n = Nat.log 2 n := by + rcases eq_or_ne n 0 with rfl | hn + · rw [log2_zero, log_zero_right] + apply eq_of_forall_le_iff + intro m + rw [Nat.le_log2 hn, ← Nat.pow_le_iff_le_log Nat.one_lt_two hn] + /-! ### Ceil logarithm -/