Summable errors in the prime-ideal Euler product

theorem NairTenenbaum.primeIdeals_sum_baseWeight_le {K : Type u_1} [Field K] [NumberField K] (S : Finset (Ideal (NumberField.RingOfIntegers K))) (hS : ∀ P ∈ S, Prime P) (f : ℕ → ℝ) (hf : ∀ (p : ℕ), 0 ≤ f p) : ∑ P ∈ S, f (rationalPrimeBelow P) ≤ ↑(Module.finrank ℚ K) * ∑ p ∈ Finset.image rationalPrimeBelow S, f p

theorem NairTenenbaum.primeIdeals_sum_baseWeight_le_tsum {K : Type u_1} [Field K] [NumberField K] (S : Finset (Ideal (NumberField.RingOfIntegers K))) (hS : ∀ P ∈ S, Prime P) (f : ℕ → ℝ) (hf : ∀ (p : ℕ), 0 ≤ f p) (hs : Summable f) : ∑ P ∈ S, f (rationalPrimeBelow P) ≤ ↑(Module.finrank ℚ K) * ∑' (n : ℕ), f n

theorem NairTenenbaum.primeIdeal_weight_sq_le {K : Type u_1} [Field K] [NumberField K] {P : Ideal (NumberField.RingOfIntegers K)} (hP : Prime P) {σ : ℝ} (hσ : 1 ≤ σ) : (↑(Ideal.absNorm P) ^ (-σ)) ^ 2 ≤ ↑(rationalPrimeBelow P) ^ (-2)

theorem NairTenenbaum.primeIdeal_higherDegree_weight_le {K : Type u_1} [Field K] [NumberField K] {P : Ideal (NumberField.RingOfIntegers K)} (hP : Prime P) (hneq : Ideal.absNorm P ≠ rationalPrimeBelow P) {σ : ℝ} (hσ : 1 ≤ σ) : ↑(Ideal.absNorm P) ^ (-σ) ≤ ↑(rationalPrimeBelow P) ^ (-2)

theorem NairTenenbaum.primeIdeal_square_error_sum_le {K : Type u_1} [Field K] [NumberField K] (S : Finset (Ideal (NumberField.RingOfIntegers K))) (hS : ∀ P ∈ S, Prime P) {σ : ℝ} (hσ : 1 ≤ σ) : ∑ P ∈ S, (↑(Ideal.absNorm P) ^ (-σ)) ^ 2 ≤ ↑(Module.finrank ℚ K) * ∑' (n : ℕ), ↑n ^ (-2)

theorem NairTenenbaum.primeIdeal_higherDegree_sum_le {K : Type u_1} [Field K] [NumberField K] (S : Finset (Ideal (NumberField.RingOfIntegers K))) (hS : ∀ P ∈ S, Prime P) {σ : ℝ} (hσ : 1 ≤ σ) : ∑ P ∈ S with Ideal.absNorm P ≠ rationalPrimeBelow P, ↑(Ideal.absNorm P) ^ (-σ) ≤ ↑(Module.finrank ℚ K) * ∑' (n : ℕ), ↑n ^ (-2)