Riemann sum

Definition

Let $a < b$, let $f \colon [a, b] \to \mathbb{R}$, and let $P = (x_0, \dots, x_n)$ be a partition of $[a, b]$. Let $t = (t_1, \dots, t_n)$ be tags with $t_i \in [x_{i-1}, x_i]$ for each $i$. The Riemann sum of $f$ for the tagged partition $(P, t)$ is $$S(f, P, t) = \sum_{i=1}^{n} f(t_i) (x_i - x_{i-1}).$$

Remarks

The left rule takes $t_i = x_{i-1}$, the right rule takes $t_i = x_i$, and the midpoint rule takes the midpoints. For bounded $f$, each Riemann sum lies between the lower and the upper Darboux sum for $P$. Mathlib has a general form for boxes, BoxIntegral.integralSum.

Explanations

L1 human

A Riemann sum adds up areas of rectangles. Each rectangle stands on a piece of the partition, and its height is the value of $f$ at the chosen tag.