The de la Vallée Poussin error term

We fix once and for all a constant pntκ > 0 and the error function pntE x = exp (-pntκ * √(log x)), and deduce from StrongPNT that θ(x) = x + O(x · pntE x) for x ≥ 2, with an explicit constant valid for all x ≥ 2.

The constant pntκ is the minimum of the constant c of StrongPNT and 1 / 2; the bound pntκ ≤ 1 / 2 lets pntE x dominate x ^ (-1/2) * log x and 1 / x.

noncomputable def IwaniecLinearSieve.pntc : ℝ

The constant c in StrongPNT.

Equations

• IwaniecLinearSieve.pntc = IwaniecLinearSievePNT.StrongPNT.choose

theorem IwaniecLinearSieve.pntc_pos : 0 < pntc

noncomputable def IwaniecLinearSieve.pntκ : ℝ

The constant κ in the error term exp (-κ √(log x)) used throughout.

Equations

• IwaniecLinearSieve.pntκ = min IwaniecLinearSieve.pntc (1 / 2)

theorem IwaniecLinearSieve.pntκ_pos : 0 < pntκ

theorem IwaniecLinearSieve.pntκ_le_half : pntκ ≤ 1 / 2

theorem IwaniecLinearSieve.pntκ_le_pntc : pntκ ≤ pntc

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

The de la Vallée Poussin error term exp (-κ √(log x)).

Equations

• IwaniecLinearSieve.pntE x = Real.exp (-IwaniecLinearSieve.pntκ * √(Real.log x))

theorem IwaniecLinearSieve.pntE_pos (x : ℝ) : 0 < pntE x

theorem IwaniecLinearSieve.pntE_nonneg (x : ℝ) : 0 ≤ pntE x

theorem IwaniecLinearSieve.pntE_le_one (x : ℝ) : pntE x ≤ 1

theorem IwaniecLinearSieve.pntE_le_pntE {x y : ℝ} (hx : 0 < x) (hxy : x ≤ y) : pntE y ≤ pntE x

theorem IwaniecLinearSieve.pntE_antitoneOn : AntitoneOn pntE (Set.Ioi 0)

theorem IwaniecLinearSieve.pntE_antitoneOn_Ici_one : AntitoneOn pntE (Set.Ici 1)

theorem IwaniecLinearSieve.tendsto_pntE : Filter.Tendsto pntE Filter.atTop (nhds 0)

theorem IwaniecLinearSieve.inv_le_pntE {x : ℝ} (hx : 2 ≤ x) : x⁻¹ ≤ pntE x

pntE dominates 1 / x.

theorem IwaniecLinearSieve.one_div_mul_log_le_pntE {x : ℝ} (hx : 2 ≤ x) : 1 / (x * Real.log x) ≤ 2 * pntE x

theorem IwaniecLinearSieve.sqrt_mul_log_le {x : ℝ} (hx : 1 ≤ x) : √x * Real.log x ≤ 12 * x * pntE x

pntE dominates x ^ (-1/2) * log x.

theorem IwaniecLinearSieve.hasDerivAt_pntE {x : ℝ} (hx : 1 < x) : HasDerivAt pntE (pntE x * (-pntκ * (x⁻¹ / (2 * √(Real.log x))))) x

theorem IwaniecLinearSieve.exists_abs_psi_sub_le : ∃ (C : ℝ) (X : ℝ), 0 ≤ C ∧ ∀ x ≥ X, |Chebyshev.psi x - x| ≤ C * x * pntE x

The prime number theorem for ψ with the error term pntE, valid from some point on.

theorem IwaniecLinearSieve.theta_asymp : ∃ (C : ℝ), 0 ≤ C ∧ ∀ x ≥ 2, |Chebyshev.theta x - x| ≤ C * x * pntE x

The prime number theorem for θ: |θ x - x| ≤ C x exp (-κ √(log x)) for all x ≥ 2.