From a251ad4621fbba21ca0d49adfd48c212dcc8f98d Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Mon, 25 Mar 2024 20:19:45 +0000
Subject: [PATCH] feat(NumberTheory/LSeries/Convolution): new file; convolution
 of sequences and products of L-series (#11634)

This is the next PR in a sequence that establishes general results on L-series.
See [this thread on Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837).

This adds the definition of the Dirichlet convolution of two sequences (as `LSeries.convolution`) and shows that the associated L-series is the product of the L-series associated to the two original sequences.
---
 Mathlib.lean                                  |   1 +
 Mathlib/NumberTheory/LSeries/Convolution.lean | 192 ++++++++++++++++++
 2 files changed, 193 insertions(+)
 create mode 100644 Mathlib/NumberTheory/LSeries/Convolution.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 7d5c756a05a82..06278a31b99a2 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2965,6 +2965,7 @@ import Mathlib.NumberTheory.KummerDedekind
 import Mathlib.NumberTheory.LSeries.AbstractFuncEq
 import Mathlib.NumberTheory.LSeries.Basic
 import Mathlib.NumberTheory.LSeries.Convergence
+import Mathlib.NumberTheory.LSeries.Convolution
 import Mathlib.NumberTheory.LSeries.Deriv
 import Mathlib.NumberTheory.LSeries.Linearity
 import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
diff --git a/Mathlib/NumberTheory/LSeries/Convolution.lean b/Mathlib/NumberTheory/LSeries/Convolution.lean
new file mode 100644
index 0000000000000..f9c58463e483c
--- /dev/null
+++ b/Mathlib/NumberTheory/LSeries/Convolution.lean
@@ -0,0 +1,192 @@
+/-
+Copyright (c) 2024 Michael Stoll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Stoll
+-/
+import Mathlib.Analysis.InnerProductSpace.Basic
+import Mathlib.NumberTheory.LSeries.Convergence
+import Mathlib.Analysis.Normed.Field.InfiniteSum
+
+/-!
+# Dirichlet convolution of sequences and products of L-series
+
+We define the *Dirichlet convolution* `f ⍟ g` of two sequences `f g : ℕ → R` with values in a
+semiring `R` by `(f ⍟ g) n = ∑ (k * m = n), f k * g m` when `n ≠ 0` and `(f ⍟ g) 0 = 0`.
+Technically, this is done by transporting the existing definition for `ArithmeticFunction R`;
+see `LSeries.convolution`. We show that these definitions agree (`LSeries.convolution_def`).
+
+We then consider the case `R = ℂ` and show that `L (f ⍟ g) = L f * L g` on the common domain
+of convergence of the L-series `L f`  and `L g` of `f` and `g`; see `LSeries_convolution`
+and `LSeries_convolution'`.
+-/
+
+open scoped LSeries.notation
+
+open Complex LSeries
+
+/-!
+### Dirichlet convolution of two functions
+-/
+
+open BigOperators
+
+/-- We turn any function `ℕ → R` into an `ArithmeticFunction R` by setting its value at `0`
+to be zero. -/
+def toArithmeticFunction {R : Type*} [Zero R] (f : ℕ → R) : ArithmeticFunction R where
+  toFun n := if n = 0 then 0 else f n
+  map_zero' := rfl
+
+/-- If we consider an arithmetic function just as a function and turn it back into an
+arithmetic function, it is the same as before. -/
+@[simp]
+lemma ArithmeticFunction.toArithmeticFunction_eq_self {R : Type*} [Zero R]
+    (f : ArithmeticFunction R) :
+    toArithmeticFunction f = f := by
+  ext n
+  simp (config := {contextual := true}) [toArithmeticFunction, ArithmeticFunction.map_zero]
+
+/-- Dirichlet convolution of two sequences.
+
+We define this in terms of the already existing definition for arithmetic functions. -/
+noncomputable def LSeries.convolution {R : Type*} [Semiring R] (f g : ℕ → R) : ℕ → R :=
+  ⇑(toArithmeticFunction f * toArithmeticFunction g)
+
+@[inherit_doc]
+scoped[LSeries.notation] infixl:70 " ⍟ " => LSeries.convolution
+
+/-- The product of two arithmetic functions defines the same function as the Dirichlet convolution
+of the functions defined by them. -/
+lemma ArithmeticFunction.coe_mul {R : Type*} [Semiring R] (f g : ArithmeticFunction R) :
+    f ⍟ g = ⇑(f * g) := by
+  simp only [convolution, ArithmeticFunction.toArithmeticFunction_eq_self]
+
+namespace LSeries
+
+lemma convolution_def {R : Type*} [Semiring R] (f g : ℕ → R) :
+    f ⍟ g = fun n ↦ ∑ p in n.divisorsAntidiagonal, f p.1 * g p.2 := by
+  ext n
+  simp only [convolution, toArithmeticFunction, ArithmeticFunction.mul_apply,
+    ArithmeticFunction.coe_mk, mul_ite, mul_zero, ite_mul, zero_mul]
+  refine Finset.sum_congr rfl fun p hp ↦ ?_
+  obtain ⟨hp₁, hp₂⟩ := Nat.mem_divisorsAntidiagonal.mp hp
+  obtain ⟨h₁, h₂⟩ := mul_ne_zero_iff.mp (hp₁.symm ▸ hp₂)
+  simp only [h₂, ↓reduceIte, h₁]
+
+@[simp]
+lemma convolution_map_zero {R : Type*} [Semiring R] (f g : ℕ → R) : (f ⍟ g) 0 = 0 := by
+  simp only [convolution_def, Nat.divisorsAntidiagonal_zero, Finset.sum_empty]
+
+
+/-!
+### Multiplication of L-series
+-/
+
+/-- We give an expression of the `LSeries.term` of the convolution of two functions
+in terms of a sum over `Nat.divisorsAntidiagonal`. -/
+lemma term_convolution (f g : ℕ → ℂ) (s : ℂ) (n : ℕ) :
+    term (f ⍟ g) s n = ∑ p in n.divisorsAntidiagonal, term f s p.1 * term g s p.2 := by
+  rcases eq_or_ne n 0 with rfl | hn
+  · simp only [term_zero, Nat.divisorsAntidiagonal_zero, Finset.sum_empty]
+  -- now `n ≠ 0`
+  rw [term_of_ne_zero hn, convolution_def, Finset.sum_div]
+  refine Finset.sum_congr rfl fun p hp ↦ ?_
+  obtain ⟨hp, hn₀⟩ := Nat.mem_divisorsAntidiagonal.mp hp
+  have ⟨hp₁, hp₂⟩ := mul_ne_zero_iff.mp <| hp.symm ▸ hn₀
+  rw [term_of_ne_zero hp₁ f s, term_of_ne_zero hp₂ g s, mul_comm_div, div_div,
+    ← mul_div_assoc, ← natCast_mul_natCast_cpow, ← Nat.cast_mul, mul_comm p.2, hp]
+
+open Set in
+/-- We give an expression of the `LSeries.term` of the convolution of two functions
+in terms of an a priori infinte sum over all pairs `(k, m)` with `k * m = n`
+(the set we sum over is infinite when `n = 0`). This is the version needed for the
+proof that `L (f ⍟ g) = L f * L g`. -/
+lemma term_convolution' (f g : ℕ → ℂ) (s : ℂ) :
+    term (f ⍟ g) s = fun n ↦
+      ∑' (b : (fun p : ℕ × ℕ ↦ p.1 * p.2) ⁻¹' {n}), term f s b.val.1 * term g s b.val.2 := by
+  ext n
+  rcases eq_or_ne n 0 with rfl | hn
+  · -- show that both sides vanish when `n = 0`; this is the hardest part of the proof!
+    refine (term_zero ..).trans ?_
+    -- the right hand sum is over the union below, but in each term, one factor is always zero
+    have hS : (fun p ↦ p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0} := by
+      ext
+      simp only [mem_preimage, mem_singleton_iff, mul_eq_zero, mem_union, mem_prod, mem_univ,
+        and_true, true_and]
+    have : ∀ p : (fun p : ℕ × ℕ ↦ p.1 * p.2) ⁻¹' {0}, term f s p.val.1 * term g s p.val.2 = 0 := by
+      rintro ⟨⟨p₁, p₂⟩, hp⟩
+      rcases hS ▸ hp with ⟨rfl, -⟩ | ⟨-, rfl⟩ <;> simp only [term_zero, zero_mul, mul_zero]
+    simp only [this, tsum_zero]
+  -- now `n ≠ 0`
+  rw [show (fun p : ℕ × ℕ ↦ p.1 * p.2) ⁻¹' {n} = n.divisorsAntidiagonal by ext; simp [hn],
+    Finset.tsum_subtype' n.divisorsAntidiagonal fun p ↦ term f s p.1 * term g s p.2,
+    term_convolution f g s n]
+
+end LSeries
+
+open Set in
+/-- The L-series of the convolution product `f ⍟ g` of two sequences `f` and `g`
+equals the product of their L-series, assuming both L-series converge. -/
+lemma LSeriesHasSum.convolution {f g : ℕ → ℂ} {s a b : ℂ} (hf : LSeriesHasSum f s a)
+    (hg : LSeriesHasSum g s b) :
+    LSeriesHasSum (f ⍟ g) s (a * b) := by
+  simp only [LSeriesHasSum, term_convolution']
+  have hsum := summable_mul_of_summable_norm hf.summable.norm hg.summable.norm
+  exact (HasSum.mul hf hg hsum).tsum_fiberwise (fun p ↦ p.1 * p.2)
+
+/-- The L-series of the convolution product `f ⍟ g` of two sequences `f` and `g`
+equals the product of their L-series, assuming both L-series converge. -/
+lemma LSeries_convolution' {f g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s)
+    (hg : LSeriesSummable g s) :
+    LSeries (f ⍟ g) s = LSeries f s * LSeries g s :=
+  (LSeriesHasSum.convolution hf.LSeriesHasSum hg.LSeriesHasSum).LSeries_eq
+
+/-- The L-series of the convolution product `f ⍟ g` of two sequences `f` and `g`
+equals the product of their L-series in their common half-plane of absolute convergence. -/
+lemma LSeries_convolution {f g : ℕ → ℂ} {s : ℂ}
+    (hf : abscissaOfAbsConv f < s.re) (hg : abscissaOfAbsConv g < s.re) :
+    LSeries (f ⍟ g) s = LSeries f s * LSeries g s :=
+  LSeries_convolution' (LSeriesSummable_of_abscissaOfAbsConv_lt_re hf)
+    (LSeriesSummable_of_abscissaOfAbsConv_lt_re hg)
+
+/-- The L-series of the convolution product `f ⍟ g` of two sequences `f` and `g`
+is summable when both L-series are summable. -/
+lemma LSeriesSummable.convolution {f g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s)
+    (hg : LSeriesSummable g s) :
+    LSeriesSummable (f ⍟ g) s :=
+  (LSeriesHasSum.convolution hf.LSeriesHasSum hg.LSeriesHasSum).LSeriesSummable
+
+namespace ArithmeticFunction
+
+/-!
+### Versions for arithmetic functions
+-/
+
+/-- The L-series of the (convolution) product of two `ℂ`-valued arithmetic functions `f` and `g`
+equals the product of their L-series, assuming both L-series converge. -/
+lemma LSeriesHasSum_mul {f g : ArithmeticFunction ℂ} {s a b : ℂ} (hf : LSeriesHasSum ↗f s a)
+    (hg : LSeriesHasSum ↗g s b) :
+    LSeriesHasSum ↗(f * g) s (a * b) :=
+  coe_mul f g ▸ hf.convolution hg
+
+/-- The L-series of the (convolution) product of two `ℂ`-valued arithmetic functions `f` and `g`
+equals the product of their L-series, assuming both L-series converge. -/
+lemma LSeries_mul' {f g : ArithmeticFunction ℂ} {s : ℂ} (hf : LSeriesSummable ↗f s)
+    (hg : LSeriesSummable ↗g s) :
+    LSeries ↗(f * g) s = LSeries ↗f s * LSeries ↗g s :=
+  coe_mul f g ▸ LSeries_convolution' hf hg
+
+/-- The L-series of the (convolution) product of two `ℂ`-valued arithmetic functions `f` and `g`
+equals the product of their L-series in their common half-plane of absolute convergence. -/
+lemma LSeries_mul {f g : ArithmeticFunction ℂ} {s : ℂ}
+    (hf : abscissaOfAbsConv ↗f < s.re) (hg : abscissaOfAbsConv ↗g < s.re) :
+    LSeries ↗(f * g) s = LSeries ↗f s * LSeries ↗g s :=
+  coe_mul f g ▸ LSeries_convolution hf hg
+
+/-- The L-series of the (convolution) product of two `ℂ`-valued arithmetic functions `f` and `g`
+is summable when both L-series are summable. -/
+lemma LSeriesSummable_mul {f g : ArithmeticFunction ℂ} {s : ℂ} (hf : LSeriesSummable ↗f s)
+    (hg : LSeriesSummable ↗g s) :
+    LSeriesSummable ↗(f * g) s :=
+  coe_mul f g ▸ hf.convolution hg
+
+end ArithmeticFunction