ZetaAppendix.lemma_abadusepoisson_from_deriv_kernel

lemma lemma_abadusepoisson_from_deriv_kernel {a b : ℝ}    (ha : ¬∃ n : ℤ, a = n) (hb : ¬∃ n : ℤ, b = n)    (hab : b > a) (ha' : 0 < a) {s : ℂ} (hs1 : s ≠ 1)    (hkernel :      Tendsto        (fun N : ℕ ↦          ∑ n ∈ range N,            ∫ y in a..b,              deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y *                ((Real.sin (2 * Real.pi * (n + 1 : ℝ) * y) /                  (Real.pi * (n + 1 : ℝ))) : ℂ))        atTop        (𝓝 (-(∫ y in a..b,          deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y * B1 y)))) :    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  dsimp only  let L : ℂ :=    (a : ℂ) ^ (-s) * B1 a - (b : ℂ) ^ (-s) * B1 b +      ∫ y in a..b, deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y * B1 y  refine ⟨L, ?_, ?_⟩  · have hboundary :=      tendsto_boundary_sine_terms (le_of_lt ha')        (le_of_lt (lt_trans ha' hab)) ha hb s    have htendsto := hboundary.sub hkernel    refine htendsto.congr' ?_ |>.trans_eq ?_    · filter_upwards with N      simpa using        (fourier_partial_sum_eq_boundary_sub_deriv_kernel          (s := s) (a := a) (b := b) ha' hab N).symm    · simp [L, sub_eq_add_neg, add_assoc]  · have hfinite := finite_euler_cpow_neg (a := a) (b := b) ha' hab s    have hmain := integral_cpow_neg_eq_main (a := a) (b := b) ha' hab hs1    calc      ∑ n ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, (n : ℂ) ^ (-s)          = (a : ℂ) ^ (-s) * B1 a - (b : ℂ) ^ (-s) * B1 b +              (∫ t in a..b, (t : ℂ) ^ (-s)) +              ∫ t in a..b, deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) t * B1 t := hfinite      _ = ((b ^ (1 - s) : ℂ) - (a ^ (1 - s) : ℂ)) / (1 - s) + L := by        rw [hmain]        simp [L, add_left_comm, add_assoc]