ZetaAppendix.lemma_aachcanc

@[blueprint  "lem:aachcanc"  (title := "Estimating an sum")  (statement := /--Let $s = \sigma + i \tau$, $\sigma,\tau \in \mathbb{R}$.Let $n\in \mathbb{Z}_{>0}$. Let $a,b\in \mathbb{Z} + \frac{1}{2}$,$b>a>\frac{|\tau|}{2\pi n}$.Write $\varphi_\nu(t) = \nu t - \frac{\tau}{2\pi} \log t$.Then\[\frac{1}{2} \sum_{\nu = \pm n}  \left. \frac{t^{-\sigma} e(\varphi_\nu(t))}{2\pi i \varphi_\nu'(t)}\right|_a^b =  \left. \frac{(-1)^n t^{-s} \cdot \frac{\tau}{2\pi t}}  {2\pi i \left(n^2 - \left(\frac{\tau}{2\pi t}\right)^2\right)}\right|_a^b.\]-/)  (proof := /--Since $e(\varphi_\nu(t)) = e(\nu t) t^{-i \tau} = (-1)^{\nu} t^{-i \tau}$ for anyhalf-integer $t$ and any integer $\nu$,\[\left. \frac{t^{-\sigma} e(\varphi_\nu(t))}{2\pi i \varphi_\nu'(t)}\right|_a^b =\left. \frac{(-1)^{\nu} t^{-s}}{2\pi i \varphi_\nu'(t)}\right|_a^b\]for $\nu = \pm n$. Clearly $(-1)^{\nu} = (-1)^n$.Since $\varphi_\nu'(t) = \nu - \alpha$ for $\alpha = \frac{\tau}{2\pi t}$,\[\frac{1}{2} \sum_{\nu = \pm n} \frac{1}{\varphi_\nu'(t)} = \frac{1/2}{n - \alpha} +\frac{1/2}{- n - \alpha} = \frac{-\alpha}{\alpha^2-n^2} = \frac{\alpha}{n^2-\alpha^2}.\]-/)  (latexEnv := "lemma")  (discussion := 551)]theorem lemma_aachcanc (s : ℂ) {n : ℤ} (hn : 0 < n) {a b : ℝ}    (ha : a > |s.im| / (2 * π * n)) (hb : b > a)    (ha' : a.IsHalfInteger) (hb' : b.IsHalfInteger) :    let ϕ : ℝ → ℝ → ℝ := fun ν t ↦ ν * t - (s.im / (2 * π)) * Real.log t    let Φ : ℝ → ℝ → ℂ := fun ν t ↦      (t ^ (-s.re) : ℝ) * e (ϕ ν t) / (2 * π * I * (deriv (ϕ ν) t))    let Ψ : ℝ → ℂ := fun t ↦ (-1) ^ n * (t ^ (-s) : ℂ) * (s.im / (2 * π * t)) /      (2 * π * I * (n ^ 2 - (s.im / (2 * π * t)) ^ 2))    (1 / 2) * (Φ n b - Φ n a + Φ (-n) b - Φ (-n) a) = Ψ b - Ψ a := by  intro phi Φ Ψ  have h_apply : ∀ t : ℝ, t > |s.im| / (2 * .pi * n) → t.IsHalfInteger → t > 0 →      (1 / 2) * (Φ n t + Φ (-n) t) = Ψ t := by    intro t ht ht' ht''    have h_bound : |s.im| < t * (2 * .pi * n) := by      rw [gt_iff_lt] at ht; exact (div_lt_iff₀ (by positivity)).mp ht    convert lemma_aachcanc_pointwise s (show n ≠ 0 by linarith) t ht' ht'' ?_ ?_ ?_ using 1    all_goals norm_num [mul_comm]    · norm_num [ht''.ne', pi_ne_zero, mul_comm]      field_simp      cases abs_cases s.im <;> nlinarith [pi_pos, h_bound]    · norm_num [ht''.ne', Real.differentiableAt_log]      field_simp      cases abs_cases s.im <;> nlinarith [pi_pos, h_bound]    · rw [sub_eq_zero, eq_comm]      norm_num [div_pow, ← mul_assoc, Complex.ext_iff]      norm_cast      norm_num      rw [div_eq_iff (by positivity)]      rw [abs_lt] at h_bound      nlinarith [pi_pos]  have hb_pos : b > 0 := lt_trans (lt_of_le_of_lt (by positivity) ha) hb  trans (1 / 2) * (Φ n b + Φ (-n) b) - (1 / 2) * (Φ n a + Φ (-n) a)  · ring  rw [h_apply b (lt_trans ha hb) hb' hb_pos, h_apply a ha ha' (lt_of_le_of_lt (by positivity) ha)]