Documentation

TauCeti.NumberTheory.ArithmeticDirichletSeries.EulerProduct.Logarithm.VonMangoldtCoeff

The logarithmic derivative as a von Mangoldt Dirichlet series #

Strictly to the right of the abscissa of absolute convergence,

logDeriv L(s) = -โˆ‘' A, ฯ‡(A) ฮ›(A) / N(A) ^ s,

the sum running over the nonzero integral ideals of ๐“ž K, with ฮ› the ideal von Mangoldt function. This is the coefficient identity: it names the exact Dirichlet coefficients of the logarithmic derivative, which is what a Tauberian argument consumes.

The prime-power expansion of logDeriv_LSeries_eq_tsum_prime_pow is the same sum written over (๐”ญ, k). The two agree termwise, because the von Mangoldt transform of a completely multiplicative weight at ๐”ญ ^ (k+1) is ฯ‡(๐”ญ) ^ (k+1) log N(๐”ญ) and N(๐”ญ ^ (k+1)) = N(๐”ญ) ^ (k+1); the transform vanishes off the prime powers, so nothing else contributes.

For general Euler-product data D, whose values at higher prime powers are independent, the coefficient at ๐”ญ ^ e is log N(๐”ญ) times the degree-e coefficient of the local series X F_๐”ญ'/F_๐”ญ. This defines the von Mangoldt function ฮ›_D of D, which is the von Mangoldt transform of the weight in the completely multiplicative case. Where the local power series are zero-free on the disks of absolute convergence, -logDeriv L(s) = โˆ‘' A, ฮ›_D(A) / N(A) ^ s, with absolute convergence.

Main definitions #

Main results #

Implementation notes #

Summability is comparison against TauCeti.summable_log_absNorm_mul_norm_idealTerm_of_re_lt_re, whose weight log N(I) dominates โ€–ฮ›(I)โ€– by norm_vonMangoldt_le_log. Passing from the (๐”ญ, k)-indexed sum to the ideal-indexed one is TauCeti.tsum_eq_tsum_idealPrimePower_of_support_subset.

For general D, PowerSeries.tsum_norm_coeff_logDeriv_mul_pow_succ_le supplies the local majorant that gives absolute convergence of the von Mangoldt series. The general coefficient identity applies to data with an absolute-convergence point ฯƒ and zero-free local series on the corresponding disks.

References #

source
theorem TauCeti.IdealArithmeticFunction.summable_idealTerm_vonMangoldtTransform {K : Type u_1} [Field K] [NumberField K] {f : IdealArithmeticFunction K} {s : โ„‚} (hs : idealAbscissaOfAbsConv K f < โ†‘s.re) :
Summable (idealTerm K f.vonMangoldtTransform s)

The von Mangoldt weighted ideal terms converge absolutely. Strictly to the right of the abscissa of absolute convergence of ฯ‡, the terms ฯ‡(A) ฮ›(A) / N(A) ^ s are summable.

ฮ›(A) is bounded by log N(A), and weighting the ideal terms by log N(A) preserves summability strictly to the right of a point of absolute convergence.

source
theorem TauCeti.MultiplicativeIdealWeight.logDeriv_LSeries_eq_neg_tsum_vonMangoldtTransform {K : Type u_1} [Field K] [NumberField K] (ฯ‡ : MultiplicativeIdealWeight K) {s : โ„‚} (hs : idealAbscissaOfAbsConv K ฯ‡.toIdealArithmeticFunction < โ†‘s.re) :
logDeriv (LSeries โ‡‘((normCoeff K) ฯ‡.toIdealArithmeticFunction)) s = -โˆ‘' (A : โ†ฅ(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), idealTerm K ฯ‡.toIdealArithmeticFunction.vonMangoldtTransform s A

The coefficient identity for the logarithmic derivative. Strictly to the right of the abscissa of absolute convergence,

logDeriv L(s) = -โˆ‘' A, ฯ‡(A) ฮ›(A) / N(A) ^ s.

The minus sign is the usual one: the Dirichlet coefficients of -L'/L are the von Mangoldt transform of the weight, nonnegative when the weight is trivial.

source
noncomputable def TauCeti.EulerProductData.vonMangoldt {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) :
IdealArithmeticFunction K

The von Mangoldt function ฮ›_D of Euler-product data. At a prime power P ^ e with e โ‰ฅ 1 it is log N(P) times the degree-e coefficient of the local logarithmic-derivative series X F_P'/F_P, and it vanishes off the prime powers. These are the Dirichlet coefficients of -L'/L (TauCeti.EulerProductData.hasSum_idealTerm_vonMangoldt_of_zeroFree); for a completely multiplicative weight they are the von Mangoldt transform of the weight.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.EulerProductData.vonMangoldt_eq_zero_of_not_isPrimePow {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) {A : โ†ฅ(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hA : ยฌIsPrimePow โ†‘A) :
    D.vonMangoldt A = 0

    ฮ›_D vanishes off the prime-power ideals.

    source
    @[simp]
    theorem TauCeti.EulerProductData.vonMangoldt_primeIdealPow {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (e : โ„•) :
    D.vonMangoldt (P.primeIdealPow e) = โ†‘(Real.log โ†‘(Ideal.absNorm P.asIdeal)) * (PowerSeries.coeff e) (D.localLogDerivSeries P)

    The value of ฮ›_D at P ^ e is log N(P) times the degree-e local logarithmic-derivative coefficient. For e = 0 both sides vanish.

    source
    @[simp]
    theorem TauCeti.EulerProductData.vonMangoldt_ofMultiplicativeIdealWeight {K : Type u_1} [Field K] [NumberField K] (ฯ‡ : MultiplicativeIdealWeight K) :
    (ofMultiplicativeIdealWeight ฯ‡).vonMangoldt = ฯ‡.toIdealArithmeticFunction.vonMangoldtTransform

    For completely multiplicative data, ฮ›_D is the von Mangoldt transform A โ†ฆ ฯ‡(A) ฮ›(A) of the weight.

    source
    theorem TauCeti.EulerProductData.summable_idealTerm_vonMangoldt_of_zeroFree {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) {ฯƒ : โ„} {s : โ„‚} (hฯƒ : idealAbscissaOfAbsConv K D.toIdealArithmeticFunction < โ†‘ฯƒ) (hne : โˆ€ (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (z : โ„‚), โ€–zโ€– < โ€–โ†‘(Ideal.absNorm P.asIdeal) ^ (-โ†‘ฯƒ)โ€– โ†’ FormalMultilinearSeries.ofScalarsSum (fun (n : โ„•) => (PowerSeries.coeff n) (D.localPowerSeries P)) z โ‰  0) (hs : ฯƒ < s.re) :
    Summable (idealTerm K D.vonMangoldt s)

    Absolute convergence of the von Mangoldt series of an Euler product. Suppose ฯƒ lies strictly to the right of the ideal-indexed abscissa of absolute convergence of D and every local power series is zero-free on the disk of radius N(P)โปฯƒ. Then the ideal-indexed series of ฮ›_D converges absolutely at every s with ฯƒ < Re(s).

    source
    theorem TauCeti.EulerProductData.hasSum_idealTerm_vonMangoldt_of_zeroFree {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) {ฯƒ : โ„} {s : โ„‚} (hฯƒ : idealAbscissaOfAbsConv K D.toIdealArithmeticFunction < โ†‘ฯƒ) (hne : โˆ€ (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (z : โ„‚), โ€–zโ€– < โ€–โ†‘(Ideal.absNorm P.asIdeal) ^ (-โ†‘ฯƒ)โ€– โ†’ FormalMultilinearSeries.ofScalarsSum (fun (n : โ„•) => (PowerSeries.coeff n) (D.localPowerSeries P)) z โ‰  0) (hs : ฯƒ < s.re) :
    HasSum (idealTerm K D.vonMangoldt s) (-logDeriv (LSeries โ‡‘((normCoeff K) D.toIdealArithmeticFunction)) s)

    The logarithmic derivative of an Euler product as a von Mangoldt series. Suppose ฯƒ lies strictly to the right of the ideal-indexed abscissa of absolute convergence of D and every local power series is zero-free on the disk of radius N(P)โปฯƒ. Then for ฯƒ < Re(s) the ideal-indexed series of ฮ›_D converges absolutely to -L'(s)/L(s), where L is the LSeries of the norm coefficients of D:

    -logDeriv L(s) = โˆ‘' A, ฮ›_D(A) / N(A) ^ s.

    source
    theorem TauCeti.EulerProductData.LSeriesHasSum_normCoeff_vonMangoldt_of_zeroFree {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) {ฯƒ : โ„} {s : โ„‚} (hฯƒ : idealAbscissaOfAbsConv K D.toIdealArithmeticFunction < โ†‘ฯƒ) (hne : โˆ€ (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (z : โ„‚), โ€–zโ€– < โ€–โ†‘(Ideal.absNorm P.asIdeal) ^ (-โ†‘ฯƒ)โ€– โ†’ FormalMultilinearSeries.ofScalarsSum (fun (n : โ„•) => (PowerSeries.coeff n) (D.localPowerSeries P)) z โ‰  0) (hs : ฯƒ < s.re) :
    LSeriesHasSum (โ‡‘((normCoeff K) D.vonMangoldt)) s (-logDeriv (LSeries โ‡‘((normCoeff K) D.toIdealArithmeticFunction)) s)

    The norm-regrouped form of TauCeti.EulerProductData.hasSum_idealTerm_vonMangoldt_of_zeroFree: the Mathlib LSeries of the norm coefficients of ฮ›_D converges absolutely to -L'(s)/L(s).

    source
    theorem TauCeti.EulerProductData.logDeriv_LSeries_eq_neg_LSeries_normCoeff_vonMangoldt_of_zeroFree {K : Type u_1} [Field K] [NumberField K] (D : EulerProductData K) {ฯƒ : โ„} {s : โ„‚} (hฯƒ : idealAbscissaOfAbsConv K D.toIdealArithmeticFunction < โ†‘ฯƒ) (hne : โˆ€ (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (z : โ„‚), โ€–zโ€– < โ€–โ†‘(Ideal.absNorm P.asIdeal) ^ (-โ†‘ฯƒ)โ€– โ†’ FormalMultilinearSeries.ofScalarsSum (fun (n : โ„•) => (PowerSeries.coeff n) (D.localPowerSeries P)) z โ‰  0) (hs : ฯƒ < s.re) :
    logDeriv (LSeries โ‡‘((normCoeff K) D.toIdealArithmeticFunction)) s = -LSeries (โ‡‘((normCoeff K) D.vonMangoldt)) s

    The coefficient identity for the logarithmic derivative of an Euler product. Under the hypotheses of TauCeti.EulerProductData.hasSum_idealTerm_vonMangoldt_of_zeroFree,

    logDeriv L(s) = -LSeries (normCoeff ฮ›_D) s.