Partial summation

Stream: Is there code for X?

[Alex Kontorovich]

Do we have partial summation, something like: If $\phi$ has continuous derivative in $[a,b]$ and $[x]$ is the floor function, then

$\sum_{a<n\le b} \phi (n) = \int_a^b \phi(x)dx +([b]+1/2-b)\phi(b)-([a]+1/2-a)\phi(a)- \int_a^b([x]+1/2-x)\phi'(x)dx$

?

[Alex Kontorovich]

Here's a formal statement, FYI:

import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.MeasureTheory.Integral.IntervalIntegral
import Mathlib.Analysis.Calculus.Deriv.Basic

open BigOperators

def funCoe (φ : ℝ → ℂ) : ℤ → ℂ := fun n ↦ φ n

/-- ** Partial summation ** -/
theorem sum_eq_int_deriv (φ : ℝ → ℂ) (a b : ℝ) (φDiff : ContDiffOn ℝ 1 φ (Set.Icc a b)) :
    (Finset.Icc (⌊a⌋ + 1) ⌊b⌋).sum (funCoe φ) =
    (∫ 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
  sorry

Of course exact? doesn't work, so I'm guessing the answer is No?

[Alex Kontorovich]

Also (and this may be related to the ongoing L-series discussion...), is there a better way to implement that funCoe? Why doesn't Lean know that if I have a function ℝ → ℂ but I'm looking for a function ℤ → ℂ, I can compose with the coercion ℤ → ℝ...?

[Floris van Doorn]

If you write fun n ↦ φ n (instead of φ) on the place where you wrote funCoe φ, then Lean is able to insert a coercion.

[Floris van Doorn]

Or even better, ∑ n in Finset.Icc (⌊a⌋ + 1) ⌊b⌋, φ n for the LHS.

[Alex Kontorovich]

But as far as the theorem, it looks like it's not in Mathlib, right?

[David Loeffler]

This is the "k = 1" case of the Euler-Maclaurin summation formula using Bernoulli polynomials, isn't it? I don't recall anything about this in the bernoulli files. It's something that's been on my radar for a while, as an accessible but not-yet-done project.

[Alex Kontorovich]

Well, yes it is, but I was hoping nobody would notice... :) Because now we'll say, "oh we shouldn't bother doing partial summation in Mathlib, we should have the full Euler-Maclaurin" and then neither will get done...

[Antoine Chambert-Loir]

That would be a nice project for LFTC 2024 in a few weeks, @Riccardo Brasca

[Riccardo Brasca]

I am a little afraid of showing beginners all the troubles we have when manipulating sums, but with the help of an expert it is surely doable!

[Geoffrey Irving]

I did the Euler-Maclaurin formula:

#maths > Euler-Maclaurin formula @ 💬