The extra logarithm in the prime-argument Euler product

The elementary harmonic-series argument gives the upper bound needed in Theorem 3, without the prime number theorem or an asymptotic Mertens theorem.

theorem NairTenenbaum.reciprocal_prime_powers_hasSum {p : ℕ} (hp : Nat.Prime p) : HasSum (fun (ν : ℕ) => (↑(p ^ ν))⁻¹) (1 - 1 / ↑p)⁻¹

theorem NairTenenbaum.reciprocal_smooth_hasSum (s : Finset ℕ) : HasSum (fun (n : ↑(Nat.factoredNumbers s)) => (↑↑n)⁻¹) (∏ p ∈ s with Nat.Prime p, (1 - 1 / ↑p)⁻¹)

theorem NairTenenbaum.harmonic_le_reciprocal_prime_product (N : ℕ) : ↑(harmonic N) ≤ ∏ p ∈ Finset.range (N + 1) with Nat.Prime p, (1 - 1 / ↑p)⁻¹

Every integer up to N is composed of primes up to N. The harmonic sum is consequently bounded by the reciprocal finite Euler product.

theorem NairTenenbaum.sieveProduct_X_le_inv_log {x : ℝ} (hx : 1 < x) : sieveProduct Polynomial.X x ≤ (Real.log x)⁻¹

An elementary Mertens upper bound with constant one.

theorem NairTenenbaum.progressionSieveProduct_X_le {q : ℕ} (hq : q ≠ 0) (x : ℝ) : progressionSieveProduct Polynomial.X q x ≤ sieveProduct Polynomial.X x * (↑q / ↑q.totient)

Omitting primes dividing q costs at most q / φ(q), with no further constant for this one-root Euler product.

theorem NairTenenbaum.progressionSieveProduct_X_le_inv_log {q : ℕ} (hq : q ≠ 0) {x : ℝ} (hx : 1 < x) : progressionSieveProduct Polynomial.X q x ≤ ↑q / ↑q.totient / Real.log x