Prime sums of a bounded multiplicative weight

For a completely multiplicative ideal weight w of a number field K, this file names two Dirichlet series over the height-one primes 𝔭 of 𝓞 K:

• the prime sum ∑_𝔭 w(𝔭) N(𝔭)⁻ˢ, TauCeti.MultiplicativeIdealWeight.primeSum;
• the prime-power sum ∑_{𝔭, e} (w(𝔭) N(𝔭)⁻ˢ) ^ (e + 1) / (e + 1), TauCeti.MultiplicativeIdealWeight.primePowSum, which on Re s > 1 is a logarithm of the L-series of w.

For a weight bounded by 1, the two differ by at most 2 [K : ℚ] on real s > 1. If moreover the L-series agrees on Re s > 1 with a function analytic and nonzero at s = 1, the prime-power sum is a primitive of its logarithmic derivative, which is continuous at 1; so both sums stay bounded as s → 1⁺.

Main results

• TauCeti.MultiplicativeIdealWeight.norm_primePowSum_sub_primeSum_le: for real t > 1, the prime-power sum differs from the prime sum by at most 2 [K : ℚ].
• TauCeti.MultiplicativeIdealWeight.hasDerivAt_primePowSum: on Re z > 1 the prime-power sum differentiates to the logarithmic derivative of any function agreeing there with the L-series.
• TauCeti.MultiplicativeIdealWeight.exists_norm_primePowSum_le and TauCeti.MultiplicativeIdealWeight.exists_norm_primeSum_le: if the L-series continues to a function analytic and nonzero at 1, both sums are bounded as t → 1⁺.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII, §13.

noncomputable def TauCeti.MultiplicativeIdealWeight.primeSum {K : Type u_1} [Field K] [NumberField K] (w : MultiplicativeIdealWeight K) (s : ℂ) : ℂ

The prime sum ∑_𝔭 w(𝔭) N(𝔭)⁻ˢ of a multiplicative ideal weight, over the height-one primes of 𝓞 K.

noncomputable def TauCeti.MultiplicativeIdealWeight.primePowSum {K : Type u_1} [Field K] [NumberField K] (w : MultiplicativeIdealWeight K) (s : ℂ) : ℂ

The prime-power sum ∑_{𝔭, e} (w(𝔭) N(𝔭)⁻ˢ) ^ (e + 1) / (e + 1) of a multiplicative ideal weight: the expansion of ∑_𝔭 -log (1 - w(𝔭) N(𝔭)⁻ˢ) over the height-one primes of 𝓞 K and the exponents.

theorem TauCeti.MultiplicativeIdealWeight.primeSum_def {K : Type u_1} [Field K] [NumberField K] (w : MultiplicativeIdealWeight K) (s : ℂ) : w.primeSum s = ∑' (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), w P.asIdeal / ↑(Ideal.absNorm P.asIdeal) ^ s

The defining sum of TauCeti.MultiplicativeIdealWeight.primeSum.

theorem TauCeti.MultiplicativeIdealWeight.primePowSum_def {K : Type u_1} [Field K] [NumberField K] (w : MultiplicativeIdealWeight K) (s : ℂ) : w.primePowSum s = ∑' (pe : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) × ℕ), (w pe.1.asIdeal / ↑(Ideal.absNorm pe.1.asIdeal) ^ s) ^ (pe.2 + 1) / (↑pe.2 + 1)

The defining sum of TauCeti.MultiplicativeIdealWeight.primePowSum.

theorem TauCeti.MultiplicativeIdealWeight.norm_toIdealArithmeticFunction_le_one {K : Type u_1} [Field K] [NumberField K] {w : MultiplicativeIdealWeight K} (hw : ∀ (I : Ideal (NumberField.RingOfIntegers K)), ‖w I‖ ≤ 1) (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : ‖w.toIdealArithmeticFunction I‖ ≤ 1

A weight bounded by 1 gives an ideal arithmetic function bounded by 1.

theorem TauCeti.MultiplicativeIdealWeight.norm_div_absNorm_cpow_le {K : Type u_1} [Field K] [NumberField K] {w : MultiplicativeIdealWeight K} (hw : ∀ (I : Ideal (NumberField.RingOfIntegers K)), ‖w I‖ ≤ 1) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {t : ℝ} (ht : 1 ≤ t) : ‖w P.asIdeal / ↑(Ideal.absNorm P.asIdeal) ^ ↑t‖ ≤ (↑(Ideal.absNorm P.asIdeal))⁻¹

For a weight bounded by 1 and real t ≥ 1, the local ratio w(𝔭) N(𝔭)⁻ᵗ has norm at most N(𝔭)⁻¹.

theorem TauCeti.MultiplicativeIdealWeight.norm_primePowSum_sub_primeSum_le {K : Type u_1} [Field K] [NumberField K] {w : MultiplicativeIdealWeight K} (hw : ∀ (I : Ideal (NumberField.RingOfIntegers K)), ‖w I‖ ≤ 1) {t : ℝ} (ht : 1 < t) : ‖w.primePowSum ↑t - w.primeSum ↑t‖ ≤ 2 * ↑(Module.finrank ℚ K)

The prime-power tail is bounded. For a weight bounded by 1 and real t > 1, the prime-power sum differs from the prime sum by at most 2 [K : ℚ].

theorem TauCeti.MultiplicativeIdealWeight.hasDerivAt_primePowSum {K : Type u_1} [Field K] [NumberField K] {w : MultiplicativeIdealWeight K} (hw : ∀ (I : Ideal (NumberField.RingOfIntegers K)), ‖w I‖ ≤ 1) {C : ℂ → ℂ} (hCL : ∀ (z : ℂ), 1 < z.re → C z = LSeries (⇑((normCoeff K) w.toIdealArithmeticFunction)) z) {z : ℂ} (hz : 1 < z.re) : HasDerivAt w.primePowSum (logDeriv C z) z

The prime-power sum is a logarithm of the L-series. For a weight bounded by 1, on Re z > 1 the prime-power sum differentiates to the logarithmic derivative of any function C agreeing there with the L-series of w.

theorem TauCeti.MultiplicativeIdealWeight.exists_norm_primePowSum_le {K : Type u_1} [Field K] [NumberField K] {w : MultiplicativeIdealWeight K} (hw : ∀ (I : Ideal (NumberField.RingOfIntegers K)), ‖w I‖ ≤ 1) {C : ℂ → ℂ} (hC : AnalyticAt ℂ C 1) (hC1 : C 1 ≠ 0) (hCL : ∀ (z : ℂ), 1 < z.re → C z = LSeries (⇑((normCoeff K) w.toIdealArithmeticFunction)) z) : ∃ (B : ℝ), ∀ᶠ (t : ℝ) in nhdsWithin 1 (Set.Ioi 1), ‖w.primePowSum ↑t‖ ≤ B

A logarithm of a continued L-series stays bounded. If the L-series of a weight bounded by 1 agrees on Re s > 1 with a function analytic and nonzero at s = 1, then its prime-power sum is bounded as t → 1⁺.

theorem TauCeti.MultiplicativeIdealWeight.exists_norm_primeSum_le {K : Type u_1} [Field K] [NumberField K] {w : MultiplicativeIdealWeight K} (hw : ∀ (I : Ideal (NumberField.RingOfIntegers K)), ‖w I‖ ≤ 1) {C : ℂ → ℂ} (hC : AnalyticAt ℂ C 1) (hC1 : C 1 ≠ 0) (hCL : ∀ (z : ℂ), 1 < z.re → C z = LSeries (⇑((normCoeff K) w.toIdealArithmeticFunction)) z) : ∃ (B : ℝ), ∀ᶠ (t : ℝ) in nhdsWithin 1 (Set.Ioi 1), ‖w.primeSum ↑t‖ ≤ B

The prime sum of a continued L-series stays bounded. If the L-series of a weight bounded by 1 agrees on Re s > 1 with a function analytic and nonzero at s = 1, then its prime sum is bounded as t → 1⁺.