TODO: Add doc-string.

theorem NumberField.Odlyzko.summable_ideal_absNorm_rpow (K : Type u_1) [Field K] [NumberField K] {σ : ℝ} (hσ : 1 < σ) : Summable fun (I : Ideal (RingOfIntegers K)) => ↑(Ideal.absNorm I) ^ (-σ)

theorem NumberField.Odlyzko.summable_primeIdealNorm_rpow (K : Type u_1) [Field K] [NumberField K] {σ : ℝ} (hσ : 1 < σ) : Summable fun (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => ↑(primeIdealNorm K P) ^ (-σ)

theorem NumberField.Odlyzko.summable_primeIdeal_log_mul_rpow (K : Type u_1) [Field K] [NumberField K] {σ : ℝ} (hσ : 1 < σ) : Summable fun (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => Real.log ↑(primeIdealNorm K P) * ↑(primeIdealNorm K P) ^ (-σ)

theorem NumberField.Odlyzko.norm_inverseNormPower_primeIdeal_lt_half (K : Type u_1) [Field K] [NumberField K] (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) {s : ℂ} (hs : 1 < s.re) : ‖inverseNormPower (primeIdealNorm K P) s‖ < 1 / 2

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

theorem NumberField.Odlyzko.norm_primeIdealFactor_sub_one_le (K : Type u_1) [Field K] [NumberField K] (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) {σ : ℝ} {s : ℂ} (hσ : 1 < σ) (hs : σ ≤ s.re) : ‖primeIdealFactor K P s - 1‖ ≤ 2 * ↑(primeIdealNorm K P) ^ (-σ)

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

theorem NumberField.Odlyzko.tprod_primeIdealFactor_ne_zero (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : ∏' (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), primeIdealFactor K P s ≠ 0