feat(data/nat/log): add some lemmas and monotonicity (#6899)

src/data/nat/log.lean

@@ -24,6 +24,33 @@ such that `b^k ≤ n`, so if `b^k = n`, it returns exactly `k`. -/
     log (n / b) + 1
   else 0
 
+lemma log_eq_zero {b n : ℕ} (hnb : n < b ∨ b ≤ 1) : log b n = 0 :=
+begin
+  rw [or_iff_not_and_not, not_lt, not_le] at hnb,
+  rw [log, ←ite_not, if_pos hnb],
+end
+
+lemma log_eq_zero_of_lt {b n : ℕ} (hn : n < b) : log b n = 0 :=
+log_eq_zero $ or.inl hn
+
+lemma log_eq_zero_of_le {b n : ℕ} (hb : b ≤ 1) : log b n = 0 :=
+log_eq_zero $ or.inr hb
+
+lemma log_zero_eq_zero {b : ℕ} : log b 0 = 0 :=
+by { cases b; refl }
+
+lemma log_one_eq_zero {b : ℕ} : log b 1 = 0 :=
+if h : b ≤ 1 then
+  log_eq_zero_of_le h
+else
+  log_eq_zero_of_lt (not_le.mp h)
+
+lemma log_b_zero_eq_zero {n : ℕ} : log 0 n = 0 :=
+log_eq_zero_of_le zero_le_one
+
+lemma log_b_one_eq_zero {n : ℕ} : log 1 n = 0 :=
+log_eq_zero_of_le rfl.ge
+
 lemma pow_le_iff_le_log (x y : ℕ) {b} (hb : 1 < b) (hy : 1 ≤ y) :
   b^x ≤ y ↔ x ≤ log b y :=
 begin
@@ -64,4 +91,20 @@ end
 lemma pow_log_le_self (b x : ℕ) (hb : 1 < b) (hx : 1 ≤ x) : b ^ log b x ≤ x :=
 by rw [pow_le_iff_le_log _ _ hb hx]
 
+lemma log_le_log_of_le {b n m : ℕ} (h : n ≤ m) : log b n ≤ log b m :=
+begin
+  cases le_or_lt b 1 with hb hb,
+  { rw log_eq_zero_of_le hb, exact zero_le _ },
+  { cases eq_zero_or_pos n with hn hn,
+    { rw [hn, log_zero_eq_zero], exact zero_le _ },
+    { rw ←pow_le_iff_le_log _ _ hb (lt_of_lt_of_le hn h),
+      exact (pow_log_le_self b n hb hn).trans h } }
+end
+
+lemma log_le_log_succ {b n : ℕ} : log b n ≤ log b n.succ :=
+log_le_log_of_le $ le_succ n
+
+lemma log_mono {b : ℕ} : monotone (λ n : ℕ, log b n) :=
+monotone_of_monotone_nat $ λ n, log_le_log_succ
+
 end nat