FKS2.cube_mul_exp_antitoneOn

lemma cube_mul_exp_antitoneOn {A C : ℝ} (hA : 0 ≤ A) (hC : 0 < C) :    AntitoneOn (fun t => A * t ^ 3 * Real.exp (-C * t)) (Set.Ici (3 / C)) := by  have hderiv : ∀ t : ℝ, HasDerivAt (fun t => A * t ^ 3 * Real.exp (-C * t))      (A * (3 * t ^ 2) * Real.exp (-C * t) +        A * t ^ 3 * (Real.exp (-C * t) * (-C))) t := by    intro t    have h1 : HasDerivAt (fun t : ℝ => A * t ^ 3) (A * (3 * t ^ 2)) t := by      simpa using (hasDerivAt_pow 3 t).const_mul A    have h2 : HasDerivAt (fun t : ℝ => -C * t) (-C) t := by      simpa using (hasDerivAt_id t).const_mul (-C)    have h3 : HasDerivAt (fun t : ℝ => Real.exp (-C * t))        (Real.exp (-C * t) * (-C)) t := (Real.hasDerivAt_exp _).comp t h2    exact h1.mul h3  apply antitoneOn_of_deriv_nonpos (convex_Ici _)  · exact (Continuous.continuousOn (by continuity))  · intro t ht    exact (hderiv t).differentiableAt.differentiableWithinAt  · intro t ht    rw [interior_Ici] at ht    rw [(hderiv t).deriv]    have htC : 3 ≤ C * t := by      rw [Set.mem_Ioi] at ht      have := (div_lt_iff₀ hC).mp ht      linarith    have hexp : (0:ℝ) ≤ Real.exp (-C * t) := Real.exp_nonneg _    have ht0 : (0:ℝ) ≤ t := by      rw [Set.mem_Ioi] at ht      have : (0:ℝ) < 3 / C := by positivity      linarith    nlinarith [sq_nonneg t, mul_nonneg (mul_nonneg hA (sq_nonneg t)) hexp,      mul_nonneg (mul_nonneg (mul_nonneg hA ht0) (sq_nonneg t)) hexp]