PT.corollary_1

@[blueprint "pt_cor_1"  (title := "PT Corollary 1")  (statement := /--Let $R = 5.573412$. For each row $\{X, \sigma, A, B, C, \epsilon_0\}$ from \cite[Table 1]{PT2021}we have$$\left|\frac{\theta(x) - x}{x}\right| \leq A_1 \left(\frac{\log x}{R}\right)^B  \exp\left(-C\sqrt{\frac{\log x}{R}}\right)$$where $A_1 = A + 0.1$.  -/)  (proof := /-- This follows trivially (and wastefully) from the work of Dusart  \cite[Cor.\ 4.5]{Dusart2018} or the authors \cite[Cor.\ 2]{PT2021}. It should also follow from  the results of \cite{FKS2}. -/)  (latexEnv := "corollary")]theorem corollary_1 (X σ A B C ε₀ : ℝ) (h : (X, σ, A, B, C, ε₀) ∈ Table_1) :  Eθ.classicalBound (A + 0.1) B C 5.573412 (exp X) := by  obtain ⟨hX, hB, hB2, hC, hCR, hA⟩ := table_1_bounds X σ A B C ε₀ h  intro x hx  have hx2 : x ≥ 2 := by    have : (2 : ℝ) < exp 1 := lt_trans (by norm_num : (2:ℝ) < 2.7182818283) exp_one_gt_d9    linarith [exp_le_exp.mpr (show (1:ℝ) ≤ X by linarith)]  have hlogx : 5.5666305 ≤ log x := by    have : X ≤ log x := le_trans (le_of_eq (log_exp X).symm) (log_le_log (exp_pos X) hx)    linarith  exact le_trans (FKS2.corollary_14 x hx2) (admissible_bound_weaken hB hB2 hC hCR hA hlogx)