A linear error for the small-prime logarithmic mass

The prime-counting estimate absorbs all prime-power congruence errors, including the finitely many primes dividing the discriminant.

theorem NairTenenbaum.card_primes_up_to_eq (z : ℝ) : (Finset.filter Nat.Prime (Finset.range (⌊z⌋₊ + 1))).card = ⌊z⌋₊.primeCounting

theorem NairTenenbaum.exists_smoothLogRootError_linear_bound {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) (hD : Q.discr ≠ 0) {A C β : ℝ} (hA : 1 ≤ A) (hC : 1 ≤ C) (hβ : 0 < β) (g : ℕ) : ∃ (x₀ : ℝ) (B : ℝ), 1 < x₀ ∧ 0 ≤ B ∧ ∀ (x y : ℝ), x₀ < x → x ^ β ≤ y → smoothLogRootError Q (C * y) (primePowerLogCutoff (A * x ^ g)) ≤ B * y