TODO: Add doc-string.

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

A completed dedekind xi used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.completedDedekindXi K s = s * (s - 1) * NumberField.Odlyzko.CompletedZeta.completed K s

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

theorem NumberField.Odlyzko.logDeriv_completedDedekindXi_rightHalfPlane (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (hs : 1 < s.re) : logDeriv (completedDedekindXi K) s = 1 / s + 1 / (s - 1) + 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

theorem NumberField.Odlyzko.poleClearedCompletedDedekindZetaContinuation_eq_neg_finrank_mul_xi (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (hs : 1 < s.re) : poleClearedCompletedDedekindZetaContinuation K s = -↑(Module.finrank ℚ K) * completedDedekindXi K s

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

theorem NumberField.Odlyzko.logDeriv_poleClearedCompletedDedekindZetaContinuation_rightHalfPlane (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (hs : 1 < s.re) : logDeriv (poleClearedCompletedDedekindZetaContinuation K) s = logDeriv (completedDedekindXi K) s

theorem NumberField.Odlyzko.logDeriv_poleClearedCompletedDedekindZetaContinuation_eq_primePower (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (hs : 1 < s.re) : logDeriv (poleClearedCompletedDedekindZetaContinuation K) s = 1 / s + 1 / (s - 1) + 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

theorem NumberField.Odlyzko.deriv_poleClearedCompletedDedekindZetaContinuation_one_sub (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (s : ℂ) : deriv (poleClearedCompletedDedekindZetaContinuation K) (1 - s) = -deriv (poleClearedCompletedDedekindZetaContinuation K) s

theorem NumberField.Odlyzko.logDeriv_poleClearedCompletedDedekindZetaContinuation_one_sub (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (_hs : poleClearedCompletedDedekindZetaContinuation K s ≠ 0) : logDeriv (poleClearedCompletedDedekindZetaContinuation K) (1 - s) = -logDeriv (poleClearedCompletedDedekindZetaContinuation K) s

theorem NumberField.Odlyzko.logDeriv_poleClearedCompletedDedekindZetaContinuation_one_sub_all (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (s : ℂ) : logDeriv (poleClearedCompletedDedekindZetaContinuation K) (1 - s) = -logDeriv (poleClearedCompletedDedekindZetaContinuation K) s