BKLNW_app.bklnw_cor_15_1

@[blueprint "bklnw-cor_15_1"  (title := "Corollary 15.1")  (statement := /-- Let $b$ be a positive constant  such that $\log 11 < b \leq 19 \log(10)$.  Then we have  $$ \left|\frac{\psi(x) - x}{x}\right|  \leq \max\left\{\frac{0.94}{e^{\frac{b}{2}}},  \varepsilon(19 \log 10)\right\}  \quad \text{for all } x \geq e^b. $$  Note that by Table 8, we have  $\varepsilon(19 \log 10)  = 1.93378 \cdot 10^{-8}$. -/)  (proof := /-- By \cite[(1.5)]{Buthe},  (A.27) holds with $B_0 = 11$,  $B = 10^{19}$, and $c = 0.94$.  Thus we may apply Lemma  \ref{bklnw-lemma_15} with $B_0 = 11$,  $B = 10^{19}$, and $c = 0.94$ from  \cite[(1.5)]{Buthe} to obtain  the claim. -/)  (latexEnv := "corollary")]theorem bklnw_cor_15_1 (b : ℝ)    (hb1 : log 11 < b)    (hb2 : b ≤ 19 * log 10)    (ε : ℝ → ℝ)    (hε : ∀ b₀ > 0, ∀ x ≥ exp b₀,      Eψ x ≤ ε b₀) :    ∀ x ≥ exp b,      Eψ x ≤ max (0.94 / exp (b / 2))        (ε (19 * log 10)) := by  have hlog11_pos : (0 : ℝ) < log 11 := by    positivity  have hbpos : b > 0 := by linarith  have h10_19 : (10 : ℝ) ^ (19 : ℕ) > 0 := by    positivity  have hlog_eq : log ((10 : ℝ) ^ (19 : ℕ)) = 19 * log 10 := by    rw [Real.log_pow]    ring  rw [← hlog_eq]  apply bklnw_lemma_15 0.94 11    ((10 : ℝ) ^ (19 : ℕ))  · intro x hx    exact Buthe.theorem_2a hx.1 hx.2  · exact hε  · constructor    · have : Real.exp (Real.log 11) < Real.exp b := Real.exp_lt_exp.mpr hb1      rwa [Real.exp_log (by norm_num : (11 : ℝ) > 0)] at this    · rw [← hlog_eq] at hb2      rw [← Real.exp_log (by positivity : (10 : ℝ) ^ (19 : ℕ) > 0)]      exact Real.exp_le_exp.mpr hb2  · exact hbpos  · norm_num  · exact h10_19