---
tag: 0HBY48G8G1
kind: definition
name: Riemann sum
msc: [26A42]
defines: 0JAEHXTVV5
uses: [069P20KYQT]
sources:
  - url: https://en.wikipedia.org/wiki/Riemann_sum
    locator: Definition
---

## Definition

Let $a < b$, let $f \colon [a, b] \to \mathbb{R}$, and let $P = (x_0, \dots, x_n)$ be a [[partition|069P20KYQT]] 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|0QRQVH0CRW]] 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.