Smooth1MellinConvergent

lemma Smooth1MellinConvergent {Ψ : ℝ → ℝ} {ε : ℝ} (diffΨ : ContDiff ℝ 1 Ψ)    (suppΨ : Ψ.support ⊆ Icc (1 / 2) 2) (hε : ε ∈ Ioo 0 1)    (Ψnonneg : ∀ x > 0, 0 ≤ Ψ x) (mass_one : ∫ x in Ioi 0, Ψ x / x = 1)    {s : ℂ} (hs : 0 < s.re) : MellinConvergent (fun x ↦ (Smooth1 Ψ ε x : ℂ)) s := by  apply mellinConvergent_of_isBigO_rpow_exp zero_lt_one _ _ _ hs  · apply ContinuousOn.locallyIntegrableOn _ (by measurability)    apply continuousOn_of_forall_continuousAt    exact fun x hx ↦ Smooth1ContinuousAt diffΨ Ψnonneg suppΨ hε.1 hx |>.ofReal  · rw [Asymptotics.isBigO_iff]    use 1    obtain ⟨c, cpos, ceq, hc⟩ := Smooth1Properties_above suppΨ    filter_upwards [eventually_ge_atTop (1 + c * ε)] with x hx    rw [hc _ _ hε hx]    simp only [ofReal_zero, norm_zero, neg_mul, one_mul, norm_eq_abs, abs_exp]    bound  · rw [Asymptotics.isBigO_iff]    use 1    filter_upwards [eventually_mem_nhdsWithin] with x hx    simp only [norm_real, norm_eq_abs, neg_zero, rpow_zero, one_mem, CStarRing.norm_of_mem_unitary,      mul_one]    rw [_root_.abs_of_nonneg <| Smooth1Nonneg Ψnonneg hx hε.1]    exact Smooth1LeOne Ψnonneg mass_one hε.1 hx