ZetaAppendix.deriv_kernel_integral_by_parts_cpow

lemma deriv_kernel_integral_by_parts_cpow {a b : ℝ} (ha : 0 < a) (hab : a < b)    (s : ℂ) (n : ℕ) :    ∫ y in a..b,        deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y *          ((Real.sin (2 * Real.pi * (n + 1 : ℝ) * y) /            (Real.pi * (n + 1 : ℝ))) : ℂ) =      deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) b *          ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * b) /            (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ) -        deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) a *          ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * a) /            (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ) -        ∫ 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)) : ℂ) := by  let u : ℝ → ℂ := fun y ↦ deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y  let v : ℝ → ℂ := fun y ↦    ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * y) /      (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ)  let u' : ℝ → ℂ := fun y ↦ s * (s + 1) * (y : ℂ) ^ (-s - 2)  let v' : ℝ → ℂ := fun y ↦    ((Real.sin (2 * Real.pi * (n + 1 : ℝ) * y) /      (Real.pi * (n + 1 : ℝ))) : ℂ)  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_deriv_ofReal_cpow_neg (s := s) (a := a) (b := b) ha))      (by        simp only [ofReal_cos, 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        simpa [u, u'] using hasDerivAt_deriv_ofReal_cpow_neg s hx_pos)      (by        intro x _hx        simpa [v, v'] using hasDerivAt_cos_antideriv n x)      (by        have hcont : ContinuousOn u' (Set.uIcc a b) := by          simpa [u', Set.uIcc_of_le hab.le] using            (continuousOn_second_deriv_ofReal_cpow_neg (s := s) (a := a) (b := b) ha)        exact hcont.intervalIntegrable)      (by        apply ContinuousOn.intervalIntegrable        simp only [ofReal_sin, ofReal_mul, ofReal_ofNat, ofReal_add, ofReal_natCast, ofReal_one,          Set.uIcc_of_le hab.le, v']        fun_prop)  simpa [u, v, u', v'] using h_ibp