Derivatives of ideal-indexed Dirichlet series #
Differentiating an ideal term idealTerm K f s I = f I / N(I) ^ s in s returns the same term
weighted by -log N(I). Summing over the nonzero integral ideals, the derivative of the
norm-regrouped L-series is therefore, up to a sign, the ideal-indexed Dirichlet series of the
logarithmic weighting TauCeti.IdealArithmeticFunction.logMul of f, the pointwise product of
f with log N(I).
This file proves that identity, its iterated form, and the resulting expression of the logarithmic
derivative as a quotient of two ideal-indexed sums. The norm-regrouped derivative, its iterated
form, and the logarithmic-derivative result assume that s lies strictly to the right of
TauCeti.idealAbscissaOfAbsConv K f, the abscissa of absolute convergence of the ideal-indexed
series; the logarithmic weight can destroy summability on the boundary line itself, which is why
a point of convergence strictly to the left is what the estimates consume.
Two facts do the work. Regrouping by absolute norm turns logMul into Mathlib's LSeries.logMul,
because the weight log N(I) is constant on a norm fibre
(TauCeti.normCoeff_logMul); and a logarithmic weight leaves the ideal-indexed series summable
strictly to the right of any point of absolute convergence
(TauCeti.summable_log_absNorm_mul_norm_idealTerm_of_re_lt_re). Mathlib's LSeries_hasDerivAt
then supplies the calculus, and TauCeti.regroupByNorm converts its conclusion back to a sum over
ideals.
Main definitions #
TauCeti.IdealArithmeticFunction.logMul: the pointwise product of an ideal arithmetic function withlog N(I), the ideal-indexed counterpart of Mathlib'sLSeries.logMul. Itsm-fold iterate weights bylog N(I) ^ m(TauCeti.IdealArithmeticFunction.logMul_iterate_apply).
Main results #
TauCeti.hasDerivAt_idealTerm: the derivative insof an ideal term is the term itself, weighted by-log N(I).TauCeti.normCoeff_logMul: regrouping by absolute norm carries the ideal-indexed logarithmic weight to Mathlib's.TauCeti.summable_idealTerm_logMul_of_re_lt_re: a logarithmic weight preserves absolute convergence strictly to the right.TauCeti.IdealArithmeticFunction.hasDerivAt_LSeries_normCoeffandTauCeti.IdealArithmeticFunction.deriv_LSeries_normCoeff: the derivative of the regroupedL-series is-∑ I, log N(I) f I N(I) ^ (-s), summed over the nonzero integral ideals.TauCeti.IdealArithmeticFunction.iteratedDeriv_LSeries_normCoeff: them-th derivative, with the weightlog N(I) ^ m.TauCeti.IdealArithmeticFunction.logDeriv_LSeries_normCoeff: the logarithmic derivative as the quotient of the two ideal-indexed sums.TauCeti.IdealArithmeticFunction.differentiableOn_LSeries_normCoeff: absolute convergence of an ideal-indexed series throughout an open set makes its norm-regroupedL-series holomorphic there.
References #
- G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter II.
The derivative of an ideal term. Differentiating f I / N(I) ^ s in s returns the same
term weighted by -log N(I).
Differentiating a sum of ideal terms termwise needs this at each term. The logarithm is the
complex one, of a positive real argument: N(I) ≥ 1 for a nonzero ideal, so it agrees with
Real.log N(I) and is real and nonnegative.
The logarithmic weighting #
The logarithmic weighting of an ideal arithmetic function: the pointwise product of f
with log N(I).
It is the ideal-indexed counterpart of Mathlib's LSeries.logMul, and it is the coefficient
system that appears, up to a sign, when the ideal-indexed Dirichlet series of f is
differentiated in s.
Equations
- f.logMul I = Complex.log ↑(Ideal.absNorm ↑I) * f I
Instances For
Evaluation of the logarithmic weighting.
Evaluation of an iterated logarithmic weighting: the weight is the m-th power of
log N(I).
The ideal term of a logarithmic weighting is the original term weighted by log N(I).
The absolute value of a logarithmically weighted ideal term: the weight log N(I) is a
nonnegative real number, so it passes through the norm unchanged.
Regrouping by absolute norm carries the logarithmic weight to Mathlib's. The weight
log N(I) depends on the ideal only through its absolute norm, so it is constant on a norm fibre
and factors out of the regrouping.
Iterating the previous identity: the m-fold logarithmic weight is carried to Mathlib's.
A logarithmic weight preserves absolute convergence strictly to the right. The strict
inequality is essential: log N(I) grows, so the weighted series can diverge on the very line
where the unweighted one converges.
Iterating a logarithmic weight still preserves absolute convergence strictly to the right:
each of the m weights is absorbed on a shorter interval of real parts.
Differentiating the regrouped L-series #
Termwise differentiation of an ideal-indexed Dirichlet series. Strictly to the right of
the ideal-indexed abscissa of absolute convergence, the norm-regrouped L-series of f is
differentiable and its derivative is the ideal-indexed series of -f.logMul, that is
-∑ I, log N(I) f I N(I) ^ (-s).
The derivative of a norm-regrouped ideal Dirichlet series. The value form of
TauCeti.IdealArithmeticFunction.hasDerivAt_LSeries_normCoeff.
The higher derivatives of a norm-regrouped ideal Dirichlet series. The m-th derivative
carries the weight log N(I) ^ m and the sign (-1) ^ m.
The logarithmic derivative of a norm-regrouped ideal Dirichlet series. Strictly to the right of the ideal-indexed abscissa of absolute convergence it is the quotient of the logarithmically weighted ideal-indexed sum by the unweighted one.
No nonvanishing hypothesis is needed: both sides are the same quotient, and
TauCeti.LSeries_normCoeff identifies the denominator with the value of the L-series.
Holomorphy after regrouping an ideal-indexed series by norm. If the ideal-indexed series
of f converges absolutely at every point of an open set U, then the L-series of its norm
coefficients is holomorphic on U.
At each point, openness supplies a nearby point strictly to its left which remains in U.
Absolute convergence there puts the original point strictly right of the abscissa of absolute
convergence, where Mathlib's LSeries is differentiable.