### 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.

### License

BSD License

### Topics

- Mathematics/Analysis

### Session Euler_MacLaurin

- Euler_MacLaurin
- Euler_MacLaurin_Landau

### Depends on

- Bernoulli Numbers
- Landau Symbols

### Used by

- Dirichlet Series
- The Hurwitz and Riemann ζ Functions

## Cite

×

Euler_MacLaurin-AFP

    @article{Euler_MacLaurin-AFP,
      author  = {Manuel Eberl},
      title   = {The Euler–MacLaurin Formula},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Euler_MacLaurin.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Mar 14, 2017 : Isabelle2016-1