Source indexedtheorem · leanprover/lean4:v4.32.0

Ramanujan.pi_bound_6

PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:843 to 857

Mathematical statement

Exact Lean statement

@[blueprint
  "ramanujan-pibound-6"
  (title := "Error estimate for theta, range 6 ")
  (statement := /-- For $x > \exp(3000)$ we have
$$E_\theta(x) \leq 379.7\left(\frac{\log x}{5.573412}\right)^{1.52}\exp\left(-1.89\sqrt{\frac{\log x}{5.573412}}\right).$$
(cf. \cite[(18)]{PT2021})-/)
  (proof := /-- This follows from Corollary \ref{pt_cor_1}. -/)
  (latexEnv := "sublemma")
  (discussion := 1094)]
theorem pi_bound_6 (x : ℝ) (hx : exp 3000 ≤ x) :
    Eθ x ≤ 379.7 * (log x / 5.573412) ^ (1.52 : ℝ) * exp (-1.89 * sqrt (log x / 5.573412))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "ramanujan-pibound-6"  (title := "Error estimate for theta, range 6 ")  (statement := /-- For $x > \exp(3000)$ we have$$E_\theta(x) \leq 379.7\left(\frac{\log x}{5.573412}\right)^{1.52}\exp\left(-1.89\sqrt{\frac{\log x}{5.573412}}\right).$$(cf. \cite[(18)]{PT2021})-/)  (proof := /-- This follows from Corollary \ref{pt_cor_1}. -/)  (latexEnv := "sublemma")  (discussion := 1094)]theorem pi_bound_6 (x : ℝ) (hx : exp 3000 ≤ x) :    Eθ x ≤ 379.7 * (log x / 5.573412) ^ (1.52 : ℝ) * exp (-1.89 * sqrt (log x / 5.573412)) := by  have h7 : Eθ x ≤ admissible_bound (379.6 + 0.1) (1.52 : ℝ) (1.89 : ℝ) (5.573412 : ℝ) x :=    PT.corollary_1 3000 0.98 379.6 1.52 1.89 4.51e-13 (by simp [PT.Table_1]) x hx  have h8 : 379.6 + 0.1 = (379.7 : ℝ) := by norm_num  simpa [h8, admissible_bound, sqrt_eq_rpow] using h7