The real Dirichlet series of ideal norms

This module connects the nonnegative real series needed for comparisons with Mathlib's Dedekind zeta function and its proved residue at one.

noncomputable def NairTenenbaum.idealNormCount (K : Type u_1) [Field K] [NumberField K] (n : ℕ) : ℕ

The number of integral ideals of a specified absolute norm.

Equations

• NairTenenbaum.idealNormCount K n = Nat.card { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = n }

noncomputable def NairTenenbaum.idealNormDirichlet (K : Type u_1) [Field K] [NumberField K] (σ : ℝ) : ℝ

The Dirichlet series counting integral ideals by their absolute norm.

Equations

• NairTenenbaum.idealNormDirichlet K σ = ∑' (n : ℕ), ↑(NairTenenbaum.idealNormCount K n) * ↑n ^ (-σ)

theorem NairTenenbaum.idealNormCount_partialSum_limit (K : Type u_1) [Field K] [NumberField K] : Filter.Tendsto (fun (n : ℕ) => (∑ k ∈ Finset.Icc 1 n, ↑(idealNormCount K k)) / ↑n) Filter.atTop (nhds (NumberField.dedekindZeta_residue K))

theorem NairTenenbaum.lSeriesSummable_idealNormCount (K : Type u_1) [Field K] [NumberField K] {σ : ℝ} (hσ : 1 < σ) : LSeriesSummable (fun (n : ℕ) => ↑(idealNormCount K n)) ↑σ

theorem NairTenenbaum.idealNormDirichlet_term_complex (K : Type u_1) [Field K] [NumberField K] {σ : ℝ} (hσ : 1 < σ) (n : ℕ) : LSeries.term (fun (n : ℕ) => ↑(idealNormCount K n)) (↑σ) n = ↑(↑(idealNormCount K n) * ↑n ^ (-σ))

theorem NairTenenbaum.summable_idealNormDirichlet (K : Type u_1) [Field K] [NumberField K] {σ : ℝ} (hσ : 1 < σ) : Summable fun (n : ℕ) => ↑(idealNormCount K n) * ↑n ^ (-σ)

theorem NairTenenbaum.idealNormDirichlet_eq_dedekindZeta (K : Type u_1) [Field K] [NumberField K] {σ : ℝ} (hσ : 1 < σ) : ↑(idealNormDirichlet K σ) = NumberField.dedekindZeta K ↑σ

theorem NairTenenbaum.idealNormDirichlet_residue (K : Type u_1) [Field K] [NumberField K] : Filter.Tendsto (fun (s : ℝ) => (s - 1) * idealNormDirichlet K s) (nhdsWithin 1 (Set.Ioi 1)) (nhds (NumberField.dedekindZeta_residue K))

theorem NairTenenbaum.exists_idealNormDirichlet_pole_bound (K : Type u_1) [Field K] [NumberField K] : ∃ (C : ℝ) (b : ℝ), 0 < C ∧ 1 < b ∧ ∀ (s : ℝ), 1 < s → s < b → idealNormDirichlet K s ≤ C / (s - 1)

theorem NairTenenbaum.exists_idealNormDirichlet_pole_lower_bound (K : Type u_1) [Field K] [NumberField K] : ∃ (c : ℝ) (b : ℝ), 0 < c ∧ 1 < b ∧ ∀ (s : ℝ), 1 < s → s < b → c / (s - 1) ≤ idealNormDirichlet K s

The positive Dedekind residue also gives the matching lower pole bound.