TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.dedekindZetaSummand (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (n : ℕ) : ℂ

A dedekind zeta summand used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.dedekindZetaSummand K s n = LSeries.term (fun (m : ℕ) => ↑(NumberField.Odlyzko.idealNormCount K m)) s n

@[simp]

theorem NumberField.Odlyzko.dedekindZetaSummand_zero (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : dedekindZetaSummand K s 0 = 0

noncomputable def NumberField.Odlyzko.idealInverseNormPower (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (I : Ideal (RingOfIntegers K)) : ℂ

An ideal inverse norm power used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.idealInverseNormPower K s I = if I = 0 then 0 else ↑(Ideal.absNorm I) ^ (-s)

theorem NumberField.Odlyzko.idealInverseNormPower_zero (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : idealInverseNormPower K s 0 = 0

theorem NumberField.Odlyzko.idealInverseNormPower_of_ne_zero (K : Type u_1) [Field K] [NumberField K] (s : ℂ) {I : Ideal (RingOfIntegers K)} (hI : I ≠ 0) : idealInverseNormPower K s I = ↑(Ideal.absNorm I) ^ (-s)

theorem NumberField.Odlyzko.summable_norm_idealInverseNormPower (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : Summable fun (I : Ideal (RingOfIntegers K)) => ‖idealInverseNormPower K s I‖

theorem NumberField.Odlyzko.summable_idealInverseNormPower (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : Summable (idealInverseNormPower K s)

theorem NumberField.Odlyzko.hasSum_idealInverseNormPower_fiber (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (n : ℕ) : HasSum (fun (I : { I : Ideal (RingOfIntegers K) // Ideal.absNorm I = n }) => idealInverseNormPower K s ↑I) (dedekindZetaSummand K s n)

theorem NumberField.Odlyzko.hasSum_idealInverseNormPower (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : HasSum (idealInverseNormPower K s) (dedekindZeta K s)

theorem NumberField.Odlyzko.hasSum_nonzeroIdeal_inverseNormPower (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : HasSum (fun (I : NonzeroIdeal K) => ↑(Ideal.absNorm ↑I) ^ (-s)) (dedekindZeta K s)