FKS2.S5_lt_dawson

lemma S5_lt_dawson (x : ℝ) (hx : x > 0) : S5 x < dawson x := by  have hf0 : exp (0^2) * (dawson 0 - S5 0) = 0 := by    unfold S5 dawson    simp  have h_deriv_f : ∀ y > 0, deriv (fun t ↦ exp (t^2) * (dawson t - S5 t)) y =      exp (y^2) * (64 / 10395) * y^12 := 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 (h_dawson.sub (hasDerivAt_S5 y))    change deriv ((fun t ↦ exp (t^2)) * (dawson - S5)) y = exp (y^2) * (64 / 10395) * y^12    rw [h_comb.deriv]    change 2 * y * exp (y^2) * (dawson y - S5 y) +      exp (y^2) *        (1 - 2 * y * dawson y - (1 - 2 * y^2 + 4/3 * y^4 - 8/15 * y^6 + 16/105 * y^8 - 32/945 * y^10)) =      exp (y^2) * (64 / 10395) * y^12    unfold S5    ring  have h_deriv_pos : ∀ y > 0, deriv (fun t ↦ exp (t^2) * (dawson t - S5 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 12)  have h_diff : Differentiable ℝ (fun t ↦ exp (t^2) * (dawson t - S5 t)) := by    apply Differentiable.mul (by fun_prop)    apply Differentiable.sub    · exact differentiable_dawson    · unfold S5; fun_prop  have hf_pos : exp (x^2) * (dawson x - S5 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)