Theorem 6.21 — the fundamental theorem of calculus (bounded integrand)

This is the fundamental theorem of calculus in the form Rudin states it, with the boundedness hypothesis that his Definition 6.1 places on a Riemann integrable function made explicit.

Let $f$ be a bounded real function on $[a,b]$ which is Riemann integrable there, $f \\in \\mathcal{R}$, and suppose there is a function $F$ on $[a,b]$ which is differentiable at every point of $[a,b]$ with $F'(x) = f(x)$. Then

No continuity of $f$ is assumed: integrability of $f$ together with the existence of an antiderivative suffices. Here $\\int_a^b f\\,dx$ is the Riemann integral in the sense of Rudin's Definition 6.2 with the integrator $\\alpha(x) = x$, i.e. the common value of $\\inf_P U(P,f)$ and $\\sup_P L(P,f)$ over all partitions $P$ of $[a,b]$.

The theorem is what makes integrals computable: it reduces integration to antidifferentiation and is the link between the differentiation theory of Chapter 5 and the integration theory of Chapter 6.

Formalization Note Rudin's class $\\mathcal{R}$ consists of bounded functions whose upper and lower integrals agree; the boundedness clause is carried here by the explicit hypothesis hfb, since the formalized upper and lower integrals are ordinary suprema and infima of sets of real numbers, which take a default value on unbounded sets. Differentiability on the closed interval is expressed as a two-sided derivative at every point of $[a,b]$, as in Rudin's statement.