BKLNW.cor_2_1

@[blueprint  "bklnw-cor-2-1"  (title := "BKLNW Corollary 2.1")  (statement := /-- $\theta(x) \leq (1 + 1.93378 \times 10^{-8}) x$. -/)  (proof := /-- We combine together Theorem \ref{from-buthe-eq-1-7} and Theorem \ref{bklnw-thm-1a-table} with $X_1 = 10^{19}$. -/)  (latexEnv := "corollary")  (discussion := 791)]theorem cor_2_1 : ∀ x > 0, θ x ≤ (1 + (1.93378e-8*BKLNW_app.table_8_margin)) * x := by  intro x hx_pos  by_cases! hx : x ≤ 1e19  · exact le_trans (le_of_lt (buthe_eq_1_7 x ⟨hx_pos, hx⟩)) (le_mul_of_one_le_left hx_pos.le (by norm_num))  · have h_exp20 : 1e19 ≥ exp 20 := by grw [← exp_one_rpow 20, Real.exp_one_lt_d9]; norm_num only    suffices Pre_inputs.default.ε (log 1e19) ≤ 1.93378e-8 * BKLNW_app.table_8_margin by      grw [(thm_1a h_exp20 h_exp20 hx.le hx.le).2, this, mul_comm]    unfold Pre_inputs.default    suffices 43 < log 1e19 ∧ log 1e19 < 44 by      change BKLNW_app.table_8_ε (log 1e19) ≤ 1.93378e-8 * BKLNW_app.table_8_margin      grw [BKLNW_app.table_8_ε.le_simp (log 1e19) (by grind)]      grind [BKLNW_app.table_8_ε']    have h1e19 : (1e19 : ℝ) = (10 : ℝ) ^ 19 := by norm_num    rw [h1e19, Real.log_pow]; push_cast    constructor <;> nlinarith [LogTables.log_10_gt, LogTables.log_10_lt]