feat(data/nat/log): add antitonicity lemmas for first argument (#9597)

`log` and `clog` are only antitone on bases >1, so we include this as an
assumption in `log_le_log_of_left_ge` (resp. `clog_le_...`) and as a
domain restriction in `log_left_gt_one_anti` (resp. `clog_left_...`).

src/data/nat/log.lean

@@ -101,9 +101,23 @@ begin
       exact (pow_log_le_self hb hn).trans h } }
 end
 
-lemma log_mono {b : ℕ} : monotone (λ n : ℕ, log b n) :=
+lemma log_le_log_of_left_ge {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : log b n ≤ log c n :=
+begin
+  cases n, { simp },
+  rw ← pow_le_iff_le_log hc (zero_lt_succ n),
+  exact calc
+    c ^ log b n.succ ≤ b ^ log b n.succ : pow_le_pow_of_le_left
+                                            (le_of_lt $ zero_lt_one.trans hc) hb _
+                 ... ≤ n.succ           : pow_log_le_self (lt_of_lt_of_le hc hb)
+                                            (zero_lt_succ n)
+end
+
+lemma log_monotone {b : ℕ} : monotone (λ n : ℕ, log b n) :=
 λ x y, log_le_log_of_le
 
+lemma log_antitone_left {n : ℕ} : antitone_on (λ b, log b n) (set.Ioi 1) :=
+λ _ hc _ _ hb, log_le_log_of_left_ge (set.mem_Iio.1 hc) hb
+
 private lemma add_pred_div_lt {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : (n + b - 1)/b < n :=
 begin
   rw [div_lt_iff_lt_mul _ _ (zero_lt_one.trans hb), ←succ_le_iff, ←pred_eq_sub_one,
@@ -200,9 +214,21 @@ begin
       exact h.trans (le_pow_clog hb _) } }
 end
 
-lemma clog_mono (b : ℕ) : monotone (clog b) :=
+lemma clog_le_clog_of_left_ge {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : clog b n ≤ clog c n :=
+begin
+  cases n, { simp },
+  rw ← le_pow_iff_clog_le (lt_of_lt_of_le hc hb),
+  exact calc
+    n.succ ≤ c ^ clog c n.succ : le_pow_clog hc _
+       ... ≤ b ^ clog c n.succ : pow_le_pow_of_le_left (le_of_lt $ zero_lt_one.trans hc) hb _
+end
+
+lemma clog_monotone (b : ℕ) : monotone (clog b) :=
 λ x y, clog_le_clog_of_le _
 
+lemma clog_antitone_left {n : ℕ} : antitone_on (λ b : ℕ, clog b n) (set.Ioi 1) :=
+λ _ hc _ _ hb, clog_le_clog_of_left_ge (set.mem_Iio.1 hc) hb
+
 lemma log_le_clog (b n : ℕ) : log b n ≤ clog b n :=
 begin
   obtain hb | hb := le_or_lt b 1,