Euler-Maclaurin formula

This lets us approximate finite sums of C^k functions with integrals, with known bounds on the remainder.

The general formula, for real end points and a family of successive derivatives, is EulerMaclaurin.sum_Ioc_eq_integral_add_of_hasDerivWithinAt in Interval.EulerMaclaurin.Formula, stated with Mathlib's periodizedBernoulli. Here it is specialised to trapezoid_sum, the trapezoidal rule with integer step size, and written with saw.

The full Euler-Maclaurin formula

theorem saw_eq_periodizedBernoulli (s : ℕ) (x : ℝ) : saw s x = (↑s.factorial)⁻¹ * periodizedBernoulli s ↑x

saw s is Mathlib's periodized Bernoulli polynomial divided by s !

def trapezoid_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (a : ℤ) : ℕ → E

Trapezoidal sum: the trapezoidal rule for integer step size on [a, a + n]

Equations

• trapezoid_sum f a 0 = 0
• trapezoid_sum f a n.succ = trapezoid_sum f a n + 2⁻¹ • (f (↑a + ↑n) + f (↑a + ↑n + 1))

@[simp]

theorem trapezoid_sum_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℤ} : trapezoid_sum f a 0 = 0

theorem trapezoid_sum_succ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℤ} {n : ℕ} : trapezoid_sum f a (n + 1) = trapezoid_sum f a n + 2⁻¹ • (f (↑a + ↑n) + f (↑a + ↑n + 1))

theorem trapezoid_sum_eq_sum_Ioc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (a : ℤ) (n : ℕ) : trapezoid_sum f a n = ∑ i ∈ Finset.Ioc a (a + ↑n), f ↑i - 2⁻¹ • (f (↑a + ↑n) - f ↑a)

The trapezoidal sum is the sum over the integers in (a, a + n], corrected by half the difference of the values at the end points

theorem intervalIntegrable_saw_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {t : Set ℝ} {a : ℤ} {s n : ℕ} (fc : ContDiffOn ℝ (↑s) f t) (u : UniqueDiffOn ℝ t) (abt : Set.Icc (↑a) (↑a + ↑n) ⊆ t) : IntervalIntegrable (fun (x : ℝ) => saw s x • iteratedDerivWithin s f t x) MeasureTheory.volume (↑a) (↑a + ↑n)

theorem trapezoid_sum_eq_integral_add_of_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℤ} {s n : ℕ} [CompleteSpace E] {F : ℕ → ℝ → E} (hF : ∀ k < s + 1, ∀ x ∈ Set.Icc (↑a) (↑a + ↑n), HasDerivWithinAt (F k) (F (k + 1) x) (Set.Icc (↑a) (↑a + ↑n)) x) (hFs : IntervalIntegrable (F (s + 1)) MeasureTheory.volume (↑a) (↑a + ↑n)) : trapezoid_sum (F 0) a n = (∫ (x : ℝ) in ↑a..↑a + ↑n, F 0 x) + ∑ m ∈ Finset.range s, (-1) ^ m • saw (m + 2) 0 • (F (m + 1) (↑a + ↑n) - F (m + 1) ↑a) + (-1) ^ s • ∫ (x : ℝ) in ↑a..↑a + ↑n, saw (s + 1) x • F (s + 1) x

The Euler-Maclaurin formula for a family of successive derivatives: F (k + 1) is a derivative of F k within [a, a + n] for k ≤ s, and F (s + 1) is interval integrable

theorem trapezoid_sum_eq_integral_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {t : Set ℝ} {a : ℤ} {s n : ℕ} [CompleteSpace E] (fc : ContDiffOn ℝ (↑s + 1) f t) (u : UniqueDiffOn ℝ t) (abt : Set.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

The Euler-Maclaurin formula