Convolution of ideal Euler-product data

Ideal Dirichlet convolution multiplies the local power series, in contrast to pointwise multiplication of ideal coefficients. This file lifts convolution to Euler-product data and identifies its local series with products in PowerSeries ℂ. Together with the existing TauCeti.normCoeff_convolution, this also identifies the regrouped coefficients with products in Mathlib's Dirichlet-convolution ring ArithmeticFunction ℂ. The local arithmetic factors also multiply in that ring, giving the algebraic input for multiplication of evaluated factors.

References

• G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter I.2.
• Mathlib's PowerSeries.coeff_mul and dvd_prime_pow.
• Mathlib's algebra homomorphism ArithmeticFunction.ofPowerSeries.

theorem TauCeti.IdealArithmeticFunction.convolution_primeIdealPow {K : Type u_1} [Field K] [NumberField K] (f g : IdealArithmeticFunction K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (n : ℕ) : f.convolution g (P.primeIdealPow n) = ∑ e ∈ Finset.antidiagonal n, f (P.primeIdealPow e.1) * g (P.primeIdealPow e.2)

At a prime power, ideal convolution is the Cauchy product of the prime-power values.

theorem TauCeti.IdealArithmeticFunction.localPowerSeries_convolution {K : Type u_1} [Field K] [NumberField K] (f g : IdealArithmeticFunction K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (f.convolution g).localPowerSeries P = f.localPowerSeries P * g.localPowerSeries P

The local prime-power series of a convolution is the product of the local series.

@[simp]

theorem TauCeti.IdealArithmeticFunction.localArithmeticFactor_convolution {K : Type u_1} [Field K] [NumberField K] (f g : IdealArithmeticFunction K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (f.convolution g).localArithmeticFactor P = f.localArithmeticFactor P * g.localArithmeticFactor P

Ideal convolution multiplies the local arithmetic factors in Mathlib's Dirichlet-convolution ring.

noncomputable def TauCeti.EulerProductData.delta {K : Type u_1} [Field K] [NumberField K] : EulerProductData K

The ideal delta function, bundled as the identity for Euler-product convolution.

@[simp]

theorem TauCeti.EulerProductData.toIdealArithmeticFunction_delta {K : Type u_1} [Field K] [NumberField K] : delta.toIdealArithmeticFunction = IdealArithmeticFunction.delta

The underlying function of the bundled convolution identity is the ideal delta function.

noncomputable def TauCeti.EulerProductData.convolution {K : Type u_1} [Field K] [NumberField K] (D E : EulerProductData K) : EulerProductData K

Convolve two ideal coefficient systems. This operation multiplies local series and is distinct from the pointwise multiplication instance on EulerProductData.

@[simp]

theorem TauCeti.EulerProductData.toIdealArithmeticFunction_convolution {K : Type u_1} [Field K] [NumberField K] (D E : EulerProductData K) : (D.convolution E).toIdealArithmeticFunction = D.toIdealArithmeticFunction.convolution E.toIdealArithmeticFunction

The underlying coefficient function of bundled convolution is ideal convolution.

@[simp]

theorem TauCeti.EulerProductData.delta_convolution {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) : delta.convolution D = D

The ideal delta function is a left identity for bundled convolution.

@[simp]

theorem TauCeti.EulerProductData.convolution_delta {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) : D.convolution delta = D

The ideal delta function is a right identity for bundled convolution.

theorem TauCeti.EulerProductData.convolution_comm {K : Type u_1} [Field K] [NumberField K] (D E : EulerProductData K) : D.convolution E = E.convolution D

Bundled ideal convolution is commutative.

theorem TauCeti.EulerProductData.convolution_assoc {K : Type u_1} [Field K] [NumberField K] (D E F : EulerProductData K) : (D.convolution E).convolution F = D.convolution (E.convolution F)

Bundled ideal convolution is associative.

@[simp]

theorem TauCeti.EulerProductData.localPowerSeries_convolution {K : Type u_1} [Field K] [NumberField K] (D E : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (D.convolution E).localPowerSeries P = D.localPowerSeries P * E.localPowerSeries P

Convolution multiplies the local power series of bundled Euler-product data.

@[simp]

theorem TauCeti.EulerProductData.localArithmeticFactor_convolution {K : Type u_1} [Field K] [NumberField K] (D E : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (D.convolution E).localArithmeticFactor P = D.localArithmeticFactor P * E.localArithmeticFactor P

Bundled convolution multiplies the local arithmetic factors in Mathlib's Dirichlet-convolution ring.