BKLNW_app.bklnw_cor_15_1'

@[blueprint "bklnw-cor_15_1_alt"  (title := "Corollary 15.1, alternative version")  (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}}},  1.93378 \cdot 10^{-8}\right\}  \quad \text{for all } x \geq e^b. $$   -/)  (proof := /-- From Table 8 we have  $\varepsilon(19 \log 10)  = 1.93378 \cdot 10^{-8}$.  Now apply Corollary \ref{bklnw-cor_15_1}  and Theorem \ref{bklnw-theorem-2}. -/)  (latexEnv := "corollary")  (discussion := 775)]theorem bklnw_cor_15_1' (b : ℝ)    (hb1 : log 11 < b)    (hb2 : b ≤ 19 * log 10) :    ∀ x ≥ exp b,      Eψ x ≤        max (0.94 / exp (b / 2))          (1.93378e-8 * table_8_margin) := by  intro x hx  grw [bklnw_cor_15_1 b hb1 hb2 table_8_ε    (fun b₀ hb₀ x hx ↦ by      grw [Eψ,        div_le_iff₀          (lt_of_lt_of_le (by positivity) hx),        theorem_2 b₀ hb₀.le x hx]) x hx]  apply max_le_max_left  suffices 43 < 19 * Real.log 10 ∧      19 * Real.log 10 < 44 by    grw [table_8_ε.le_simp (19 * log 10)      (by grind)]    grind [table_8_ε']  constructor <;>    nlinarith [LogTables.log_10_gt,      LogTables.log_10_lt]