ZetaAppendix.fourier_partial_sum_eq_boundary_sub_deriv_kernel

lemma fourier_partial_sum_eq_boundary_sub_deriv_kernel (s : ℂ) {a b : ℝ}    (ha : 0 < a) (hab : a < b) (N : ℕ) :    let f : ℝ → ℂ := fun y ↦      if a ≤ y ∧ y ≤ b then (y ^ (-s.re) : ℝ) * e (-(s.im / (2 * π)) * Real.log y) else 0    ∑ n ∈ Icc 1 N, (FourierTransform.fourier f n + FourierTransform.fourier f (-n)) =      ((b : ℂ) ^ (-s) *          ((∑ n ∈ range N,            Real.sin (2 * Real.pi * (n + 1 : ℝ) * b) /              (Real.pi * (n + 1 : ℝ))) : ℂ) -        (a : ℂ) ^ (-s) *          ((∑ n ∈ range N,            Real.sin (2 * Real.pi * (n + 1 : ℝ) * a) /              (Real.pi * (n + 1 : ℝ))) : ℂ)) -        ∑ 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 : ℝ))) : ℂ) := by  dsimp only  rw [fourier_partial_sum_eq_range_cos (s := s) (a := a) (b := b) ha hab N]  calc    ∑ n ∈ range N,        2 * ∫ y in a..b, (y : ℂ) ^ (-s) *          Real.cos (2 * Real.pi * (n + 1 : ℝ) * y)        = ∑ n ∈ range N,          ((b : ℂ) ^ (-s) *              ((Real.sin (2 * Real.pi * (n + 1 : ℝ) * b) /                (Real.pi * (n + 1 : ℝ))) : ℂ) -            (a : ℂ) ^ (-s) *              ((Real.sin (2 * Real.pi * (n + 1 : ℝ) * a) /                (Real.pi * (n + 1 : ℝ))) : ℂ) -            ∫ y in a..b,              deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y *                ((Real.sin (2 * Real.pi * (n + 1 : ℝ) * y) /                  (Real.pi * (n + 1 : ℝ))) : ℂ)) := by          apply sum_congr rfl          intro n _hn          exact cosine_integral_by_parts_cpow ha hab s n    _ = ((b : ℂ) ^ (-s) *          ((∑ n ∈ range N,            Real.sin (2 * Real.pi * (n + 1 : ℝ) * b) /              (Real.pi * (n + 1 : ℝ))) : ℂ) -        (a : ℂ) ^ (-s) *          ((∑ n ∈ range N,            Real.sin (2 * Real.pi * (n + 1 : ℝ) * a) /              (Real.pi * (n + 1 : ℝ))) : ℂ)) -        ∑ 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 : ℝ))) : ℂ) := by          simp [sum_sub_distrib, mul_sum]