Theorems · Theorem · numerical analysis

trapezoidal_error_le

∀ {f : ℝ → ℝ} {a b : ℝ},
  DifferentiableOn ℝ f (Set.uIcc a b) →
    DifferentiableOn ℝ (derivWithin f (Set.uIcc a b)) (Set.uIcc a b) →
      ∀ {ζ : ℝ},
        (∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.uIcc a b) x| ≤ ζ) →
          ∀ {N : ℕ}, 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]].

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Cited by

1 results in Mathlib

Foundations

Depth 269 from the axioms · uses propext, Classical.choice, Quot.sound