MellinOfSmooth1b

@[blueprint  (title := "MellinOfSmooth1b")  (statement := /--  Given $0<\sigma_1\le\sigma_2$, for any $s$ such that $\sigma_1\le\mathcal Re(s)\le\sigma_2$,  we have  $$\mathcal{M}(\widetilde{1_{\epsilon}})(s) = O\left(\frac{1}{\epsilon|s|^2}\right).$$  -/)  (proof := /-- Use Lemma \ref{MellinOfSmooth1a} and the bound in Lemma \ref{MellinOfPsi}. -/)  (latexEnv := "lemma")]lemma MellinOfSmooth1b {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν)    (suppν : ν.support ⊆ Set.Icc (1 / 2) 2) :    ∃ (C : ℝ) (_ : 0 < C), ∀ (σ₁ : ℝ) (_ : 0 < σ₁)    (s) (_ : σ₁ ≤ s.re) (_ : s.re ≤ 2) (ε : ℝ) (_ : 0 < ε) (_ : ε < 1),    ‖𝓜 (fun x ↦ (Smooth1 ν ε x : ℂ)) s‖ ≤ C * (ε * ‖s‖ ^ 2)⁻¹ := by  obtain ⟨C, Cpos, hC⟩ := MellinOfPsi diffν suppν  refine ⟨C, Cpos, ?_⟩  intro σ₁ σ₁pos s hs1 hs2 ε εpos ε_lt_one  rw [MellinOfSmooth1a diffν suppν εpos <| lt_of_le_of_lt' hs1 σ₁pos]  have hh1 : ε * σ₁ ≤ (ε * s).re := by    simp only [mul_re, ofReal_re, ofReal_im, zero_mul, sub_zero]    nlinarith  have hh2 : (ε * s).re ≤ 2 := by    simp only [mul_re, ofReal_re, ofReal_im, zero_mul, sub_zero]    nlinarith  calc    ‖s⁻¹ * 𝓜 (fun x ↦ (ν x : ℂ)) (ε * s)‖ =        ‖s⁻¹‖ * ‖𝓜 (fun x ↦ (ν x : ℂ)) (ε * s)‖ := by simp    _                        ≤ ‖s⁻¹‖ * (C * (ε * ‖s‖)⁻¹) := by      gcongr      convert! hC (ε * σ₁) (by positivity) (ε * s) hh1 hh2      simp [abs_eq_self.mpr εpos.le]    _                        = C * (ε * ‖s‖ ^ 2)⁻¹ := by      simp only [norm_inv, mul_inv_rev]      ring