ZetaAppendix.hasSum_second_ibp_integral_series

lemma hasSum_second_ibp_integral_series {a b : ℝ} (ha : 0 < a) (hab : a < b)    (s : ℂ) :    HasSum      (fun n : ℕ ↦        ∫ y in a..b,          (s * (s + 1) * (y : ℂ) ^ (-s - 2)) *            ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * y) /              (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ))      (∫ y in a..b,        (s * (s + 1) * (y : ℂ) ^ (-s - 2)) *          (((-(Int.fract y ^ 2 - Int.fract y + 1 / 6) / 2) : ℝ) : ℂ)) := by  let H : ℝ → ℂ := fun y ↦ s * (s + 1) * (y : ℂ) ^ (-s - 2)  let W : ℕ → ℝ → ℂ := fun n y ↦    ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * y) /      (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ)  let Wlim : ℝ → ℂ := fun y ↦    (((-(Int.fract y ^ 2 - Int.fract y + 1 / 6) / 2) : ℝ) : ℂ)  have hH_cont : ContinuousOn H (Set.uIcc a b) := by    simpa [H, Set.uIcc_of_le hab.le] using      (continuousOn_second_deriv_ofReal_cpow_neg (s := s) (a := a) (b := b) ha)  obtain ⟨C0, hC0⟩ := isCompact_uIcc.exists_bound_of_continuousOn hH_cont  let C : ℝ := max C0 0  have hC_nonneg : 0 ≤ C := le_max_right _ _  have hC : ∀ y ∈ Set.uIcc a b, ‖H y‖ ≤ C := by    intro y hy    exact (hC0 y hy).trans (le_max_left _ _)  have hbase_sum :      Summable fun n : ℕ ↦        C * (1 / (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) :=    summable_one_div_two_pi_sq_nat_add_one_sq.mul_left C  refine intervalIntegral.hasSum_integral_of_dominated_convergence    (μ := volume)    (F := fun n y ↦ H y * W n y)    (f := fun y ↦ H y * Wlim y)    (bound := fun n _y ↦ C * (1 / (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2))) ?_ ?_ ?_ ?_ ?_  · intro n    refine ContinuousOn.aestronglyMeasurable_of_subset_isCompact ?_      isCompact_uIcc measurableSet_uIoc Set.uIoc_subset_uIcc    refine hH_cont.mul ?_    simp only [ofReal_cos, ofReal_mul, ofReal_ofNat, ofReal_add, ofReal_natCast, ofReal_one, W]    fun_prop  · intro n    filter_upwards with y hy    calc      ‖H y * W n y‖ = ‖H y‖ * ‖W n y‖ := norm_mul _ _      _ ≤ C * (1 / (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) := by        exact mul_le_mul (hC y (Set.uIoc_subset_uIcc hy))          (by simpa [W] using cos_antideriv_norm_bound n y)          (by positivity) hC_nonneg  · exact ae_of_all _ fun _y _hy ↦ hbase_sum  · exact intervalIntegrable_const  · refine ae_of_all _ fun y _hy ↦ ?_    simpa [H, W, Wlim] using (hasSum_cos_antideriv_complex y).mul_left (H y)