Comparison of a series and an integral

Statement

Let $a$ be a real number, let $n$ be a natural number, and let $f \colon [a, a + n] \to \mathbb{R}$ be a decreasing function. Then $$\sum_{i=1}^{n} f(a + i) \le \int_a^{a+n} f(x)\, dx \le \sum_{i=0}^{n-1} f(a + i).$$

Remarks

On each interval $[a + i, a + i + 1]$ we have $f(a + i + 1) \le f(x) \le f(a + i)$. Integrate and add over $i$. The integral exists because monotone functions are Riemann integrable. With $f(x) = 1/x$ and $a = 1$ it gives $\ln(n + 1) \le H_n \le 1 + \ln n$ for the harmonic numbers. Mathlib states the first inequality as AntitoneOn.sum_le_integral.

Explanations

L1 human

The sum of the values at the right ends of unit intervals is an area of rectangles below the graph of a decreasing function. The sum of the values at the left ends is an area of rectangles above it.