Theorems · Theorem · numerical analysis

sum_trapezoidal_integral_adjacent_intervals

∀ {f : ℝ → ℝ} {N : ℕ} {a h : ℝ},
  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.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Cited by

2 results in Mathlib

Foundations

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