sum_eq_int_deriv

@[blueprint  (title := "sum-eq-int-deriv")  (statement := /--  Let $a < b$, and let $\phi$ be continuously differentiable on $[a, b]$.  Then  \[  \sum_{a < n \le b} \phi(n) = \int_a^b \phi(x) \, dx    + \left(\lfloor b \rfloor + \frac{1}{2} - b\right) \phi(b)    - \left(\lfloor a \rfloor + \frac{1}{2} - a\right) \phi(a)    - \int_a^b \left(\lfloor x \rfloor + \frac{1}{2} - x\right) \phi'(x) \, dx.  \]  -/)  (proof := /-- This is first order Euler-Maclaurin.  -/)  (latexEnv := "lemma")]lemma sum_eq_int_deriv {φ : ℝ → ℂ} {a b : ℝ} (apos : 0 ≤ a) (a_lt_b : a < b)    (φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x)    (derivφCont : ContinuousOn (deriv φ) [[a, b]]) :    ∑ n ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊, φ n =      (∫ x in a..b, φ x) + (⌊b⌋₊ + 1 / 2 - b) * φ b - (⌊a⌋₊ + 1 / 2 - a) * φ a        - ∫ x in a..b, (⌊x⌋ + 1 / 2 - x) * deriv φ x := by  rw [uIcc_of_le a_lt_b.le] at φDiff  convert sum_eq_integral_add_integral_deriv apos a_lt_b.le (fun t ht ↦ (φDiff t ht).differentiableAt) derivφCont using 1  unfold B1  push_cast  suffices ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = -∫ (t : ℝ) in a..b, deriv φ t * (↑t - ↑⌊t⌋₊ - 1 / 2) by    rw [this]    ring_nf!  rw [← intervalIntegral.integral_neg]  refine intervalIntegral.integral_congr fun x hx ↦ ?_  rw [uIcc_of_le a_lt_b.le, mem_Icc] at hx  rw [← Int.natCast_floor_eq_floor (by linarith)]  norm_cast  push_cast  ring