The Euler-Maclaurin summation formula #
Let $E$ be a complete real normed space, let $a \le b$ be real numbers and let $p \ge 1$. Let
$P_n(t) = B_n(\{t\})$ be the periodic Bernoulli function, which in Lean is
periodizedBernoulli n, evaluated at the class of the real number $t$. For a function
$f : \mathbb{R} \to E$ which is $C^p$ on $[a, b]$,
$$\sum_{a < i \le b} f(i) = \int_a^b f(t) , dt
- \sum_{k = 0}^{p - 1} \frac{(-1)^{k + 1}}{(k + 1)!} \bigl( P_{k + 1}(b) f^{(k)}(b) - P_{k + 1}(a) f^{(k)}(a) \bigr)
- \frac{(-1)^{p + 1}}{p!} \int_a^b P_p(t) f^{(p)}(t) , dt.$$ The sum is over the integers in `(a, b]`, written `Finset.Ioc ⌊a⌋ ⌊b⌋`. For integer end points the boundary values of the periodic function are Bernoulli numbers, and the formula reads $$\sum_{i = a + 1}^{b} f(i) = \int_a^b f(t) , dt
- \sum_{k = 0}^{p - 1} \frac{B'_{k + 1}}{(k + 1)!} \bigl( f^{(k)}(b) - f^{(k)}(a) \bigr)
- \frac{(-1)^{p + 1}}{p!} \int_a^b P_p(t) f^{(p)}(t) , dt,$$
with
B'_n = bernoulli' n.trapezoid_sum_eq_integral_addinInterval.EulerMaclaurin.EulerMaclaurinis derived from this form. Bounds for the remainder are inInterval.EulerMaclaurin.RemainderBound.
The proof integrates by parts against the polynomial t ↦ bernoulliFun (k + 1) (t - c), so the
corners of the periodic function never enter an integral. On an interval containing no integer this
gives the formula with an empty sum; across one integer it produces that integer's term; the general
case is an induction on the number of integers in (a, b]. The derivatives are taken within
[a, b], so they are one-sided only at the end points, and the last one need only be interval
integrable.
Main results #
EulerMaclaurin.sum_Ioc_eq_integral_add_of_hasDerivWithinAt: the formula for real end points and a familyF : ℕ → ℝ → Eof successive derivatives, whereF pneed only be interval integrable.EulerMaclaurin.sum_Ioc_eq_integral_add: the same for a function that isC^pon[a, b].EulerMaclaurin.sum_Ioc_int_eq_integral_add_of_hasDerivWithinAt: integer end points.ContDiffOn.hasDerivWithinAt_iteratedDerivWithin: the derivative of an iterated derivative within a set, used to pass fromC^pto a family of derivatives.
References #
- T. M. Apostol, An elementary view of Euler's summation formula, Amer. Math. Monthly 106 (1999).
- R. L. Graham, D. E. Knuth, O. Patashnik, Concrete Mathematics, section 9.5.
- NIST Digital Library of Mathematical Functions, section 2.10(i).
On a set with unique derivatives, the m-th iterated derivative of a function which is C^n
within the set at x, m < n, has the (m + 1)-th iterated derivative as its derivative within
the set at x.
On a set with unique derivatives, the m-th iterated derivative of a C^n function, m < n,
has the (m + 1)-th iterated derivative as its derivative within the set at every point of the
set.
The Euler-Maclaurin summation formula for real end points, for a family F : ℕ → ℝ → E of
successive derivatives. Let a ≤ b be real numbers, p ≥ 1, and suppose that for k < p the
function F k has derivative F (k + 1) within [a, b], and that F p is interval integrable on
[a, b]. Then the sum of F 0 i over the integers i ∈ (a, b] equals
$$\int_a^b F_0 + \sum_{k < p} \frac{(-1)^{k + 1}}{(k + 1)!}
\bigl(P_{k + 1}(b) F_k(b) - P_{k + 1}(a) F_k(a)\bigr)
- \frac{(-1)^{p + 1}}{p!} \int_a^b P_p F_p,$$
where
P_n = periodizedBernoulli n, evaluated at the class of a real number.
The Euler-Maclaurin summation formula for real end points and a C^p function. Let
a ≤ b be real numbers and p ≥ 1. If f is C^p on [a, b], then the sum of f i over the
integers i ∈ (a, b] equals
$$\int_a^b f + \sum_{k < p} \frac{(-1)^{k + 1}}{(k + 1)!}
\bigl(P_{k + 1}(b) f^{(k)}(b) - P_{k + 1}(a) f^{(k)}(a)\bigr)
- \frac{(-1)^{p + 1}}{p!} \int_a^b P_p f^{(p)},$$
where
P_n = periodizedBernoulli nand the derivativesf^(k)areiteratedDerivWithinon[a, b].
The Euler-Maclaurin summation formula for integer end points, for a family
F : ℕ → ℝ → E of successive derivatives. Let a ≤ b be integers, p ≥ 1, and suppose that for
k < p the function F k has derivative F (k + 1) within [a, b], and that F p is interval
integrable on [a, b]. Then ∑ i ∈ Finset.Ioc a b, F 0 i equals
$$\int_a^b F_0 + \sum_{k < p} \frac{B'_{k + 1}}{(k + 1)!} (F_k(b) - F_k(a))
- \frac{(-1)^{p + 1}}{p!} \int_a^b P_p F_p,$$
where
B'_n = bernoulli' nandP_p = periodizedBernoulli p.