Source indexedtheorem · leanprover/lean4:v4.32.0

FKS.psi_bound

PrimeNumberTheoremAnd.IEANTN.TMEEMT · PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:601 to 612

Source documentation

Some results from \cite{FKS}

Exact Lean statement

@[blueprint
  "thm:fks-psi"
  (title := "Fiori-Kadiri-Swidinsky $\\psi$ bound")
  (statement := /-- For $x \geq 2$, we have $|\psi(x) - x| \leq x \cdot 9.22022\, (\log x)^{1.5} \exp(-0.8476836\sqrt{\log x})$. -/)
  (latexEnv := "theorem")]
theorem psi_bound (x : ℝ) (hx : x ≥ 2) :
    |ψ x - x| ≤ x * 9.22022 * (log x) ^ (1.5 : ℝ) * exp (-0.8476836 * sqrt (log x))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "thm:fks-psi"  (title := "Fiori-Kadiri-Swidinsky $\\psi$ bound")  (statement := /-- For $x \geq 2$, we have $|\psi(x) - x| \leq x \cdot 9.22022\, (\log x)^{1.5} \exp(-0.8476836\sqrt{\log x})$. -/)  (latexEnv := "theorem")]theorem psi_bound (x : ℝ) (hx : x ≥ 2) :    |ψ x - x| ≤ x * 9.22022 * (log x) ^ (1.5 : ℝ) * exp (-0.8476836 * sqrt (log x)) := by  have h_ineq : |ψ x - x| / x ≤ 9.22022 * (log x) ^ (3 / 2 : ℝ) * exp (-0.8476836 * sqrt (log x)) := by    have := FKS.FKS_corollary_1_4    convert! this x hx using 1; norm_num [exp_neg, sqrt_eq_rpow, rpow_neg, div_eq_mul_inv]; ring_nf    norm_num [admissible_bound, exp_neg, sqrt_eq_rpow, rpow_neg, div_eq_mul_inv]; ring_nf  rw [div_le_iff₀] at h_ineq <;> ring_nf at * <;> grind