feat(data/padics/padic_norm): lemmas about padic_val_nat (#3230)

Collection of lemmas about `padic_val_nat`, culminating in `lemma prod_pow_prime_padic_val_nat : ∀ (n : nat) (s : n ≠ 0) (m : nat) (pr : n < m),  ∏ p in finset.filter nat.prime (finset.range m), pow p (padic_val_nat p n) = n`.



Co-authored-by: Johan Commelin <johan@commelin.net>

Author: Smaug123

src/algebra/big_operators.lean

@@ -654,6 +654,21 @@ lemma sum_range_one {δ : Type*} [add_comm_monoid δ] (f : ℕ → δ) :
 
 attribute [to_additive finset.sum_range_one] prod_range_one
 
+open multiset
+lemma prod_multiset_count [decidable_eq α] [comm_monoid α] (s : multiset α) :
+  s.prod = ∏ m in s.to_finset, m ^ (s.count m) :=
+begin
+  apply s.induction_on, { rw [prod_zero, to_finset_zero, finset.prod_empty] },
+  intros a s ih, by_cases has : a ∈ s.to_finset,
+  { rw [prod_cons, to_finset_cons, finset.insert_eq_of_mem has, ih,
+      ← finset.insert_erase has, finset.prod_insert (finset.not_mem_erase _ _),
+      finset.prod_insert (finset.not_mem_erase _ _), ← mul_assoc, count_cons_self, pow_succ],
+    congr' 1, refine finset.prod_congr rfl (λ x hx, _), rw [count_cons_of_ne (finset.ne_of_mem_erase hx)] },
+  rw [prod_cons, to_finset_cons, finset.prod_insert has, count_cons_self],
+  rw mem_to_finset at has, rw [count_eq_zero_of_not_mem has, pow_one], congr' 1,
+  rw ih, refine finset.prod_congr rfl (λ x hx, _), rw mem_to_finset at hx, rw count_cons_of_ne,
+  rintro rfl, exact has hx
+end
 
 /-- To prove a property of a product, it suffices to prove that the property is multiplicative and holds on factors.
 -/

src/algebra/char_zero.lean

@@ -63,6 +63,16 @@ not_congr cast_eq_zero
 lemma cast_add_one_ne_zero (n : ℕ) : (n + 1 : α) ≠ 0 :=
 by exact_mod_cast n.succ_ne_zero
 
+@[simp, norm_cast]
+theorem cast_dvd_char_zero {α : Type*} [field α] [char_zero α] {m n : ℕ}
+  (n_dvd : n ∣ m) : ((m / n : ℕ) : α) = m / n :=
+begin
+  by_cases hn : n = 0,
+  { subst hn,
+    simp },
+  { exact cast_dvd n_dvd (cast_ne_zero.mpr hn), },
+end
+
 end nat
 
 @[field_simps] lemma two_ne_zero' {α : Type*} [add_monoid α] [has_one α] [char_zero α] : (2:α) ≠ 0 :=

src/data/nat/basic.lean

@@ -1535,6 +1535,24 @@ begin
   cc
 end
 
+@[simp]
+lemma div_div_div_eq_div : ∀ {a b c : ℕ} (dvd : b ∣ a) (dvd2 : a ∣ c), (c / (a / b)) / b = c / a
+| 0 _ := by simp
+| (a + 1) 0 := λ _ dvd _, by simpa using dvd
+| (a + 1) (c + 1) :=
+have a_split : a + 1 ≠ 0 := succ_ne_zero a,
+have c_split : c + 1 ≠ 0 := succ_ne_zero c,
+λ b dvd dvd2,
+begin
+  rcases dvd2 with ⟨k, rfl⟩,
+  rcases dvd with ⟨k2, pr⟩,
+  have k2_nonzero : k2 ≠ 0 := λ k2_zero, by simpa [k2_zero] using pr,
+  rw [nat.mul_div_cancel_left k (nat.pos_of_ne_zero a_split), pr,
+    nat.mul_div_cancel_left k2 (nat.pos_of_ne_zero c_split), nat.mul_comm ((c + 1) * k2) k,
+    ←nat.mul_assoc k (c + 1) k2, nat.mul_div_cancel _ (nat.pos_of_ne_zero k2_nonzero),
+    nat.mul_div_cancel _ (nat.pos_of_ne_zero c_split)],
+end
+
 lemma pow_dvd_of_le_of_pow_dvd {p m n k : ℕ} (hmn : m ≤ n) (hdiv : p ^ n ∣ k) : p ^ m ∣ k :=
 have p ^ m ∣ p ^ n, from pow_dvd_pow _ hmn,
 dvd_trans this hdiv

src/data/nat/cast.lean

@@ -98,6 +98,14 @@ eq_sub_of_add_eq $ by rw [← cast_add, nat.sub_add_cancel h]
 | (n+1) := (cast_add _ _).trans $
 show ((m * n : ℕ) : α) + m = m * (n + 1), by rw [cast_mul n, left_distrib, mul_one]
 
+@[simp] theorem cast_dvd {α : Type*} [field α] {m n : ℕ} (n_dvd : n ∣ m) (n_nonzero : (n:α) ≠ 0) : ((m / n : ℕ) : α) = m / n :=
+begin
+  rcases n_dvd with ⟨k, rfl⟩,
+  have : n ≠ 0, {rintro rfl, simpa using n_nonzero},
+  rw nat.mul_div_cancel_left _ (nat.pos_iff_ne_zero.2 this),
+  rw [nat.cast_mul, mul_div_cancel_left _ n_nonzero],
+end
+
 /-- `coe : ℕ → α` as a `ring_hom` -/
 def cast_ring_hom (α : Type*) [semiring α] : ℕ →+* α :=
 { to_fun := coe,

src/data/nat/gcd.lean

@@ -266,6 +266,20 @@ H.coprime_dvd_right (dvd_mul_left _ _)
 theorem coprime.coprime_mul_right_right {k m n : ℕ} (H : coprime m (n * k)) : coprime m n :=
 H.coprime_dvd_right (dvd_mul_right _ _)
 
+theorem coprime.coprime_div_left {m n a : ℕ} (cmn : coprime m n) (dvd : a ∣ m) : coprime (m / a) n :=
+begin
+  by_cases a_split : (a = 0),
+  { subst a_split,
+    rw zero_dvd_iff at dvd,
+    simpa [dvd] using cmn, },
+  { rcases dvd with ⟨k, rfl⟩,
+    rw nat.mul_div_cancel_left _ (nat.pos_of_ne_zero a_split),
+    exact coprime.coprime_mul_left cmn, },
+end
+
+theorem coprime.coprime_div_right {m n a : ℕ} (cmn : coprime m n) (dvd : a ∣ n) : coprime m (n / a) :=
+(coprime.coprime_div_left cmn.symm dvd).symm
+
 lemma coprime_mul_iff_left {k m n : ℕ} : coprime (m * n) k ↔ coprime m k ∧ coprime n k :=
 ⟨λ h, ⟨coprime.coprime_mul_right h, coprime.coprime_mul_left h⟩,
   λ ⟨h, _⟩, by rwa [coprime, coprime.gcd_mul_left_cancel n h]⟩

src/data/nat/prime.lean

@@ -117,6 +117,9 @@ theorem dvd_prime {p m : ℕ} (pp : prime p) : m ∣ p ↔ m = 1 ∨ m = p :=
 theorem dvd_prime_two_le {p m : ℕ} (pp : prime p) (H : 2 ≤ m) : m ∣ p ↔ m = p :=
 (dvd_prime pp).trans $ or_iff_right_of_imp $ not.elim $ ne_of_gt H
 
+theorem prime_dvd_prime_iff_eq {p q : ℕ} (pp : p.prime) (qp : q.prime) : p ∣ q ↔ p = q :=
+dvd_prime_two_le qp (prime.two_le pp)
+
 theorem prime.not_dvd_one {p : ℕ} (pp : prime p) : ¬ p ∣ 1
 | d := (not_le_of_gt pp.one_lt) $ le_of_dvd dec_trivial d
 
@@ -375,6 +378,10 @@ begin
   { simp only [this, nat.factors, nat.div_self (nat.prime.pos hp)], },
 end
 
+/-- `factors` can be constructed inductively by extracting `min_fac`, for sufficiently large `n`. -/
+lemma factors_add_two (n : ℕ) :
+  factors (n+2) = (min_fac (n+2)) :: (factors ((n+2) / (min_fac (n+2)))) := rfl
+
 theorem prime.coprime_iff_not_dvd {p n : ℕ} (pp : prime p) : coprime p n ↔ ¬ p ∣ n :=
 ⟨λ co d, pp.not_dvd_one $ co.dvd_of_dvd_mul_left (by simp [d]),
  λ nd, coprime_of_dvd $ λ m m2 mp, ((dvd_prime_two_le pp m2).1 mp).symm ▸ nd⟩

src/data/padics/padic_norm.lean

@@ -7,6 +7,8 @@ import algebra.gcd_domain
 import algebra.field_power
 import ring_theory.multiplicity
 import data.real.cau_seq
+import tactic.ring_exp
+import tactic.basic
 
 /-!
 # p-adic norm
@@ -157,6 +159,24 @@ begin
     using padic_val_rat_def p n_nonzero,
 end
 
+lemma one_le_padic_val_nat_of_dvd {n p : nat} [prime : fact p.prime] (nonzero : n ≠ 0) (div : p ∣ n) :
+  1 ≤ padic_val_nat p n :=
+begin
+  rw @padic_val_nat_def _ prime _ nonzero,
+  let one_le_mul : _ ≤ multiplicity p n :=
+    @multiplicity.le_multiplicity_of_pow_dvd _ _ _ p n 1 (begin norm_num, exact div end),
+  simp only [enat.coe_one] at one_le_mul,
+  rcases one_le_mul with ⟨_, q⟩,
+  dsimp at q,
+  solve_by_elim,
+end
+
+@[simp]
+lemma padic_val_nat_zero (m : nat) : padic_val_nat m 0 = 0 := by simpa
+
+@[simp]
+lemma padic_val_nat_one (m : nat) : padic_val_nat m 1 = 0 := by simp [padic_val_nat]
+
 end padic_val_nat
 
 namespace padic_val_rat
@@ -297,6 +317,137 @@ theorem min_le_padic_val_rat_add {q r : ℚ}
 
 end padic_val_rat
 
+namespace padic_val_nat
+
+/--
+A rewrite lemma for `padic_val_nat p (q * r)` with conditions `q ≠ 0`, `r ≠ 0`.
+-/
+protected lemma mul (p : ℕ) [p_prime : fact p.prime] {q r : ℕ} (hq : q ≠ 0) (hr : r ≠ 0) :
+  padic_val_nat p (q * r) = padic_val_nat p q + padic_val_nat p r :=
+begin
+  apply int.coe_nat_inj,
+  simp only [padic_val_rat_of_nat, nat.cast_mul],
+  rw padic_val_rat.mul,
+  norm_cast,
+  exact cast_ne_zero.mpr hq,
+  exact cast_ne_zero.mpr hr,
+end
+
+/--
+Dividing out by a prime factor reduces the padic_val_nat by 1.
+-/
+protected lemma div {p : ℕ} [p_prime : fact p.prime] {b : ℕ} (dvd : p ∣ b) :
+  (padic_val_nat p (b / p)) = (padic_val_nat p b) - 1 :=
+begin
+  by_cases b_split : (b = 0),
+  { simp [b_split], },
+  { have split_frac : padic_val_rat p (b / p) = padic_val_rat p b - padic_val_rat p p :=
+      padic_val_rat.div p (nat.cast_ne_zero.mpr b_split) (nat.cast_ne_zero.mpr (nat.prime.ne_zero p_prime)),
+    rw padic_val_rat.padic_val_rat_self (nat.prime.one_lt p_prime) at split_frac,
+    have r : 1 ≤ padic_val_nat p b := one_le_padic_val_nat_of_dvd b_split dvd,
+    exact_mod_cast split_frac, }
+end
+
+end padic_val_nat
+
+section padic_val_nat
+
+/--
+If a prime doesn't appear in `n`, `padic_val_nat p n` is `0`.
+-/
+lemma padic_val_nat_of_not_dvd {p : ℕ} [fact p.prime] {n : ℕ} (not_dvd : ¬(p ∣ n)) :
+  padic_val_nat p n = 0 :=
+begin
+  by_cases hn : n = 0,
+  { subst hn, simp at not_dvd, trivial, },
+  { rw padic_val_nat_def hn,
+    exact (@multiplicity.unique' _ _ _ p n 0 (by simp) (by simpa using not_dvd)).symm,
+    assumption, },
+end
+
+lemma padic_val_nat_primes {p q : ℕ} [p_prime : fact p.prime] [q_prime : fact q.prime] (neq : p ≠ q) :
+  padic_val_nat p q = 0 :=
+@padic_val_nat_of_not_dvd p p_prime q $ (not_congr (iff.symm (prime_dvd_prime_iff_eq p_prime q_prime))).mp neq
+
+protected lemma padic_val_nat.div' {p : ℕ} [p_prime : fact p.prime] :
+  ∀ {m : ℕ} (cpm : coprime p m) {b : ℕ} (dvd : m ∣ b), padic_val_nat p (b / m) = padic_val_nat p b
+| 0 := λ cpm b dvd, by { rw zero_dvd_iff at dvd, rw [dvd, nat.zero_div], }
+| (n + 1) :=
+  λ cpm b dvd,
+  begin
+    rcases dvd with ⟨c, rfl⟩,
+    rw [mul_div_right c (nat.succ_pos _)],by_cases hc : c = 0,
+    { rw [hc, mul_zero] },
+    { rw padic_val_nat.mul,
+      { suffices : ¬ p ∣ (n+1),
+        { rw [padic_val_nat_of_not_dvd this, zero_add] },
+        contrapose! cpm,
+        exact p_prime.dvd_iff_not_coprime.mp cpm },
+      { exact nat.succ_ne_zero _ },
+      { exact hc } },
+  end
+
+lemma padic_val_nat_eq_factors_count (p : ℕ) [hp : fact p.prime] :
+  ∀ (n : ℕ), padic_val_nat p n = (factors n).count p
+| 0 := rfl
+| 1 := by { rw padic_val_nat_one, refl }
+| (m + 2) :=
+let n := m + 2 in
+let q := min_fac n in
+have hq : fact q.prime := min_fac_prime (show m + 2 ≠ 1, by linarith),
+have wf : n / q < n := nat.div_lt_self (nat.succ_pos _) hq.one_lt,
+begin
+  rw factors_add_two,
+  show padic_val_nat p n = list.count p (q :: (factors (n / q))),
+  rw [list.count_cons', ← padic_val_nat_eq_factors_count],
+  split_ifs with h,
+  have p_dvd_n : p ∣ n,
+    { have: q ∣ n := nat.min_fac_dvd n,
+      cc },
+  { rw [←h, padic_val_nat.div],
+    { have: 1 ≤ padic_val_nat p n := one_le_padic_val_nat_of_dvd (by linarith) p_dvd_n,
+      exact (nat.sub_eq_iff_eq_add this).mp rfl, },
+    { exact p_dvd_n, }, },
+  { suffices : p.coprime q,
+    { rw [padic_val_nat.div' this (min_fac_dvd n), add_zero], },
+    rwa nat.coprime_primes hp hq, },
+end
+
+open_locale big_operators
+
+lemma prod_pow_prime_padic_val_nat (n : nat) (hn : n ≠ 0) (m : nat) (pr : n < m) :
+  ∏ p in finset.filter nat.prime (finset.range m), p ^ (padic_val_nat p n) = n :=
+begin
+  rw ← nat.pos_iff_ne_zero at hn,
+  have H : (factors n : multiset ℕ).prod = n,
+  { rw [multiset.coe_prod, prod_factors hn], },
+  rw finset.prod_multiset_count at H,
+  conv_rhs { rw ← H, },
+  refine finset.prod_bij_ne_one (λ p hp hp', p) _ _ _ _,
+  { rintro p hp hpn,
+    rw [finset.mem_filter, finset.mem_range] at hp,
+    haveI Hp : fact p.prime := hp.2,
+    rw [multiset.mem_to_finset, multiset.mem_coe, mem_factors_iff_dvd hn Hp],
+    contrapose! hpn,
+    rw [padic_val_nat_of_not_dvd hpn, nat.pow_zero], },
+  { intros, assumption },
+  { intros p hp hpn,
+    rw [multiset.mem_to_finset, multiset.mem_coe] at hp,
+    haveI Hp : fact p.prime := mem_factors hp,
+    simp only [exists_prop, ne.def, finset.mem_filter, finset.mem_range],
+    refine ⟨p, ⟨_, Hp⟩, ⟨_, rfl⟩⟩,
+    { rw mem_factors_iff_dvd hn Hp at hp, exact lt_of_le_of_lt (le_of_dvd hn hp) pr },
+    { rw padic_val_nat_eq_factors_count,
+      simp only [pow_eq_pow, ne.def, multiset.coe_count] at hpn,
+      convert hpn } },
+  { intros p hp hpn,
+    rw [finset.mem_filter, finset.mem_range] at hp,
+    haveI Hp : fact p.prime := hp.2,
+    rw [padic_val_nat_eq_factors_count, multiset.coe_count, pow_eq_pow] }
+end
+
+end padic_val_nat
+
 /--
 If `q ≠ 0`, the p-adic norm of a rational `q` is `p ^ (-(padic_val_rat p q))`.
 If `q = 0`, the p-adic norm of `q` is 0.