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 #
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' := ⋯ }
Instances For
If we consider an arithmetic function just as a function and turn it back into an arithmetic function, it is the same as before.
Dirichlet convolution of two sequences.
We define this in terms of the already existing definition for arithmetic functions.
Equations
Instances For
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))
Instances For
The product of two arithmetic functions defines the same function as the Dirichlet convolution of the functions defined by them.
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
.
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
.
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.
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.
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.
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 #
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.
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.
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.
The L-series of the (convolution) product of two ℂ
-valued arithmetic functions f
and g
is summable when both L-series are summable.