PT.corollary_2

@[blueprint "thm:pt_2"  (title := "PT Corollary 2")  (statement := /--  One has  \[  |\pi(x) - \mathrm{li}(x)| \leq 235 x (\log x)^{0.52} \exp(-0.8 \sqrt{\log x})  \]  for all $x \geq \exp(2000)$.  -/)  (latexEnv := "theorem")]theorem corollary_2 : Eπ.classicalBound 235 1.52 0.8 1 (exp 2000) := 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 : ℝ) + 4 / 5 * log x^(1 / 2 : ℝ)) ≤        235 * log x ^ (38 / 25 : ℝ)    by    convert mul_le_mul_of_nonneg_right h_div (exp_nonneg (-4 / 5 * log x^(1 / 2 : ℝ))) using 1    · rw [exp_add (-2119 / 2500 * log x^(1 / 2 : ℝ)) (4 / 5 * 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,      OfNat.ofNat_ne_zero, false_or]    left    linarith  suffices h_div :      92211 / 10000 * exp (-2119 / 2500 * log x^(1 / 2 : ℝ) + 4 / 5 * log x^(1 / 2 : ℝ)) ≤        235 * log x ^ (38 / 25 - 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 : ℝ) + 4 / 5 * log x^(1 / 2 : ℝ) < 0 := by linarith  have hexpone :      exp (-(2119 / 2500) * log x^(1 / 2 : ℝ) + 4 / 5 * log x^(1 / 2 : ℝ)) < 1 := by    exact exp_lt_one_iff.mpr hneg  have hcompare : 0 ≤ (38 / 25 - 3 / 2 : ℝ) := by linarith  have hlogone : log x ≥ 1 := by nlinarith [log_exp 2000, log_le_log (by positivity) hx]  have hlogone2 : (log x)^(0:ℝ) ≤ (log x)^(38 / 25 - 3 / 2 : ℝ) :=    by exact rpow_le_rpow_of_exponent_le hlogone hcompare  rw [rpow_zero (log x)] at hlogone2  linarith