The Mertens upper bound reduced to quantitative ideal counting

A power-saving error in the ideal count implies a bounded error in its weighted von Mangoldt sum. The quantitative ideal-count hypothesis is explicit here; this module does not assert that it follows from the qualitative mean theorem.

theorem NairTenenbaum.reciprocal_logDerivative_le_of_power_error {a v : ArithmeticFunction ℝ} (ha : ∀ (n : ℕ), 0 ≤ a n) (hv : ∀ (n : ℕ), 0 ≤ v n) (hconv : v * a = arithmeticLogWeight a) {κ E C θ x : ℝ} (hκ : 0 < κ) (hE : 0 ≤ E) (hC : 0 ≤ C) (herror : ∀ (t : ℝ), 1 ≤ t → |arithmeticSummatory (⇑a) t - κ * t| ≤ E * t ^ θ) (hbound : ∀ (t : ℝ), 1 ≤ t → arithmeticSummatory (⇑v) t ≤ C * t) (hθ : 0 ≤ θ) (hθ1 : θ < 1) (hx : 1 ≤ x) : arithmeticSummatory (fun (n : ℕ) => v n / ↑n) x ≤ Real.log x + E * (C + 1) / (κ * (1 - θ))

theorem NairTenenbaum.idealMangoldtReciprocalSum_le_of_power_error (K : Type u_1) [Field K] [NumberField K] {E θ : ℝ} (hE : 0 ≤ E) (hθ : 0 ≤ θ) (hθ1 : θ < 1) (herror : ∀ (t : ℝ), 1 ≤ t → |arithmeticSummatory (⇑(idealNormArithmetic K)) t - NumberField.dedekindZeta_residue K * t| ≤ E * t ^ θ) {x : ℝ} (hx : 1 ≤ x) : idealMangoldtReciprocalSum K x ≤ Real.log x + E * (↑(Module.finrank ℚ K) * (Real.log 4 + 4) + 1) / (NumberField.dedekindZeta_residue K * (1 - θ))

theorem NairTenenbaum.exists_primeRootLogSum_mertens_bound_of_power_error (K : Type u_1) [Field K] [NumberField K] {Q : Polynomial ℤ} (N : ℕ) (hmatch : ∀ (p : ℕ), Nat.Prime p → N < p → rootCount Q p = idealNormCount K p) {E θ : ℝ} (hE : 0 ≤ E) (hθ : 0 ≤ θ) (hθ1 : θ < 1) (herror : ∀ (t : ℝ), 1 ≤ t → |arithmeticSummatory (⇑(idealNormArithmetic K)) t - NumberField.dedekindZeta_residue K * t| ≤ E * t ^ θ) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (x : ℝ), 1 ≤ x → primeRootLogSum Q x ≤ Real.log x + B