limiting_fourier

@[blueprint  "limiting"  (title := "Limiting Fourier identity")  (statement := /--  If $\psi: \R \to \C$ is $C^2$ and compactly supported and $x \geq 1$, then  $$ \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} )    - A \int_{-\log x}^\infty \hat \psi(\frac{u}{2\pi})\ du    = \int_\R G(1+it) \psi(t) x^{it}\ dt.$$  -/)  (proof := /--  By Lemma \ref{first-fourier} and Lemma \ref{second-fourier}, we know that for any $\sigma>1$,  we have  $$ \sum_{n=1}^\infty \frac{f(n)}{n^\sigma} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} )    - A x^{1-\sigma} \int_{-\log x}^\infty e^{-u(\sigma-1)} \hat \psi(\frac{u}{2\pi})\ du    = \int_\R G(\sigma+it) \psi(t) x^{it}\ dt.$$  Now take limits as $\sigma \to 1$ using dominated convergence together with \eqref{cheby}  and Lemma \ref{decay} to obtain the result.  -/)  (latexEnv := "lemma")]lemma limiting_fourier (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})    (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (ψ : CS 2 ℂ) (hx : 1 ≤ x) :    ∑' n, f n / n * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * π) * log (n / x)) -      A * ∫ u in Set.Ici (-log x), 𝓕 (ψ : ℝ → ℂ) (u / (2 * π)) =      ∫ (t : ℝ), (G (1 + t * I)) * (ψ t) * x ^ (t * I) := by   have l1 := limiting_fourier_lim1 hcheby ψ (by linarith)  have l2 := limiting_fourier_lim2 A ψ hx  have l3 := limiting_fourier_lim3 hG ψ hx  apply tendsto_nhds_unique_of_eventuallyEq (l1.sub l2) l3  simpa [eventuallyEq_nhdsWithin_iff] using! Eventually.of_forall (limiting_fourier_aux hG' hf ψ hx)