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

S x = ∑_{p ≤ x} 1/p = log (log x) + c₅ + O(pntE x), by partial summation against θ.

theorem IwaniecLinearSieve.exists_abs_sub_le_of_cauchy {T g : ℝ → ℝ} {a : ℝ} (h : ∀ (x y : ℝ), a ≤ x → x ≤ y → |T y - T x| ≤ g x) (hg : Filter.Tendsto g Filter.atTop (nhds 0)) : ∃ (c : ℝ), ∀ x ≥ a, |T x - c| ≤ g x

If |T y - T x| ≤ g x whenever a ≤ x ≤ y and g → 0, then T has a limit c with |T x - c| ≤ g x for x ≥ a.

noncomputable def IwaniecLinearSieve.S (x : ℝ) : ℝ

S x = ∑_{p ≤ x} 1/p.

Equations

• IwaniecLinearSieve.S x = ∑ p ∈ IwaniecLinearSieve.primesLT (↑⌊x⌋₊ + 1), (↑p)⁻¹

theorem IwaniecLinearSieve.S_eq_sum (x : ℝ) : S x = ∑ k ∈ Finset.range (⌊x⌋₊ + 1), if Nat.Prime k then (↑k)⁻¹ else 0

noncomputable def IwaniecLinearSieve.logPrime (k : ℕ) : ℝ

The weight log p at primes p, and 0 elsewhere.

Equations

• IwaniecLinearSieve.logPrime k = if Nat.Prime k then Real.log ↑k else 0

theorem IwaniecLinearSieve.sum_logPrime_eq_theta (t : ℝ) : ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, logPrime k = Chebyshev.theta t

theorem IwaniecLinearSieve.S_sub_S {x y : ℝ} (hxy : x ≤ y) : S y - S x = ∑ k ∈ Finset.Ioc ⌊x⌋₊ ⌊y⌋₊, (↑k * Real.log ↑k)⁻¹ * logPrime k

theorem IwaniecLinearSieve.hasDerivAt_inv_mul_log {t : ℝ} (ht : 1 < t) : HasDerivAt (fun (t : ℝ) => (t * Real.log t)⁻¹) (-((Real.log t + 1) / (t * Real.log t) ^ 2)) t

theorem IwaniecLinearSieve.hasDerivAt_log_log_sub_inv_log {t : ℝ} (ht : 1 < t) : HasDerivAt (fun (t : ℝ) => Real.log (Real.log t) - (Real.log t)⁻¹) ((Real.log t + 1) / (t * Real.log t) ^ 2 * t) t

theorem IwaniecLinearSieve.continuousOn_log_add_one_div {x y : ℝ} (hx : 1 < x) : ContinuousOn (fun (t : ℝ) => (Real.log t + 1) / (t * Real.log t) ^ 2) (Set.Icc x y)

theorem IwaniecLinearSieve.S_sub_loglog_eq {x y : ℝ} (hx : 2 ≤ x) (hxy : x ≤ y) : S y - Real.log (Real.log y) - (S x - Real.log (Real.log x)) = (y * Real.log y)⁻¹ * (Chebyshev.theta y - y) - (x * Real.log x)⁻¹ * (Chebyshev.theta x - x) + ∫ (t : ℝ) in x..y, (Real.log t + 1) / (t * Real.log t) ^ 2 * (Chebyshev.theta t - t)

Partial summation: the variation of S x - log (log x) in terms of θ x - x.

theorem IwaniecLinearSieve.half_le_log {t : ℝ} (ht : 2 ≤ t) : 1 / 2 ≤ Real.log t

theorem IwaniecLinearSieve.continuousOn_deriv_pntE {x y : ℝ} (hx : 1 < x) : ContinuousOn (fun (t : ℝ) => pntE t * (-pntκ * (t⁻¹ / (2 * √(Real.log t))))) (Set.Icc x y)

theorem IwaniecLinearSieve.abs_integrand_le {C t : ℝ} (hC : 0 ≤ C) (ht : 2 ≤ t) (hθ : |Chebyshev.theta t - t| ≤ C * t * pntE t) : |(Real.log t + 1) / (t * Real.log t) ^ 2 * (Chebyshev.theta t - t)| ≤ -(12 * C / pntκ) * (pntE t * (-pntκ * (t⁻¹ / (2 * √(Real.log t)))))

The integrand in S_sub_loglog_eq is dominated by a multiple of -pntE'.

theorem IwaniecLinearSieve.exists_abs_S_sub_loglog_sub_le : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (x y : ℝ), 2 ≤ x → x ≤ y → |S y - Real.log (Real.log y) - (S x - Real.log (Real.log x))| ≤ K * pntE x

theorem IwaniecLinearSieve.S_asymp : ∃ (c₅ : ℝ) (C : ℝ), ∀ x ≥ 2, |S x - Real.log (Real.log x) - c₅| ≤ C * pntE x

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