MellinOfSmooth1c

@[blueprint  (title := "MellinOfSmooth1c")  (statement := /--  At $s=1$, we have  $$\mathcal{M}(\widetilde{1_{\epsilon}})(1) = 1+O(\epsilon)).$$  -/)  (proof := /--  Follows from Lemmas \ref{MellinOfSmooth1a}, \ref{MellinOfDeltaSpikeAt1} and  \ref{MellinOfDeltaSpikeAt1_asymp}.  -/)  (latexEnv := "lemma")]lemma MellinOfSmooth1c {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν)    (suppν : ν.support ⊆ Icc (1 / 2) 2)    (mass_one : ∫ x in Ioi 0, ν x / x = 1) :    (fun ε ↦ 𝓜 (fun x ↦ (Smooth1 ν ε x : ℂ)) 1 - 1) =O[𝓝[>]0] id := by  have h := MellinOfDeltaSpikeAt1_asymp diffν suppν mass_one  rw [Asymptotics.isBigO_iff] at h ⊢  obtain ⟨c, hc⟩ := h  use c  filter_upwards [hc, Ioo_mem_nhdsGT (by linarith : (0 : ℝ) < 1)] with ε hε hε'  rw [MellinOfSmooth1a diffν suppν hε'.1 (s := 1) (by norm_num)]  simp only [inv_one, mul_one, one_mul, id_eq, Real.norm_eq_abs]  exact hε