Arbitrary-order Euler--Maclaurin summation

This file is adapted from Interval/EulerMaclaurin/Bernoulli.lean and Interval/EulerMaclaurin/EulerMaclaurin.lean in girving/interval at commit f4a3231fd735cdf6d5265864d9a9207744a7aca2, licensed under Apache-2.0.

The source has been modified, namespaced for Expdb, and updated for newer version of Mathlib.

Periodic Bernoulli functions

noncomputable def Expdb.EulerMaclaurin.saw (s : ℕ) (x : ℝ) : ℝ

The scaled periodic Bernoulli function of order s.

Equations

• Expdb.EulerMaclaurin.saw s x = (↑s.factorial)⁻¹ * periodizedBernoulli s ↑x

Non-explicit bounds

noncomputable def Expdb.EulerMaclaurin.sawBound (s : ℕ) : ℝ

A uniform bound for the absolute value of saw s.

Equations

• Expdb.EulerMaclaurin.sawBound s = sSup (Set.range fun (x : ℝ) => |Expdb.EulerMaclaurin.saw s x|)

@[simp]

theorem Expdb.EulerMaclaurin.sawBound_nonneg {s : ℕ} : 0 ≤ sawBound s

The uniform bound for saw is nonnegative.

Euler--Maclaurin on one unit interval

The full formula

theorem Expdb.EulerMaclaurin.sum_Icc_eq_integral_add {s : ℕ} {a : ℤ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {t : Set ℝ} {n : ℕ} [CompleteSpace E] (fc : ContDiffOn ℝ (↑s + 1) f t) (u : UniqueDiffOn ℝ t) (abt : Set.Icc (↑a) (↑a + ↑n) ⊆ t) : ∑ k ∈ Finset.Icc a (a + ↑n), f ↑k = (∫ (x : ℝ) in ↑a..↑a + ↑n, f x) + 2⁻¹ • (f ↑a + f (↑a + ↑n)) + ∑ 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 arbitrary-order Euler--Maclaurin formula for a sum over consecutive integers.

theorem Expdb.EulerMaclaurin.norm_sum_Icc_nat_sub_integral_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {t : Set ℝ} [CompleteSpace E] {a b s : ℕ} (hab : a ≤ b) (fc : ContDiffOn ℝ (↑s + 1) f t) (u : UniqueDiffOn ℝ t) (abt : Set.Icc ↑a ↑b ⊆ t) {C₀ : ℝ} (hendpoint : ∀ x ∈ Set.Icc ↑a ↑b, ‖f x‖ ≤ C₀) (C : ℕ → ℝ) (hderiv : ∀ (k : ℕ), 1 ≤ k → k ≤ s + 1 → ∀ x ∈ Set.Icc ↑a ↑b, ‖iteratedDerivWithin k f t x‖ ≤ C k) : ‖∑ n ∈ Finset.Icc a b, f ↑n - ∫ (x : ℝ) in ↑a..↑b, f x‖ ≤ C₀ + ∑ m ∈ Finset.range s, |saw (m + 2) 0| * (2 * C (m + 1)) + sawBound (s + 1) * C (s + 1) * ↑(b - a)

A convenient norm form of Euler--Maclaurin for natural endpoints. Uniform bounds on the function and its derivatives control the difference between the inclusive sum and its integral; the right-hand side records the endpoint, correction-term, and remainder contributions.