ZetaSum_aux1

@[blueprint  (title := "ZetaSum-aux1")  (statement := /--  Let $0 < a < b$ be natural numbers and $s\in \C$ with $s \ne 1$ and $s \ne 0$.  Then  \[  \sum_{a < n \le b} \frac{1}{n^s} =  \frac{b^{1-s} - a^{1-s}}{1-s} + \frac{b^{-s}-a^{-s}}{2}    + s \int_a^b \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx.  \]  -/)  (proof := /-- Apply Lemma \ref{sum_eq_int_deriv} to the function $x \mapsto x^{-s}$. -/)  (latexEnv := "lemma")]lemma ZetaSum_aux1 {a b : ℕ} {s : ℂ} (s_ne_one : s ≠ 1) (s_ne_zero : s ≠ 0) (ha : a ∈ Ioo 0 b) :    ∑ n ∈ Finset.Ioc a b, 1 / (n : ℂ) ^ s =    (b ^ (1 - s) - a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / b ^ (s)) - 1 / 2 * (1 / a ^ s)      + s * ∫ x in a..b, (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1)) := by  let φ := fun (x : ℝ) ↦ 1 / (x : ℂ) ^ s  let φ' := fun (x : ℝ) ↦ -s * (x : ℂ) ^ (-(s + 1))  have xpos : ∀ x ∈ [[(a : ℝ), b]], 0 < x := fun x hx ↦ xpos_of_uIcc ha hx  have φDiff : ∀ x ∈ [[(a : ℝ), b]], HasDerivAt φ (deriv φ x) x :=    fun x hx ↦ ZetaSum_aux1φDiff (xpos x hx)  have φderiv : ∀ x ∈ [[(a : ℝ), b]], deriv φ x = φ' x := by    exact fun x hx ↦ ZetaSum_aux1φderiv s_ne_zero (xpos x hx)  have derivφCont : ContinuousOn (deriv φ) [[a, b]] := ZetaSum_aux1derivφCont s_ne_zero ha  convert sum_eq_int_deriv (by linarith) (by exact_mod_cast ha.2) φDiff derivφCont using 1  · congr <;> simp only [Nat.floor_natCast]  · rw [Nat.floor_natCast, Nat.floor_natCast, ← intervalIntegral.integral_const_mul]    simp_rw [mul_div, ← mul_div, φ, ZetaSum_aux1₁ s_ne_one ha]    conv => rhs; rw [sub_eq_add_neg]    congr; any_goals norm_cast; simp only [one_div, add_sub_cancel_left]    rw [← intervalIntegral.integral_neg, intervalIntegral.integral_congr]    simp only [φ, one_div] at φderiv    intro x hx; simp_rw [φderiv x hx, φ']; ring_nf