ZetaAppendix.cosine_integral_by_parts_cpow

lemma cosine_integral_by_parts_cpow {a b : ℝ} (ha : 0 < a) (hab : a < b)    (s : ℂ) (n : ℕ) :    2 * ∫ y in a..b, (y : ℂ) ^ (-s) *        Real.cos (2 * Real.pi * (n + 1 : ℝ) * y) =      (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  let u : ℝ → ℂ := fun y ↦ (y : ℂ) ^ (-s)  let v : ℝ → ℂ := fun y ↦    ((Real.sin (2 * Real.pi * (n + 1 : ℝ) * y) /      (Real.pi * (n + 1 : ℝ))) : ℂ)  let u' : ℝ → ℂ := deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s))  let v' : ℝ → ℂ := fun y ↦    ((2 * Real.cos (2 * Real.pi * (n + 1 : ℝ) * y)) : ℂ)  have hIoo_to_Icc :      ∀ {x : ℝ}, x ∈ Set.Ioo (min a b) (max a b) → x ∈ Set.Icc a b := by    intro x hx    rw [min_eq_left hab.le, max_eq_right hab.le] at hx    exact Set.Ioo_subset_Icc_self hx  have h_ibp :      ∫ y in a..b, u y * v' y =        u b * v b - u a * v a - ∫ y in a..b, u' y * v y := by    exact intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivAt      (by        simpa [u, Set.uIcc_of_le hab.le] using          (Complex.continuousOn_ofReal_cpow (r := -s) (a := a) (b := b) ha))      (by        simp only [ofReal_sin, ofReal_mul, ofReal_ofNat, ofReal_add, ofReal_natCast, ofReal_one,          Set.uIcc_of_le hab.le, v]        fun_prop)      (by        intro x hx        have hx_pos : 0 < x := lt_of_lt_of_le ha (hIoo_to_Icc hx).1        have hdiff : DifferentiableAt ℝ (fun t : ℝ ↦ (t : ℂ) ^ (-s)) x := by          by_cases hs : s = 0          · simp [hs]          · exact DifferentiableAt.ofReal_cpow_const              (f := fun x : ℝ ↦ x) (c := -s) differentiableAt_id hx_pos.ne'              (neg_ne_zero.mpr hs)        simpa [u, u'] using hdiff.hasDerivAt)      (by        intro x _hx        simpa [v, v'] using hasDerivAt_sine_antideriv n x)      (by        have hcont : ContinuousOn u' (Set.uIcc a b) := by          simpa [u', Set.uIcc_of_le hab.le] using            (Complex.continuousOn_deriv_ofReal_cpow_neg (s := s) (a := a) (b := b) ha)        exact hcont.intervalIntegrable)      (by        apply ContinuousOn.intervalIntegrable        simp only [ofReal_cos, ofReal_mul, ofReal_ofNat, ofReal_add, ofReal_natCast, ofReal_one,          Set.uIcc_of_le hab.le, v']        fun_prop)  have h_lhs :      ∫ y in a..b, u y * v' y =        2 * ∫ y in a..b, (y : ℂ) ^ (-s) *          Real.cos (2 * Real.pi * (n + 1 : ℝ) * y) := by    rw [← intervalIntegral.integral_const_mul]    apply intervalIntegral.integral_congr    intro y _hy    simp [u, v']    ring  simpa [u, v, u'] using h_lhs.symm.trans h_ibp