analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
The intermediate value theorem (IVT) is a fundamental principle of analysis which allows one to find a desired value by interpolation. It says that a continuous function from an interval to the real numbers (all with its Euclidean topology) takes all values in between and .
The IVT in its general form was not used by Euclid. Although it is hard to doubt that Euclid believed that, for any given angle, there was an angle with one-third the measure, this angle cannot be constructed by the methods available to Euclid, so he would never refer to it (see at Euclidean geometry). In contrast, Archimedes made general arguments in which a quantity is approached from above and below, allowing him not only to trisect the angle but also to calculate π.
As normally stated, the IVT is not valid in constructive mathematics, although there are constructively valid versions. These versions either weaken the conclusion to an approximate zero, or to strengthen the hypothesis to require the functions satisfy additional properties or have other structures, such as locally nonconstancy and lifting to locators in functions in the given example below. Even interpreted classically, these are prima facie weaker results.
(classical IVT, assuming excluded middle)
Let be a continuous function from a compact closed interval to the real line, and suppose that while . Then there exists a point in the unit interval such that .
Let be defined as . Then we can define a function by .
By this example the interval is a connected topological space (this is where excluded middle is used).
By this prop. also its image is connected. By this example that image is itself an interval. This implies the claim is true for . Since linear functions preserve the properties of an interval being compact and closed, if the claim is true for , it is true for .
(constructive IVT with weakened conclusion)
For real numbers and , let be a pointwise continuous function from the closed interval to the real line, and supposed that and . Then for every positive number there exists a point in the unit interval such that .
This proof originally appeared in Frank 2020.
Let us inductively define the following sequences:
Then
and the sequence is a Cauchy sequence, because for natural numbers ,
Lemma: For every natural number , either 1. there exists a such that , or 2. and . This could be proved by induction on natural numbers:
When , and .
Now, assume that the above lemma is true for a particular . If there exists a such that , then there exists a such that . Otherwise, either , , or .
If , then we define
so that and .
If , then we define
so that and .
If , then there exists a such that .
Thus, the above lemma is true.
Now, by pointwise continuity at , let be such that implies . Choose a natural number such that
If there exists a such that , then the intermediate value is true. Otherwise, and , and so
and so that means that
which means that .
If excluded middle is true, then the classical IVT follows from the above theorem:
By way of contradiction (applying the double negation law of classical logic), suppose that for every in . Then the extra hypothesis of Theorem is certainly satisfied, so there exists some such that after all. (Constructively, this is enough to show that the classical theorem has no counterexample.)
There is also another constructively valid version of the IVT, where the conclusion is classically the contrapositive of the classical IVT, but which is weaker constructively since the reverse contrapositive rule does not hold constructively:
Let be a continuous function from a compact closed interval to the real line, and suppose that or for all . Then is either everywhere positive or everywhere negative.
This appeared in Bauer 2016.
(constructive IVT with strengthened hypothesis, assuming the interval endpoints and the zero have locators and that the function is locally nonzero)
For real numbers and with locators, let be a pointwise continuous function from the closed interval to the real line that is a locally nonzero function and that lifts to locators, and suppose that and . Then, there exists a point in with a locator such that .
(constructive IVT with strengthened hypothesis, assuming weak countable choice and that the function is locally nonzero)
Assuming weak countable choice, for real numbers and , let be a pointwise continuous function from the closed interval to the real line that is a locally nonzero function, and suppose that and . Then, there exists a point in with a locator such that .
(constructive IVT with strengthened hypothesis, assuming weak countable choice and that the function is uniformly continuous)
Let be a uniformly continuous function from the unit interval to the real line, and suppose that while . Suppose further that, for any points in the unit interval with , there exists a point such that and . (In other words, the non-zero set is dense.) Then there exists a point in the unit interval such that .
(constructive IVT with strengthened hypothesis, assuming that the function is strictly monotonic with strictly between and )
Let be a strictly monotonic from the unit interval to the real line, and suppose that while . Then there exists a point in the unit interval such that .
We construct Dedekind cuts and and by the Dedekind completeness of the real numbers, there is a unique such that .
Peter Schuster?; Unique existence, approximate solutions,
and countable choice; doi.
Matt F.; answer to Approximate intermediate value theorem in pure constructive mathematics; MathOverflow; web.
Matthew Frank?, Interpolating Between Choices for the Approximate Intermediate Value Theorem (arxiv:1701.02227), Logical Methods in Computer Science, July 14, 2020, Volume 16, Issue 3 - doi:10.23638/LMCS-16(3:5)2020
Paul Taylor; The intermediate value theorem; A lambda calculus for real analysis, 14; web.
Auke Booij, Extensional constructive real analysis via locators, (abs:1805.06781)
Andrej Bauer, Five Stages of Accepting Constructive Mathematics, Bulletin of the American Mathematical Society, Volume 54, Number 3, July 2017, Pages 481–498. (doi:10.1090/bull/1556, pdf)
On the intermediate value theorem in cohesive homotopy type theory, see:
Last revised on February 19, 2024 at 12:40:51. See the history of this page for a list of all contributions to it.