wiener_ikehara_smooth

@[blueprint  "WienerIkeharaSmooth"  (title := "Smoothed Wiener-Ikehara")  (statement := /--    If $\Psi: (0,\infty) \to \C$ is smooth and compactly supported away from the origin, then,  $$ \sum_{n=1}^\infty f(n) \Psi( \frac{n}{x} ) = A x \int_0^\infty \Psi(y)\ dy + o(x)$$  as $x \to \infty$.  -/)  (proof := /--  By Lemma \ref{bij}, we can write  $$ y \Psi(y) = \hat \psi( \frac{1}{2\pi} \log y )$$  for all $y>0$ and some Schwartz function $\psi$.  Making this substitution, the claim is then  equivalent after standard manipulations to  $$ \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} )    = A \int_{-\infty}^\infty \hat \psi(\frac{u}{2\pi})\ du + o(1)$$  and the claim follows from Lemma \ref{schwarz-id}.  -/)  (latexEnv := "corollary")]lemma wiener_ikehara_smooth (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (hcheby : cheby f)    (hG : ContinuousOn G {s | 1 ≤ s.re})    (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re})    (hsmooth : ContDiff ℝ ∞ Ψ) (hsupp : HasCompactSupport Ψ)    (hplus : closure (Function.support Ψ) ⊆ Set.Ioi 0) :    Tendsto (fun x : ℝ ↦ (∑' n, f n * Ψ (n / x)) / x - A * ∫ y in Set.Ioi 0, Ψ y)      atTop (𝓝 0) := by   let h (x : ℝ) : ℂ := rexp (2 * π * x) * Ψ (exp (2 * π * x))  have h1 : ContDiff ℝ ∞ h := by    have : ContDiff ℝ ∞ (fun x : ℝ => (rexp (2 * π * x))) := (contDiff_const.mul contDiff_id).exp    exact (contDiff_ofReal.comp this).mul (hsmooth.comp this)  have h2 : HasCompactSupport h := by    have : 2 * π ≠ 0 := by simp [pi_ne_zero]    simpa using! (comp_exp_support hsupp hplus).comp_smul this |>.mul_left  obtain ⟨g, hg⟩ := fourier_surjection_on_schwartz (toSchwartz h h1 h2)   have l1 {y} (hy : 0 < y) : y * Ψ y = 𝓕 g (1 / (2 * π) * Real.log y) := by    simp only [one_div, mul_inv_rev, hg, toSchwartz, ofReal_exp, ofReal_mul, ofReal_ofNat,      toSchwartz_apply, ofReal_inv, h]    field_simp    norm_cast    rw [Real.exp_log hy]   have key := limiting_cor_schwartz g hf hcheby hG hG'   have l2 : ∀ᶠ x in atTop, ∑' (n : ℕ), f n / ↑n * 𝓕 g (1 / (2 * π) * Real.log (↑n / x)) =      ∑' (n : ℕ), f n * Ψ (↑n / x) / x := by    filter_upwards [eventually_gt_atTop 0] with x hx    congr ; ext n    by_cases hn : n = 0    · simp [hn, (comp_exp_support0 hplus).self_of_nhds]    rw [← l1 (by positivity)]    have : (n : ℂ) ≠ 0 := by simpa using hn    have : (x : ℂ) ≠ 0 := by simpa using hx.ne.symm    simp only [ofReal_div, ofReal_natCast]    field_simp   have l3 : ∀ᶠ x in atTop, ↑A * ∫ (u : ℝ) in Ici (-Real.log x), 𝓕 g (u / (2 * π)) =      ↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y := by    filter_upwards [eventually_gt_atTop 0] with x hx    congr 1    simp only [hg, toSchwartz, ofReal_exp, ofReal_mul, ofReal_ofNat, toSchwartz_apply,      ofReal_div, h]    norm_cast ; field_simp; norm_cast    rw [MeasureTheory.integral_Ici_eq_integral_Ioi]    exact wiener_ikehara_smooth_aux hsmooth.continuous hsupp hplus x hx   have l4 : Tendsto (fun x => (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y)      atTop (𝓝 0) := by    exact wiener_ikehara_smooth_sub (hsmooth.continuous.integrable_of_hasCompactSupport hsupp) hplus   simpa [tsum_div_const] using (key.congr' <| EventuallyEq.sub l2 l3) |>.add l4