TODO: Add doc-string.

theorem NumberField.Odlyzko.hasDerivAt_localFactor {q : ℕ} (hq : 1 < q) {s : ℂ} (hs : 0 < s.re) : HasDerivAt (localFactor q) (-(inverseNormPower q s * Complex.log ↑q / (1 - inverseNormPower q s) ^ 2)) s

theorem NumberField.Odlyzko.logDeriv_localFactor {q : ℕ} (hq : 1 < q) {s : ℂ} (hs : 0 < s.re) : logDeriv (localFactor q) s = -(Complex.log ↑q * inverseNormPower q s / (1 - inverseNormPower q s))

theorem NumberField.Odlyzko.hasSum_logDeriv_localFactor {q : ℕ} (hq : 1 < q) {s : ℂ} (hs : 0 < s.re) : HasSum (fun (e : ℕ) => Complex.log ↑q * inverseNormPower q s ^ (e + 1)) (-logDeriv (localFactor q) s)

theorem NumberField.Odlyzko.logDeriv_primeIdealFactor (K : Type u_1) [Field K] [NumberField K] (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) {s : ℂ} (hs : 0 < s.re) : logDeriv (primeIdealFactor K P) s = -(Complex.log ↑(primeIdealNorm K P) * inverseNormPower (primeIdealNorm K P) s / (1 - inverseNormPower (primeIdealNorm K P) s))

theorem NumberField.Odlyzko.hasSum_neg_logDeriv_primeIdealFactor (K : Type u_1) [Field K] [NumberField K] (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) {s : ℂ} (hs : 0 < s.re) : HasSum (fun (e : ℕ) => Complex.log ↑(primeIdealNorm K P) * inverseNormPower (primeIdealNorm K P) s ^ (e + 1)) (-logDeriv (primeIdealFactor K P) s)

def NumberField.Odlyzko.dedekindZetaHalfPlane : Set ℂ

A dedekind zeta half plane used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.dedekindZetaHalfPlane = {s : ℂ | 1 < s.re}

theorem NumberField.Odlyzko.isOpen_dedekindZetaHalfPlane : IsOpen dedekindZetaHalfPlane

theorem NumberField.Odlyzko.multipliableLocallyUniformlyOn_primeIdealFactor (K : Type u_1) [Field K] [NumberField K] : MultipliableLocallyUniformlyOn (primeIdealFactor K) dedekindZetaHalfPlane

theorem NumberField.Odlyzko.summable_logDeriv_primeIdealFactor (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : Summable fun (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => logDeriv (primeIdealFactor K P) s

theorem NumberField.Odlyzko.logDeriv_dedekindZeta_eq_tsum_primeIdeal (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : logDeriv (dedekindZeta K) s = ∑' (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), logDeriv (primeIdealFactor K P) s

theorem NumberField.Odlyzko.neg_logDeriv_dedekindZeta_eq_tsum_primeIdeal (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : -logDeriv (dedekindZeta K) s = ∑' (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), -logDeriv (primeIdealFactor K P) s

noncomputable def NumberField.Odlyzko.primePowerLogTerm (K : Type u_1) [Field K] [NumberField K] (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (e : ℕ) (s : ℂ) : ℂ

A prime power log term used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.primePowerLogTerm K P e s = Complex.log ↑(NumberField.Odlyzko.primeIdealNorm K P) * NumberField.Odlyzko.inverseNormPower (NumberField.Odlyzko.primeIdealNorm K P) s ^ (e + 1)

theorem NumberField.Odlyzko.primePowerLogTerm_eq_log_mul_cexp_neg (K : Type u_1) [Field K] [NumberField K] (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (e : ℕ) (s : ℂ) : primePowerLogTerm K P e s = ↑(Real.log ↑(primeIdealNorm K P)) * Complex.exp (-(↑↑(e + 1) * ↑(Real.log ↑(primeIdealNorm K P))) * s)

theorem NumberField.Odlyzko.norm_primePowerLogTerm (K : Type u_1) [Field K] [NumberField K] (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (e : ℕ) (s : ℂ) : ‖primePowerLogTerm K P e s‖ = Real.log ↑(primeIdealNorm K P) * (↑(primeIdealNorm K P) ^ (-s.re)) ^ (e + 1)

theorem NumberField.Odlyzko.summable_norm_primePowerLogTerm (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : Summable fun (pe : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) × ℕ) => ‖primePowerLogTerm K pe.1 pe.2 s‖

theorem NumberField.Odlyzko.neg_logDeriv_dedekindZeta_eq_tsum_primePower (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : -logDeriv (dedekindZeta K) s = ∑' (pe : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) × ℕ), primePowerLogTerm K pe.1 pe.2 s