ZetaAppendix.lemma_abadusepoisson

@[blueprint  "lem:abadusepoisson"  (title := "Poisson summation for a partial sum of $\\zeta(s)$")  (statement := /--Let $a,b\in \mathbb{R}\setminus \mathbb{Z}$, $b>a>0$. Let $s\in \mathbb{C}\setminus \{1\}$.Define $f:\mathbb{R}\to\mathbb{C}$ by $f(y) = 1_{[a,b]}(y)/y^s$. Then$$\sum_{a < n\leq b} \frac{1}{n^s} = \frac{b^{1-s} - a^{1-s}}{1-s}  + \lim_{N\to \infty} \sum_{n=1}^N (\widehat{f}(n) + \widehat{f}(-n)).$$-/)  (proof := /--Since $a\notin \mathbb{Z}$, $\sum_{a < n\leq b} \frac{1}{n^s} = \sum_{n\in \mathbb{Z}} f(n)$.By Poisson summation (as in \cite[Thm.~D.3]{MR2378655})$$\sum_{n\in \mathbb{Z}} f(n) = \lim_{N\to \infty} \sum_{n=-N}^N \widehat{f}(n) =\widehat{f}(0) + \lim_{N\to \infty} \sum_{n=1}^N (\widehat{f}(n) + \widehat{f}(-n)),$$where we use the facts that $f$ is in $L^1$, of bounded variation, and(by $a,b\not\in \mathbb{Z}$) continuous at every integer. Now$$\widehat{f}(0) = \int_{\mathbb{R}} f(y) dy  = \int_a^b \frac{dy}{y^s} = \frac{b^{1-s}-a^{1-s}}{1-s}.$$-/)  (latexEnv := "lemma")  (discussion := 568)]theorem lemma_abadusepoisson {a b : ℝ} (ha : ¬∃ n : ℤ, a = n) (hb : ¬∃ n : ℤ, b = n)    (hab : b > a) (ha' : 0 < a) {s : ℂ} (hs1 : s ≠ 1) :    let f : ℝ → ℂ := fun y ↦      if a ≤ y ∧ y ≤ b then (y ^ (-s.re) : ℝ) * e (-(s.im / (2 * π)) * Real.log y) else 0    ∃ L : ℂ, Filter.atTop.Tendsto      (fun (N : ℕ) ↦ ∑ n ∈ Icc 1 N,        (FourierTransform.fourier f n + FourierTransform.fourier f (-n))) (nhds L) ∧      ∑ n ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, (n : ℂ) ^ (-s) =        ((b ^ (1 - s) : ℂ) - (a ^ (1 - s) : ℂ)) / (1 - s) + L := by  exact lemma_abadusepoisson_from_deriv_kernel ha hb hab ha' hs1 (tendsto_deriv_kernel_to_neg_B1 (a := a) (b := b) ha' hab s)