The fundamental theorem of the infinitesimal calculus (FTC) states that the antiderivatives and indefinite integrals of a function (typically a real-valued function on a closed interval in the real line) are the same. It is now such a truism that calculus textbooks tend to use ‘indefinite integral’ to simply mean an antiderivative, but there is a different concept, definable from the definite integral and sometimes called the semidefinite integral, that is really in play here.
The FTC is usually split into two parts. The first part (sometimes called the second part) states that every indefinite integral is an antiderivative. The second part (sometimes called the first part) states that every antiderivative is an indefinite integral. Somewhere in here (usually in the first part) we also want to state that such antiderivatives and indefinite integrals actually exist. Their uniqueness (such as it is) may also be included.
The second part is a low-dimensional version of the Stokes theorem.
The FTC may or may not actually be true, depending on what class of functions is considered and what notions of derivative and integral are used.
Let be a function. Recall that an antiderivative of is a solution to the differential equation
Also recall (or learn) than an indefinite integral of is any function of the form
for a real constant .
Suppose that and are appropriate functions, and use an appropriate notion of derivative and integral. Then:
This holds under any of the following conditions:
One may rephrase the first part in various ways as follows. First, simply incorporating the definitions of ‘indefinite integral’ and ‘antiderivative’, we have
Taking for granted that adding a constant to a function leaves its derivative unchanged, this simplifies to
When combined with the chain rule, this generalizes to
Taking for granted that , this generalizes to
Writing for and for and multiplying both sides by , we get the differential form
In other words, the differential and definite integral operators cancel upon performing the substitution directed by the limits of the definite integral.
One may rephrase the second part in various ways as follows. First, simply incorporating the definitions of ‘indefinite integral’ and ‘antiderivative’, we have
for some constant . Taking for granted that , we see that , so
It is sufficient to consider the special case where :
This can also be written
to match the last version of the first part; again, the differential and definite integral operators cancel (but now in the opposite order) upon performing the substitution directed by the limits of the definite integral.
If convenient, one may prove the theorem first for the unit interval . By applying a suitable affine transformation, we can deduce the corresponding result for each interval where and are real numbers with .
In classical mathematics and pointwise constructive mathematics, existence of definite integrals must be proved first; existence of indefinite integrals follows. We can then prove that every indefinite integral is an antiderivative by applying the mean value theorem. Uniqueness of antiderivatives has a simple direct proof; since at least one antiderivative is an indefinite integral, this shows that every antiderivative is an indefinite integral. Of course, we have existence of an antiderivative, so now everything is proved.
In the locale-theoretic approach, we essentially define an antiderivative to be an indefinite integral. Formally, the data in a continuously differentiable map on consists of a continuous map (its derivative) and a real number (its value at ). We must prove the existence of indefinite integrals directly; a definite integral up to each point is not sufficient. Then there is nothing more to prove (but one might want to prove that differentiation has its usual properties).
Conversely, in synthetic differential geometry, we essentially define an indefinite integral to be an antiderivative. We must prove uniqueness of antiderivatives; but their existence is given by an axiom, the integration axiom, and then there is nothing more to prove. Sometimes one studies versions of SDG without this axiom; then there is no FTC (and indeed no integrals).
In the literature, the first part of the FTC is sometimes stated as merely existence of an antiderivative. The purpose of this section is to show, independent of foundations, that the second part gives the integral formula for the antiderivative as an indefinite integral.
Suppose is in . By assumption, there is such that . By the other part of the fundamental theorem, we have . Thus, . Differentiating gives the required result.
Wikipedia, Fundamental theorem of calculus
Steve Vickers, The Fundamental Theorem of Calculus point-free, with applications to exponentials and logarithms, (arXiv:2312.05228)
Steve Vickers, The Fundamental Theorem of Calculus: point-free, talk at the Topos Institute Colloquium, 30 May 2024 (video, slides)
Last revised on June 5, 2024 at 02:28:26. See the history of this page for a list of all contributions to it.