ZetaAppendix.lemma_aachIBP

@[blueprint  "lem:aachIBP"  (title := "Fourier transform of a truncated power law")  (statement := /--Let $s = \sigma + i \tau$, $\sigma\geq 0$, $\tau\in \mathbb{R}$.Let $\nu\in \mathbb{R}\setminus \{0\}$, $b>a>\frac{|\tau|}{2\pi |\nu|}$.Then\begin{equation}\label{eq:aachquno}\int_a^b t^{-s} e(\nu t) dt = \left. \frac{t^{-\sigma} e(\varphi_\nu(t))}{2\pi i \varphi_\nu'(t)}\right|_a^b + \sigma \int_a^b \frac{t^{-\sigma-1}}{2\pi i \varphi_\nu'(t)} e(\varphi_\nu(t)) dt + \int_a^b \frac{t^{-\sigma} \varphi_\nu''(t)}{2\pi i (\varphi_\nu'(t))^2} e(\varphi_\nu(t)) dt,\end{equation}where $\varphi_\nu(t) = \nu t - \frac{\tau}{2\pi} \log t$.-/)  (proof := /--We write $t^{-s} e(\nu t) = t^{-\sigma} e(\varphi_\nu(t))$ and integrate by parts with$u = t^{-\sigma}/(2\pi i \varphi_\nu'(t))$, $v = e(\varphi_\nu(t))$.Here $\varphi_\nu'(t) = \nu - \tau/(2\pi t)\ne 0$ for $t\in [a,b]$ because$t\geq a > |\tau|/(2\pi |\nu|)$ implies $|\nu|>|\tau|/(2\pi t)$.Clearly\[u dv = \frac{ t^{-\sigma}}{2\pi i \varphi_\nu'(t)} \cdot 2\pi i \varphi_\nu'(t)  e(\varphi_\nu(t)) dt = t^{-\sigma} e(\varphi_\nu(t)) dt,\]while\[du = \left(\frac{-\sigma t^{-\sigma-1}}{2\pi i \varphi_\nu'(t)}  - \frac{t^{-\sigma} \varphi_\nu''(t)}{2\pi i (\varphi_\nu'(t))^2}\right) dt.\]-/)  (latexEnv := "lemma")  (discussion := 546)]theorem lemma_aachIBP (s : ℂ) (ν : ℝ) (hν : ν ≠ 0) (a b : ℝ)    (ha : a > |s.im| / (2 * π * |ν|)) (hb : b > a) :    let φ : ℝ → ℝ := fun t ↦ ν * t - (s.im / (2 * π)) * Real.log t    let Φ : ℝ → ℂ := fun t ↦      (t ^ (-s.re) : ℝ) * e (φ t) / (2 * π * I * (deriv φ t))    ∫ t in Set.Icc a b, t ^ (-s) * e (ν * t) = Φ b - Φ a +      (s.re * ∫ t in Set.Icc a b,        (t ^ (-s.re - 1) : ℝ) / (2 * π * I * (deriv φ t)) * e (φ t)) +      ∫ t in Set.Icc a b, (t ^ (-s.re) : ℝ) * (deriv (deriv φ) t) /        (2 * π * I * (deriv φ t) ^ 2) * e (φ t) := by  have ha_pos : 0 < a := lt_of_le_of_lt (div_nonneg (abs_nonneg _) (by positivity)) ha  intro φ Φ  have hIcc_pos : Set.Icc a b ⊆ Set.Ioi 0 := fun t ht ↦ lt_of_lt_of_le ha_pos ht.1  have h_lhs : ∫ t in Set.Icc a b, t ^ (-s) * e (ν * t) =      ∫ t in Set.Icc a b, (t ^ (-s.re) : ℝ) * e (φ t) := by    refine setIntegral_congr_fun measurableSet_Icc ?_    intro t ht    simpa [φ] using phase_rewrite t s ν (hIcc_pos ht)  rw [h_lhs]  have h_phi_ne : ∀ t ∈ Set.Icc a b, deriv φ t ≠ 0 := by    intro t ht    exact phi_deriv_ne_zero s ν a t ha ha_pos hν ht.1  have hsmooth : ContDiffOn ℝ 2 φ (Set.Ioi 0) := by    simp only [φ]    apply ContDiffOn.sub    · fun_prop    · apply ContDiffOn.mul contDiffOn_const      exact contDiffOn_log.mono (fun x hx ↦ ne_of_gt hx)  have h_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ φ t :=    fun t ht ↦ (hsmooth.differentiableOn (by norm_num)).differentiableAt      (Ioi_mem_nhds (hIcc_pos ht))  have h_diff2 : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ (deriv φ) t := by    intro t ht    have h := hsmooth.contDiffAt (Ioi_mem_nhds (hIcc_pos ht))    have h1 : ContDiffAt ℝ 1 (deriv φ) t := h.derivWithin (by norm_num)    exact h1.differentiableAt (by norm_num)  have h_cont : ContinuousOn φ (Set.Icc a b) :=    (hsmooth.mono (fun x hx ↦ lt_of_lt_of_le ha_pos hx.1)).continuousOn  have h_deriv_cont : ContinuousOn (fun t ↦ deriv φ t) (Set.Icc a b) := by    have h1 : ContinuousOn (deriv φ) (Set.Ioi 0) :=      hsmooth.continuousOn_deriv_of_isOpen isOpen_Ioi (by norm_num)    exact h1.mono (fun x hx ↦ lt_of_lt_of_le ha_pos hx.1)  have h_deriv2_cont : ContinuousOn (fun t ↦ deriv (deriv φ) t) (Set.Icc a b) := by    have h1 : ContDiffOn ℝ 1 (deriv φ) (Set.Ioi 0) :=      ((contDiffOn_succ_iff_deriv_of_isOpen isOpen_Ioi).mp hsmooth).2.2    exact (h1.continuousOn_deriv_of_isOpen isOpen_Ioi (by norm_num)).mono      (fun x hx ↦ lt_of_lt_of_le ha_pos hx.1)  exact integral_power_phase_ibp s.re φ a b hb ha_pos h_phi_ne h_diff h_diff2    h_cont h_deriv_cont h_deriv2_cont