Euler-Maclaurin formula

Stream: maths

[Geoffrey Irving]

As the main step to the full Stirling series for the gamma function, I've formalized the Euler-Maclaurin formula for approximating a sum by an integral using the first few derivatives, with an explicit error term:

/-- Trapezoidal sum: the trapezoidal rule for integer step size on `[a, a + n]` -/
def trapezoid_sum (f : ℝ → E) (a : ℤ) : ℕ → E
  | 0 => 0
  | n + 1 => trapezoid_sum f a n + (2⁻¹ : ℝ) • (f (a + n) + f (a + n + 1))

/-- The Euler-Maclaurin formula -/
theorem sum_eq_integral_add [CompleteSpace E] (fc : ContDiffOn ℝ (s + 1) f t)
    (u : UniqueDiffOn ℝ t) (abt : Icc (a : ℝ) (a + n) ⊆ t) :
    trapezoid_sum f a n = (∫ x in a..a + n, f x) +
      ∑ m ∈ Finset.range s, (-1 : ℝ) ^ m • saw (m + 2) 0 •
        (iteratedDerivWithin (m + 1) f t (a + n) - iteratedDerivWithin (m + 1) f t a) +
      (-1 : ℝ) ^ s • ∫ x in a..a + n, saw (s+1) x • iteratedDerivWithin (s+1) f t x := by
  ...

[Geoffrey Irving]

It's in a larger repo, but the few files in that EulerMaclaurin directory have no dependence on the other directories. However, I'm unlikely to have time to do the upstreaming for a good while. I could break it out into a separate repo if that would be useful.

[David Loeffler]

Your function saw n seems a lot like docs#periodizedBernoulli; but your treatment seems to be rather more general.

[Geoffrey Irving]

Interesting, I didn't notice periodizedBernoulli.

[Geoffrey Irving]

I was roughly following the notation in Olver, Asymptotics and Special Functions, Chapter 8.1.

[Ruben Van de Velde]

I saw a lemma I liked and upstreamed it in #19849, and added some related ones. Hope that's okay

[Geoffrey Irving]

^ Neat, thank you! I’ll sync to dedup that soon.

[Geoffrey Irving]

https://github.com/girving/interval/commit/e366b3b40110e89567769f2574e9a4d28b25ec65 uses Euler-Maclaurin to derive the effective Stirling series for log gamma, though with two limitations:

1. It's only over the reals. It would be straightforward to extend this to the complex numbers, but the result might be off by some multiple of 2πi.
2. The bound on the remainder is the norm of the last included term, but I think it should be the last excluded term (which is usually but not always smaller in applications).

The remainder bound required a few more facts about Bernoulli polynomials which might be straightforward to upstream (though not by me soon, since I'm back at work on Monday). In particular, I have a proof of the reflection formula and the multiplication theorem, zero-free regions of the Bernoulli polynomials, and extents for the even Bernoulli polynomials.