FKS2.part1_decay_bound

lemma part1_decay_bound    (t powfac expfac : ℝ)    (ht : t ≥ 1000)    (hpow_le_div : powfac ≤ (5.5666305 : ℝ) / t)    (hexpfac_nonneg : 0 ≤ expfac)    (h_exp_half :      expfac * exp (-(1 / 2 : ℝ) * t) ≤ exp (-(1 / 4 : ℝ) * t)) :    powfac * expfac * ((2 * t) * exp (-(1 / 2 : ℝ) * t))      ≤ (2 * (5.5666305 : ℝ)) * exp (-(230 : ℝ)) := by  have ht_pos : 0 < t := by linarith [ht]  have hpow_t : powfac * (2 * t) ≤ 2 * (5.5666305 : ℝ) := by    have hmul : powfac * (2 * t) ≤ ((5.5666305 : ℝ) / t) * (2 * t) :=      mul_le_mul_of_nonneg_right hpow_le_div (by positivity)    have ht_eq : ((5.5666305 : ℝ) / t) * (2 * t) = 2 * (5.5666305 : ℝ) := by      field_simp [ht_pos.ne']    calc      powfac * (2 * t) ≤ ((5.5666305 : ℝ) / t) * (2 * t) := hmul      _ = 2 * (5.5666305 : ℝ) := ht_eq  have hexp230 :      exp (-(1 / 4 : ℝ) * t) ≤ exp (-(230 : ℝ)) := by    refine (Real.exp_le_exp).2 ?_    linarith [ht]  calc    powfac * expfac * ((2 * t) * exp (-(1 / 2 : ℝ) * t))        = (powfac * (2 * t)) * (expfac * exp (-(1 / 2 : ℝ) * t)) := by ring_nf    _ ≤ (2 * (5.5666305 : ℝ)) * exp (-(1 / 4 : ℝ) * t) := by      exact mul_le_mul hpow_t h_exp_half        (mul_nonneg hexpfac_nonneg (Real.exp_nonneg _)) (by positivity)    _ ≤ (2 * (5.5666305 : ℝ)) * exp (-(230 : ℝ)) := by      exact mul_le_mul_of_nonneg_left hexp230 (by positivity)