FKS2.part2_decay_bound

lemma part2_decay_bound    (t powfac expfac : ℝ)    (ht : t ≥ 1000)    (hpow_le_div : powfac ≤ (5.5666305 : ℝ) / t)    (hexpfac_nonneg : 0 ≤ expfac)    (h_exp_third :      expfac * exp (-(2 / 3 : ℝ) * t) ≤ exp (-(5 / 12 : ℝ) * t)) :    powfac * expfac * ((5 * t * t) * exp (-(2 / 3 : ℝ) * t))      ≤ (2500 * (5.5666305 : ℝ)) * exp (-(230 : ℝ)) := by  have ht_pos : 0 < t := by linarith [ht]  have hpow_t2 : powfac * (5 * t * t) ≤ 5 * (5.5666305 : ℝ) * t := by    have hmul : powfac * (5 * t * t) ≤ ((5.5666305 : ℝ) / t) * (5 * t * t) :=      mul_le_mul_of_nonneg_right hpow_le_div (by positivity)    have ht_eq : ((5.5666305 : ℝ) / t) * (5 * t * t) = 5 * (5.5666305 : ℝ) * t := by      field_simp [ht_pos.ne']    calc      powfac * (5 * t * t) ≤ ((5.5666305 : ℝ) / t) * (5 * t * t) := hmul      _ = 5 * (5.5666305 : ℝ) * t := ht_eq  have h_t_exp :      t * exp (-(1 / 1000 : ℝ) * t) ≤ 500 :=    t_mul_exp_neg_one_thousandth_le_five_hundred t ht  have hexp_big :      exp (-(5 / 12 : ℝ) * t) ≤ exp (-(230 : ℝ)) * exp (-(1 / 1000 : ℝ) * t) :=    exp_neg_five_twelfths_mul_le t ht  have hmix :      exp (-(5 / 12 : ℝ) * t) * t ≤ exp (-(230 : ℝ)) * 500 := by    have hstep1 :        exp (-(5 / 12 : ℝ) * t) * t ≤          (exp (-(230 : ℝ)) * exp (-(1 / 1000 : ℝ) * t)) * t :=      mul_le_mul_of_nonneg_right hexp_big (by positivity)    have h_t_exp' : exp (-(1 / 1000 : ℝ) * t) * t ≤ 500 := by      calc        exp (-(1 / 1000 : ℝ) * t) * t = t * exp (-(1 / 1000 : ℝ) * t) := by ac_rfl        _ ≤ 500 := h_t_exp    have hstep2 :        (exp (-(230 : ℝ)) * exp (-(1 / 1000 : ℝ) * t)) * t ≤ exp (-(230 : ℝ)) * 500 := by      have hmul := mul_le_mul_of_nonneg_left h_t_exp' (Real.exp_nonneg (-(230 : ℝ)))      calc        (exp (-(230 : ℝ)) * exp (-(1 / 1000 : ℝ) * t)) * t            = exp (-(230 : ℝ)) * (exp (-(1 / 1000 : ℝ) * t) * t) := by simp [mul_assoc]        _ ≤ exp (-(230 : ℝ)) * 500 := hmul    exact hstep1.trans hstep2  calc    powfac * expfac * ((5 * t * t) * exp (-(2 / 3 : ℝ) * t))        = (powfac * (5 * t * t)) * (expfac * exp (-(2 / 3 : ℝ) * t)) := by ac_rfl    _ ≤ (5 * (5.5666305 : ℝ) * t) * exp (-(5 / 12 : ℝ) * t) := by      exact mul_le_mul hpow_t2 h_exp_third        (mul_nonneg hexpfac_nonneg (Real.exp_nonneg _)) (by positivity)    _ = (5 * (5.5666305 : ℝ)) * (exp (-(5 / 12 : ℝ) * t) * t) := by ac_rfl    _ ≤ (5 * (5.5666305 : ℝ)) * (exp (-(230 : ℝ)) * 500) := by      gcongr    _ = (2500 * (5.5666305 : ℝ)) * exp (-(230 : ℝ)) := by ring_nf