FKS2.filter_tendsto_dawson_at_top_zero

lemma filter_tendsto_dawson_at_top_zero : Filter.Tendsto dawson Filter.atTop (nhds 0) := by  have h_dawson_le : ∀ x > 0, dawson x ≤ 1 / x := by    intro x hx    have h_deriv : ∀ t, HasDerivAt (fun t ↦ exp (x * t) / x) (exp (x * t)) t := by      intro t      have h := ((hasDerivAt_id t).const_mul x).exp.div_const x      rwa [mul_one, mul_div_cancel_right₀ _ (ne_of_gt hx)] at h    have hc : Continuous (fun t ↦ exp (x * t)) := by fun_prop    have h_int_val : ∫ t in 0..x, exp (x * t) = exp (x * x) / x - exp (x * 0) / x :=      intervalIntegral.integral_eq_sub_of_hasDerivAt (fun t _ ↦ h_deriv t) (hc.intervalIntegrable 0 x)    have h_int_le_exp : ∫ t in 0..x, exp (x * t) ≤ exp (x ^ 2) / x := by      rw [h_int_val, mul_zero, exp_zero, ← sq]      have : 0 ≤ 1 / x := one_div_nonneg.mpr hx.le      linarith    have hc1 : Continuous (fun t : ℝ ↦ exp (t ^ 2)) := continuous_exp.comp (continuous_pow 2)    have h_mono : ∫ t in 0..x, exp (t ^ 2) ≤ ∫ t in 0..x, exp (x * t) := by      refine intervalIntegral.integral_mono_on hx.le (hc1.intervalIntegrable 0 x)        (hc.intervalIntegrable 0 x) (fun t ht ↦ exp_le_exp.mpr ?_)      rw [Set.mem_Icc] at ht      rw [sq, mul_comm x]      exact mul_le_mul_of_nonneg_left ht.2 ht.1    unfold dawson    calc exp (-x ^ 2) * ∫ t in 0..x, exp (t ^ 2)      _ ≤ exp (-x ^ 2) * (exp (x ^ 2) / x) := mul_le_mul_of_nonneg_left (le_trans h_mono h_int_le_exp) (exp_pos _).le      _ = 1 / x := by        rw [show exp (-x ^ 2) * (exp (x ^ 2) / x) = (exp (-x ^ 2) * exp (x ^ 2)) / x by ring]        rw [← exp_add, neg_add_cancel, exp_zero]  apply squeeze_zero'  · filter_upwards [Filter.eventually_gt_atTop (0 : ℝ)] with x hx    exact dawson_nonneg hx.le  · filter_upwards [Filter.eventually_gt_atTop (0 : ℝ)] with x hx    exact h_dawson_le x hx  · simpa only [inv_eq_one_div] using tendsto_inv_atTop_zero