The degree-one prime-ideal sum and the polynomial root sum

theorem NairTenenbaum.primeIdeals_degreeOne_sum_le {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) (S : Finset (Ideal (NumberField.RingOfIntegers K))) (hS : ∀ P ∈ S, Prime P) (hdeg : ∀ P ∈ S, Ideal.absNorm P = rationalPrimeBelow P) (hgood : ∀ P ∈ S, (rationalPrimeBelow P).Coprime (RingOfIntegers.exponent θ)) (σ : ℝ) : ∑ P ∈ S, ↑(Ideal.absNorm P) ^ (-σ) ≤ ∑ p ∈ Finset.image rationalPrimeBelow S, ↑(rootCount (minpoly ℤ θ) p) * ↑p ^ (-σ)

theorem NairTenenbaum.primeIdeals_bad_sum_le {K : Type u_1} [Field K] [NumberField K] {D : ℕ} (hD : D ≠ 0) (S : Finset (Ideal (NumberField.RingOfIntegers K))) (hS : ∀ P ∈ S, Prime P) (hbad : ∀ P ∈ S, rationalPrimeBelow P ∣ D) {σ : ℝ} (hσ : 1 ≤ σ) : ∑ P ∈ S, ↑(Ideal.absNorm P) ^ (-σ) ≤ ↑(Module.finrank ℚ K) * ↑D.primeFactors.card

theorem NairTenenbaum.primeIdeals_sum_le_rootSum_add_error {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) (hD : RingOfIntegers.exponent θ ≠ 0) (S : Finset (Ideal (NumberField.RingOfIntegers K))) (hS : ∀ P ∈ S, Prime P) {σ : ℝ} (hσ : 1 ≤ σ) : ∑ P ∈ S, ↑(Ideal.absNorm P) ^ (-σ) ≤ ∑ p ∈ Finset.image rationalPrimeBelow S, ↑(rootCount (minpoly ℤ θ) p) * ↑p ^ (-σ) + ↑(Module.finrank ℚ K) * (↑(RingOfIntegers.exponent θ).primeFactors.card + ∑' (n : ℕ), ↑n ^ (-2))

theorem NairTenenbaum.primeIdeals_eulerExponent_le {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) (hD : RingOfIntegers.exponent θ ≠ 0) (S : Finset (Ideal (NumberField.RingOfIntegers K))) (hS : ∀ P ∈ S, Prime P) {σ : ℝ} (hσ : 1 ≤ σ) : ∑ P ∈ S, (↑(Ideal.absNorm P) ^ (-σ) + 2 * (↑(Ideal.absNorm P) ^ (-σ)) ^ 2) ≤ ∑ p ∈ Finset.image rationalPrimeBelow S, ↑(rootCount (minpoly ℤ θ) p) * ↑p ^ (-σ) + ↑(Module.finrank ℚ K) * (↑(RingOfIntegers.exponent θ).primeFactors.card + 3 * ∑' (n : ℕ), ↑n ^ (-2))