JY.corollary_1_3

@[blueprint  "thm:jy_13"  (title := "JY Corollary 1.3")  (statement := /--  One has  \[  |\pi(x) - \mathrm{li}(x)| \leq 9.59 x (\log x)^{0.515} \exp(-0.8274 \sqrt{\log x})  \]  for all $x \geq 2$.  -/)  (latexEnv := "theorem")]theorem corollary_1_3 : Eπ.classicalBound 9.59 1.515 0.8274 1 2 := by  have := FKS2.corollary_22  intro x hx  have hx2 : x ≥ 2 := by grind [add_one_le_exp 2000]  refine (this x hx2).trans ?_  simp only [admissible_bound]; norm_num  suffices h_div :      92211 / 10000 * log x ^ (3 / 2 : ℝ) *        exp (-2119 / 2500 * log x^(1 / 2 : ℝ) + 4137 / 5000 * log x^(1 / 2 : ℝ)) ≤        959 / 100 * log x ^ (303 / 200 : ℝ)    by    convert mul_le_mul_of_nonneg_right h_div        (exp_nonneg (-4137 / 5000 * log x^(1 / 2 : ℝ))) using 1    · rw [exp_add (-2119 / 2500 * log x^(1 / 2 : ℝ)) (4137 / 5000 * log x^(1 / 2 : ℝ))]      ring_nf      norm_num [mul_assoc, ← exp_add]    simp only [one_div, mul_eq_mul_left_iff, exp_eq_exp, _root_.mul_eq_zero]    left    linarith  suffices h_div :      92211 / 10000 * exp (-2119 / 2500 * log x^(1 / 2 : ℝ) +        4137 / 5000 * log x^(1 / 2 : ℝ)) ≤        959 / 100 * log x ^ (303 / 200 - 3 / 2 : ℝ)    by    convert! mul_le_mul_of_nonneg_right h_div        (rpow_nonneg (log_nonneg (show x ≥ 1 by linarith)) (3 / 2 : ℝ)) using 1 <;>      ring_nf    rw [← rpow_add (log_pos (by linarith : x > 1))]    norm_num  have hsqrtlogpos : 0 < log x ^ (1/2:ℝ) :=    by exact rpow_pos_of_pos (log_pos (by linarith : x > 1)) (1/2:ℝ)  have hneg :      -(2119 / 2500) * log x^(1 / 2 : ℝ) + 4137 / 5000 * log x^(1 / 2 : ℝ) < 0 :=    by linarith  have hexpone :      exp (-(2119 / 2500) * log x^(1 / 2 : ℝ) + 4137 / 5000 * log x^(1 / 2 : ℝ)) < 1 := by    exact exp_lt_one_iff.mpr hneg   suffices h_calc : 92211/10000 ≤ 959/100 * log x ^(303 / 200 - 3/2 : ℝ) by linarith  refine le_trans ?_ <| mul_le_mul_of_nonneg_left    (rpow_le_rpow (by grind) (log_two_gt_d9.le.trans (log_le_log (by grind) hx)) (by grind))    (by grind)  norm_num  rw [← log_le_log_iff (by positivity) (by positivity),    log_mul (by positivity) (by positivity), log_rpow (by positivity),    div_mul_eq_mul_div, add_div', le_div_iff₀] <;>    norm_num [← log_rpow, mul_comm, ← log_mul, log_le_log_iff]