feat(Nat/log): Nat.log 2 = Nat.log2 and linear bound on Nat.log (#15096)

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 <[email protected]>
Co-authored-by: Yury G. Kudryashov <[email protected]>

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 -/