FKS2.dawson_lt_S6

lemma dawson_lt_S6 (x : ℝ) (hx : x > 0) : dawson x < S6 x := by  have hf0 : exp (0^2) * (S6 0 - dawson 0) = 0 := by    unfold S6 dawson    simp  have h_deriv_f : ∀ y > 0, deriv (fun t ↦ exp (t^2) * (S6 t - dawson t)) y =      exp (y^2) * (128 / 135135) * y^14 := by    intro y hy    have h_dawson : HasDerivAt dawson (1 - 2 * y * dawson y) y :=      differentiable_dawson.differentiableAt.hasDerivAt.congr_deriv (deriv_dawson y)    have h_exp := hasDerivAt_exp_sq y    have h_comb := h_exp.mul ((hasDerivAt_S6 y).sub h_dawson)    change deriv ((fun t ↦ exp (t^2)) * (S6 - dawson)) y = exp (y^2) * (128 / 135135) * y^14    rw [h_comb.deriv]    change 2 * y * exp (y^2) * (S6 y - dawson y) +      exp (y^2) *        (1 - 2 * y^2 + 4/3 * y^4 - 8/15 * y^6 + 16/105 * y^8 - 32/945 * y^10 + 64/10395 * y^12 -          (1 - 2 * y * dawson y)) =      exp (y^2) * (128 / 135135) * y^14    unfold S6    ring  have h_deriv_pos : ∀ y > 0, deriv (fun t ↦ exp (t^2) * (S6 t - dawson t)) y > 0 := fun y hy => by    rw [h_deriv_f y hy]    exact mul_pos (mul_pos (exp_pos _) (by norm_num)) (pow_pos hy 14)  have h_diff : Differentiable ℝ (fun t ↦ exp (t^2) * (S6 t - dawson t)) := by    apply Differentiable.mul (by fun_prop)    apply Differentiable.sub    · unfold S6; fun_prop    · exact differentiable_dawson  have hf_pos : exp (x^2) * (S6 x - dawson x) > 0 :=    pos_of_deriv_pos_of_zero h_diff hf0 h_deriv_pos hx  exact lt_of_sub_pos (pos_of_mul_pos_right hf_pos (exp_pos _).le)