FKS2.nu_asymp_le_remark_15_margin

theorem nu_asymp_le_remark_15_margin (x₀ : ℝ) (h : Real.log x₀ ≥ 1000) :    ν_asymp (FKS.A x₀) (3 / 2) 2 5.5666305 x₀ ≤ remark_15_margin := by  set t : ℝ := Real.log x₀  have ht : t ≥ 1000 := by simpa [t] using h  have ht_pos : 0 < t := by linarith [ht]   have hA_pos : 0 < FKS.A x₀ := by linarith [FKS_A_one_le x₀ h]  have h_invA_le_one : 1 / FKS.A x₀ ≤ 1 :=    (div_le_iff₀ hA_pos).2 (by simpa using FKS_A_one_le x₀ h)   have hxhalf_abs : |x₀ ^ (-(1 / 2 : ℝ))| ≤ exp (-(1 / 2 : ℝ) * t) := by    simpa [t, mul_assoc, mul_left_comm, mul_comm] using Real.abs_rpow_le_exp_log_mul x₀ (-(1 / 2 : ℝ))  have hxthird_abs : |x₀ ^ (-(2 / 3 : ℝ))| ≤ exp (-(2 / 3 : ℝ) * t) := by    simpa [t, mul_assoc, mul_left_comm, mul_comm] using Real.abs_rpow_le_exp_log_mul x₀ (-(2 / 3 : ℝ))   have hpow_le_div : ((5.5666305 : ℝ) / t) ^ (3 / 2 : ℝ) ≤ (5.5666305 : ℝ) / t := by    simpa using Real.rpow_le_rpow_of_exponent_ge (by positivity)      ((div_le_iff₀ (by linarith)).2 (by linarith)) (by norm_num : (1 : ℝ) ≤ 3 / 2)   have h_exp_half :      exp (2 * Real.sqrt (t / 5.5666305)) * exp (-(1 / 2 : ℝ) * t) ≤ exp (-(1 / 4 : ℝ) * t) := by    rw [← Real.exp_add]; exact Real.exp_le_exp.2 (by nlinarith [two_mul_sqrt_div_le_quarter t ht])  have h_exp_third :      exp (2 * Real.sqrt (t / 5.5666305)) * exp (-(2 / 3 : ℝ) * t) ≤ exp (-(5 / 12 : ℝ) * t) := by    rw [← Real.exp_add]; exact Real.exp_le_exp.2 (by nlinarith [two_mul_sqrt_div_le_quarter t ht])   have h_inside :      BKLNW.a₁ t * t * x₀ ^ (-(1 / 2 : ℝ)) + BKLNW.a₂ t * t * x₀ ^ (-(2 / 3 : ℝ))        ≤ (2 * t) * exp (-(1 / 2 : ℝ) * t) + (5 * t * t) * exp (-(2 / 3 : ℝ) * t) := by    linarith [term_inside_bound ht_pos.le (BKLNW_a1_nonneg t ht) (BKLNW_a1_le_two_of_ge_1000 t ht) hxhalf_abs,      term_inside_bound ht_pos.le (BKLNW_a2_nonneg t) (BKLNW_a2_le_five_mul_of_ge_1000 t ht) hxthird_abs]  have hhalf_rewrite : ((-1 : ℝ) / 2) = -(1 / 2 : ℝ) := by norm_num  have hthird_rewrite : ((-2 : ℝ) / 3) = -(2 / 3 : ℝ) := by norm_num   let powfac : ℝ := ((5.5666305 : ℝ) / t) ^ (3 / 2 : ℝ)  let expfac : ℝ := exp (2 * Real.sqrt (t / 5.5666305))  have hpowfac_nonneg : 0 ≤ powfac := by unfold powfac; positivity  have hexpfac_nonneg : 0 ≤ expfac := by unfold expfac; positivity   have h_main0 :      ν_asymp (FKS.A x₀) (3 / 2) 2 5.5666305 x₀        ≤ (1 / FKS.A x₀) * powfac * expfac *            ((2 * t) * exp (-(1 / 2 : ℝ) * t) + (5 * t * t) * exp (-(2 / 3 : ℝ) * t)) := by    simpa [hhalf_rewrite, hthird_rewrite, ν_asymp, t, powfac, expfac, mul_assoc, mul_left_comm, mul_comm] using      mul_le_mul_of_nonneg_left h_inside (by positivity : 0 ≤ (1 / FKS.A x₀) * powfac * expfac)   have h_main1 : ν_asymp (FKS.A x₀) (3 / 2) 2 5.5666305 x₀      ≤ powfac * expfac * ((2 * t) * exp (-(1 / 2 : ℝ) * t) + (5 * t * t) * exp (-(2 / 3 : ℝ) * t)) :=    h_main0.trans (by simpa [mul_assoc] using mul_le_mul_of_nonneg_right h_invA_le_one (by positivity))   have h_split :      powfac * expfac * ((2 * t) * exp (-(1 / 2 : ℝ) * t) + (5 * t * t) * exp (-(2 / 3 : ℝ) * t))        ≤ (2 * (5.5666305 : ℝ)) * exp (-(230 : ℝ)) + (2500 * (5.5666305 : ℝ)) * exp (-(230 : ℝ)) := by    rw [mul_add]    exact add_le_add      (part1_decay_bound t powfac expfac ht hpow_le_div hexpfac_nonneg h_exp_half)      (part2_decay_bound t powfac expfac ht hpow_le_div hexpfac_nonneg h_exp_third)   have h_main2 : ν_asymp (FKS.A x₀) (3 / 2) 2 5.5666305 x₀ ≤ (60000 : ℝ) * exp (-(230 : ℝ)) :=    h_main1.trans (h_split.trans (by      rw [← add_mul]; exact mul_le_mul_of_nonneg_right (by norm_num) (by positivity)))   simpa [remark_15_margin] using h_main2.trans sixty_thousand_mul_exp_neg_230_le