Documentation

Mathlib.NumberTheory.LSeries.Convolution

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) :

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

Equations
Instances For
    theorem toArithmeticFunction_congr {R : Type u_1} [Zero R] {f : R} {f' : R} (h : ∀ {n : }, n 0f n = f' n) :
    @[simp]

    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 : R) (g : R) :
    R

    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
      Instances For
        theorem LSeries.convolution_congr {R : Type u_1} [Semiring R] {f : R} {f' : R} {g : R} {g' : R} (hf : ∀ {n : }, n 0f n = f' n) (hg : ∀ {n : }, n 0g n = g' n) :
        theorem ArithmeticFunction.coe_mul {R : Type u_1} [Semiring R] (f : ArithmeticFunction R) (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 : R) (g : R) :
        LSeries.convolution f g = fun (n : ) => pn.divisorsAntidiagonal, f p.1 * g p.2
        @[simp]
        theorem LSeries.convolution_map_zero {R : Type u_1} [Semiring R] (f : R) (g : R) :

        Multiplication of L-series #

        theorem LSeries.term_convolution (f : ) (g : ) (s : ) (n : ) :
        LSeries.term (LSeries.convolution f g) s n = pn.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 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.

        theorem LSeriesHasSum.convolution {f : } {g : } {s : } {a : } {b : } (hf : LSeriesHasSum f s a) (hg : LSeriesHasSum g s 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) :

        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) :

        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) :

        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 : ArithmeticFunction } {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 : ArithmeticFunction } {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 : ArithmeticFunction } {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 : ArithmeticFunction } {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.