feat(data/nat/log): review/extend API (#17809)

urkud · urkud · commit dc9db5411687 · 2022-12-06T20:53:41.000Z
* Add `nat.lt_mul_self_iff`.
* Mark `nat.log_eq_zero_iff` as `@[simp]`.
* Add a `@[simp]` lemma `nat.log_pos_iff`.
* Assume `≠ 0` instead of `0 &lt;` in `nat.pow_le_iff_le_log` and
  `nat.lt_pow_iff_log_lt`, add implications with weaker assumptions:
  - `nat.le_log_of_pow_le`,
  - `nat.log_lt_of_lt_pow`,
  - `nat.lt_pow_of_log_lt`,
  - `nat.pow_le_of_le_log`.
* Add `nat.log_eq_iff` and `nat.log_eq_of_pow_le_of_lt_pow`.
* Assume `n ≠ 0` instead of `0 &lt; n` in `nat.log_mul_base`, use implicit arguments.
* Add `nat.log_eq_iff` and `nat.log_eq_of_pow_le_of_lt_pow`.
* Add `nat.log_eq_one_iff'`, a version of `log_eq_one_iff` with seemingly weaker RHS.
* Drop assumption `1 &lt; b` in `nat.pow_log_le_self`.
diff --git a/src/data/int/log.lean b/src/data/int/log.lean
@@ -92,13 +92,10 @@ lemma zpow_log_le_self {b : ℕ} {r : R} (hb : 1 < b) (hr : 0 < r) :
 begin
   cases le_total 1 r with hr1 hr1,
   { rw log_of_one_le_right _ hr1,
-    refine le_trans _ (nat.floor_le hr.le),
-    rw [zpow_coe_nat, ←nat.cast_pow, nat.cast_le],
-    exact nat.pow_log_le_self hb (nat.floor_pos.mpr hr1) },
+    rw [zpow_coe_nat, ← nat.cast_pow, ← nat.le_floor_iff hr.le],
+    exact nat.pow_log_le_self b (nat.floor_pos.mpr hr1).ne' },
   { rw [log_of_right_le_one _ hr1, zpow_neg, zpow_coe_nat, ← nat.cast_pow],
-    apply inv_le_of_inv_le hr,
-    refine (nat.le_ceil _).trans (nat.cast_le.2 _),
-    exact nat.le_pow_clog hb _ },
+    exact inv_le_of_inv_le hr (nat.ceil_le.1 $ nat.le_pow_clog hb _) },
 end
 
 lemma lt_zpow_succ_log_self {b : ℕ} (hb : 1 < b) (r : R) :
diff --git a/src/data/nat/choose/factorization.lean b/src/data/nat/choose/factorization.lean
@@ -49,22 +49,16 @@ end
 A `pow` form of `nat.factorization_choose_le`
 -/
 lemma pow_factorization_choose_le (hn : 0 < n) : p ^ (choose n k).factorization p ≤ n :=
-begin
-  cases le_or_lt p 1,
-  { exact (pow_le_pow_of_le_left' h _).trans ((le_of_eq (one_pow _)).trans hn) },
-  { exact (pow_le_iff_le_log h hn).mpr factorization_choose_le_log },
-end
+pow_le_of_le_log hn.ne' factorization_choose_le_log
 
 /--
 Primes greater than about `sqrt n` appear only to multiplicity 0 or 1 in the binomial coefficient.
 -/
 lemma factorization_choose_le_one (p_large : n < p ^ 2) : (choose n k).factorization p ≤ 1 :=
 begin
   apply factorization_choose_le_log.trans,
-  rcases n.eq_zero_or_pos with rfl | hn0, { simp },
-  refine lt_succ_iff.1 ((lt_pow_iff_log_lt _ hn0).1 p_large),
-  contrapose! hn0,
-  exact lt_succ_iff.1 (lt_of_lt_of_le p_large (pow_le_one' hn0 2)),
+  rcases eq_or_ne n 0 with rfl | hn0, { simp },
+  exact lt_succ_iff.1 (log_lt_of_lt_pow hn0 p_large),
 end
 
 lemma factorization_choose_of_lt_three_mul
diff --git a/src/data/nat/log.lean b/src/data/nat/log.lean
@@ -31,170 +31,157 @@ such that `b^k ≤ n`, so if `b^k = n`, it returns exactly `k`. -/
     log (n / b) + 1
   else 0
 
-private lemma log_eq_zero_aux {b n : ℕ} (hnb : n < b ∨ b ≤ 1) : log b n = 0 :=
+@[simp] lemma log_eq_zero_iff {b n : ℕ} : log b n = 0 ↔ n < b ∨ b ≤ 1 :=
 begin
-  rw [or_iff_not_and_not, not_lt, not_le] at hnb,
-  rw [log, ←ite_not, if_pos hnb]
+  rw [log, ite_eq_right_iff],
+  simp only [nat.succ_ne_zero, imp_false, decidable.not_and_distrib, not_le, not_lt]
 end
 
 lemma log_of_lt {b n : ℕ} (hb : n < b) : log b n = 0 :=
-log_eq_zero_aux (or.inl hb)
+log_eq_zero_iff.2 (or.inl hb)
 
 lemma log_of_left_le_one {b : ℕ} (hb : b ≤ 1) (n) : log b n = 0 :=
-log_eq_zero_aux (or.inr hb)
+log_eq_zero_iff.2 (or.inr hb)
 
-lemma log_of_one_lt_of_le {b n : ℕ} (h : 1 < b) (hn : b ≤ n) : log b n = log b (n / b) + 1 :=
-by { rw log, exact if_pos ⟨hn, h⟩ }
-
-lemma log_eq_zero_iff {b n : ℕ} : log b n = 0 ↔ n < b ∨ b ≤ 1 :=
-⟨λ h_log, begin
-  by_contra' h,
-  have := log_of_one_lt_of_le h.2 h.1,
-  rw h_log at this,
-  exact succ_ne_zero _ this.symm
-end, log_eq_zero_aux⟩
+@[simp] lemma log_pos_iff {b n : ℕ} : 0 < log b n ↔ b ≤ n ∧ 1 < b :=
+by rw [pos_iff_ne_zero, ne.def, log_eq_zero_iff, not_or_distrib, not_lt, not_le]
 
-lemma log_eq_one_iff {b n : ℕ} : log b n = 1 ↔ n < b * b ∧ 1 < b ∧ b ≤ n :=
--- This is best possible: if b = 2, n = 5, then 1 < b and b ≤ n but n > b * b.
-begin
-  refine ⟨λ h_log, _, _⟩,
-  { have bound : 1 < b ∧ b ≤ n,
-    { contrapose h_log,
-      rw [not_and_distrib, not_lt, not_le, or_comm, ←log_eq_zero_iff] at h_log,
-      rw h_log,
-      exact nat.zero_ne_one, },
-    cases bound with one_lt_b b_le_n,
-    refine ⟨_, one_lt_b, b_le_n⟩,
-    rw [log_of_one_lt_of_le one_lt_b b_le_n, succ_inj',
-        log_eq_zero_iff, nat.div_lt_iff_lt_mul (lt_trans zero_lt_one one_lt_b)] at h_log,
-    exact h_log.resolve_right (λ b_small, lt_irrefl _ (lt_of_lt_of_le one_lt_b b_small)), },
-  { rintros ⟨h, one_lt_b, b_le_n⟩,
-    rw [log_of_one_lt_of_le one_lt_b b_le_n, succ_inj',
-        log_eq_zero_iff, nat.div_lt_iff_lt_mul (lt_trans zero_lt_one one_lt_b)],
-    exact or.inl h, },
-end
+lemma log_pos {b n : ℕ} (hb : 1 < b) (hbn : b ≤ n) : 0 < log b n := log_pos_iff.2 ⟨hbn, hb⟩
 
-@[simp] lemma log_zero_left : ∀ n, log 0 n = 0 :=
-log_of_left_le_one zero_le_one
-
-@[simp] lemma log_zero_right (b : ℕ) : log b 0 = 0 :=
-by { rw log, cases b; refl }
-
-@[simp] lemma log_one_left : ∀ n, log 1 n = 0 :=
-log_of_left_le_one le_rfl
+lemma log_of_one_lt_of_le {b n : ℕ} (h : 1 < b) (hn : b ≤ n) : log b n = log b (n / b) + 1 :=
+by { rw log, exact if_pos ⟨hn, h⟩ }
 
-@[simp] lemma log_one_right (b : ℕ) : log b 1 = 0 :=
-if h : b ≤ 1 then
-  log_of_left_le_one h 1
-else
-  log_of_lt (not_le.mp h)
+@[simp] lemma log_zero_left : ∀ n, log 0 n = 0 := log_of_left_le_one zero_le_one
+@[simp] lemma log_zero_right (b : ℕ) : log b 0 = 0 := log_eq_zero_iff.2 (le_total 1 b)
+@[simp] lemma log_one_left : ∀ n, log 1 n = 0 := log_of_left_le_one le_rfl
+@[simp] lemma log_one_right (b : ℕ) : log b 1 = 0 := log_eq_zero_iff.2 (lt_or_le _ _)
 
-/-- `pow b` and `log b` (almost) form a Galois connection. -/
-lemma pow_le_iff_le_log {b : ℕ} (hb : 1 < b) {x y : ℕ} (hy : 0 < y) : b ^ x ≤ y ↔ x ≤ 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. -/
+lemma pow_le_iff_le_log {b : ℕ} (hb : 1 < b) {x y : ℕ} (hy : y ≠ 0) : b ^ x ≤ y ↔ x ≤ log b y :=
 begin
   induction y using nat.strong_induction_on with y ih generalizing x,
   cases x,
-  { exact iff_of_true hy (zero_le _) },
+  { exact iff_of_true hy.bot_lt (zero_le _) },
   rw log, split_ifs,
   { have b_pos : 0 < b := zero_le_one.trans_lt hb,
-    rw [succ_eq_add_one, add_le_add_iff_right, ←ih (y / b) (div_lt_self hy hb)
-      (nat.div_pos h.1 b_pos), le_div_iff_mul_le b_pos, pow_succ'] },
-  { refine iff_of_false (λ hby, h ⟨le_trans _ hby, hb⟩) (not_succ_le_zero _),
-    convert pow_mono hb.le (zero_lt_succ x),
-    exact (pow_one b).symm }
+    rw [succ_eq_add_one, add_le_add_iff_right, ←ih (y / b) (div_lt_self hy.bot_lt hb)
+      (nat.div_pos h.1 b_pos).ne', le_div_iff_mul_le b_pos, pow_succ'] },
+  { exact iff_of_false (λ hby, h ⟨(le_self_pow hb.le x.succ_ne_zero).trans hby, hb⟩)
+      (not_succ_le_zero _) }
 end
 
-lemma lt_pow_iff_log_lt {b : ℕ} (hb : 1 < b) {x y : ℕ} (hy : 0 < y) : y < b ^ x ↔ log b y < x :=
+lemma lt_pow_iff_log_lt {b : ℕ} (hb : 1 < b) {x y : ℕ} (hy : y ≠ 0) : y < b ^ x ↔ log b y < x :=
 lt_iff_lt_of_le_iff_le (pow_le_iff_le_log hb hy)
 
-lemma log_pow {b : ℕ} (hb : 1 < b) (x : ℕ) : log b (b ^ x) = x :=
-eq_of_forall_le_iff $ λ z,
-by { rw ←pow_le_iff_le_log hb (pow_pos (zero_lt_one.trans hb) _),
-    exact (pow_right_strict_mono hb).le_iff_le }
-
-lemma log_pos {b n : ℕ} (hb : 1 < b) (hn : b ≤ n) : 0 < log b n :=
-by { rwa [←succ_le_iff, ←pow_le_iff_le_log hb (hb.le.trans hn), pow_one] }
+lemma pow_le_of_le_log {b x y : ℕ} (hy : y ≠ 0) (h : x ≤ log b y) : b ^ x ≤ y :=
+begin
+  refine (le_or_lt b 1).elim (λ hb, _) (λ hb, (pow_le_iff_le_log hb hy).2 h),
+  rw [log_of_left_le_one hb, nonpos_iff_eq_zero] at h,
+  rwa [h, pow_zero, one_le_iff_ne_zero]
+end
 
-lemma log_mul_base (b n : ℕ) (hb : 1 < b) (hn : 0 < n) : log b (n * b) = log b n + 1 :=
-eq_of_forall_le_iff $ λ z,
+lemma le_log_of_pow_le {b x y : ℕ} (hb : 1 < b) (h : b ^ x ≤ y) : x ≤ log b y :=
 begin
-  cases z,
-  { simp },
-  have : 0 < b := zero_lt_one.trans hb,
-  rw [←pow_le_iff_le_log hb, pow_succ', (strict_mono_mul_right_of_pos this).le_iff_le,
-      pow_le_iff_le_log hb hn, nat.succ_le_succ_iff],
-  simp [hn, this]
+  rcases ne_or_eq y 0 with hy | rfl,
+  exacts [(pow_le_iff_le_log hb hy).1 h, (h.not_lt (pow_pos (zero_lt_one.trans hb) _)).elim]
 end
 
+lemma pow_log_le_self (b : ℕ) {x : ℕ} (hx : x ≠ 0) : b ^ log b x ≤ x :=
+pow_le_of_le_log hx le_rfl
+
+lemma log_lt_of_lt_pow {b x y : ℕ} (hy : y ≠ 0) : y < b ^ x → log b y < x :=
+lt_imp_lt_of_le_imp_le (pow_le_of_le_log hy)
+
+lemma 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 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 _)
+
+lemma log_eq_iff {b m n : ℕ} (h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0) :
+  log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1) :=
 begin
-  cases x.eq_zero_or_pos with hx hx,
-  { simp only [hx, log_zero_right, pow_one],
-    exact pos_of_gt hb },
-  rw [←not_le, pow_le_iff_le_log hb hx, not_le],
-  exact lt_succ_self _,
+  rcases em (1 < b ∧ n ≠ 0) with ⟨hb, hn⟩|hbn,
+  { rw [le_antisymm_iff, ← lt_succ_iff, ← pow_le_iff_le_log, ← lt_pow_iff_log_lt, and.comm];
+      assumption },
+  { have hm : m ≠ 0, from h.resolve_right hbn,
+    rw [not_and_distrib, not_lt, ne.def, not_not] at hbn,
+    rcases hbn with hb|rfl,
+    { simpa only [log_of_left_le_one hb, hm.symm, false_iff, not_and, not_lt]
+        using le_trans (pow_le_pow_of_le_one' hb m.le_succ) },
+    { simpa only [log_zero_right, hm.symm, false_iff, not_and, not_lt, le_zero_iff, pow_succ]
+        using mul_eq_zero_of_right _ } }
 end
 
-lemma pow_log_le_self {b : ℕ} (hb : 1 < b) {x : ℕ} (hx : 0 < x) : b ^ log b x ≤ x :=
-(pow_le_iff_le_log hb hx).2 le_rfl
+lemma log_eq_of_pow_le_of_lt_pow {b m n : ℕ} (h₁ : b ^ m ≤ n) (h₂ : n < b ^ (m + 1)) :
+  log b n = m :=
+begin
+  rcases eq_or_ne m 0 with rfl | hm,
+  { rw [pow_one] at h₂, exact log_of_lt h₂ },
+  { exact (log_eq_iff (or.inl hm)).2 ⟨h₁, h₂⟩ }
+end
 
-@[mono] lemma log_mono_right {b n m : ℕ} (h : n ≤ m) : log b n ≤ log b m :=
+lemma log_pow {b : ℕ} (hb : 1 < b) (x : ℕ) : log b (b ^ x) = x :=
+log_eq_of_pow_le_of_lt_pow le_rfl (pow_lt_pow hb x.lt_succ_self)
+
+lemma log_eq_one_iff' {b n : ℕ} : log b n = 1 ↔ b ≤ n ∧ n < b * b:=
+by rw [log_eq_iff (or.inl one_ne_zero), pow_add, pow_one]
+
+lemma log_eq_one_iff {b n : ℕ} : log b n = 1 ↔ n < b * b ∧ 1 < b ∧ b ≤ n :=
+log_eq_one_iff'.trans ⟨λ h, ⟨h.2, lt_mul_self_iff.1 (h.1.trans_lt h.2), h.1⟩, λ h, ⟨h.2.2, h.1⟩⟩
+
+lemma log_mul_base {b n : ℕ} (hb : 1 < b) (hn : n ≠ 0) : log b (n * b) = log b n + 1 :=
 begin
+  apply log_eq_of_pow_le_of_lt_pow; rw [pow_succ'],
+  exacts [mul_le_mul_right' (pow_log_le_self _ hn) _,
+    (mul_lt_mul_right (zero_lt_one.trans hb)).2 (lt_pow_succ_log_self hb _)]
+end
+
+lemma pow_log_le_add_one (b : ℕ) : ∀ x, b ^ log b x ≤ x + 1
+| 0 := by rw [log_zero_right, pow_zero]
+| (x + 1) := (pow_log_le_self b x.succ_ne_zero).trans (x + 1).le_succ
+
+lemma log_monotone {b : ℕ} : monotone (log b) :=
+begin
+  refine monotone_nat_of_le_succ (λ n, _),
   cases le_or_lt b 1 with hb hb,
   { rw log_of_left_le_one hb, exact zero_le _ },
-  { cases nat.eq_zero_or_pos n with hn hn,
-    { rw [hn, log_zero_right], exact zero_le _ },
-    { rw ←pow_le_iff_le_log hb (hn.trans_le h),
-      exact (pow_log_le_self hb hn).trans h } }
+  { exact le_log_of_pow_le hb (pow_log_le_add_one _ _) }
 end
 
+@[mono] lemma log_mono_right {b n m : ℕ} (h : n ≤ m) : log b n ≤ log b m :=
+log_monotone h
+
 @[mono] lemma log_anti_left {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : log b n ≤ log c n :=
 begin
-  cases n, { rw [log_zero_right, log_zero_right] },
-  rw ←pow_le_iff_le_log hc (zero_lt_succ n),
-  calc c ^ log b n.succ ≤ b ^ log b n.succ : pow_le_pow_of_le_left
-                                              (zero_lt_one.trans hc).le hb _
-                    ... ≤ n.succ           : pow_log_le_self (hc.trans_le hb)
-                                              (zero_lt_succ n)
+  rcases eq_or_ne n 0 with rfl | hn, { rw [log_zero_right, log_zero_right] },
+  apply le_log_of_pow_le hc,
+  calc c ^ log b n ≤ b ^ log b n : pow_le_pow_of_le_left' hb _
+               ... ≤ n           : pow_log_le_self _ hn
 end
 
-lemma log_monotone {b : ℕ} : monotone (log b) :=
-λ x y, log_mono_right
-
 lemma log_antitone_left {n : ℕ} : antitone_on (λ b, log b n) (set.Ioi 1) :=
 λ _ hc _ _ hb, log_anti_left (set.mem_Iio.1 hc) hb
 
-@[simp] lemma log_div_mul_self (b n : ℕ) : log b (n / b * b) = log b n :=
-eq_of_forall_le_iff (λ z, ⟨λ h, h.trans (log_monotone (div_mul_le_self _ _)), λ h, begin
-  rcases b with _|_|b,
-  { rwa log_zero_left at * },
-  { rwa log_one_left at * },
-  rcases n.zero_le.eq_or_lt with rfl|hn,
-  { rwa [nat.zero_div, zero_mul] },
-  cases le_or_lt b.succ.succ n with hb hb,
-  { cases z,
-    { apply zero_le },
-    rw [←pow_le_iff_le_log, pow_succ'] at h ⊢,
-    { rwa [(strict_mono_mul_right_of_pos nat.succ_pos').le_iff_le,
-            nat.le_div_iff_mul_le nat.succ_pos'] },
-    all_goals { simp [hn, nat.div_pos hb nat.succ_pos'] } },
-  { simpa [div_eq_of_lt, hb, log_of_lt] using h }
-end⟩)
-
 @[simp] lemma log_div_base (b n : ℕ) : log b (n / b) = log b n - 1 :=
 begin
+  cases le_or_lt b 1 with hb hb,
+  { rw [log_of_left_le_one hb, log_of_left_le_one hb, nat.zero_sub] },
   cases lt_or_le n b with h h,
   { rw [div_eq_of_lt h, log_of_lt h, log_zero_right] },
-  rcases n.zero_le.eq_or_lt with rfl|hn,
-  { rw [nat.zero_div, log_zero_right] },
-  rcases b with _|_|b,
-  { rw [log_zero_left, log_zero_left] },
-  { rw [log_one_left, log_one_left] },
-  rw [←succ_inj', ←succ_inj'],
-  simp_rw succ_eq_add_one,
-  rw [nat.sub_add_cancel, ←log_mul_base];
-  { simp [succ_le_iff, log_pos, h, nat.div_pos] },
+  rw [log_of_one_lt_of_le hb h, add_tsub_cancel_right]
+end
+
+@[simp] lemma log_div_mul_self (b n : ℕ) : log b (n / b * b) = log b n :=
+begin
+  cases le_or_lt b 1 with hb hb,
+  { rw [log_of_left_le_one hb, log_of_left_le_one hb] },
+  cases lt_or_le n b with h h,
+  { rw [div_eq_of_lt h, zero_mul, log_zero_right, log_of_lt h] },
+  rw [log_mul_base hb (nat.div_pos h (zero_le_one.trans_lt hb)).ne', log_div_base,
+    tsub_add_cancel_of_le (succ_le_iff.2 $ log_pos hb h)]
 end
 
 private lemma add_pred_div_lt {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : (n + b - 1) / b < n :=
@@ -315,7 +302,7 @@ begin
   cases n,
   { rw log_zero_right,
     exact zero_le _},
-  exact (pow_right_strict_mono hb).le_iff_le.1 ((pow_log_le_self hb $ succ_pos _).trans $
+  exact (pow_right_strict_mono hb).le_iff_le.1 ((pow_log_le_self b n.succ_ne_zero).trans $
     le_pow_clog hb _),
 end
 
diff --git a/src/data/nat/multiplicity.lean b/src/data/nat/multiplicity.lean
@@ -58,13 +58,12 @@ calc
       begin
         rw [mem_filter, mem_Ico, mem_Ico, lt_succ_iff, ←@part_enat.coe_le_coe i, part_enat.coe_get,
           ←pow_dvd_iff_le_multiplicity, and.right_comm],
-        refine (and_iff_left_of_imp (λ h, _)).symm,
+        refine (and_iff_left_of_imp (λ h, lt_of_le_of_lt _ hb)).symm,
         cases m,
         { rw [zero_pow, zero_dvd_iff] at h,
-          exact (hn.ne' h.2).elim,
-          { exact h.1 } },
-        exact ((pow_le_iff_le_log (succ_lt_succ $ nat.pos_of_ne_zero $ succ_ne_succ.1 hm) hn).1 $
-          le_of_dvd hn h.2).trans_lt hb,
+          exacts [(hn.ne' h.2).elim, h.1] },
+        exact le_log_of_pow_le (one_lt_iff_ne_zero_and_ne_one.2 ⟨m.succ_ne_zero, hm⟩)
+          (le_of_dvd hn h.2)
       end
 
 namespace prime
diff --git a/src/data/nat/order/basic.lean b/src/data/nat/order/basic.lean
@@ -291,6 +291,10 @@ begin
   simp [add_comm, nat.add_sub_assoc, one_le_iff_ne_zero.2 hi]
 end
 
+@[simp] theorem lt_mul_self_iff : ∀ {n : ℕ}, n < n * n ↔ 1 < n
+| 0 := iff_of_false (lt_irrefl _) zero_le_one.not_lt
+| (n + 1) := lt_mul_iff_one_lt_left n.succ_pos
+
 /-!
 ### Recursion and induction principles
 
