Analytic multiplication of ideal Euler factors

Ideal Dirichlet convolution multiplies evaluated Euler factors wherever both local series converge absolutely. The local statement needs convergence only at the specified prime, and includes boundary points of convergence. Absolute convergence over all nonzero ideals then gives an unrestricted product of the convolution's Euler factors, with value the product of the two original Dirichlet series.

The algebraic bridge is Mathlib's algebra homomorphism ArithmeticFunction.ofPowerSeries; evaluation uses ArithmeticFunction.LSeries_mul'. Thus the formal Cauchy-product identity for the local series is transported through the existing arithmetic-function API.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII, for ideal Euler products.
• Mathlib's ArithmeticFunction.ofPowerSeries and ArithmeticFunction.LSeries_mul'.

theorem TauCeti.IdealArithmeticFunction.LSeries_localArithmeticFactor_convolution {K : Type u_1} [Field K] [NumberField K] (f g : IdealArithmeticFunction K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {s : ℂ} (hf : LSeriesSummable (⇑(f.localArithmeticFactor P)) s) (hg : LSeriesSummable (⇑(g.localArithmeticFactor P)) s) : LSeries (⇑((f.convolution g).localArithmeticFactor P)) s = LSeries (⇑(f.localArithmeticFactor P)) s * LSeries (⇑(g.localArithmeticFactor P)) s

Ideal convolution multiplies the evaluated local arithmetic factors wherever both local Dirichlet series converge absolutely, without requiring multiplicativity.

@[simp]

theorem TauCeti.EulerProductData.eulerFactor_convolution {K : Type u_1} [Field K] [NumberField K] (D E : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {s : ℂ} (hD : LSeriesSummable (⇑(D.localArithmeticFactor P)) s) (hE : LSeriesSummable (⇑(E.localArithmeticFactor P)) s) : (D.convolution E).eulerFactor P s = D.eulerFactor P s * E.eulerFactor P s

Convolution multiplies evaluated Euler factors wherever the two local Dirichlet series converge absolutely. No convergence at other primes is required.

theorem TauCeti.EulerProductData.hasProd_eulerFactor_convolution {K : Type u_1} [Field K] [NumberField K] (D E : EulerProductData K) {s : ℂ} (hD : Summable (idealTerm K D.toIdealArithmeticFunction s)) (hE : Summable (idealTerm K E.toIdealArithmeticFunction s)) : HasProd (fun (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => (D.convolution E).eulerFactor P s) (LSeries (⇑((normCoeff K) D.toIdealArithmeticFunction)) s * LSeries (⇑((normCoeff K) E.toIdealArithmeticFunction)) s)

The Euler factors of a convolution have an unrestricted product equal to the product of the original norm-regrouped Dirichlet series, whenever both ideal-indexed series converge absolutely.