ZetaAppendix.second_ibp_limit_eq_neg_B1_integral_on_unit

lemma second_ibp_limit_eq_neg_B1_integral_on_unit {u v : ℝ}    (huv : u ≤ v) (hu_pos : 0 < u) (m : ℕ)    (hmu : (m : ℝ) ≤ u) (hvm : v ≤ (m + 1 : ℝ)) (s : ℂ) :    deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) v *        (((-(Int.fract v ^ 2 - Int.fract v + 1 / 6) / 2) : ℝ) : ℂ) -      deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) u *        (((-(Int.fract u ^ 2 - Int.fract u + 1 / 6) / 2) : ℝ) : ℂ) -      ∫ y in u..v,        (s * (s + 1) * (y : ℂ) ^ (-s - 2)) *          (((-(Int.fract y ^ 2 - Int.fract y + 1 / 6) / 2) : ℝ) : ℂ) =        -(∫ y in u..v,          deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y * ((B1 y : ℝ) : ℂ)) := by  let H : ℝ → ℂ := fun y ↦ deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y  let W : ℝ → ℂ := fun y ↦    (((-(Int.fract y ^ 2 - Int.fract y + 1 / 6) / 2) : ℝ) : ℂ)  let H' : ℝ → ℂ := fun y ↦ s * (s + 1) * (y : ℂ) ^ (-s - 2)  let W' : ℝ → ℂ := fun y ↦ (((-B1 y) : ℝ) : ℂ)  have hIoo_to_unit :      ∀ {x : ℝ}, x ∈ Set.Ioo (min u v) (max u v) →        x ∈ Set.Ioo (m : ℝ) (m + 1 : ℝ) := by    intro x hx    rw [min_eq_left huv, max_eq_right huv] at hx    exact ⟨lt_of_le_of_lt hmu hx.1, lt_of_lt_of_le hx.2 hvm⟩  have h_ibp :      ∫ y in u..v, H y * W' y =        H v * W v - H u * W u - ∫ y in u..v, H' y * W y := by    exact intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivAt      (by        simpa [H, Set.uIcc_of_le huv] using          (Complex.continuousOn_deriv_ofReal_cpow_neg (s := s) (a := u) (b := v) hu_pos))      (by        exact continuous_bernoulli2_primitive.continuousOn)      (by        intro x hx        rw [min_eq_left huv, max_eq_right huv] at hx        have hx_pos : 0 < x := lt_trans hu_pos hx.1        simpa [H, H'] using hasDerivAt_deriv_ofReal_cpow_neg s hx_pos)      (by        intro x hx        simpa [W, W'] using hasDerivAt_bernoulli2_primitive_of_mem_Ioo m          (hIoo_to_unit hx))      (by        have hcont : ContinuousOn H' (Set.uIcc u v) := by          simpa [H', Set.uIcc_of_le huv] using            (continuousOn_second_deriv_ofReal_cpow_neg (s := s) (a := u) (b := v) hu_pos)        exact hcont.intervalIntegrable)      (by        have hB1 := intervalIntegrable_B1_complex (le_of_lt hu_pos) huv        simpa [W'] using! hB1.neg)  have hleft :      ∫ y in u..v, H y * W' y =        -(∫ y in u..v, H y * ((B1 y : ℝ) : ℂ)) := by    rw [← intervalIntegral.integral_neg]    apply intervalIntegral.integral_congr    intro y    simp [W']  calc    deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) v * W v -        deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) u * W u -        ∫ y in u..v, H' y * W y        = ∫ y in u..v, H y * W' y := by          simpa [H, W, H'] using h_ibp.symm    _ = -(∫ y in u..v, H y * ((B1 y : ℝ) : ℂ)) := hleft