FKS2.F_strictAnti

lemma F_strictAnti : StrictAntiOn (fun t ↦ exp (t^2) * ((1 : ℝ) - (2 : ℝ) * t * dawson t)) (Set.Ioi (0 : ℝ)) := by  have h_diff : Differentiable ℝ (fun t ↦ exp (t^2) * ((1 : ℝ) - (2 : ℝ) * t * dawson t)) := by    apply Differentiable.mul (by fun_prop)    exact (differentiable_const _).sub (differentiable_id.const_mul (2 : ℝ) |>.mul differentiable_dawson)  refine strictAntiOn_of_deriv_neg (convex_Ioi _) h_diff.continuous.continuousOn (fun x hx ↦ ?_)  rw [interior_Ioi] at hx  have h_deriv_eq : deriv (fun t ↦ exp (t^2) * ((1 : ℝ) - (2 : ℝ) * t * dawson t)) x = -2 * exp (x^2) * dawson x := by    have h_dawson : HasDerivAt dawson (1 - 2 * x * dawson x) x :=      differentiable_dawson.differentiableAt.hasDerivAt.congr_deriv (deriv_dawson x)    exact ((hasDerivAt_exp_sq x).mul      ((hasDerivAt_const x 1).sub        (((hasDerivAt_id x).const_mul 2).mul h_dawson))).deriv.trans (by dsimp; ring)  rw [h_deriv_eq]  nlinarith [exp_pos (x^2), dawson_pos hx]