FKS2.corollary_26

@[blueprint  "fks2-corollary-26"  (title := "FKS2 Corollary 26")  (statement := /--  One has  \[  |\pi(x) - \mathrm{Li}(x)| \leq 0.4298 \frac{x}{\log x}  \]  for all $x \geq 2$.  -/)  (proof := /--  The paper verifies this by combining explicit small-prime checks, Buthe's  estimates up to $10^{19}$, and the numerical/asymptotic FKS2 bounds above  $10^{19}$.  In this formal proof, after the Table 6 threshold convention in  Corollary \ref{cor:alt1}, the row  $[0.826, 0.25, 1.00, 1.000]$ only applies for $x \ge \exp(1)$.   We therefore split at $e$.  For $2 \le x < e$, one has $\pi(x)=1$, and the  integral definition gives $0 \le \Li(x) \le 2$; together with  $\log x / x \le 1/e \le 0.4298$, this gives $E_\pi(x) \le 0.4298$.  For  $x \ge e$, we apply Corollary \ref{cor:alt1} with the row  $[0.826,0.25,1.00,1.000]$ and then compare the resulting admissible bound to  $0.4298$.  -/)  (latexEnv := "corollary")  (discussion := 723)]theorem corollary_26 : Eπ.bound 0.4298 2 := by  intro x hx  by_cases hsmall : x < Real.exp 1  · exact Eπ_le_on_two_e hx hsmall  · have hxe : Real.exp (1.000 : ℝ) ≤ x := by      rw [show (1.000 : ℝ) = 1 by norm_num]; exact not_lt.mp hsmall    have h1 := corollary_23 0.826 0.25 1.00 1.000 table6_mem    exact le_trans (h1 x hxe) (admissible_bound_le_0826 x (by linarith))