feat(data/nat/factorization/basic): add lemma `factorization_eq_card_…

…pow_dvd` (#15014)

Adds lemma 
`factorization_eq_card_pow_dvd (pp : p.prime) : n.factorization p = ((Ico 1 n).filter (λ i, p ^ i ∣ n)).card`
This is a counterpart to `multiplicity_eq_card_pow_dvd` defined and proved in terms of `factorization`.

Also proves some upper bounds on `n.factorization p`:
`factorization_lt (hn : n ≠ 0) : n.factorization p < n`
`factorization_le_of_le_pow (hb : n ≤ p ^ b) : n.factorization p ≤ b`

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

src/data/nat/factorization/basic.lean

@@ -6,6 +6,7 @@ Authors: Stuart Presnell
 import data.nat.prime
 import data.finsupp.multiset
 import algebra.big_operators.finsupp
+import data.nat.interval
 
 /-!
 # Prime factorizations
@@ -237,6 +238,24 @@ end
 lemma pow_factorization_le {n : ℕ} (p : ℕ) (hn : n ≠ 0) : p ^ n.factorization p ≤ n :=
 le_of_dvd hn.bot_lt (nat.pow_factorization_dvd n p)
 
+/-- A crude upper bound on `n.factorization p` -/
+lemma factorization_lt {n : ℕ} (p : ℕ) (hn : n ≠ 0) : n.factorization p < n :=
+begin
+  by_cases pp : p.prime, swap, { simp [factorization_eq_zero_of_non_prime n pp], exact hn.bot_lt },
+  rw ←pow_lt_iff_lt_right pp.two_le,
+  apply lt_of_le_of_lt (pow_factorization_le p hn),
+  exact lt_of_lt_of_le (lt_two_pow n) (pow_le_pow_of_le_left (by linarith) pp.two_le n),
+end
+
+/-- An upper bound on `n.factorization p` -/
+lemma factorization_le_of_le_pow {n p b : ℕ} (hb : n ≤ p ^ b) : n.factorization p ≤ b :=
+begin
+  rcases eq_or_ne n 0 with rfl | hn, { simp },
+  by_cases pp : p.prime, 
+  { exact (pow_le_iff_le_right pp.two_le).1 (le_trans (pow_factorization_le p hn) hb) },
+  { simp [factorization_eq_zero_of_non_prime n pp] }
+end
+
 lemma div_pow_factorization_ne_zero {n : ℕ} (p : ℕ) (hn : n ≠ 0) :
   n / p ^ n.factorization p ≠ 0 :=
 begin
@@ -382,6 +401,36 @@ begin
     simp [←factorization_le_iff_dvd he_pos hd_pos, h1, hea', heb'] },
 end
 
+lemma set_of_pow_dvd_eq_Icc_factorization {n p : ℕ} (pp : p.prime) (hn : n ≠ 0) :
+  {i : ℕ | i ≠ 0 ∧ p ^ i ∣ n} = set.Icc 1 (n.factorization p) :=
+by { ext, simp [lt_succ_iff, one_le_iff_ne_zero, pp.pow_dvd_iff_le_factorization hn] }
+
+/-- The set of positive powers of prime `p` that divide `n` is exactly the set of
+positive natural numbers up to `n.factorization p`. -/
+lemma Icc_factorization_eq_pow_dvd (n : ℕ) {p : ℕ} (pp : prime p) :
+  Icc 1 ((n.factorization) p) = (Ico 1 n).filter (λ (i : ℕ), p ^ i ∣ n) :=
+begin
+  rcases eq_or_ne n 0 with rfl | hn, { simp },
+  ext x,
+  simp only [mem_Icc, finset.mem_filter, mem_Ico, and_assoc, and.congr_right_iff,
+    pp.pow_dvd_iff_le_factorization hn, iff_and_self],
+  exact λ H1 H2, lt_of_le_of_lt H2 (factorization_lt p hn),
+end
+
+lemma factorization_eq_card_pow_dvd (n : ℕ) {p : ℕ} (pp : p.prime) :
+  n.factorization p = ((Ico 1 n).filter (λ i, p ^ i ∣ n)).card :=
+by simp [←Icc_factorization_eq_pow_dvd n pp]
+
+lemma Ico_filter_pow_dvd_eq {n p b : ℕ} (pp : p.prime) (hn : n ≠ 0) (hb : n ≤ p ^ b):
+  (Ico 1 n).filter (λ i, p ^ i ∣ n) = (Icc 1 b).filter (λ i, p ^ i ∣ n) :=
+begin
+  ext x,
+  simp only [finset.mem_filter, mem_Ico, mem_Icc, and.congr_left_iff, and.congr_right_iff],
+  rintro h1 -,
+  simp [lt_of_pow_dvd_right hn pp.two_le h1,
+    (pow_le_iff_le_right pp.two_le).1 ((le_of_dvd hn.bot_lt h1).trans hb)],
+end
+
 /-! ### Factorization and coprimes -/
 
 /-- For coprime `a` and `b`, the power of `p` in `a * b` is the sum of the powers in `a` and `b` -/

src/data/nat/pow.lean

@@ -194,6 +194,12 @@ by rw ←pow_one p; exact pow_dvd_of_le_of_pow_dvd hk hpk
 lemma pow_div {x m n : ℕ} (h : n ≤ m) (hx : 0 < x) : x ^ m / x ^ n = x ^ (m - n) :=
 by rw [nat.div_eq_iff_eq_mul_left (pow_pos hx n) (pow_dvd_pow _ h), pow_sub_mul_pow _ h]
 
+lemma lt_of_pow_dvd_right {p i n : ℕ} (hn : n ≠ 0) (hp : 2 ≤ p) (h : p ^ i ∣ n) : i < n :=
+begin
+  rw ←pow_lt_iff_lt_right hp,
+  exact lt_of_le_of_lt (le_of_dvd hn.bot_lt h) (lt_pow_self (succ_le_iff.mp hp) n),
+end
+
 /-! ### `shiftl` and `shiftr` -/
 
 lemma shiftl_eq_mul_pow (m) : ∀ n, shiftl m n = m * 2 ^ n