feat(data/nat/multiplicity): weaken hypothesis on set bounds (#6903)

src/data/nat/multiplicity.lean

@@ -5,6 +5,7 @@ Authors: Chris Hughes
 -/
 import data.nat.bitwise
 import data.nat.parity
+import data.nat.log
 import ring_theory.int.basic
 import algebra.big_operators.intervals
 
@@ -29,18 +30,18 @@ namespace nat
 
 /-- The multiplicity of a divisor `m` of `n`, is the cardinality of the set of
   positive natural numbers `i` such that `p ^ i` divides `n`. The set is expressed
-  by filtering `Ico 1 b` where `b` is any bound at least `n` -/
-lemma multiplicity_eq_card_pow_dvd {m n b : ℕ} (hm1 : m ≠ 1) (hn0 : 0 < n) (hb : n ≤ b):
+  by filtering `Ico 1 b` where `b` is any bound greater than `log m n` -/
+lemma multiplicity_eq_card_pow_dvd {m n b : ℕ} (hm1 : m ≠ 1) (hn0 : 0 < n) (hb : log m n < b):
   multiplicity m n = ↑((finset.Ico 1 b).filter (λ i, m ^ i ∣ n)).card :=
 calc multiplicity m n = ↑(Ico 1 $ ((multiplicity m n).get (finite_nat_iff.2 ⟨hm1, hn0⟩) + 1)).card :
   by simp
 ... = ↑((finset.Ico 1 b).filter (λ i, m ^ i ∣ n)).card : congr_arg coe $ congr_arg card $
   finset.ext $ λ i,
-  have hmn : ¬ m ^ n ∣ n,
+  have hmn : ¬ m ^ (log m n).succ ∣ n,
     from if hm0 : m = 0
     then λ _, by cases n; simp [*, lt_irrefl, pow_succ'] at *
-    else mt (le_of_dvd hn0) (not_le_of_gt $ lt_pow_self
-      (lt_of_le_of_ne (nat.pos_of_ne_zero hm0) hm1.symm) _),
+    else mt (le_of_dvd hn0) (not_le_of_lt $ pow_succ_log_gt_self m n
+        (hm1.symm.le_iff_lt.mp (zero_lt_iff.mpr hm0.intro)) hn0),
   ⟨λ hi, begin
       simp only [Ico.mem, mem_filter, lt_succ_iff] at *,
       exact ⟨⟨hi.1, lt_of_le_of_lt hi.2 $
@@ -76,15 +77,15 @@ lemma multiplicity_pow_self {p n : ℕ} (hp : p.prime) : multiplicity p (p ^ n)
 multiplicity_pow_self hp.ne_zero (prime_iff_prime.mp hp).not_unit n
 
 /-- The multiplicity of a prime in `n!` is the sum of the quotients `n / p ^ i`.
-  This sum is expressed over the set `Ico 1 b` where `b` is any bound at least `n` -/
+  This sum is expressed over the set `Ico 1 b` where `b` is any bound greater than `log p n` -/
 lemma multiplicity_factorial {p : ℕ} (hp : p.prime) :
-  ∀ {n b : ℕ}, n ≤ b → multiplicity p n! = (∑ i in Ico 1 b, n / p ^ i : ℕ)
+  ∀ {n b : ℕ}, log p n < b → multiplicity p n! = (∑ i in Ico 1 b, n / p ^ i : ℕ)
 | 0     b hb := by simp [Ico, hp.multiplicity_one]
 | (n+1) b hb :=
   calc multiplicity p (n+1)! = multiplicity p n! + multiplicity p (n+1) :
     by rw [factorial_succ, hp.multiplicity_mul, add_comm]
   ... = (∑ i in Ico 1 b, n / p ^ i : ℕ) + ((finset.Ico 1 b).filter (λ i, p ^ i ∣ n+1)).card :
-    by rw [multiplicity_factorial (le_of_succ_le hb),
+    by rw [multiplicity_factorial (lt_of_le_of_lt log_le_log_succ hb),
       ← multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) (succ_pos _) hb]
   ... = (∑ i in Ico 1 b, (n / p ^ i + if p^i ∣ n+1 then 1 else 0) : ℕ) :
     by rw [sum_add_distrib, sum_boole]; simp
@@ -127,8 +128,8 @@ begin
 end
 
 /-- A prime power divides `n!` iff it is at most the sum of the quotients `n / p ^ i`.
-  This sum is expressed over the set `Ico 1 b` where `b` is any bound at least `n` -/
-lemma pow_dvd_factorial_iff {p : ℕ} {n r b : ℕ} (hp : p.prime) (hbn : n ≤ b) :
+  This sum is expressed over the set `Ico 1 b` where `b` is any bound greater than `log p n` -/
+lemma pow_dvd_factorial_iff {p : ℕ} {n r b : ℕ} (hp : p.prime) (hbn : log p n < b) :
    p ^ r ∣ n! ↔ r ≤ ∑ i in Ico 1 b, n / p ^ i :=
 by rw [← enat.coe_le_coe, ← hp.multiplicity_factorial hbn, ← pow_dvd_iff_le_multiplicity]
 
@@ -146,8 +147,8 @@ calc ∑ i in finset.Ico 1 b, n / p ^ i
 
 /-- The multiplity of `p` in `choose n k` is the number of carries when `k` and `n - k`
   are added in base `p`. The set is expressed by filtering `Ico 1 b` where `b`
-  is any bound at least `n`. -/
-lemma multiplicity_choose {p n k b : ℕ} (hp : p.prime) (hkn : k ≤ n) (hnb : n ≤ b) :
+  is any bound greater than `log p n`. -/
+lemma multiplicity_choose {p n k b : ℕ} (hp : p.prime) (hkn : k ≤ n) (hnb : log p n < b) :
   multiplicity p (choose n k) =
   ((Ico 1 b).filter (λ i, p ^ i ≤ k % p ^ i + (n - k) % p ^ i)).card :=
 have h₁ : multiplicity p (choose n k) + multiplicity p (k! * (n - k)!) =
@@ -156,8 +157,8 @@ have h₁ : multiplicity p (choose n k) + multiplicity p (k! * (n - k)!) =
   begin
     rw [← hp.multiplicity_mul, ← mul_assoc, choose_mul_factorial_mul_factorial hkn,
         hp.multiplicity_factorial hnb, hp.multiplicity_mul,
-        hp.multiplicity_factorial (le_trans hkn hnb),
-        hp.multiplicity_factorial (le_trans (nat.sub_le_self _ _) hnb),
+        hp.multiplicity_factorial ((log_le_log_of_le hkn).trans_lt hnb),
+        hp.multiplicity_factorial (lt_of_le_of_lt (log_le_log_of_le (nat.sub_le_self _ _)) hnb),
         multiplicity_choose_aux hp hkn],
     simp [add_comm],
   end,
@@ -174,20 +175,21 @@ if hkn : n < k then by simp [choose_eq_zero_of_lt hkn]
 else if hk0 : k = 0 then by simp [hk0]
 else if hn0 : n = 0 then by cases k; simp [hn0, *] at *
 else begin
-  rw [multiplicity_choose hp (le_of_not_gt hkn) (le_refl _),
-    multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) (nat.pos_of_ne_zero hk0) (le_of_not_gt hkn),
-    multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) (nat.pos_of_ne_zero hn0) (le_refl _),
+  rw [multiplicity_choose hp (le_of_not_gt hkn) (lt_succ_self _),
+    multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) (nat.pos_of_ne_zero hk0)
+      (lt_succ_of_le (log_le_log_of_le (le_of_not_gt hkn))),
+    multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) (nat.pos_of_ne_zero hn0) (lt_succ_self _),
     ← enat.coe_add, enat.coe_le_coe],
-  calc ((Ico 1 n).filter (λ i, p ^ i ∣ n)).card
-      ≤ ((Ico 1 n).filter (λ i, p ^ i ≤ k % p ^ i + (n - k) % p ^ i) ∪
-        (Ico 1 n).filter (λ i, p ^ i ∣ k) ).card :
+  calc ((Ico 1 (log p n).succ).filter (λ i, p ^ i ∣ n)).card
+      ≤ ((Ico 1 (log p n).succ).filter (λ i, p ^ i ≤ k % p ^ i + (n - k) % p ^ i) ∪
+        (Ico 1 (log p n).succ).filter (λ i, p ^ i ∣ k) ).card :
     card_le_of_subset $ λ i, begin
       have := @le_mod_add_mod_of_dvd_add_of_not_dvd k (n - k) (p ^ i),
       simp [nat.add_sub_cancel' (le_of_not_gt hkn)] at * {contextual := tt},
       tauto
     end
-  ... ≤ ((Ico 1 n).filter (λ i, p ^ i ≤ k % p ^ i + (n - k) % p ^ i)).card +
-        ((Ico 1 n).filter (λ i, p ^ i ∣ k)).card :
+  ... ≤ ((Ico 1 (log p n).succ).filter (λ i, p ^ i ≤ k % p ^ i + (n - k) % p ^ i)).card +
+        ((Ico 1 (log p n).succ).filter (λ i, p ^ i ∣ k)).card :
     card_union_le _ _
 end
 
@@ -196,30 +198,18 @@ lemma multiplicity_choose_prime_pow {p n k : ℕ} (hp : p.prime)
   multiplicity p (choose (p ^ n) k) + multiplicity p k = n :=
 le_antisymm
   (have hdisj : disjoint
-      ((Ico 1 (p ^ n)).filter (λ i, p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i))
-      ((Ico 1 (p ^ n)).filter (λ i, p ^ i ∣ k)),
+      ((Ico 1 n.succ).filter (λ i, p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i))
+      ((Ico 1 n.succ).filter (λ i, p ^ i ∣ k)),
     by simp [disjoint_right, *, dvd_iff_mod_eq_zero, nat.mod_lt _ (pow_pos hp.pos _)]
         {contextual := tt},
-  have filter_subset_Ico : filter (λ i, p ^ i ≤ k % p ^ i +
-      (p ^ n - k) % p ^ i ∨ p ^ i ∣ k) (Ico 1 (p ^ n)) ⊆ Ico 1 n.succ,
-    from begin
-      simp only [finset.subset_iff, Ico.mem, mem_filter, and_imp, true_and] {contextual := tt},
-      assume i h1i hip h,
-      refine lt_succ_of_le (le_of_not_gt (λ hin, _)),
-      have hpik : ¬ p ^ i ∣ k, from mt (le_of_dvd hk0)
-        (not_le_of_gt (lt_of_le_of_lt hkn (pow_right_strict_mono hp.two_le hin))),
-      have hpn : k % p ^ i + (p ^ n - k) % p ^ i < p ^ i,
-        from calc k % p ^ i + (p ^ n - k) % p ^ i
-              ≤ k + (p ^ n - k) : add_le_add (mod_le _ _) (mod_le _ _)
-          ... = p ^ n : nat.add_sub_cancel' hkn
-          ... < p ^ i : pow_right_strict_mono hp.two_le hin,
-      simpa [hpik, not_le_of_gt hpn] using h
-    end,
   begin
-    rw [multiplicity_choose hp hkn (le_refl _),
-      multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) hk0 hkn, ← enat.coe_add,
-      enat.coe_le_coe, ← card_disjoint_union hdisj, filter_union_right],
-    exact le_trans (card_le_of_subset filter_subset_Ico) (by simp)
+    rw [multiplicity_choose hp hkn (lt_succ_self _),
+      multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) hk0
+        (lt_succ_of_le (log_le_log_of_le hkn)),
+      ← enat.coe_add, enat.coe_le_coe, log_pow _ _ hp.one_lt,
+      ← card_disjoint_union hdisj, filter_union_right],
+    have filter_le_Ico := (Ico 1 n.succ).card_filter_le _,
+    rwa Ico.card 1 n.succ at filter_le_Ico,
   end)
   (by rw [← hp.multiplicity_pow_self];
     exact multiplicity_le_multiplicity_choose_add hp _ _)