ZetaAppendix.integral_power_phase_ibp

theorem integral_power_phase_ibp (σ : ℝ) (φ : ℝ → ℝ) (a b : ℝ) (hab : a < b) (ha_pos : 0 < a)    (h_phi_ne : ∀ t ∈ Set.Icc a b, deriv φ t ≠ 0)    (h_phi_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ φ t)    (h_phi_diff2 : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ (deriv φ) t)    (h_phi_cont : ContinuousOn φ (Set.Icc a b))    (h_deriv_cont : ContinuousOn (fun t ↦ deriv φ t) (Set.Icc a b))    (h_deriv2_cont : ContinuousOn (fun t ↦ deriv (deriv φ) t) (Set.Icc a b)) :    let Φ : ℝ → ℂ := fun t ↦ (t ^ (-σ) : ℝ) * e (φ t) / (2 * π * I * (deriv φ t))    ∫ t in Set.Icc a b, (t ^ (-σ) : ℝ) * e (φ t) = Φ b - Φ a +      (σ * ∫ t in Set.Icc a b, (t ^ (-σ - 1) : ℝ) / (2 * π * I * (deriv φ t)) * e (φ t)) +      ∫ t in Set.Icc a b, (t ^ (-σ) : ℝ) * (deriv (deriv φ) t) /        (2 * π * I * (deriv φ t) ^ 2) * e (φ t) := by  intro Φ  have hab_le : a ≤ b := le_of_lt hab  rw [integral_Icc_eq_interval hab_le, integral_Icc_eq_interval hab_le,    integral_Icc_eq_interval hab_le]  let u : ℝ → ℂ := fun t ↦ ((t ^ (-σ) : ℝ) : ℂ) / (2 * π * I * ↑(deriv φ t))  let v : ℝ → ℂ := fun t ↦ e (φ t)  let u' : ℝ → ℂ := fun t ↦ ((-σ * t ^ (-σ - 1) : ℝ) : ℂ) / (2 * π * I * ↑(deriv φ t)) +      ((t ^ (-σ) : ℝ) : ℂ) * (-↑(deriv (deriv φ) t) / (2 * π * I * ↑(deriv φ t) ^ 2))  let v' : ℝ → ℂ := fun t ↦ 2 * π * I * ↑(deriv φ t) * e (φ t)  have h_uv_eq_Phi : ∀ t, u t * v t = Φ t := by    intro t    simp only [u, v, Φ]    ring_nf  have h_lhs : ∫ x in a..b, ((x ^ (-σ) : ℝ) : ℂ) * e (φ x) =      ∫ x in a..b, u x * v' x := by    apply intervalIntegral.integral_congr    intro x hx    rw [uIcc_of_le hab_le] at hx    simp only [u, v']    field_simp [h_phi_ne x hx]  rw [h_lhs]  have h_ibp : (∫ x in a..b, u x * v' x) = u b * v b - u a * v a - ∫ x in a..b, u' x * v x := by    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 Ioo_subset_Icc_self hx    exact intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivAt      (by        rw [uIcc_of_le hab_le]        exact ContinuousOn.div          (continuousOn_rpow_toComplex a b (-σ) ha_pos)          (continuousOn_denom1 φ a b h_deriv_cont)          (denom1_ne_zero φ a b h_phi_ne))      (by        rw [uIcc_of_le hab_le]        exact continuousOn_e_comp φ _ h_phi_cont)      (by        intro x hx        have hx_in : x ∈ Set.Icc a b := hIoo_to_Icc hx        have hx_pos : 0 < x := lt_of_lt_of_le ha_pos hx_in.1        exact hasDerivAt_u_full σ φ x hx_pos (h_phi_diff2 x hx_in) (h_phi_ne x hx_in))      (by        intro x hx        exact hasDerivAt_e_comp φ x (h_phi_diff x (hIoo_to_Icc hx)))      (by simpa [u'] using        intervalIntegrable_u' σ φ a b hab_le ha_pos h_deriv_cont h_deriv2_cont h_phi_ne)      (by simpa [v'] using intervalIntegrable_v' φ a b hab_le h_phi_cont h_deriv_cont)  rw [h_ibp]  simp only [h_uv_eq_Phi, sub_eq_add_neg, ← intervalIntegral.integral_neg, add_assoc]  congr 1  have h_cong : ∫ x in a..b, -(u' x * v x) =      ∫ x in a..b,        (σ * (((x ^ (-σ - 1) : ℝ) : ℂ) / (2 * π * I * ↑(deriv φ x)) * e (φ x)) +          ((x ^ (-σ) : ℝ) : ℂ) * ↑(deriv (deriv φ) x) /            (2 * π * I * ↑(deriv φ x) ^ 2) * e (φ x)) := by    apply intervalIntegral.integral_congr    intro x hx    simp only [u', v]    rw [neg_mul, show (↑(-(σ * x ^ (-σ - 1))) : ℂ) = -((↑σ : ℂ) * ↑(x ^ (-σ - 1))) by norm_cast]    ring_nf  have h_int_term1 : IntervalIntegrable      (fun x ↦ ((x ^ (-σ - 1) : ℝ) : ℂ) / (2 * π * I * ↑(deriv φ x)) * e (φ x)) volume a b :=    intervalIntegrable_term1 σ φ a b hab_le ha_pos h_phi_cont h_deriv_cont h_phi_ne  have h_int_term2 : IntervalIntegrable      (fun x ↦ ((x ^ (-σ) : ℝ) : ℂ) * ↑(deriv (deriv φ) x) /        (2 * π * I * ↑(deriv φ x) ^ 2) * e (φ x)) volume a b :=    intervalIntegrable_term2 σ φ a b hab_le ha_pos h_phi_cont h_deriv_cont h_deriv2_cont h_phi_ne  rw [h_cong, intervalIntegral.integral_add (h_int_term1.const_mul σ) h_int_term2,      intervalIntegral.integral_const_mul, sub_eq_add_neg]