feat(NumberTheory/ArithmeticFunction/LFunction): ofPowerSeries produces multiplicative power series (#37767)

This PR proves that `ArithmeticFunction.ofPowerSeries` produces multiplicative power series. I had to assume `CommRing` in order to use `PowerSeries.subst`.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/NumberTheory/ArithmeticFunction/LFunction.lean

@@ -42,10 +42,6 @@ For context, here is a diagram of the possible routes from polynomials to L-func
           | (product)                 | (product)                 | (product)
           v                 T=q⁻ˢ     V               s ∈ ℂ       V
 [multivariate power series] ----> [Dirichlet series] ----> [L-function in s] (the Euler product)
-
-## TODO
-
-* If each `q` is a prime power, then `ArithmeticFunction.ofPowerSeries q f` is multiplicative.
 -/
 
 @[expose] public section
@@ -54,7 +50,11 @@ namespace ArithmeticFunction
 
 section PowerSeries
 
-variable {R : Type*} [CommSemiring R]
+variable {R : Type*}
+
+section CommSemiring
+
+variable [CommSemiring R]
 
 /-- The arithmetic function corresponding to the Dirichlet series `f(q⁻ˢ)`.
 For example, if `f = 1 + X + X² + ...` and `q = p`, then `f(q⁻ˢ) = 1 + p⁻ˢ + p⁻²ˢ + ...`.
@@ -147,6 +147,71 @@ theorem ofPowerSeries_apply_one (q : ℕ) (f : PowerSeries R) :
   · rw [← pow_zero q, ofPowerSeries_apply_pow hq, PowerSeries.coeff_zero_eq_constantCoeff]
   · simp [ofPowerSeries, dif_neg hq]
 
+end CommSemiring
+
+section CommRing
+
+variable [CommRing R]
+
+/-- In `ArithmeticFunction.ofPowerSeries`, replacing the base `q` with a power `q ^ k` corresponds
+to substituting `X` with `X ^ k` in the original power series. -/
+theorem ofPowerSeries_pow (q : ℕ) {k : ℕ} (hk : k ≠ 0) (f : PowerSeries R) :
+    ofPowerSeries (q ^ k) f = ofPowerSeries q (f.subst (PowerSeries.X ^ k)) := by
+  classical
+  by_cases hq : 1 < q
+  · ext n
+    by_cases hn : ∃ i, q ^ i = n
+    · obtain ⟨i, rfl⟩ := hn
+      rw [ofPowerSeries_apply_pow hq, PowerSeries.coeff_subst_X_pow hk]
+      split_ifs with hn
+      · obtain ⟨j, rfl⟩ := hn
+        rw [pow_mul, ofPowerSeries_apply_pow (one_lt_pow' hq hk)]
+        simp [hk]
+      · rw [ofPowerSeries_apply (one_lt_pow' hq hk), Function.extend_apply', Pi.zero_apply]
+        simp_rw [← pow_mul, Nat.pow_right_inj hq, eq_comm, ← dvd_def]
+        exact hn
+    · rwa [ofPowerSeries_apply hq, ofPowerSeries_apply (one_lt_pow' hq hk),
+        Function.extend_apply', Function.extend_apply']
+      contrapose! hn
+      obtain ⟨i, rfl⟩ := hn
+      exact ⟨k * i, pow_mul q k i⟩
+  · simp [ofPowerSeries, hq, hk]
+
+-- todo: generalize to `CommSemiring`
+/-- `ArithmeticFunction.ofPowerSeries` produces multiplicative power series. -/
+theorem isMultiplicative_ofPowerSeries_of_isPrimePow
+    (q : ℕ) (hq : IsPrimePow q) (f : PowerSeries R) (hf : f.constantCoeff = 1) :
+    IsMultiplicative (ofPowerSeries q f) := by
+  refine ⟨(ofPowerSeries_apply_one q f).trans hf, fun {m n} hmn ↦ ?_⟩
+  obtain ⟨p, k, hp, hk, rfl⟩ := hq
+  rw [← Nat.prime_iff] at hp
+  rw [ofPowerSeries_pow p hk.ne']
+  by_cases hm : ∃ i, p ^ i = m
+  · obtain ⟨i, rfl⟩ := hm
+    by_cases hn : ∃ j, p ^ j = n
+    · obtain ⟨j, rfl⟩ := hn
+      cases i
+      · simp [hk.ne', hf]
+      · cases j
+        · simp [hk.ne', hf]
+        · simp [hp.ne_one] at hmn
+    · simp_rw [ofPowerSeries_apply hp.one_lt]
+      rw [Function.extend_apply', Function.extend_apply' _ _ _ hn,
+        Pi.zero_apply, Pi.zero_apply, mul_zero]
+      contrapose! hn
+      obtain ⟨j, hj⟩ := hn
+      obtain ⟨v, -, rfl⟩ := (Nat.dvd_prime_pow hp).mp (Dvd.intro_left _ hj.symm)
+      exact ⟨v, rfl⟩
+  · simp_rw [ofPowerSeries_apply hp.one_lt]
+    rw [Function.extend_apply', Function.extend_apply' _ _ _ hm,
+      Pi.zero_apply, Pi.zero_apply, zero_mul]
+    contrapose! hm
+    obtain ⟨i, hi⟩ := hm
+    obtain ⟨j, -, rfl⟩ := (Nat.dvd_prime_pow hp).mp ⟨n, hi⟩
+    exact ⟨j, rfl⟩
+
+end CommRing
+
 end PowerSeries
 
 section EulerProduct