Mertens' product theorem with the de la Vallée Poussin error term

R z = ∏_{p < z} (1 - 1/p) = c_R / log z + O(pntE z / log z).

theorem IwaniecLinearSieve.one_sub_inv_pos {p : ℕ} (hp : Nat.Prime p) : 0 < 1 - (↑p)⁻¹

theorem IwaniecLinearSieve.one_sub_inv_le_one (p : ℕ) : 1 - (↑p)⁻¹ ≤ 1

theorem IwaniecLinearSieve.primesLT_mono {z w : ℝ} (hzw : z ≤ w) : primesLT z ⊆ primesLT w

theorem IwaniecLinearSieve.R_eq_mul_prod_sdiff {z w : ℝ} (hzw : z ≤ w) : R w = R z * ∏ p ∈ primesLT w \ primesLT z, (1 - (↑p)⁻¹)

theorem IwaniecLinearSieve.R_antitone : Antitone R

noncomputable def IwaniecLinearSieve.SLT (z : ℝ) : ℝ

∑_{p < z} 1/p.

Equations

• IwaniecLinearSieve.SLT z = ∑ p ∈ IwaniecLinearSieve.primesLT z, (↑p)⁻¹

theorem IwaniecLinearSieve.S_sub_SLT {z : ℝ} (hz : 0 < z) : 0 ≤ S z - SLT z ∧ S z - SLT z ≤ z⁻¹

S counts primes p ≤ z and SLT primes p < z; they differ by at most 1 / z.

theorem IwaniecLinearSieve.abs_log_one_sub_inv_add_inv_le {p : ℝ} (hp : 2 ≤ p) : |Real.log (1 - p⁻¹) + p⁻¹| ≤ (p - 1)⁻¹ - p⁻¹

0 ≤ -log (1 - 1/p) - 1/p ≤ 1/(p-1) - 1/p.

theorem IwaniecLinearSieve.sum_Ico_inv_sub_inv {m M : ℕ} (hmM : m ≤ M) : ∑ n ∈ Finset.Ico m M, ((↑n - 1)⁻¹ - (↑n)⁻¹) = (↑m - 1)⁻¹ - (↑M - 1)⁻¹

theorem IwaniecLinearSieve.abs_sum_log_one_sub_inv_add_inv_le {z w : ℝ} (hz : 2 ≤ z) (hzw : z ≤ w) : |∑ p ∈ primesLT w \ primesLT z, (Real.log (1 - (↑p)⁻¹) + (↑p)⁻¹)| ≤ 2 * z⁻¹

The tail of ∑_p (-log (1 - 1/p) - 1/p) is at most 2 / z.

theorem IwaniecLinearSieve.log_R_eq (z : ℝ) : Real.log (R z) = ∑ p ∈ primesLT z, Real.log (1 - (↑p)⁻¹)

theorem IwaniecLinearSieve.abs_exp_sub_one_le_mul_exp (d : ℝ) : |Real.exp d - 1| ≤ |d| * Real.exp |d|

theorem IwaniecLinearSieve.exists_abs_log_R_add_loglog_sub_le : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (z w : ℝ), 2 ≤ z → z ≤ w → |Real.log (R w) + Real.log (Real.log w) - (Real.log (R z) + Real.log (Real.log z))| ≤ K * pntE z

theorem IwaniecLinearSieve.R_asymp : ∃ cR > 0, ∃ (C : ℝ), ∀ z ≥ 2, |R z * Real.log z - cR| ≤ C * pntE z

Mertens' product theorem with the de la Vallée Poussin error term.

theorem IwaniecLinearSieve.R_lower : ∃ c > 0, ∀ z ≥ 2, c / Real.log z ≤ R z

Lower bound R z ≫ 1 / log z.

theorem IwaniecLinearSieve.R_upper : ∃ C > 0, ∀ z ≥ 2, R z ≤ C / Real.log z

Upper bound R z ≪ 1 / log z.