FKS2.remark_15'

theorem remark_15' (x₀ : ℝ) (hx₀_pos : 0 < x₀) (h : log x₀ ≥ 1000) :    Eθ.classicalBound ((FKS.A x₀) * (1 + remark_15_margin)) (3 / 2) 2 5.5666305 x₀ := by    have hν : ν_asymp (FKS.A x₀) (3 / 2) 2 5.5666305 x₀ ≤ (1 + remark_15_margin) - 1 := by      exact nu_asymp_le_remark_15_margin_sub_one x₀ h    have hEψ : Eψ.classicalBound (FKS.A x₀) (3 / 2) 2 5.5666305 x₀ :=      FKS.theorem_1_2b x₀ h    have hB : (3 / 2 : ℝ) > 2 ^ 2 / (8 * (5.5666305 : ℝ)) := by      have hR : (0 : ℝ) < 5.5666305 := by norm_num      have hden : (0 : ℝ) < 8 * (5.5666305 : ℝ) := by nlinarith      have : (2 ^ 2 : ℝ) / (8 * (5.5666305 : ℝ)) < (3 / 2 : ℝ) := by        refine (div_lt_iff₀ hden).2 ?_        nlinarith [hR]      simpa using this    have hA_pos : FKS.A x₀ > 0 := by linarith [FKS_A_one_le x₀ h]    have hx₀_ge7 : 7 ≤ Real.log x₀ := by linarith    have hθ :        Eθ.classicalBound ((FKS.A x₀) * (1 + ν_asymp (FKS.A x₀) (3 / 2) 2 5.5666305 x₀))          (3 / 2) 2 5.5666305 x₀ :=      proposition_13 (FKS.A x₀) (3 / 2) 2 5.5666305 x₀ hA_pos (by norm_num) hx₀_pos hx₀_ge7 hEψ hB    have hA_nonneg : 0 ≤ FKS.A x₀ := by      have hbound₀ : Eψ (exp (log x₀)) ≤ admissible_bound (FKS.A x₀) (3 / 2) 2 5.5666305 (exp (log x₀)) :=        hEψ (exp (log x₀)) (Real.le_exp_log x₀)      have hEψ_nonneg : 0 ≤ Eψ (exp (log x₀)) := by        unfold Eψ        positivity      have hlogx₀_pos : 0 < log x₀ := by linarith      have hR : (0 : ℝ) < 5.5666305 := by norm_num      have hlogx₀R_pos : 0 < log x₀ / (5.5666305 : ℝ) := div_pos hlogx₀_pos hR      have hfactor_pos :          0 <            (log x₀ / (5.5666305 : ℝ)) ^ (3 / 2 : ℝ) *              exp (-2 * (log x₀ / (5.5666305 : ℝ)) ^ ((1 : ℝ) / (2 : ℝ))) := by        exact mul_pos (Real.rpow_pos_of_pos hlogx₀R_pos _) (Real.exp_pos _)      have hbound₀' :          Eψ (exp (log x₀)) ≤            (FKS.A x₀) *              ((log x₀ / (5.5666305 : ℝ)) ^ (3 / 2 : ℝ) *                exp (-2 * (log x₀ / (5.5666305 : ℝ)) ^ ((1 : ℝ) / (2 : ℝ)))) := by        simpa [admissible_bound, Real.log_exp, mul_assoc, mul_left_comm, mul_comm] using hbound₀      have hmul_nonneg :          0 ≤            (FKS.A x₀) *              ((log x₀ / (5.5666305 : ℝ)) ^ (3 / 2 : ℝ) *                exp (-2 * (log x₀ / (5.5666305 : ℝ)) ^ ((1 : ℝ) / (2 : ℝ)))) := by        linarith      have hmul_nonneg' :          0 ≤            ((log x₀ / (5.5666305 : ℝ)) ^ (3 / 2 : ℝ) *                exp (-2 * (log x₀ / (5.5666305 : ℝ)) ^ ((1 : ℝ) / (2 : ℝ)))) *              (FKS.A x₀) := by        simpa [mul_assoc, mul_left_comm, mul_comm] using hmul_nonneg      exact nonneg_of_mul_nonneg_right hmul_nonneg' hfactor_pos    have hA :        (FKS.A x₀) * (1 + ν_asymp (FKS.A x₀) (3 / 2) 2 5.5666305 x₀) ≤          (FKS.A x₀) * (1 + remark_15_margin) := by      have h1 : 1 + ν_asymp (FKS.A x₀) (3 / 2) 2 5.5666305 x₀ ≤ 1 + remark_15_margin := by        linarith      exact mul_le_mul_of_nonneg_left h1 hA_nonneg    intro x hx    have hrpow_nonneg : 0 ≤ (log x / (5.5666305 : ℝ)) ^ (3 / 2 : ℝ) := by      by_cases hbase : 0 ≤ log x / (5.5666305 : ℝ)      · exact Real.rpow_nonneg hbase _      · have hbase' : log x / (5.5666305 : ℝ) ≤ 0 := le_of_not_ge hbase        rw [Real.rpow_def_of_nonpos hbase']        have hcos : Real.cos ((3 / 2 : ℝ) * π) = 0 := by          have hsplit : ((3 / 2 : ℝ) * π) = π / 2 + π := by ring          rw [hsplit, Real.cos_add_pi]          norm_num [Real.cos_pi_div_two]        rw [hcos]        norm_num    have hθx := hθ x hx    unfold admissible_bound at hθx ⊢    have hA' :        ((FKS.A x₀) * (1 + ν_asymp (FKS.A x₀) (3 / 2) 2 5.5666305 x₀)) *            (log x / (5.5666305 : ℝ)) ^ (3 / 2 : ℝ) ≤          ((FKS.A x₀) * (1 + remark_15_margin)) * (log x / (5.5666305 : ℝ)) ^ (3 / 2 : ℝ) :=      mul_le_mul_of_nonneg_right hA hrpow_nonneg    exact le_trans hθx (mul_le_mul_of_nonneg_right hA' (Real.exp_nonneg _))