feat(number_theory/factorization): evaluating arithmetic functions at…

… prime powers (#13817)




Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>

archive/100-theorems-list/70_perfect_numbers.lean

@@ -34,7 +34,7 @@ open arithmetic_function finset
 open_locale arithmetic_function
 
 lemma sigma_two_pow_eq_mersenne_succ (k : ℕ) : σ 1 (2 ^ k) = mersenne (k + 1) :=
-by simp [mersenne, prime_two, ← geom_sum_mul_add 1 (k+1)]
+by simp [sigma_one_apply, mersenne, prime_two, ← geom_sum_mul_add 1 (k+1)]
 
 /-- Euclid's theorem that Mersenne primes induce perfect numbers -/
 theorem perfect_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : (mersenne (k + 1)).prime) :
@@ -44,7 +44,7 @@ begin
     is_multiplicative_sigma.map_mul_of_coprime
         (nat.prime_two.coprime_pow_of_not_dvd (odd_mersenne_succ _)),
     sigma_two_pow_eq_mersenne_succ],
-  { simp [pr, nat.prime_two] },
+  { simp [pr, nat.prime_two, sigma_one_apply] },
   { apply mul_pos (pow_pos _ k) (mersenne_pos (nat.succ_pos k)),
     norm_num }
 end

src/data/int/cast.lean

@@ -119,6 +119,11 @@ begin
   rw [int.mul_div_cancel_left _ this, int.cast_mul, mul_div_cancel_left _ n_nonzero],
 end
 
+@[simp, norm_cast] theorem cast_ite [has_zero α] [has_one α] [has_add α] [has_neg α]
+  (P : Prop) [decidable P] (m n : ℤ) :
+  ((ite P m n : ℤ) : α) = ite P m n :=
+apply_ite _ _ _ _
+
 /-- `coe : ℤ → α` as an `add_monoid_hom`. -/
 def cast_add_hom (α : Type*) [add_group α] [has_one α] : ℤ →+ α := ⟨coe, cast_zero, cast_add⟩
 

src/data/list/dedup.lean

@@ -71,4 +71,10 @@ begin
     rw [dedup_cons_of_not_mem' h, insert_of_not_mem h]]
 end
 
+lemma repeat_dedup {x : α} : ∀ {k}, k ≠ 0 → (repeat x k).dedup = [x]
+| 0 h := (h rfl).elim
+| 1 _ := rfl
+| (n+2) _ := by rw [repeat_succ, dedup_cons_of_mem (mem_repeat.2 ⟨n.succ_ne_zero, rfl⟩),
+    repeat_dedup n.succ_ne_zero]
+
 end list

src/number_theory/arithmetic_function.lean

@@ -91,11 +91,11 @@ variable [has_one R]
 
 instance : has_one (arithmetic_function R) := ⟨⟨λ x, ite (x = 1) 1 0, rfl⟩⟩
 
-@[simp]
-lemma one_one : (1 : arithmetic_function R) 1 = 1 := rfl
+lemma one_apply {x : ℕ} : (1 : arithmetic_function R) x = ite (x = 1) 1 0 := rfl
 
-@[simp]
-lemma one_apply_ne {x : ℕ} (h : x ≠ 1) : (1 : arithmetic_function R) x = 0 := if_neg h
+@[simp] lemma one_one : (1 : arithmetic_function R) 1 = 1 := rfl
+
+@[simp] lemma one_apply_ne {x : ℕ} (h : x ≠ 1) : (1 : arithmetic_function R) x = 0 := if_neg h
 
 end has_one
 end has_zero
@@ -132,6 +132,14 @@ lemma coe_coe [has_zero R] [has_one R] [has_add R] [has_neg R] {f : arithmetic_f
   ((f : arithmetic_function ℤ) : arithmetic_function R) = f :=
 by { ext, simp, }
 
+@[simp] lemma nat_coe_one [add_zero_class R] [has_one R] :
+  ((1 : arithmetic_function ℕ) : arithmetic_function R) = 1 :=
+by { ext n, simp [one_apply] }
+
+@[simp] lemma int_coe_one [add_monoid R] [has_one R] [has_neg R] :
+  ((1 : arithmetic_function ℤ) : arithmetic_function R) = 1 :=
+by { ext n, simp [one_apply] }
+
 section add_monoid
 
 variable [add_monoid R]
@@ -185,6 +193,18 @@ instance [semiring R] : has_mul (arithmetic_function R) := ⟨(•)⟩
 lemma mul_apply [semiring R] {f g : arithmetic_function R} {n : ℕ} :
   (f * g) n = ∑ x in divisors_antidiagonal n, f x.fst * g x.snd := rfl
 
+lemma mul_apply_one [semiring R] {f g : arithmetic_function R} :
+  (f * g) 1 = f 1 * g 1 :=
+by simp
+
+@[simp, norm_cast] lemma nat_coe_mul [semiring R] {f g : arithmetic_function ℕ} :
+  (↑(f * g) : arithmetic_function R) = f * g :=
+by { ext n, simp }
+
+@[simp, norm_cast] lemma int_coe_mul [ring R] {f g : arithmetic_function ℤ} :
+  (↑(f * g) : arithmetic_function R) = f * g :=
+by { ext n, simp }
+
 section module
 variables {M : Type*} [semiring R] [add_comm_monoid M] [module R M]
 
@@ -635,16 +655,23 @@ begin
   simp [pow, (ne_of_lt (nat.succ_pos k)).symm],
 end
 
+lemma pow_zero_eq_zeta : pow 0 = ζ := by { ext n, simp }
+
 /-- `σ k n` is the sum of the `k`th powers of the divisors of `n` -/
 def sigma (k : ℕ) : arithmetic_function ℕ :=
 ⟨λ n, ∑ d in divisors n, d ^ k, by simp⟩
 
 localized "notation `σ` := nat.arithmetic_function.sigma" in arithmetic_function
 
-@[simp]
 lemma sigma_apply {k n : ℕ} : σ k n = ∑ d in divisors n, d ^ k := rfl
 
-lemma sigma_one_apply {n : ℕ} : σ 1 n = ∑ d in divisors n, d := by simp
+lemma sigma_one_apply (n : ℕ) : σ 1 n = ∑ d in divisors n, d := by simp [sigma_apply]
+
+lemma sigma_zero_apply (n : ℕ) : σ 0 n = (divisors n).card := by simp [sigma_apply]
+
+lemma sigma_zero_apply_prime_pow {p i : ℕ} (hp : p.prime) :
+  σ 0 (p ^ i) = i + 1 :=
+by rw [sigma_zero_apply, divisors_prime_pow hp, card_map, card_range]
 
 lemma zeta_mul_pow_eq_sigma {k : ℕ} : ζ * pow k = σ k :=
 begin
@@ -657,13 +684,20 @@ begin
   simp [hx],
 end
 
-lemma is_multiplicative_zeta : is_multiplicative ζ :=
-⟨by simp, λ m n cop, begin
-  cases m, {simp},
-  cases n, {simp},
-  simp [nat.succ_ne_zero]
+lemma is_multiplicative_one [monoid_with_zero R] : is_multiplicative (1 : arithmetic_function R) :=
+is_multiplicative.iff_ne_zero.2 ⟨by simp,
+begin
+  intros m n hm hn hmn,
+  rcases eq_or_ne m 1 with rfl | hm',
+  { simp },
+  rw [one_apply_ne, one_apply_ne hm', zero_mul],
+  rw [ne.def, nat.mul_eq_one_iff, not_and_distrib],
+  exact or.inl hm'
 end⟩
 
+lemma is_multiplicative_zeta : is_multiplicative ζ :=
+is_multiplicative.iff_ne_zero.2 ⟨by simp, by simp {contextual := tt}⟩
+
 lemma is_multiplicative_id : is_multiplicative arithmetic_function.id :=
 ⟨rfl, λ _ _ _, rfl⟩
 
@@ -681,7 +715,7 @@ lemma is_multiplicative_pow {k : ℕ} : is_multiplicative (pow k) :=
 is_multiplicative_id.ppow
 
 lemma is_multiplicative_sigma {k : ℕ} :
-  is_multiplicative (sigma k) :=
+  is_multiplicative (σ k) :=
 begin
   rw [← zeta_mul_pow_eq_sigma],
   apply ((is_multiplicative_zeta).mul is_multiplicative_pow)
@@ -728,6 +762,12 @@ begin
   simp [h0, card_factors_mul, h],
 end
 
+@[simp] lemma card_factors_apply_prime {p : ℕ} (hp : p.prime) : Ω p = 1 :=
+card_factors_eq_one_iff_prime.2 hp
+
+@[simp] lemma card_factors_apply_prime_pow {p k : ℕ} (hp : p.prime) : Ω (p ^ k) = k :=
+by rw [card_factors_apply, hp.factors_pow, list.length_repeat]
+
 /-- `ω n` is the number of distinct prime factors of `n`. -/
 def card_distinct_factors : arithmetic_function ℕ :=
 ⟨λ n, n.factors.dedup.length, by simp⟩
@@ -736,6 +776,8 @@ localized "notation `ω` := nat.arithmetic_function.card_distinct_factors" in ar
 
 lemma card_distinct_factors_zero : ω 0 = 0 := by simp
 
+@[simp] lemma card_distinct_factors_one : ω 1 = 0 := by simp [card_distinct_factors]
+
 lemma card_distinct_factors_apply {n : ℕ} :
   ω n = n.factors.dedup.length := rfl
 
@@ -750,6 +792,13 @@ begin
     refl }
 end
 
+@[simp] lemma card_distinct_factors_apply_prime_pow {p k : ℕ} (hp : p.prime) (hk : k ≠ 0) :
+  ω (p ^ k) = 1 :=
+by rw [card_distinct_factors_apply, hp.factors_pow, list.repeat_dedup hk, list.length_singleton]
+
+@[simp] lemma card_distinct_factors_apply_prime {p : ℕ} (hp : p.prime) : ω p = 1 :=
+by rw [←pow_one p, card_distinct_factors_apply_prime_pow hp one_ne_zero]
+
 /-- `μ` is the Möbius function. If `n` is squarefree with an even number of distinct prime factors,
   `μ n = 1`. If `n` is squarefree with an odd number of distinct prime factors, `μ n = -1`.
   If `n` is not squarefree, `μ n = 0`. -/
@@ -759,11 +808,12 @@ def moebius : arithmetic_function ℤ :=
 localized "notation `μ` := nat.arithmetic_function.moebius" in arithmetic_function
 
 @[simp]
-lemma moebius_apply_of_squarefree {n : ℕ} (h : squarefree n): μ n = (-1) ^ (card_factors n) :=
+lemma moebius_apply_of_squarefree {n : ℕ} (h : squarefree n) : μ n = (-1) ^ card_factors n :=
 if_pos h
 
-@[simp]
-lemma moebius_eq_zero_of_not_squarefree {n : ℕ} (h : ¬ squarefree n): μ n = 0 := if_neg h
+@[simp] lemma moebius_eq_zero_of_not_squarefree {n : ℕ} (h : ¬ squarefree n) : μ n = 0 := if_neg h
+
+lemma moebius_apply_one : μ 1 = 1 := by simp
 
 lemma moebius_ne_zero_iff_squarefree {n : ℕ} : μ n ≠ 0 ↔ squarefree n :=
 begin
@@ -782,6 +832,28 @@ begin
   { rcases h with h | h; simp [h] }
 end
 
+lemma moebius_apply_prime {p : ℕ} (hp : p.prime) : μ p = -1 :=
+by rw [moebius_apply_of_squarefree hp.squarefree, card_factors_apply_prime hp, pow_one]
+
+lemma moebius_apply_prime_pow {p k : ℕ} (hp : p.prime) (hk : k ≠ 0) :
+  μ (p ^ k) = if k = 1 then -1 else 0 :=
+begin
+  split_ifs,
+  { rw [h, pow_one, moebius_apply_prime hp] },
+  rw [moebius_eq_zero_of_not_squarefree],
+  rw [squarefree_pow_iff hp.ne_one hk, not_and_distrib],
+  exact or.inr h,
+end
+
+lemma moebius_apply_is_prime_pow_not_prime {n : ℕ} (hn : is_prime_pow n) (hn' : ¬ n.prime) :
+  μ n = 0 :=
+begin
+  obtain ⟨p, k, hp, hk, rfl⟩ := (is_prime_pow_nat_iff _).1 hn,
+  rw [moebius_apply_prime_pow hp hk.ne', if_neg],
+  rintro rfl,
+  exact hn' (by simpa),
+end
+
 lemma is_multiplicative_moebius : is_multiplicative μ :=
 begin
   rw is_multiplicative.iff_ne_zero,
@@ -792,60 +864,35 @@ end
 
 open unique_factorization_monoid
 
-@[simp] lemma coe_moebius_mul_coe_zeta [ring R] : (μ * ζ : arithmetic_function R) = 1 :=
+@[simp] lemma moebius_mul_coe_zeta : (μ * ζ : arithmetic_function ℤ) = 1 :=
 begin
-  ext x,
-  cases x,
-  { simp only [divisors_zero, sum_empty, ne.def, not_false_iff, coe_mul_zeta_apply,
-      zero_ne_one, one_apply_ne] },
-  cases x,
-  { simp only [moebius_apply_of_squarefree, card_factors_one, squarefree_one, divisors_one,
-      int.cast_one, sum_singleton, coe_mul_zeta_apply, one_one, int_coe_apply, pow_zero] },
-  rw [coe_mul_zeta_apply, one_apply_ne (ne_of_gt (succ_lt_succ (nat.succ_pos _)))],
-  simp_rw [int_coe_apply],
-  rw [←int.cast_sum, ← sum_filter_ne_zero],
-  convert int.cast_zero,
-  simp only [moebius_ne_zero_iff_squarefree],
-  suffices :
-    ∑ (y : finset ℕ) in
-      (unique_factorization_monoid.normalized_factors x.succ.succ).to_finset.powerset,
-    ite (squarefree y.val.prod) ((-1:ℤ) ^ Ω y.val.prod) 0 = 0,
-  { have h : ∑ i in _, ite (squarefree i) ((-1:ℤ) ^ Ω i) 0 = _ :=
-      (sum_divisors_filter_squarefree (nat.succ_ne_zero _)),
-    exact (eq.trans (by congr') h).trans this },
-  apply eq.trans (sum_congr rfl _) (sum_powerset_neg_one_pow_card_of_nonempty _),
-  { intros y hy,
-    rw [finset.mem_powerset, ← finset.val_le_iff, multiset.to_finset_val] at hy,
-    have h : unique_factorization_monoid.normalized_factors y.val.prod = y.val,
-    { apply factors_multiset_prod_of_irreducible,
-      intros z hz,
-      apply irreducible_of_normalized_factor _ (multiset.subset_of_le
-        (le_trans hy (multiset.dedup_le _)) hz) },
-    rw [if_pos],
-    { rw [card_factors_apply, ← multiset.coe_card, ← factors_eq, h, finset.card] },
-    rw [unique_factorization_monoid.squarefree_iff_nodup_normalized_factors, h],
-    { apply y.nodup },
-    rw [ne.def, multiset.prod_eq_zero_iff],
-    intro con,
-    rw ← h at con,
-    exact not_irreducible_zero (irreducible_of_normalized_factor 0 con) },
-  { rw finset.nonempty,
-    rcases wf_dvd_monoid.exists_irreducible_factor _ (nat.succ_ne_zero _) with ⟨i, hi⟩,
-    { rcases exists_mem_normalized_factors_of_dvd (nat.succ_ne_zero _) hi.1 hi.2 with ⟨j, hj, hj2⟩,
-      use j,
-      apply multiset.mem_to_finset.2 hj },
-    rw nat.is_unit_iff,
-    norm_num },
+  ext n,
+  refine rec_on_pos_prime_pos_coprime _ _ _ _ n,
+  { intros p n hp hn,
+    rw [coe_mul_zeta_apply, sum_divisors_prime_pow hp, sum_range_succ'],
+    simp_rw [function.embedding.coe_fn_mk, pow_zero, moebius_apply_one,
+      moebius_apply_prime_pow hp (nat.succ_ne_zero _), nat.succ_inj', sum_ite_eq', mem_range,
+      if_pos hn, add_left_neg],
+    rw one_apply_ne,
+    rw [ne.def, pow_eq_one_iff],
+    { exact hp.ne_one },
+    { exact hn.ne' } },
+  { rw [zero_hom.map_zero, zero_hom.map_zero] },
+  { simp },
+  { intros a b ha hb hab ha' hb',
+    rw [is_multiplicative.map_mul_of_coprime _ hab, ha', hb',
+      is_multiplicative.map_mul_of_coprime is_multiplicative_one hab],
+    exact is_multiplicative_moebius.mul is_multiplicative_zeta.nat_cast }
 end
 
-@[simp] lemma coe_zeta_mul_coe_moebius [comm_ring R] : (ζ * μ : arithmetic_function R) = 1 :=
-by rw [mul_comm, coe_moebius_mul_coe_zeta]
+@[simp] lemma coe_zeta_mul_moebius : (ζ * μ : arithmetic_function ℤ) = 1 :=
+by rw [mul_comm, moebius_mul_coe_zeta]
 
-@[simp] lemma moebius_mul_coe_zeta : (μ * ζ : arithmetic_function ℤ) = 1 :=
-by rw [← int_coe_int μ, coe_moebius_mul_coe_zeta]
+@[simp] lemma coe_moebius_mul_coe_zeta [ring R] : (μ * ζ : arithmetic_function R) = 1 :=
+by rw [←coe_coe, ←int_coe_mul, moebius_mul_coe_zeta, int_coe_one]
 
-@[simp] lemma coe_zeta_mul_moebius : (ζ * μ : arithmetic_function ℤ) = 1 :=
-by rw [← int_coe_int μ, coe_zeta_mul_coe_moebius]
+@[simp] lemma coe_zeta_mul_coe_moebius [ring R] : (ζ * μ : arithmetic_function R) = 1 :=
+by rw [←coe_coe, ←int_coe_mul, coe_zeta_mul_moebius, int_coe_one]
 
 section comm_ring
 variable [comm_ring R]