FKS2.corollary_14

@[blueprint  "fks2-corollary-14"  (title := "FKS2 Corollary 14")  (statement := /--  We have an admissible bound for $E_\theta$ with $A = 121.0961$, $B=3/2$, $C=2$,  $R = 5.5666305$, $x_0=2$.  -/)  (proof := /-- By Corollary \ref{fks_cor_13}, with $R = 5.5666305$, and using the admissible asymptotic bound for $E_\psi(x)$ with $A_\psi = 121.096$, $B = 3/2$, $C = 2$, for all $x \geq x_0 = e^{30}$, we can obtain $\nu_{asymp}(x_0) \leq 6.3376 \cdot 10^{-7}$, from which one can conclude an admissible asymptotic bound for $E_\theta(x)$ with $A_\theta = 121.0961$, $B = 3/2$, $C = 2$, for all $x \geq x_0 = e^{30}$. Additionally, the minimum value of $\varepsilon_{\theta,asymp}(x)$ for $2 \leq x \leq e^{30}$ is roughly $2.6271\ldots$ at $x=2$. The results found in \cite[Table 13 and 14]{BKLNW} give $E_\theta(x) \leq 1 < \varepsilon_{\theta,asymp}(2) \leq \varepsilon_{\theta,asymp}(x)$ for all $2 \leq x \leq e^{30}$. -/)  (latexEnv := "corollary")  (discussion := 672)]theorem corollary_14 : Eθ.classicalBound 121.0961 (3 / 2) 2 5.5666305 2 := by  have hsmall_adm :      ∀ {x : ℝ}, 2 ≤ x → x ≤ Real.exp 30 →      (1 : ℝ) ≤ admissible_bound 121.0961 (3 / 2) 2 5.5666305 x := corollary_14_small_adm   have hfloor30 : ⌊(30 : ℝ) / Real.log 2⌋₊ = 43 := floor_30_div_log2_eq_43  have ha1 : BKLNW.a₁ 30 ≤ 1 + 1.9339e-8 := bklnw_a1_30_le  have ha2 : BKLNW.a₂ 30 ≤ 42.42 := bklnw_a2_30_le  have hcoef :      (1 / (121.096 : ℝ)) * (5.5666305 / 30) ^ (3 / 2 : ℝ) * Real.exp (2 * Real.sqrt (30 / 5.5666305)) ≤ 0.06865 := coeff_bound_30  have hν : ν_asymp 121.096 (3 / 2) 2 5.5666305 (Real.exp 30) ≤ 8.25e-7 := nu_asymp_bound_30   have hA : 121.096 * (1 + ν_asymp 121.096 (3 / 2) 2 5.5666305 (Real.exp 30)) ≤ 121.0961 := by    nlinarith [hν]   have hEψ30 : Eψ.classicalBound 121.096 (3 / 2) 2 5.5666305 (Real.exp 30) := epsi_classicalBound_30  have hB : (3 / 2 : ℝ) > 2 ^ 2 / (8 * 5.5666305) := by norm_num  have hEθ30 :      Eθ.classicalBound (121.096 * (1 + ν_asymp 121.096 (3 / 2) 2 5.5666305 (Real.exp 30)))        (3 / 2) 2 5.5666305 (Real.exp 30) :=    proposition_13 121.096 (3 / 2) 2 5.5666305 (Real.exp 30) (by norm_num) (by norm_num) (exp_pos 30) (by rw [Real.log_exp]; norm_num) hEψ30 hB   rw [Eθ.classicalBound]  intro x hx  by_cases hx30 : x ≤ Real.exp 30  · have hx_pos : 0 < x := by linarith    have hExp30_le_1e19 : Real.exp 30 ≤ (1e19 : ℝ) := by      have h30lelog : (30 : ℝ) ≤ Real.log (1e19) := by        have h1e19 : (1e19 : ℝ) = (10 : ℝ) ^ 19 := by norm_num        rw [h1e19, Real.log_pow]        norm_num        nlinarith [LogTables.log_10_gt]      have : Real.exp 30 ≤ Real.exp (Real.log (1e19)) := (Real.exp_le_exp).2 h30lelog      simpa [Real.exp_log (by norm_num : (0 : ℝ) < 1e19)] using this    have hx_le_1e19 : x ≤ (1e19 : ℝ) := le_trans hx30 hExp30_le_1e19    have hθlt : θ x < x := BKLNW.buthe_eq_1_7 x ⟨hx_pos, hx_le_1e19⟩    have hEθ1 : Eθ x ≤ 1 := by      unfold Eθ      have habs : |θ x - x| ≤ x := by        have hleft : -x ≤ θ x - x := by linarith [theta_nonneg x]        have hright : θ x - x ≤ x := by linarith [hθlt]        exact abs_le.mpr ⟨hleft, hright⟩      exact (div_le_iff₀ hx_pos).mpr (by nlinarith [habs])    have hAdm1 : (1 : ℝ) ≤ admissible_bound 121.0961 (3 / 2) 2 5.5666305 x := hsmall_adm hx hx30    exact le_trans hEθ1 hAdm1  · have hx30' : Real.exp 30 ≤ x := le_of_lt (lt_of_not_ge hx30)    have hmain : Eθ x ≤ admissible_bound        (121.096 * (1 + ν_asymp 121.096 (3 / 2) 2 5.5666305 (Real.exp 30)))        (3 / 2) 2 5.5666305 x := hEθ30 x hx30'    have hlog_div_nonneg : 0 ≤ Real.log x / 5.5666305 := by      have hx_ge1 : (1 : ℝ) ≤ x := by        have h1exp30 : (1 : ℝ) < Real.exp 30 := (Real.one_lt_exp_iff).2 (by norm_num : (0 : ℝ) < 30)        exact le_trans h1exp30.le hx30'      exact div_nonneg (Real.log_nonneg hx_ge1) (by norm_num)    have hpow_nonneg : 0 ≤ (Real.log x / 5.5666305) ^ (3 / 2 : ℝ) :=      Real.rpow_nonneg hlog_div_nonneg _    have hexp_nonneg : 0 ≤ Real.exp (-2 * (Real.log x / 5.5666305) ^ ((1 : ℝ) / (2 : ℝ))) := by positivity    have hAmono : admissible_bound        (121.096 * (1 + ν_asymp 121.096 (3 / 2) 2 5.5666305 (Real.exp 30)))        (3 / 2) 2 5.5666305 x ≤ admissible_bound 121.0961 (3 / 2) 2 5.5666305 x := by      let t : ℝ := (Real.log x / 5.5666305) ^ (3 / 2 : ℝ)      let e : ℝ := Real.exp (-2 * (Real.log x / 5.5666305) ^ ((1 : ℝ) / (2 : ℝ)))      have ht_nonneg : 0 ≤ t := by simpa [t] using hpow_nonneg      have he_nonneg : 0 ≤ e := by simpa [e] using hexp_nonneg      have hAt :          (121.096 * (1 + ν_asymp 121.096 (3 / 2) 2 5.5666305 (Real.exp 30))) * t ≤ 121.0961 * t :=        mul_le_mul_of_nonneg_right hA ht_nonneg      have hAte :          ((121.096 * (1 + ν_asymp 121.096 (3 / 2) 2 5.5666305 (Real.exp 30))) * t) * e ≤          (121.0961 * t) * e :=        mul_le_mul_of_nonneg_right hAt he_nonneg      unfold admissible_bound      simpa [t, e, mul_assoc, mul_left_comm, mul_comm] using hAte    exact le_trans hmain hAmono