Bounds for the remainder of the Euler-Maclaurin formula

The remainder term of the formula of order p in Interval.EulerMaclaurin.Formula is ((-1) ^ (p + 1) / p !) • ∫ t in a..b, periodizedBernoulli p t • g t, where g is the p-th derivative. If |bernoulliFun p x| ≤ D on [0, 1], its norm is at most D / p ! * ∫ ‖g‖, which bounds the error of every form of the formula. Useful choices of D are bernoulliBound p (the best constant, abs_bernoulliFun_le), |bernoulli p| for even p (abs_bernoulliFun_le_even), and the rational constant 4 * p ! / 6 ^ p, valid for every p, which needs no transcendental number and so suits certified numerics.

Main results

• abs_bernoulliFun_le_tsum: |bernoulliFun k x| ≤ 2 * (∑' n, 1 / n ^ k) * k ! / (2 * π) ^ k for 2 ≤ k and x ∈ [0, 1], from the Fourier expansion of the Bernoulli polynomials.
• abs_bernoulliFun_le_four_mul_factorial_div_six_pow: |bernoulliFun k x| ≤ 4 * k ! / 6 ^ k for every k and x ∈ [0, 1].
• bernoulliBound_le_four_mul_factorial_div_six_pow and sawBound_le_four_div_six_pow: bernoulliBound k ≤ 4 * k ! / 6 ^ k and sawBound k ≤ 4 / 6 ^ k, so that with abs_saw_le, |saw k x| ≤ 4 / 6 ^ k in every order, including odd orders, where bernoulliBound is not evaluated.
• EulerMaclaurin.norm_smul_integral_periodizedBernoulli_smul_le: the bound for the remainder term.
• EulerMaclaurin.norm_sum_Ioc_sub_integral_sub_le_of_abs_bernoulliFun_le_of_hasDerivWithinAt and EulerMaclaurin.norm_sum_Ioc_sub_integral_sub_le_of_abs_bernoulliFun_le: the error bound in terms of any uniform bound D, for a family of derivatives and for a C^p function.
• EulerMaclaurin.norm_sum_Ioc_sub_integral_sub_le_of_hasDerivWithinAt: the error bound 4 / 6 ^ p * ∫ ‖F p‖.
• EulerMaclaurin.norm_sum_Ioc_sub_integral_sub_le_abs_bernoulli_of_hasDerivWithinAt: the classical error bound |bernoulli (2 * m)| / (2 * m) ! * ∫ ‖F (2 * m)‖ in even order.

theorem abs_bernoulliFun_le_tsum {k : ℕ} (hk : 2 ≤ k) {x : ℝ} (hx : x ∈ Set.Icc 0 1) : |bernoulliFun k x| ≤ (2 * ∑' (n : ℕ), 1 / ↑n ^ k) * ↑k.factorial / (2 * Real.pi) ^ k

Explicit bound for the Bernoulli polynomials in terms of ∑' n, 1 / n ^ k. For k ≥ 2 and x ∈ [0, 1], |B_k(x)| ≤ 2 * (∑ n ≥ 1, 1 / n ^ k) * k! / (2 π) ^ k. The proof takes norms termwise in the Fourier expansion hasSum_one_div_nat_pow_mul_fourier.

theorem abs_bernoulliFun_le_four_mul_factorial_div_six_pow (k : ℕ) {x : ℝ} (hx : x ∈ Set.Icc 0 1) : |bernoulliFun k x| ≤ 4 * ↑k.factorial / 6 ^ k

Rational bound for the Bernoulli polynomials. For every k and x ∈ [0, 1], |B_k(x)| ≤ 4 * k! / 6 ^ k. No transcendental constant occurs, which is convenient for certified numerical estimates. For k ≥ 2 it follows from abs_bernoulliFun_le_tsum since the series is at most π ^ 2 / 6 < 2 and 6 < 2 π; the cases k = 0 and k = 1 are direct.

theorem bernoulliBound_le_four_mul_factorial_div_six_pow (k : ℕ) : bernoulliBound k ≤ 4 * ↑k.factorial / 6 ^ k

The best constant bernoulliBound k is at most the rational constant 4 * k ! / 6 ^ k.

theorem sawBound_le_four_div_six_pow (k : ℕ) : sawBound k ≤ 4 / 6 ^ k

An explicit upper bound for sawBound in every order: |saw k x| ≤ sawBound k ≤ 4 / 6 ^ k. bernoulliBound is defined as a maximum and is evaluated only in even order (bernoulliBound_eq_abs_bernoulli'); this bound needs no parity assumption.

theorem EulerMaclaurin.norm_integral_periodizedBernoulli_smul_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : ℝ → E} {a b : ℝ} {p : ℕ} {D : ℝ} (hab : a ≤ b) (hD : ∀ x ∈ Set.Icc 0 1, |bernoulliFun p x| ≤ D) (hg : IntervalIntegrable g MeasureTheory.volume a b) : ‖∫ (t : ℝ) in a..b, periodizedBernoulli p ↑t • g t‖ ≤ D * ∫ (t : ℝ) in a..b, ‖g t‖

The generic bound for the remainder integral. If |B_p(x)| ≤ D for x ∈ [0, 1], then ‖∫ t in a..b, P_p t • g t‖ ≤ D * ∫ t in a..b, ‖g t‖ for a ≤ b and g interval integrable, where P_p = periodizedBernoulli p. Only interval integrability of g is used, not that of the product with the periodic Bernoulli function.

theorem EulerMaclaurin.norm_smul_integral_periodizedBernoulli_smul_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : ℝ → E} {a b : ℝ} {p : ℕ} {D : ℝ} (hab : a ≤ b) (hD : ∀ x ∈ Set.Icc 0 1, |bernoulliFun p x| ≤ D) (hg : IntervalIntegrable g MeasureTheory.volume a b) : ‖((-1) ^ (p + 1) / ↑p.factorial) • ∫ (t : ℝ) in a..b, periodizedBernoulli p ↑t • g t‖ ≤ D / ↑p.factorial * ∫ (t : ℝ) in a..b, ‖g t‖

Bound for the remainder term of the Euler-Maclaurin formula, with its coefficient. The term ((-1) ^ (p + 1) / p !) • ∫ t in a..b, periodizedBernoulli p t • g t is the remainder term of every form of the formula in Interval.EulerMaclaurin.Formula, where g is the p-th derivative. If |B_p(x)| ≤ D for x ∈ [0, 1], its norm is at most D / p ! * ∫ t in a..b, ‖g t‖. Rewriting with a form of the formula and applying this bound gives the error bound for that form.

theorem EulerMaclaurin.norm_sum_Ioc_sub_integral_sub_le_of_abs_bernoulliFun_le_of_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {p : ℕ} {D : ℝ} (hp : p ≠ 0) {F : ℕ → ℝ → E} (hab : a ≤ b) (hD : ∀ x ∈ Set.Icc 0 1, |bernoulliFun p x| ≤ D) (hF : ∀ k < p, ∀ x ∈ Set.Icc a b, HasDerivWithinAt (F k) (F (k + 1) x) (Set.Icc a b) x) (hFp : IntervalIntegrable (F p) MeasureTheory.volume a b) : ‖(∑ i ∈ Finset.Ioc ⌊a⌋ ⌊b⌋, F 0 ↑i - ∫ (t : ℝ) in a..b, F 0 t) - ∑ k ∈ Finset.range p, ((-1) ^ (k + 1) / ↑(k + 1).factorial) • (periodizedBernoulli (k + 1) ↑b • F k b - periodizedBernoulli (k + 1) ↑a • F k a)‖ ≤ D / ↑p.factorial * ∫ (t : ℝ) in a..b, ‖F p t‖

Error bound for the Euler-Maclaurin formula in terms of a uniform bound for the Bernoulli polynomial, for a family of derivatives. Under the hypotheses of EulerMaclaurin.sum_Ioc_eq_integral_add_of_hasDerivWithinAt, if |B_p(x)| ≤ D for x ∈ [0, 1], the difference between the sum over the integers in (a, b] and the integral plus the boundary terms of order p is at most D / p ! * ∫ ‖F p‖. Useful choices of D are D = bernoulliBound p for every p (abs_bernoulliFun_le), D = 1 / 2 for p = 1, D = 2 * ζ(p) * p ! / (2 * π) ^ p for p ≥ 2 (abs_bernoulliFun_le_tsum), D = |B_p| for even p, and D = 4 * p ! / 6 ^ p.

theorem EulerMaclaurin.norm_sum_Ioc_sub_integral_sub_le_of_abs_bernoulliFun_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f : ℝ → E} {p : ℕ} {D : ℝ} (hp : p ≠ 0) (hab : a ≤ b) (hD : ∀ x ∈ Set.Icc 0 1, |bernoulliFun p x| ≤ D) (hf : ContDiffOn ℝ (↑p) f (Set.Icc a b)) : ‖(∑ i ∈ Finset.Ioc ⌊a⌋ ⌊b⌋, f ↑i - ∫ (t : ℝ) in a..b, f t) - ∑ k ∈ Finset.range p, ((-1) ^ (k + 1) / ↑(k + 1).factorial) • (periodizedBernoulli (k + 1) ↑b • iteratedDerivWithin k f (Set.Icc a b) b - periodizedBernoulli (k + 1) ↑a • iteratedDerivWithin k f (Set.Icc a b) a)‖ ≤ D / ↑p.factorial * ∫ (t : ℝ) in a..b, ‖iteratedDerivWithin p f (Set.Icc a b) t‖

Error bound for the Euler-Maclaurin formula for a C^p function, in terms of a uniform bound for the Bernoulli polynomial: the case of EulerMaclaurin.norm_sum_Ioc_sub_integral_sub_le_of_abs_bernoulliFun_le_of_hasDerivWithinAt for the derivatives iteratedDerivWithin k f (Set.Icc a b).

theorem EulerMaclaurin.norm_sum_Ioc_sub_integral_sub_le_of_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {p : ℕ} (hp : p ≠ 0) {F : ℕ → ℝ → E} (hab : a ≤ b) (hF : ∀ k < p, ∀ x ∈ Set.Icc a b, HasDerivWithinAt (F k) (F (k + 1) x) (Set.Icc a b) x) (hFp : IntervalIntegrable (F p) MeasureTheory.volume a b) : ‖(∑ i ∈ Finset.Ioc ⌊a⌋ ⌊b⌋, F 0 ↑i - ∫ (t : ℝ) in a..b, F 0 t) - ∑ k ∈ Finset.range p, ((-1) ^ (k + 1) / ↑(k + 1).factorial) • (periodizedBernoulli (k + 1) ↑b • F k b - periodizedBernoulli (k + 1) ↑a • F k a)‖ ≤ 4 / 6 ^ p * ∫ (t : ℝ) in a..b, ‖F p t‖

Error bound for the Euler-Maclaurin formula with the rational constant. Under the hypotheses of EulerMaclaurin.sum_Ioc_eq_integral_add_of_hasDerivWithinAt, the difference between the sum over the integers in (a, b] and the integral plus the boundary terms of order p is at most 4 / 6 ^ p * ∫ ‖F p‖.

theorem EulerMaclaurin.norm_sum_Ioc_sub_integral_sub_le_abs_bernoulli_of_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {m : ℕ} (hm : m ≠ 0) {F : ℕ → ℝ → E} (hab : a ≤ b) (hF : ∀ k < 2 * m, ∀ x ∈ Set.Icc a b, HasDerivWithinAt (F k) (F (k + 1) x) (Set.Icc a b) x) (hFp : IntervalIntegrable (F (2 * m)) MeasureTheory.volume a b) : ‖(∑ i ∈ Finset.Ioc ⌊a⌋ ⌊b⌋, F 0 ↑i - ∫ (t : ℝ) in a..b, F 0 t) - ∑ k ∈ Finset.range (2 * m), ((-1) ^ (k + 1) / ↑(k + 1).factorial) • (periodizedBernoulli (k + 1) ↑b • F k b - periodizedBernoulli (k + 1) ↑a • F k a)‖ ≤ |↑(bernoulli (2 * m))| / ↑(2 * m).factorial * ∫ (t : ℝ) in a..b, ‖F (2 * m) t‖

Error bound for the Euler-Maclaurin formula in even order. Under the hypotheses of EulerMaclaurin.sum_Ioc_eq_integral_add_of_hasDerivWithinAt with p = 2 * m, the difference between the sum over the integers in (a, b] and the integral plus the boundary terms of order 2 * m is at most |B_{2m}| / (2m)! * ∫ ‖F (2 * m)‖, the classical form of the error term.