Abstract: 
The EulerMacLaurin 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_MacLaurinAFP,
author = {Manuel Eberl},
title = {The Euler–MacLaurin Formula},
journal = {Archive of Formal Proofs},
month = mar,
year = 2017,
note = {\url{http://isaafp.org/entries/Euler_MacLaurin.shtml},
Formal proof development},
ISSN = {2150914x},
}
