The analytic Euler product of an ideal arithmetic function #
TauCeti.EulerProductData.normCoeff_eq_eulerProduct identifies the norm coefficients of bundled
Euler-product data with a formal Euler product, coefficient by coefficient. This file supplies the
analytic statement it does not: where the Dirichlet series indexed by the nonzero ideals converges
absolutely, the infinite product of the local Euler factors converges, in the unrestricted sense
of HasProd over the height-one primes, to the LSeries of the norm coefficients.
The local factor at a height-one prime P is the LSeries of the canonical local arithmetic
factor, equivalently the prime-power Dirichlet series ∑' e, f (P ^ e) / N(P ^ e) ^ s. For a
completely multiplicative weight that series is geometric, and the factor takes the familiar
closed form (1 - χ(P) N(P) ^ (-s))⁻¹; specializing to the trivial weight gives the Euler
product of the Dedekind zeta function.
Main definitions #
TauCeti.EulerProductData.eulerFactor: the local Euler factor at a height-one prime.
Main results #
TauCeti.EulerProductData.hasProd_eulerFactor: the analytic Euler product, when the ideal-indexed Dirichlet series converges absolutely ats.TauCeti.EulerProductData.norm_absNorm_cpow_neg_le_radius_localPowerSeries: a lower bound for the convergence radius of a local power series from absolute convergence at a real point.TauCeti.MultiplicativeIdealWeight.hasProd_eulerFactor: the same product, with the local factors in the closed geometric form available for a completely multiplicative weight.TauCeti.MultiplicativeIdealWeight.LSeries_ne_zero_of_summable_idealTerm: theL-series is nonzero wherever the ideal-indexed series converges absolutely.TauCeti.dedekindZeta_eulerProduct_hasProd: the Euler product of the Dedekind zeta function, valid onRe s > 1.TauCeti.dedekindZeta_ne_zero_of_one_lt_re: the Dedekind zeta function is nonzero onRe s > 1.IsDedekindDomain.HeightOneSpectrum.one_lt_norm_absNorm_cpowandIsDedekindDomain.HeightOneSpectrum.absNorm_cpow_sub_one_ne_zero: analytic bounds for the complex powers of prime-ideal norms on the right half-plane.IsDedekindDomain.HeightOneSpectrum.logDeriv_one_sub_absNorm_cpow_neg: the logarithmic derivative of a deleted Euler factor.
The nonvanishing is pointwise, at each s where the ideal-indexed series converges absolutely, and
nothing is claimed off that region. It is not a formality: an unconditionally convergent product of
nonzero factors may still vanish.
References #
- J. Neukirch, Algebraic Number Theory, Chapter VII.
- Mathlib's
EulerProductAPI, whoseNat.Primes-indexed statements this file mirrors for the height-one primes of a number field.
The absolute norm of a height-one prime, cast to ℂ, is nonzero.
On Re s > 0, N(𝔭) ^ s lies outside the closed unit disc.
The parameter N(𝔭) ^ (-s) strictly decreases in norm as Re s increases.
On Re s > 0, N(𝔭) ^ s - 1 is nonzero.
The logarithmic derivative of a deleted Euler factor 1 - N(𝔭) ^ (-s).
The local Euler factor #
The local Euler factor of D at a height-one prime P, evaluated at s.
Equations
- D.eulerFactor P s = LSeries (⇑(D.localArithmeticFactor P)) s
Instances For
The local Euler factor is the LSeries of the canonical local arithmetic factor.
The local Euler factor is the Dirichlet series over the powers of P.
Restriction to a set of primes, analytically #
The ideal terms of a restriction of f are the ideal terms of f, cut off outside the ideals
supported on the prescribed set of primes.
Restricting to a set of primes never increases an ideal term.
Absolute convergence of the ideal-indexed Dirichlet series is inherited by every restriction to a set of primes.
Absolute convergence of the ideal-indexed Dirichlet series makes every local Euler factor an
absolutely convergent LSeries.
The norm coefficients of the restriction of f to no primes are Mathlib's Kronecker delta.
An ideal term at a power of P is the corresponding coefficient times the matching power of
N(P) ^ (-s).
The prime terms are a subseries of the ideal terms. Each height-one prime contributes its
own ideal as the e = 1 member of its power series, and distinct primes give distinct ideals, so
absolute convergence over ideals restricts to the primes. Multiplicativity plays no part.
Absolute convergence of the ideal-indexed Dirichlet series makes every bundled local Euler
factor an absolutely convergent LSeries.
The abscissa of absolute convergence of a local Euler factor is at most the abscissa of the ideal-indexed series.
Absolute convergence of a local Euler factor at a real point gives a lower bound for the analytic radius of its local power series.
Absolute convergence at σ gives a radius bound for the local power series, and the
prime-norm parameter at s lies strictly inside that radius when σ < Re(s).
Convergence of the finite Euler product. Where the local Euler factors over a finite set
S of primes are absolutely convergent LSeries, so are the norm coefficients of the restriction
of D to S.
The finite Euler product, analytically. Where the local Euler factors over a finite set S
of primes are absolutely convergent LSeries, the LSeries of the norm coefficients of the
restriction of D to S is their finite product over S.
The infinite Euler product #
The analytic Euler product. If the ideal-indexed Dirichlet series of D converges
absolutely at s, then its local Euler factors have an unrestricted
infinite product over the height-one primes, and that product is the LSeries of the norm
coefficients of D.
The hypothesis is absolute convergence of the ideal-indexed series, not of the regrouped one: regrouping can only improve convergence, and the finite partial products of the local factors are sums over ideals, not over norms.
The local Euler factors are multipliable wherever the ideal-indexed Dirichlet series converges absolutely.
The analytic Euler product, as an equality of the unrestricted product with the LSeries.
Completely multiplicative weights #
The ideal terms of a completely multiplicative weight along the powers of a prime form a geometric progression.
The local ratio of a convergent weight is a contraction. Absolute convergence of the ideal-indexed Dirichlet series forces the geometric ratio at each prime to have modulus less than one, because the powers of that prime already contribute a geometric subseries.
The local ratios are summable over the primes. The multiplicative specialisation of
IdealArithmeticFunction.summable_idealTerm_primeIdealPow_one: at a prime the ideal term is the
ratio χ(P) N(P)⁻ˢ.
Absolute convergence puts every local ratio χ(P) N(P)⁻ˢ strictly inside the unit disc, so no
local Euler factor has a vanishing denominator.
The local Euler factor of a completely multiplicative weight is the geometric closed form
(1 - χ(P) N(P)⁻ˢ)⁻¹.
The Euler product of a completely multiplicative ideal weight.
The Euler product does not vanish. Where the ideal-indexed Dirichlet series converges
absolutely, the L-series of the norm coefficients is nonzero.
This is pointwise nonvanishing at such an s and no more: it says nothing where the series does not
converge absolutely, and does not by itself furnish a holomorphic logarithm on a region.
The Dedekind zeta function #
The Euler product of the Dedekind zeta function. For Re s > 1 the Dedekind zeta function
of K is the unrestricted product over the height-one primes of 𝓞 K of the local factors
(1 - N(𝔭) ^ (-s))⁻¹.
This is the ideal-theoretic counterpart of Mathlib's riemannZeta_eulerProduct_hasProd, and it
is not obtained from it: the product is indexed by the primes of 𝓞 K, whose norms repeat and
whose count above a rational prime is the splitting behaviour of K.
The Dedekind zeta function does not vanish on Re s > 1. For every s with 1 < s.re,
NumberField.dedekindZeta K s ≠ 0.
Nothing is claimed on Re s ≤ 1; in particular this says nothing about the line
Re s = 1.