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'.

Dirichlet convolution of two functions

def toArithmeticFunction {R : Type u_1} [Zero R] (f : ℕ → R) : ArithmeticFunction R

We turn any function ℕ → R into an ArithmeticFunction R by setting its value at 0 to be zero.

Equations

• toArithmeticFunction f = { toFun := fun (n : ℕ) => if n = 0 then 0 else f n, map_zero' := ⋯ }

theorem toArithmeticFunction_congr {R : Type u_1} [Zero R] {f f' : ℕ → R} (h : ∀ {n : ℕ}, n ≠ 0 → f n = f' n) : toArithmeticFunction f = toArithmeticFunction f'

@[simp]

theorem ArithmeticFunction.toArithmeticFunction_eq_self {R : Type u_1} [Zero R] (f : ArithmeticFunction R) : toArithmeticFunction ⇑f = f

If we consider an arithmetic function just as a function and turn it back into an arithmetic function, it is the same as before.

noncomputable def LSeries.convolution {R : Type u_1} [Semiring R] (f g : ℕ → R) : ℕ → R

Dirichlet convolution of two sequences.

We define this in terms of the already existing definition for arithmetic functions.

Equations

• LSeries.convolution f g = ⇑(toArithmeticFunction f * toArithmeticFunction g)

def LSeries.notation.«term_⍟_» : Lean.TrailingParserDescr

Dirichlet convolution of two sequences.

We define this in terms of the already existing definition for arithmetic functions.

Equations

• LSeries.notation.«term_⍟_» = Lean.ParserDescr.trailingNode `LSeries.notation.«term_⍟_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⍟ ") (Lean.ParserDescr.cat `term 71))

theorem LSeries.convolution_congr {R : Type u_1} [Semiring R] {f f' g g' : ℕ → R} (hf : ∀ {n : ℕ}, n ≠ 0 → f n = f' n) (hg : ∀ {n : ℕ}, n ≠ 0 → g n = g' n) : LSeries.convolution f g = LSeries.convolution f' g'

theorem ArithmeticFunction.coe_mul {R : Type u_1} [Semiring R] (f g : ArithmeticFunction R) : LSeries.convolution ⇑f ⇑g = ⇑(f * g)

The product of two arithmetic functions defines the same function as the Dirichlet convolution of the functions defined by them.

theorem LSeries.convolution_def {R : Type u_1} [Semiring R] (f g : ℕ → R) : LSeries.convolution f g = fun (n : ℕ) => ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2

@[simp]

theorem LSeries.convolution_map_zero {R : Type u_1} [Semiring R] (f g : ℕ → R) : LSeries.convolution f g 0 = 0

Multiplication of L-series

theorem LSeries.term_convolution (f g : ℕ → ℂ) (s : ℂ) (n : ℕ) : LSeries.term (LSeries.convolution f g) s n = ∑ p ∈ n.divisorsAntidiagonal, LSeries.term f s p.1 * LSeries.term g s p.2

We give an expression of the LSeries.term of the convolution of two functions in terms of a sum over Nat.divisorsAntidiagonal.

theorem LSeries.term_convolution' (f g : ℕ → ℂ) (s : ℂ) : LSeries.term (LSeries.convolution f g) s = fun (n : ℕ) => ∑' (b : ↑((fun (p : ℕ × ℕ) => p.1 * p.2) ⁻¹' {n})), LSeries.term f s (↑b).1 * LSeries.term g s (↑b).2

We give an expression of the LSeries.term of the convolution of two functions in terms of an a priori infinite 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.

theorem LSeriesHasSum.convolution {f g : ℕ → ℂ} {s a b : ℂ} (hf : LSeriesHasSum f s a) (hg : LSeriesHasSum g s b) : LSeriesHasSum (LSeries.convolution f g) s (a * b)

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.

theorem LSeries_convolution' {f g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s) (hg : LSeriesSummable g s) : LSeries (LSeries.convolution f g) s = LSeries f s * LSeries g s

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.

theorem LSeries_convolution {f g : ℕ → ℂ} {s : ℂ} (hf : LSeries.abscissaOfAbsConv f < ↑s.re) (hg : LSeries.abscissaOfAbsConv g < ↑s.re) : LSeries (LSeries.convolution f g) s = LSeries f s * LSeries g s

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.

theorem LSeriesSummable.convolution {f g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s) (hg : LSeriesSummable g s) : LSeriesSummable (LSeries.convolution f g) s

The L-series of the convolution product f ⍟ g of two sequences f and g is summable when both L-series are summable.

Versions for arithmetic functions

theorem ArithmeticFunction.LSeriesHasSum_mul {f g : ArithmeticFunction ℂ} {s a b : ℂ} (hf : LSeriesHasSum (fun (n : ℕ) => f n) s a) (hg : LSeriesHasSum (fun (n : ℕ) => g n) s b) : LSeriesHasSum (fun (n : ℕ) => (f * g) n) s (a * b)

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.

theorem ArithmeticFunction.LSeries_mul' {f g : ArithmeticFunction ℂ} {s : ℂ} (hf : LSeriesSummable (fun (n : ℕ) => f n) s) (hg : LSeriesSummable (fun (n : ℕ) => g n) s) : LSeries (fun (n : ℕ) => (f * g) n) s = LSeries (fun (n : ℕ) => f n) s * LSeries (fun (n : ℕ) => g n) s

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.

theorem ArithmeticFunction.LSeries_mul {f g : ArithmeticFunction ℂ} {s : ℂ} (hf : (LSeries.abscissaOfAbsConv fun (n : ℕ) => f n) < ↑s.re) (hg : (LSeries.abscissaOfAbsConv fun (n : ℕ) => g n) < ↑s.re) : LSeries (fun (n : ℕ) => (f * g) n) s = LSeries (fun (n : ℕ) => f n) s * LSeries (fun (n : ℕ) => g n) s

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.

theorem ArithmeticFunction.LSeriesSummable_mul {f g : ArithmeticFunction ℂ} {s : ℂ} (hf : LSeriesSummable (fun (n : ℕ) => f n) s) (hg : LSeriesSummable (fun (n : ℕ) => g n) s) : LSeriesSummable (fun (n : ℕ) => (f * g) n) s

The L-series of the (convolution) product of two ℂ-valued arithmetic functions f and g is summable when both L-series are summable.