The trapezoidal rule

This file contains a definition of integration on [[a, b]] via the trapezoidal rule, along with an error bound in terms of a bound on the second derivative of the integrand.

Main results

• trapezoidal_error_le: the convergence theorem for the trapezoidal rule.

References

We follow the proof on (Wikipedia)[https://en.wikipedia.org/wiki/Trapezoidal_rule] for the error bound.

noncomputable def trapezoidal_integral (f : ℝ → ℝ) (N : ℕ) (a b : ℝ) : ℝ

Integration of f from a to b using the trapezoidal rule with N+1 total evaluations of f. (Note the off-by-one problem here: N counts the number of trapezoids, not the number of evaluations.)

noncomputable def trapezoidal_error (f : ℝ → ℝ) (N : ℕ) (a b : ℝ) : ℝ

The absolute error of trapezoidal integration.

theorem trapezoidal_integral_symm (f : ℝ → ℝ) {N : ℕ} (N_nonzero : 0 < N) (a b : ℝ) : trapezoidal_integral f N a b = -trapezoidal_integral f N b a

Just like exact integration, the trapezoidal approximation retains the same magnitude but changes sign when the endpoints are swapped.

theorem trapezoidal_error_symm (f : ℝ → ℝ) {N : ℕ} (N_nonzero : 0 < N) (a b : ℝ) : trapezoidal_error f N a b = -trapezoidal_error f N b a

The absolute error of the trapezoidal rule does not change when the endpoints are swapped.

@[simp]

theorem trapezoidal_integral_eq (f : ℝ → ℝ) (N : ℕ) (a : ℝ) : trapezoidal_integral f N a a = 0

Just like exact integration, the trapezoidal integration from a to a is zero.

@[simp]

theorem trapezoidal_error_eq (f : ℝ → ℝ) (N : ℕ) (a : ℝ) : trapezoidal_error f N a a = 0

The error of the trapezoidal integration from a to a is zero.

@[simp]

theorem trapezoidal_integral_one (f : ℝ → ℝ) (a b : ℝ) : trapezoidal_integral f 1 a b = (b - a) / 2 * (f a + f b)

An exact formula for integration with a single trapezoid (the "midpoint rule").

theorem sum_trapezoidal_integral_adjacent_intervals {f : ℝ → ℝ} {N : ℕ} {a h : ℝ} (N_nonzero : 0 < N) : ∑ i ∈ Finset.range N, trapezoidal_integral f 1 (a + ↑i * h) (a + (↑i + 1) * h) = trapezoidal_integral f N a (a + ↑N * h)

A basic trapezoidal equivalent to IntervalIntegral.sum_integral_adjacent_intervals. More general theorems are certainly possible, but many of them can be derived from repeated applications of this one.

theorem trapezoidal_integral_ext {f : ℝ → ℝ} {N : ℕ} {a h : ℝ} (N_nonzero : 0 < N) : trapezoidal_integral f N a (a + ↑N * h) + trapezoidal_integral f 1 (a + ↑N * h) (a + (↑N + 1) * h) = trapezoidal_integral f (N + 1) a (a + (↑N + 1) * h)

A simplified version of the previous theorem, for use in proofs by induction and the like.

theorem sum_trapezoidal_error_adjacent_intervals {f : ℝ → ℝ} {N : ℕ} {a h : ℝ} (N_nonzero : 0 < N) (h_f_int : IntervalIntegrable f MeasureTheory.volume a (a + ↑N * h)) : ∑ i ∈ Finset.range N, trapezoidal_error f 1 (a + ↑i * h) (a + (↑i + 1) * h) = trapezoidal_error f N a (a + ↑N * h)

Since we have sum_[]_adjacent_intervals theorems for both exact and trapezoidal integration, it's natural to combine them into a similar formula for the error. This theorem is in particular used in the proof of the general error bound.

theorem trapezoidal_error_le {f : ℝ → ℝ} {a b : ℝ} (h_df : DifferentiableOn ℝ f (Set.uIcc a b)) (h_ddf : DifferentiableOn ℝ (derivWithin f (Set.uIcc a b)) (Set.uIcc a b)) (h_ddf_integrable : IntervalIntegrable (iteratedDerivWithin 2 f (Set.uIcc a b)) MeasureTheory.volume a b) {ζ : ℝ} (fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.uIcc a b) x| ≤ ζ) {N : ℕ} (N_nonzero : 0 < N) : |trapezoidal_error f N a b| ≤ |b - a| ^ 3 * ζ / (12 * ↑N ^ 2)

The standard error bound for trapezoidal integration on the general interval [[a, b]].

theorem trapezoidal_error_le_of_c2 {f : ℝ → ℝ} {a b : ℝ} (h_f_c2 : ContDiffOn ℝ 2 f (Set.uIcc a b)) {ζ : ℝ} (fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.uIcc a b) x| ≤ ζ) {N : ℕ} (N_nonzero : 0 < N) : |trapezoidal_error f N a b| ≤ |b - a| ^ 3 * ζ / (12 * ↑N ^ 2)

The error bound for trapezoidal integration in the slightly weaker, but very common, case where f is C^2.