[Merged by Bors] - feat: define prodPrimeFactors as an ArithmeticFunction

Mathlib/Data/Nat/Squarefree.lean

@@ -428,6 +428,13 @@ lemma prod_primeFactors_invOn_squarefree :
       {s | ∀ p ∈ s, p.Prime} {n | Squarefree n} :=
   ⟨fun _s ↦ primeFactors_prod, fun _n ↦ prod_primeFactors_of_squarefree⟩
 
+theorem prod_primeFactors_sdiff_of_squarefree {n : ℕ} (hn : Squarefree n) {t : Finset ℕ}
+    (ht : t ⊆ n.primeFactors) :
+    ∏ a in (n.primeFactors \ t), a = n / ∏ a in t, a := by
+  refine symm $ Nat.div_eq_of_eq_mul_left (Finset.prod_pos
+    fun p hp => (prime_of_mem_factors (List.mem_toFinset.mp (ht hp))).pos) ?_
+  rw [Finset.prod_sdiff ht, prod_primeFactors_of_squarefree hn]
+
 end Nat
 
 -- Porting note: comment out NormNum tactic, to be moved to another file.

Mathlib/NumberTheory/ArithmeticFunction.lean

@@ -47,8 +47,12 @@ to form the Dirichlet ring.
  * `prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero` for functions to a `CommGroupWithZero`
 
 ## Notation
-The arithmetic functions `ζ` and `σ` have Greek letter names, which are localized notation in
-the namespace `ArithmeticFunction`.
+All notation is localized in the namespace `ArithmeticFunction`.
+
+The arithmetic functions `ζ`, `σ`, `ω`, `Ω` and `μ` have Greek letter names.
+
+The arithmetic function $$n \mapsto \prod_{p \mid n} f(p)$$ is given custom notation
+`∏ᵖ p ∣ n, f p` when applied to `n`.
 
 ## Tags
 arithmetic functions, dirichlet convolution, divisors
@@ -590,6 +594,31 @@ theorem pdiv_zeta [DivisionSemiring R] (f : ArithmeticFunction R) :
 
 end Pdiv
 
+section ProdPrimeFactors
+
+/-- The map $n \mapsto \prod_{p \mid n} f(p)$ as an arithmetic function -/
+def prodPrimeFactors [CommMonoidWithZero R] (f : ℕ → R) : ArithmeticFunction R where
+  toFun d := if d = 0 then 0 else ∏ p in d.primeFactors, f p
+  map_zero' := if_pos rfl
+
+open Std.ExtendedBinder
+
+/-- `∏ᵖ p ∣ n, f p` is custom notation for `prodPrimeFactors f n` -/
+scoped syntax (name := bigproddvd) "∏ᵖ " extBinder " ∣ " term ", " term:67 : term
+scoped macro_rules (kind := bigproddvd)
+  | `(∏ᵖ $x:ident ∣ $n, $r) => `(prodPrimeFactors (fun $x ↦ $r) $n)
+
+@[simp]
+theorem prodPrimeFactors_apply [CommMonoidWithZero R] {f: ℕ → R} {n : ℕ} (hn : n ≠ 0) :
+    ∏ᵖ p ∣ n, f p = ∏ p in n.primeFactors, f p :=
+  if_neg hn
+
+theorem prodPrimeFactors_apply_of_ne_zero [CommMonoidWithZero R] {f : ℕ → R} {n : ℕ}
+    (hn : n ≠ 0) : ∏ᵖ p ∣ n, f p = ∏ p in n.primeFactors, f p :=
+  prodPrimeFactors_apply hn
+
+end ProdPrimeFactors
+
 /-- Multiplicative functions -/
 def IsMultiplicative [MonoidWithZero R] (f : ArithmeticFunction R) : Prop :=
   f 1 = 1 ∧ ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
@@ -625,6 +654,18 @@ theorem map_prod {ι : Type*} [CommMonoidWithZero R] (g : ι → ℕ) {f : Nat.A
     exact .prod_right fun i hi => hs.2 _ hi (hi.ne_of_not_mem has).symm
 #align nat.arithmetic_function.is_multiplicative.map_prod Nat.ArithmeticFunction.IsMultiplicative.map_prod
 
+theorem map_prod_of_prime [CommSemiring R] {f : ArithmeticFunction R}
+    (h_mult : ArithmeticFunction.IsMultiplicative f)
+    (t : Finset ℕ) (ht : ∀ p ∈ t, p.Prime) :
+    f (∏ a in t, a) = ∏ a : ℕ in t, f a :=
+  map_prod _ h_mult t fun x hx y hy hxy => (coprime_primes (ht x hx) (ht y hy)).mpr hxy
+
+theorem map_prod_of_subset_primeFactors [CommSemiring R] {f : ArithmeticFunction R}
+    (h_mult : ArithmeticFunction.IsMultiplicative f) (l : ℕ)
+    (t : Finset ℕ) (ht : t ⊆ l.primeFactors) :
+     f (∏ a in t, a) = ∏ a : ℕ in t, f a :=
+  map_prod_of_prime h_mult t fun _ a => prime_of_mem_primeFactors (ht a)
+
 theorem nat_cast {f : ArithmeticFunction ℕ} [Semiring R] (h : f.IsMultiplicative) :
     IsMultiplicative (f : ArithmeticFunction R) :=
                                  -- porting note: was `by simp [cop, h]`
@@ -754,6 +795,29 @@ theorem eq_iff_eq_on_prime_powers [CommMonoidWithZero R] (f : ArithmeticFunction
   exact Finset.prod_congr rfl fun p hp ↦ h p _ (Nat.prime_of_mem_primeFactors hp)
 #align nat.arithmetic_function.is_multiplicative.eq_iff_eq_on_prime_powers Nat.ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers
 
+theorem prodPrimeFactors [CommMonoidWithZero R] (f : ℕ → R) :
+    IsMultiplicative (prodPrimeFactors f) := by
+  rw [iff_ne_zero]
+  refine ⟨prodPrimeFactors_apply one_ne_zero, ?_⟩
+  intro x y hx hy hxy
+  have hxy₀: x*y ≠ 0 := by exact Nat.mul_ne_zero hx hy
+  rw [prodPrimeFactors_apply hxy₀, prodPrimeFactors_apply hx, prodPrimeFactors_apply hy,
+    Nat.primeFactors_mul hx hy, ← Finset.prod_union hxy.disjoint_primeFactors]
+
+theorem prodPrimeFactors_add_of_squarefree [CommSemiring R] {f g : ArithmeticFunction R}
+    (hf : IsMultiplicative f) (hg : IsMultiplicative g) {n : ℕ} (hn : Squarefree n) :
+    ∏ᵖ p ∣ n, (f + g) p = (f * g) n := by
+  rw [prodPrimeFactors_apply_of_ne_zero hn.ne_zero]
+  simp_rw [add_apply (f:=f) (g:=g)]
+  rw [Finset.prod_add, mul_apply, sum_divisorsAntidiagonal (f · * g ·),
+    ← divisors_filter_squarefree_of_squarefree hn, sum_divisors_filter_squarefree hn.ne_zero,
+    factors_eq]
+  apply Finset.sum_congr rfl
+  intro t ht
+  erw [t.prod_val, ← prod_primeFactors_sdiff_of_squarefree hn (Finset.mem_powerset.mp ht),
+    hf.map_prod_of_subset_primeFactors n t (Finset.mem_powerset.mp ht),
+    ← hg.map_prod_of_subset_primeFactors n (_ \ t) (Finset.sdiff_subset _ t)]
+
 theorem lcm_apply_mul_gcd_apply [CommMonoidWithZero R] {f : ArithmeticFunction R}
     (hf : f.IsMultiplicative) {x y : ℕ} :
     f (x.lcm y) * f (x.gcd y) = f x * f y := by
@@ -1043,6 +1107,27 @@ theorem isMultiplicative_moebius : IsMultiplicative μ := by
     cardFactors_mul hn hm, pow_add]
 #align nat.arithmetic_function.is_multiplicative_moebius Nat.ArithmeticFunction.isMultiplicative_moebius
 
+theorem IsMultiplicative.prodPrimeFactors_one_add_of_squarefree [CommSemiring R]
+    {f : ArithmeticFunction R} (h_mult : f.IsMultiplicative) {n : ℕ} (hn : Squarefree n) :
+    ∏ p in n.primeFactors, (1 + f p) = ∑ d in n.divisors, f d := by
+  trans (∏ᵖ p ∣ n, ((ζ:ArithmeticFunction R) + f) p)
+  · simp_rw [prodPrimeFactors_apply hn.ne_zero, add_apply, natCoe_apply]
+    apply Finset.prod_congr rfl; intro p hp;
+    rw [zeta_apply_ne (prime_of_mem_factors $ List.mem_toFinset.mp hp).ne_zero, cast_one]
+  rw [isMultiplicative_zeta.nat_cast.prodPrimeFactors_add_of_squarefree h_mult hn,
+    coe_zeta_mul_apply]
+
+theorem IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree [CommRing R]
+    (f : ArithmeticFunction R) (hf : f.IsMultiplicative) {n : ℕ} (hn : Squarefree n) :
+    ∏ p in n.primeFactors, (1 - f p) = ∑ d in n.divisors, μ d * f d := by
+  trans (∏ p in n.primeFactors, (1 + (ArithmeticFunction.pmul (μ:ArithmeticFunction R) f) p))
+  · apply Finset.prod_congr rfl; intro p hp
+    rw [pmul_apply, intCoe_apply, ArithmeticFunction.moebius_apply_prime
+        (prime_of_mem_factors (List.mem_toFinset.mp hp))]
+    ring
+  · rw [(isMultiplicative_moebius.int_cast.pmul hf).prodPrimeFactors_one_add_of_squarefree hn]
+    simp_rw [pmul_apply, intCoe_apply]
+
 open UniqueFactorizationMonoid
 
 @[simp]