Taylor's theorem with the integral remainder

Statement

Let $k \ge 0$, let $a \ne x$ be real numbers, and let $J$ be the closed interval with endpoints $a$ and $x$. Let $f$ be a real function on $J$ such that $f^{(k+1)}$ exists and is continuous on $J$. Then $$f(x) = P_k(x) + \int_a^x \frac{f^{(k+1)}(t)}{k!} (x - t)^k \, dt,$$ where $P_k$ is the Taylor polynomial of degree $k$ of $f$ at $a$.

Remarks

For $k = 0$ it is the fundamental theorem of calculus, $f(x) = f(a) + \int_a^x f'(t)\, dt$. Repeated integration by parts gives the general case. The hypotheses can be weakened to absolute continuity of $f^{(k)}$. Mathlib states it as taylor_integral_remainder_of_absolutelyContinuous.

Explanations

L1 human

The integral form gives the error exactly, as an average of the next derivative with weights. It needs no unknown point $\xi$.