Ramanujan.pi_bound_3

@[blueprint  "ramanujan-pibound-3"  (title := "Error estimate for theta, range 3")  (statement := /-- For $\exp(58) < x < \exp(1169)$ we have$$E_\theta(x) \leq \sqrt\frac{8}{17\pi}\left(\frac{\log x}{6.455}\right)^{\frac{1}{4}}\exp\left(-\sqrt{\frac{\log x}{6.455}}\right).$$(cf. \cite[(18)]{PT2021})-/)  (proof := /-- This follows from Theorem \ref{trudgian:theorem 1-theta}. -/)  (latexEnv := "sublemma")  (discussion := 991)]theorem pi_bound_3 (x : ℝ) (hx : x ∈ Set.Ico (exp 58) (exp 1169)) :    Eθ x ≤ sqrt (8 / (17 * π)) * (log x / 6.455) ^ (1 / 4 : ℝ) * exp (-sqrt (log x / 6.455)) := by  set M₄₃ : Fin 5 → ℝ := ![8.6315e-7, 3.7979e-5, 2.4334e-2, 5.7184e1, 1.3441e5]  have htab43 : ((43 : ℝ), M₄₃) ∈ BKLNW.Table_15 := by simp [BKLNW.Table_15, M₄₃]  have hM43 : M₄₃ ⟨1, by norm_num⟩ = 3.7979e-5 := rfl  have hfin43 : (⟨1, by norm_num⟩ : Fin 5).val + 1 = 2 := rfl  have hx_ge_exp43 : x ≥ exp (43 : ℝ) := by    have : exp (43 : ℝ) ≤ exp 58 := by      exact exp_le_exp.mpr (by norm_num)    linarith [hx.1]  obtain ⟨hlb43, hub43⟩ :=    BKLNW.thm_1b_table (by norm_num : (43 : ℝ) > 0) htab43 ⟨1, by norm_num⟩ hx_ge_exp43  rw [hM43, hfin43] at hlb43 hub43  have hE : Eθ x ≤ (3.7979e-5 : ℝ) / (log x) ^ 2 := by    unfold Eθ    have hxpos : 0 < x := lt_of_lt_of_le (exp_pos _) hx.1    have hx_gt_one : 1 < x := by      have : (1 : ℝ) < exp 58 := by nlinarith [add_one_le_exp (58 : ℝ)]      linarith [hx.1]    have hpow_pos : 0 < (log x) ^ 2 := pow_pos (log_pos hx_gt_one) 2    rw [div_le_div_iff₀ hxpos hpow_pos]    have h1 : θ x - x ≤ 3.7979e-5 / (log x) ^ 2 * x := by nlinarith    have h2 : x - θ x ≤ 3.7979e-5 / (log x) ^ 2 * x := by nlinarith    calc |θ x - x| * (log x) ^ 2        ≤ 3.7979e-5 / (log x) ^ 2 * x * (log x) ^ 2 := by            apply mul_le_mul_of_nonneg_right _ (le_of_lt hpow_pos)            rw [abs_le]; exact ⟨by linarith, h1⟩        _ = 3.7979e-5 * x := by            have hdc : 3.7979e-5 / (log x) ^ 2 * (log x) ^ 2 = 3.7979e-5 :=              div_mul_cancel₀ _ (ne_of_gt hpow_pos)            calc 3.7979e-5 / (log x) ^ 2 * x * (log x) ^ 2                = (3.7979e-5 / (log x) ^ 2 * (log x) ^ 2) * x := by ring              _ = 3.7979e-5 * x := by rw [hdc]   have hlog_ge_58 : (58 : ℝ) ≤ log x := by    have h := log_le_log (show 0 < exp 58 by positivity) hx.1    simpa using h  have hlog_le_1169 : log x ≤ (1169 : ℝ) := by    have h := log_le_log (show 0 < x by linarith [hx.1, exp_pos 58]) hx.2.le    simpa using h   have hleft_const : (3.7979e-5 : ℝ) / (log x) ^ 2 ≤ (3.7979e-5 : ℝ) / (58 : ℝ) ^ 2 := by    have hpow : (58 : ℝ) ^ 2 ≤ (log x) ^ 2 := by      nlinarith    exact div_le_div_of_nonneg_left (by norm_num : (0 : ℝ) ≤ 3.7979e-5)      (by positivity : 0 < (58 : ℝ) ^ 2) hpow   have hpi : π ≤ (3.15 : ℝ) := LogTables.pi_le_3_15  have hfrac : (8 / (17 * (3.15 : ℝ)) : ℝ) ≤ 8 / (17 * π) := by    gcongr  have hsqrt_frac : sqrt (8 / (17 * (3.15 : ℝ)) : ℝ) ≤ sqrt (8 / (17 * π)) :=    sqrt_le_sqrt hfrac  have h038 : (0.38 : ℝ) ≤ sqrt (8 / (17 * (3.15 : ℝ)) : ℝ) := by    refine (Real.le_sqrt (by norm_num) (by positivity)).2 ?_    norm_num  have hA_lb : (0.38 : ℝ) ≤ sqrt (8 / (17 * π)) := le_trans h038 hsqrt_frac   have hexp13_5 : (1 / (900000 : ℝ)) ≤ exp (-(13.5 : ℝ)) :=    LogTables.inv_900000_le_exp_neg_13_5  have hsqrt_lt13_5 : sqrt (1169 / 6.455 : ℝ) < 13.5 :=    (sqrt_lt (by positivity) (by positivity)).2 (by norm_num)  have hexp_const : (1 / (900000 : ℝ)) ≤ exp (-sqrt (1169 / 6.455 : ℝ)) := by    have hmono : exp (-(13.5 : ℝ)) ≤ exp (-sqrt (1169 / 6.455 : ℝ)) :=      exp_le_exp.mpr (by linarith)    grind   have hratio_le : log x / 6.455 ≤ (1169 / 6.455 : ℝ) := by    gcongr  have hsqrt_le : sqrt (log x / 6.455 : ℝ) ≤ sqrt (1169 / 6.455 : ℝ) :=    sqrt_le_sqrt hratio_le  have hexp_var : exp (-sqrt (1169 / 6.455 : ℝ)) ≤ exp (-sqrt (log x / 6.455 : ℝ)) :=    exp_le_exp.mpr (by linarith)  have hexp_lb : (1 / (900000 : ℝ)) ≤ exp (-sqrt (log x / 6.455 : ℝ)) :=    le_trans hexp_const hexp_var   have hprod2 : (0.38 : ℝ) * (1 / (900000 : ℝ)) ≤      sqrt (8 / (17 * π)) * exp (-sqrt (log x / 6.455 : ℝ)) :=    mul_le_mul hA_lb hexp_lb (by positivity) (by positivity)  have hpow_ge_one : (1 : ℝ) ≤ (log x / 6.455) ^ (1 / 4 : ℝ) := by    have hbase_ge_one : (1 : ℝ) ≤ log x / 6.455 := by      have hdiv58 : (58 / 6.455 : ℝ) ≤ log x / 6.455 := by        gcongr      have h58_ge_one : (1 : ℝ) ≤ (58 / 6.455 : ℝ) := by        norm_num      grind    exact one_le_rpow hbase_ge_one (by positivity : (0 : ℝ) ≤ (1 / 4 : ℝ))  have hmul_factor :      sqrt (8 / (17 * π)) * exp (-sqrt (log x / 6.455 : ℝ)) ≤        sqrt (8 / (17 * π)) * (log x / 6.455) ^ (1 / 4 : ℝ) * exp (-sqrt (log x / 6.455 : ℝ)) := by    calc      sqrt (8 / (17 * π)) * exp (-sqrt (log x / 6.455 : ℝ))          = sqrt (8 / (17 * π)) * (1 : ℝ) * exp (-sqrt (log x / 6.455 : ℝ)) := by ring      _ ≤ sqrt (8 / (17 * π)) * (log x / 6.455) ^ (1 / 4 : ℝ) * exp (-sqrt (log x / 6.455 : ℝ)) := by        gcongr  have hprod3 : (0.38 : ℝ) * (1 / (900000 : ℝ)) ≤      sqrt (8 / (17 * π)) * (log x / 6.455) ^ (1 / 4 : ℝ) * exp (-sqrt (log x / 6.455 : ℝ)) := by    grind   have hconst_cmp : (3.7979e-5 : ℝ) / (58 : ℝ) ^ 2 ≤ (0.38 : ℝ) * (1 / (900000 : ℝ)) := by    norm_num   exact le_trans (le_trans (le_trans hE hleft_const) hconst_cmp) (by    simpa using hprod3)