TODO: Add doc-string.

theorem NumberField.Odlyzko.abscissaOfAbsConv_idealNormCount_le_one (K : Type u_1) [Field K] [NumberField K] : (LSeries.abscissaOfAbsConv fun (n : ℕ) => ↑(idealNormCount K n)) ≤ 1

theorem NumberField.Odlyzko.hasDerivAt_dedekindZeta (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : HasDerivAt (dedekindZeta K) (-LSeries (LSeries.logMul fun (n : ℕ) => ↑(idealNormCount K n)) s) s

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

theorem NumberField.Odlyzko.logDeriv_dedekindDiscriminantFactor (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : logDeriv (CompletedZeta.discriminantFactor K) s = Complex.log ↑|↑(discr K)| / 2

theorem NumberField.Odlyzko.differentiableAt_dedekindArchimedeanFactor_of_isTotallyComplex (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (hs : 0 < s.re) : DifferentiableAt ℂ (CompletedZeta.archimedeanFactor K) s

theorem NumberField.Odlyzko.logDeriv_completedDedekindZeta_of_isTotallyComplex (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (hs : 0 < s.re) (hζne : dedekindZeta K s ≠ 0) (hζdiff : DifferentiableAt ℂ (dedekindZeta K) s) : logDeriv (CompletedZeta.completed K) s = Complex.log ↑|↑(discr K)| / 2 + ↑(InfinitePlace.nrComplexPlaces K) * (s.digamma - Complex.log (2 * ↑Real.pi)) + logDeriv (dedekindZeta K) s

theorem NumberField.Odlyzko.dedekindZeta_ne_zero_of_one_lt_re (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : dedekindZeta K s ≠ 0

theorem NumberField.Odlyzko.completedDedekindZeta_ne_zero_of_one_lt_re (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : CompletedZeta.completed K s ≠ 0

theorem NumberField.Odlyzko.logDeriv_completedDedekindZeta_rightHalfPlane (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (hs : 1 < s.re) : logDeriv (CompletedZeta.completed K) s = Complex.log ↑|↑(discr K)| / 2 + ↑(InfinitePlace.nrComplexPlaces K) * (s.digamma - Complex.log (2 * ↑Real.pi)) + logDeriv (dedekindZeta K) s

theorem NumberField.Odlyzko.logDeriv_completedDedekindZeta_rightHalfPlane_eq_primePower (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (hs : 1 < s.re) : logDeriv (CompletedZeta.completed K) s = Complex.log ↑|↑(discr K)| / 2 + ↑(InfinitePlace.nrComplexPlaces K) * (s.digamma - Complex.log (2 * ↑Real.pi)) - ∑' (pe : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) × ℕ), primePowerLogTerm K pe.1 pe.2 s