The Dedekind zeta function across the line Re s = 1

Let K be a number field of degree d = [K : ℚ]. The number of nonzero integral ideals of 𝓞 K of absolute norm at most x is ρ x + O(x ^ (1 - 1 / d)), where ρ = dedekindZeta_residue K: summing the ray class ideal counts over the classes of the trivial modulus recovers the total count, and every class has the same main term.

By partial summation this power saving continues the Dedekind zeta function across the line Re s = 1, with a single simple pole there. Comparing the Dirichlet coefficients of ζ_K with ρ times those of the Riemann zeta function, the difference has partial sums O(n ^ (1 - 1 / d)), so its L-series continues holomorphically to Re s > 1 - 1 / d; and ζ(s) - 1 / (s - 1) is entire (Mathlib's riemannZeta₀). Hence ζ_K(s) - ρ / (s - 1) agrees on Re s > 1 with a function holomorphic on Re s > 1 - 1 / d.

Deleting finitely many Euler factors multiplies ζ_K by the entire function ∏ 𝔭 ∈ S, (1 - N(𝔭) ^ (-s)), so the Dedekind zeta function with the Euler factors at a finite set S of primes deleted has the same kind of continuation, with residue ρ * ∏ 𝔭 ∈ S, (1 - N(𝔭) ^ (-1)) at its simple pole s = 1. This is the L-series of the trivial member of a family of ideal weights with bad primes S, such as the trivial Galois character of a Galois extension, whose bad primes are the ramified ones.

The continuation has no zeros on the line Re s = 1. Off the pole this is the classical 3-4-1 argument: the Euler product gives 1 ≤ ‖ζ_K(σ) ^ 3 ζ_K(σ + it) ^ 4 ζ_K(σ + 2it)‖ for σ > 1, which a zero at 1 + it would contradict as σ → 1⁺. It is the case of the trivial weight of the criterion TauCeti.UnitaryIdealWeight.ne_zero_of_eqOn_LSeries for unitary ideal weights, whose pointwise square is again the trivial weight, so ζ_K itself supplies the continuation of the square's L-series. Consequently (s - 1) ζ_K(s) continues holomorphically to Re s > 1 - 1 / d without zeros on Re s ≥ 1, and -ζ_K'(s) / ζ_K(s) - 1 / (s - 1), the negative logarithmic derivative of ζ_K(s) with its pole removed, extends continuously from Re s > 1 to Re s ≥ 1. This is the boundary behaviour a Tauberian theorem needs to count prime ideals.

Main results

• TauCeti.setOf_one_le_re_subset_setOf_one_sub_one_div_finrank_lt_re: the closed half-plane Re s ≥ 1 lies in the half-plane of continuation.
• TauCeti.isBigO_card_idealsLE_sub: the number of nonzero integral ideals of norm at most x is ρ x + O(x ^ (1 - 1 / [K : ℚ])).
• TauCeti.exists_differentiableOn_eq_dedekindZeta_sub: ζ_K(s) - ρ / (s - 1) extends holomorphically from Re s > 1 to Re s > 1 - 1 / [K : ℚ].
• TauCeti.exists_differentiableOn_eq_LSeries_ofBadPrimes_sub: the same for the Dedekind zeta function with the Euler factors at a finite set of primes deleted, with the correspondingly corrected residue.
• TauCeti.ne_zero_of_eqOn_dedekindZeta: a continuation of ζ_K differentiable at a point s ≠ 1 of the line Re s = 1 does not vanish there.
• TauCeti.exists_continuousOn_eq_neg_deriv_dedekindZeta_div_sub: -ζ_K'(s) / ζ_K(s) - 1 / (s - 1) extends continuously from Re s > 1 to Re s ≥ 1.

References

• S. Lang, Algebraic Number Theory, Chapter VI and Chapter VIII, §3.
• J. Neukirch, Algebraic Number Theory, Chapter VII, §5.
• G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter II.1.
• H. Davenport, Multiplicative Number Theory, Chapter 4, for the 3-4-1 argument.
• The regularization by (s - 1) ζ_K(s) follows Mathlib's DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁ (Mathlib/NumberTheory/LSeries/DirichletContinuation.lean).

theorem TauCeti.setOf_one_le_re_subset_setOf_one_sub_one_div_finrank_lt_re (K : Type u_1) [Field K] [NumberField K] : {s : ℂ | 1 ≤ s.re} ⊆ {s : ℂ | 1 - 1 / ↑(Module.finrank ℚ K) < s.re}

The closed half-plane Re s ≥ 1 lies in the half-plane of the Dedekind zeta continuation.

theorem TauCeti.isBigO_card_idealsLE_sub (K : Type u_1) [Field K] [NumberField K] : (fun (x : ℝ) => ↑(idealsLE K x).card - NumberField.dedekindZeta_residue K * x) =O[Filter.atTop] fun (x : ℝ) => x ^ (1 - (↑(Module.finrank ℚ K))⁻¹)

The ideal count with a power saving. The number of nonzero integral ideals of 𝓞 K of absolute norm at most x is dedekindZeta_residue K * x + O(x ^ (1 - 1 / [K : ℚ])).

theorem TauCeti.exists_differentiableOn_eq_dedekindZeta_sub (K : Type u_1) [Field K] [NumberField K] : ∃ (G : ℂ → ℂ), DifferentiableOn ℂ G {s : ℂ | 1 - 1 / ↑(Module.finrank ℚ K) < s.re} ∧ ∀ (s : ℂ), 1 < s.re → G s = NumberField.dedekindZeta K s - ↑(NumberField.dedekindZeta_residue K) / (s - 1)

The Dedekind zeta function across Re s = 1. There is a function holomorphic on the half-plane Re s > 1 - 1 / [K : ℚ] that agrees with ζ_K(s) - ρ / (s - 1) on Re s > 1, where ρ = dedekindZeta_residue K. So ζ_K continues meromorphically to Re s > 1 - 1 / [K : ℚ], with a single pole, simple with residue ρ, at s = 1.

theorem TauCeti.exists_differentiableOn_eq_LSeries_ofBadPrimes_sub (K : Type u_1) [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : ∃ (G : ℂ → ℂ), DifferentiableOn ℂ G {s : ℂ | 1 - 1 / ↑(Module.finrank ℚ K) < s.re} ∧ ∀ (s : ℂ), 1 < s.re → G s = LSeries (⇑((normCoeff K) (MultiplicativeIdealWeight.ofBadPrimes ↑S ⋯).toIdealArithmeticFunction)) s - (↑(NumberField.dedekindZeta_residue K) * ∏ P ∈ S, (1 - ↑(Ideal.absNorm P.asIdeal) ^ (-1))) / (s - 1)

The Dedekind zeta function with finitely many Euler factors deleted, across Re s = 1. For a finite set S of primes of 𝓞 K, there is a function holomorphic on the half-plane Re s > 1 - 1 / [K : ℚ] that agrees on Re s > 1 with L_S(s) - ρ_S / (s - 1). Here L_S is the L-series of the indicator of the ideals prime to S, that is ζ_K(s) * ∏ 𝔭 ∈ S, (1 - N(𝔭) ^ (-s)), and ρ_S = dedekindZeta_residue K * ∏ 𝔭 ∈ S, (1 - N(𝔭) ^ (-1)) is its residue at s = 1.

theorem TauCeti.ne_zero_of_eqOn_dedekindZeta {K : Type u_1} [Field K] [NumberField K] {f : ℂ → ℂ} {s : ℂ} (hs : s.re = 1) (hs1 : s ≠ 1) (hf : DifferentiableAt ℂ f s) (hfζ : Set.EqOn f (NumberField.dedekindZeta K) {z : ℂ | 1 < z.re}) : f s ≠ 0

The Dedekind zeta function has no zeros on the line Re s = 1 away from its pole. If f agrees with ζ_K on Re s > 1 and is complex differentiable at a point s ≠ 1 with Re s = 1, then f s ≠ 0. By exists_differentiableOn_eq_dedekindZeta_sub, such an f exists: the meromorphic continuation of ζ_K.

theorem TauCeti.exists_continuousOn_eq_neg_deriv_dedekindZeta_div_sub (K : Type u_1) [Field K] [NumberField K] : ∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | 1 ≤ s.re} ∧ ∀ (s : ℂ), 1 < s.re → G s = -deriv (NumberField.dedekindZeta K) s / NumberField.dedekindZeta K s - 1 / (s - 1)

The regularized logarithmic derivative of the Dedekind zeta function. The function -ζ_K'(s) / ζ_K(s) - 1 / (s - 1) extends from Re s > 1 to a function continuous on Re s ≥ 1: the pole of ζ_K at s = 1 is simple, and ζ_K has no zeros on Re s ≥ 1.