# The Euler–MacLaurin Formula

 Title: The Euler–MacLaurin Formula Author: Manuel Eberl Submission date: 2017-03-10 Abstract: The Euler-MacLaurin formula relates the value of a discrete sum to that of the corresponding integral in terms of the derivatives at the borders of the summation and a remainder term. Since the remainder term is often very small as the summation bounds grow, this can be used to compute asymptotic expansions for sums. This entry contains a proof of this formula for functions from the reals to an arbitrary Banach space. Two variants of the formula are given: the standard textbook version and a variant outlined in Concrete Mathematics that is more useful for deriving asymptotic estimates. As example applications, we use that formula to derive the full asymptotic expansion of the harmonic numbers and the sum of inverse squares. BibTeX: @article{Euler_MacLaurin-AFP, author = {Manuel Eberl}, title = {The Euler–MacLaurin Formula}, journal = {Archive of Formal Proofs}, month = mar, year = 2017, note = {\url{https://isa-afp.org/entries/Euler_MacLaurin.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Bernoulli, Landau_Symbols Used by: Dirichlet_Series, Zeta_Function