Dedekind zeta function and polar density

TheoremSummability of Dedekind zeta terms for σ > 1#✓fully proved

For σ > 1, the Dedekind zeta terms (N v) ^ (-σ) are summable over the height-one primes of the ring of integers.

theorem summable_heightOneSpectrum_absNorm_rpow_neg_of_one_lt
    (F : Type*) [Field F] [NumberField F] {σ : ℝ} (hσ : 1 < σ) :
    Summable fun v : HeightOneSpectrum (𝓞 F) => ((Ideal.absNorm v.asIdeal : ℕ) : ℝ) ^ (-σ)

DefinitionPartial Dedekind zeta function#✓fully proved

Let \(K\) be a number field and \(S\) a set of nonzero prime ideals of its ring of integers \(\mathcal{O}_K\). For such a prime \(\mathfrak{p}\) let \(N(\mathfrak{p}) = |\mathcal{O}_K / \mathfrak{p}|\) be its absolute norm. The partial Dedekind zeta function of \(S\) is the function \(\zeta_{K,S} : \mathbb{C} \to \mathbb{C}\) given by the Euler product

\[\zeta_{K,S}(s) = \prod_{\mathfrak{p} \in S} \left(1 - N(\mathfrak{p})^{-s}\right)^{-1}.\]

Here a factor with \(N(\mathfrak{p})^{-s} = 1\) is taken to be \(0\), and the product is an unconditional infinite product, defined without any convergence hypothesis: where it does not converge unconditionally its value is \(1\), so analytic results must state the required region of convergence explicitly.

noncomputable def partialDedekindZeta
    (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) : ℂ → ℂ :=
  fun s ↦ ∏' (𝔭 : S), (1 - (Ideal.absNorm 𝔭.1.asIdeal : ℂ) ^ (-s))⁻¹

Used by 3

Used byPolar density · The empty set has polar density zero · Uniqueness of the polar density

DefinitionPolar density#✓fully proved

Let \(K\) be a number field, let \(S\) be a set of height-one primes of the ring of integers of \(K\), and let \(\zeta_S\) be the partial Dedekind zeta function of \(S\). A rational number \(\rho\) is a polar density of \(S\) when there exist a positive integer \(n\), an integer \(m\) and a function \(F : \mathbb{C} \to \mathbb{C}\) such that \(F\) is meromorphic at \(1\), \(F(s) = \zeta_S(s)^n\) for all \(s\) with \(\operatorname{Re} s > 1\) in some neighbourhood of \(1\), the meromorphic order of \(F\) at \(1\) equals \(-m\), and \(\rho = m / n\).

Meromorphy is required of the continuation \(F\), not of the Euler product defining \(\zeta_S\).

def HasPolarDensity (S : Set (HeightOneSpectrum (𝓞 K))) (ρ : ℚ) : Prop :=
  ∃ (n : ℕ+) (m : ℤ) (F : ℂ → ℂ),
    MeromorphicAt F (1 : ℂ) ∧
      F =ᶠ[nhdsWithin (1 : ℂ) {z : ℂ | (1 : ℝ) < z.re}]
        (fun s => NumberField.partialDedekindZeta K S s ^ (n : ℕ)) ∧
      meromorphicOrderAt F (1 : ℂ) = (↑(-m) : WithTop ℤ) ∧
      ρ = (m : ℚ) / (n : ℚ)

Uses 1 · Used by 2

Statement usesPartial Dedekind zeta function

Used byThe empty set has polar density zero · Uniqueness of the polar density

TheoremUniqueness of the polar density#✓fully proved

Let \(K\) be a number field and let \(S\) be a set of height-one primes of the ring of integers of \(K\). If \(\rho_1\) and \(\rho_2\) are both polar densities of \(S\), then \(\rho_1 = \rho_2\).

The point \(1\) lies in the closure of the half-plane \(\operatorname{Re} s > 1\), so two meromorphic functions that agree on that half-plane near \(1\) agree on a punctured neighbourhood of \(1\) and have the same order there.

theorem HasPolarDensity.unique {S : Set (HeightOneSpectrum (𝓞 K))} {ρ₁ ρ₂ : ℚ}
    (h₁ : S.HasPolarDensity ρ₁) (h₂ : S.HasPolarDensity ρ₂) : ρ₁ = ρ₂

Uses 2

Statement usesPolar density

Proof usesPartial Dedekind zeta function

TheoremThe empty set has polar density zero#✓fully proved

For every number field \(K\), the empty set of height-one primes of the ring of integers of \(K\) has polar density \(0\).

The partial Dedekind zeta function of the empty set is the constant \(1\), so the constant continuation \(F = 1\) with \(n = 1\) and \(m = 0\) witnesses this.

@[simp] theorem hasPolarDensity_empty (K : Type*) [Field K] [NumberField K] :
    (∅ : Set (HeightOneSpectrum (𝓞 K))).HasPolarDensity 0

Uses 2

Statement usesPolar density

Proof usesPartial Dedekind zeta function

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.